The Coq mailing list

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

I'm using Coq 8.4pl4, which I think does not have Matthieu Sozeau's
new treatment of universes (is that true?).  Consider the examples:

   Definition I := fun (t:Type) (x:t) => x.
   Definition II := I (forall t:Type, t -> t) I.

This is accepted, as it should be (by universe polymorphism), as the 2
instances of "I" in Definition II can get different types.

But consider

   Set Printing Universes.
   Parameter K : forall t:Type, t -> t.
   Print K.
   *** [ K : forall t : Type (* Top.1 *), t -> t ]
   Print Universes
       (* no constraint on Top.1 shown *)

So far, OK.  But...

   Check (K (forall t:Type, t -> t) K).

This is accepted, wrongly, as the 2 instances of "K" must have the same type.

   Definition KK := K (forall t:Type, t -> t) K.

This is accepted, and now we have an ill-typed term bound in the global 
context.

--Randy