The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  No they don't have the same type actually, as you mention id has
type forall T : Type(i), T -> T for a _specific_ i, while (fun T :
Type(j), id T) has type forall T : Type(j), T -> T for a _different_
j. Actually for a j smaller or equal to i. This type, being itself of
type j+1 and being typechecked as first argument of id adds a
constraint that j is _strictly_ smaller than i.
Best,
-- Matthieu

2014-09-11 15:04 GMT+02:00 Michel Levy 
<michel.levy1948 AT gmail.com>:
> I'm using  Coq 8.4pl3 (January 2014) with coqtop.
> I try this (classical) example :
> Coq<Definition id (T:Type)(x:T):=x.
> Coq<Check (id (forall T:Type,T->T) id)
> I was expecting an error, because the id declared is typed forall T:
> Type(i),T->T
> while it is expected to be typed forall T:type(j),T->T where i and j are any
> naturals numbers.
>
> But with this Coq version, I have
> Coq < Check (id (forall T:Type,T->T) id).
> id (forall T : Type, T -> T) (fun T : Type => id T)
>      : forall T : Type, T -> T
>
> I don't understand why the left id is replaced by (fun T:Type => id T),
> especially because id and (fun T:Type => id T) have
> the same type.
>
>
> --
> email : 
> michel.levy1948 AT gmail.com
> http://membres-liglab.imag.fr/michel.levy



-- 
-- Matthieu