The Coq mailing list

[Randy Pollack <rap AT dcs.ed.ac.uk>]

Bruno Barras writes:
 > 
 > >  Definition I [T:Type; t:T] : T := t.
 > >  Check (I ((T:Type)T->T) I).   (* self application of I fails *)
 > > 
 > >  Error: Universe Inconsistency
 > > 
 > >  Definition J [T:Type; t:T] : T := t.
 > >  Check (I ((T:Type)T->T) J).   (* application of I to J succeeds *)
 > > 
 > >  (I (T:Type)T->T J)
 > >       : (T:Type)T->T
 > > 
 > As far as I understand it, it is correct since we do not have
 > universe polymorphism, so you have to write two instances of the
 > identity.

Agreed, this is not a bug in Coq V6.3.1; it is the intended behavior,
chosen for reasons of efficiency and simplicity, as Bruno points out.

But I wouldn't want to call this "correct", as this behavior is not
"referentially transparent".  There are pairs of terms that are
definitionally equal, e.g (I ((T:Type)T->T) I) and
(I ((T:Type)T->T) ([T:Type; t:T]t)), but do not typecheck the same in
Coq.

 > Regarding the V7beta problem, this is because Check of Coq V7beta does
 > typecheck the term without checking the generated universe constraints
 > are compatible with the current environment. I consider this is a bug
 > and the behaviour of V6.3.1 should be restored.
 > 
 > Meanwhile, you'd better use Definition rather than Check:
 > 
 > Parameter K: (T:Type)T->T.
 > Definition y := (K ((T:Type)T->T) K).
 > 
 > Error: Universe Inconsistency.

Interesting.  So there is just a bug in "Check" in V7beta, but real
type-checking (as in checking a Definition) is correct.  This again
raises the question whether V7beta intends to be referentially
transparent.  That would be a good thing.

Best,
Randy