The Coq mailing list

["Georges Gonthier" <gonthier AT microsoft.com>]

> > I really want to define
> > Inductive Lambda : Set -> Set :=
> >  | var : forall A:Set, A -> Lambda A
> >  | app : forall A:Set, Lambda A -> Lambda A -> Lambda A
> >  | lambda : forall A:Set, Lambda (option A) -> Lambda A.
> > I cannot fix this my changing Set to Type because then the statement
of
> > the join function:
> > Definition joinStatement :=
> >    forall (T:Type)(l:Lambda (Lambda T)),(Lambda T).
> > causes a universe inconsistency.
> 
>  The inductive definition Lambda you give above obtained replacing Set
with
>  Type and the joinStatement above does not cause a universe
inconsistency.
>  The universe inconsistency must be generated by something else you
are
>  doing, and it may be possible to avoid it.

   Since Russell and I discussed this issue privately, I should point
out the problem here, before anyone else stumbles on this pitfall:
  Coq doesn't raise a universe inconsistency with the definition above
because of a loophole in the typing rule for inductive definitions,
which essentially puts no upper bound on the universe of the argument of
a dependent inductive.
  Let me use the exType example of the Coq manual to explain this:

Inductive exType (P : Type_i -> Prop) : Type_j :=
  ExType : forall X : Type_k, P X -> exType P.

which of course you would enter without the type indices. The
constraints given by the W-Ind rule are k < j and k <= i, not i < j as
stated in the manual. Thus exType (fun X => X = exType (fun _ => True))
does not by itself cause an inconsistency; trying to construct a value
of this type will, however (e.g., ExType _ _ (refl_equal (exType (fun _
=> True)))). The same would apply if exType were rewritten as a a
dependent inductive like Lambda.
   In short, universe constraints are only fully checked for
constructors; while this is probably sufficient to avoid inconsistency
(I'm not familiar enough with the model construction to assert this
formally, though), it does cause fairly quirky error reporting, which is
compounded by the fact that there is no documented way of inspecting
universe constraints. If you manage not to call the wrong constructors,
you can go quite a long way with an essentially inconsistent development
without triggering a universe error. I managed to define all of
Russell's functions, including "join", without violating universe
consistency; adding a trivial proof that the lift of the identity is the
identity triggered that dreaded error, however...
   A final note : these paradoxical types need not be empty. Take
Inductive succ (A : Type) := Zero | Succ (x : A).
Inductive le A : Type -> Type :=
| ReflLe : le A A
| SuccLe B : le A B -> le A (Succ B).
Definition xxx : le (le Set Set) (le Set Set)) := ReflLe (ReflLe Set).
goes down without an inconsistency, but SuccLe _ xxx causes one.

Georges Gonthier