The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Indeed, eta allows to lower the second I/K’s levels in your definitions.
What’s impossible however is to use K at a type larger or equal to it’s 
declared universe.

Definition T := Type. (* Fix a level *)
Parameter K : forall t:T, t -> t.
Fail Check (K (forall t:T, t -> t) K).

All the examples you gave do not use polymorphism, but typical ambiguity + 
eta-expansion only. In 8.4, only Inductves like:

 Inductive I (A : Type(* l *)) : A -> Type (* l *) := i : A -> I

can be “polymorphic” on A, that is you can instantiate I at 
different incompatible levels, all lower than the initial global 
level l.

Hope this helps,
— Matthieu

On 5 sept. 2014, at 23:17, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> 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
>