The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Matej Kosik wrote:
> In Coq, the `list' function has the type `Type -> Type'. This means that
> whenever apply some value whose type can be converted to `Type', I will
> get a value whose type is `Type'.
>
> [...]
>
> There is, however, one thing I do not understand. How could the type of
> the whole term (`list nat' or `list bool') be `Set' instead of `Type' as
> the type of the `list' function suggests?
>   

The answer involves the fact that [list] isn't really just a function.  
Coq includes a kind of fake, "template-style" universe polymorphism, 
where inductive definitions are effectively copied automatically to make 
it possible to use [Set] instead of [Type] in some places.  The Coq 
type-checker automatically detects opportunities to do this.

I looked quickly for a reference to this in the manual but didn't find 
one, so I hope my description of the feature is accurate. =)