The Coq mailing list

[Randy Pollack <rap AT inf.ed.ac.uk>]

To further explain Hugo's reply, consider this variation

Definition type_of1 (T:Type) (t:T) : Type := T.
Definition type_of2 (T:Type) (t:T) : Type := T.
Eval compute in (type_of1 (type_of2 (Type))).

This is well typed, without universe inconsistency, because type_of1
and type_of1 can be assigned different universe levels.

This is a contrived example, but I have found that in practice, universe
inconsistency can sometimes be fixed by making multiple definitions of
the "same" constant.

Best,
Randy
--
Quoting Hugo Herbelin 
<hugo.herbelin AT inria.fr>:

>   Hi,
>
>   This is because type_of is defined at a _fixed_ Type universe, say
> i:
>
>      type_of : forall T : Type(i), T -> Type(i)
>
> so that it cannot be applied to itself. Indeed (without implicit
> arguments) the expression
>
>     type_of T t
>
>   has always type Type(i) whatever t and T are. Then
>
>     type_of Type(j) (type_of T t)
>
>   requires the constraints i=j and j<i which are unsatisfiable.
>
>   If Coq had universe polymorphism (as e.g. the Lego system has),
> then
> type_of would have had type
>
>      type_of : forall T : Type(i), T -> Type(i)
>
> for all i (not for only once). Hence, with universe polymorphism,
> your term would have been typable. But that's not the case of Coq...
>
>   For references on universe polymorphism, you can look at "Type
> checking with universes" by R. Harper and R. Pollack in Theoretical
> Computer Science 89 (1991).
>
>   Hugo Herbelin
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


--
Randy Pollack
Phone: +44 131 650 5145          URL: http://homepages.inf.ed.ac.uk/rap/
Computer Science, Edinburgh Univ. Kings Buildings, Edinburgh EH9 3JZ, UK