The Coq mailing list

[Benjamin Werner <werner AT pauillac.inria.fr>]

  Hello

> 
> Inductive listn : nat->Type :=
>   niln:(listn O)
>  | consn :(A:Type)(n:nat) A->(listn n)->(listn (S n)).

OK. Let me point out that this construction will be generaly of very
little use. Indeed, you never "know" what the types of the elements
can be, so you will not be able to do much with them.

> When I try to build listn with elements of type listn :
> 
> Parameter X:Type.
> Parameter x1,x2:X.
> 
> Definition l1 := (consn x1 (consn x2 niln)).  (* OK *)
> Definition l2 := (consn l1 niln)
> 
> Coq answers "Error: Universe Inconsistency"

Type is not really impredicative (or polymorphic). Actually Type
stands for Type(i), with i some universe index.

Now, listn is of type nat->Type(i)

The point is that (A:Type(j))T is of type max(j+1,k), if T:Type(k)

Furthermore, the constructors have to live in the same universe
as the inductive type itself. So the type of consn is actually

(A:Type(j))(n:nat) A->(listn n)->(listn (S n)).

with j<i

Thus, you cannot apply (listn n) to consn.

> 
> But if I change "Type" by "Set" :
> Inductive listn : nat->Set :=
>   niln:(listn O)
>  | consn :(A:Set)(n:nat) A->(listn n)->(listn (S n)).
> 
> l2 is defined.

Set is impredicative, so you can quantify over anything in a type of
type Set.

Explaining the reasons for the universe constraints would be out of
the scope of the coq-club. But again, let me point out that a "usable"
version of listn would probably not encounter the problem.

Cheers,

Benjamin Werner
----------------------------------------------------------------------------
Projet LogiCal
INRIA-Rocquencourt, BP 105, F-78 153 LE CHESNAY cedex, FRANCE
E-mail: 
Benjamin.Werner AT inria.fr
Phone:  +33 (1) 39 63 52 31
Mobile: +33 (6) 63 53 43 44
Fax:    +33 (1) 39 63 56 84
http://logical.inria.fr/~werner/
-----------------------------------------------------------------------------