The Coq mailing list

[Loic Pottier <Loic.Pottier AT sophia.inria.fr>]

How can I know the universe of a constant?

Here are two examples mysterious for me:

------------------------------
coqtop
Welcome to Coq V6.2.3 (December 1998)
--------- session 1

Implicit Arguments On.

Mutual Inductive tel: Type :=
     T0: tel
    | Tc: (T:Type) (T ->tel) ->tel .

Mutual Inductive el_tel: tel ->Type :=
     el_T0: (el_tel T0)
    | el_Tc: (T:Type) (x:T) (f:T ->tel) (el_tel (f x)) ->(el_tel (Tc f)) .

Definition relation := [E:Type] E -> E ->Prop.

Definition Rel := (Tc [Carrier:Type](Tc [Equal:Carrier -> Carrier ->Prop]T0)).

Definition setrel := (relation (el_tel Rel)).

Definition Rel1 := (Tc [Carrier:Type](Tc [Equal:(relation Carrier)]T0)).

Error during interpretation of command:
Definition Rel1 := (Tc [Carrier:Type](Tc [Equal:(relation Carrier)]T0)).
Error: Universe Inconsistency

---------------
Now I switch definitions of setrel and Rel1:

------- session 2

Reset Initial.

Implicit Arguments On.

Mutual Inductive tel: Type :=
     T0: tel
    | Tc: (T:Type) (T ->tel) ->tel .

Mutual Inductive el_tel: tel ->Type :=
     el_T0: (el_tel T0)
    | el_Tc: (T:Type) (x:T) (f:T ->tel) (el_tel (f x)) ->(el_tel (Tc f)) .

Definition relation := [E:Type] E -> E ->Prop.

Definition Rel := (Tc [Carrier:Type](Tc [Equal:Carrier -> Carrier ->Prop]T0)).

Definition Rel1 := (Tc [Carrier:Type](Tc [Equal:(relation Carrier)]T0)).

Definition setrel := (relation (el_tel Rel)).

Error during interpretation of command:
Definition setrel := (relation (el_tel Rel)).
Error: Universe Inconsistency

-------------------------

I suppose that when it is defined, the constant relation is floating 
in the universes, and after the definition of setrel  (or Rel1 in 
session 2), its universe is fixed. If it is true, why ?

Loïc