The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.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