The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

There is no inconsistency here.  You are seeing the result of on-the-fly eta-expansion.  Note that [Definition KKs := K (forall t:Set, t -> t) K.] is also accepted, because the eta-expansion of [K] can be retyped as [forall t:Set, t -> t].  If you [Print KK], you'll notice that it uses [Type (* Top.2 *)], and the universe graph contains the constraint "Top.2 < Top.1".

-Jason

On Fri, Sep 5, 2014 at 5:02 PM, Randy Pollack <rpollack AT inf.ed.ac.uk> wrote:

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