The Coq mailing list

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

In Lego, besides the anonymous Type there is also explicit syntax
Type(0), Type(1), ...  If no anonymous Type is ever used (since the
initial state) then the universe graph remains empty.  (But Lego's
libraries do use anonymous Type.)  I find this very useful.

Lego also supports type level variables Type(name).  This is
completely anonymous when first used, but all occurrences of
Type(name) will be constrained to the same universe level.  I'm not
sure this is very useful in practice.

Another thing to point out, that may be of use to Coq users, is that
Coq's implementation of Universe polymorphism (as contrasted with
typical ambiguity) is not complete.  Thus, when Coq says "Error:
Universe Inconsistency", it is not necessarily true that your input
cannot be typed.  Here is an example (in Coq V6.3.1).

 Reset Initial.
 Definition I [T:Type; t:T] : T := t.
 Check (I ((T:Type)T->T) I).   (* self application of I fails *)

Coq says

 Error during interpretation of command:
 Check (I ((T:Type)T->T) I).
 Error: Universe Inconsistency

Now enter 

 Definition J [T:Type; t:T] : T := t.
 Check (I ((T:Type)T->T) J).   (* application of I to J succeeds *)

Coq accepts this

 (I (T:Type)T->T J)
      : (T:Type)T->T

The definition J contains a new instance of Type, not constrained by
occurrences in I.  (See my old paper with Bob Harper for details.)
Such examples also occur with inductive definitions.

BTW, Coq 7.0beta does accept the self application of I above.  I
haven't tried to discover how complete the new implementation is
w.r.t.  universe polymorphism.  Can Jean-Christophe or Hugo answer
this question?

Best,
Randy