The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> I understand that Type is not impredicative and so when we
> say
>
> Inductive prod : Type -> Type -> Type := 
>   | pair : forall A : Type, ..
>
> the type of A must be a "lower" Type than the Type in the result of
> prod. However, it seems to me that the alternative definition (with A a
> parameter to the datatype) introduces the same impredicativity "through
> the backdoor".
>
> I presume that one definition introduces a paradox somewhere but the
> other doesn't.

Maybe.  I just know that the typing rules for Gallina add "<=" for 
parameters and "<" for constructor arguments.  There's probably a good 
meta-theoretical reason for it, but you probably don't need to know the 
reason to program effectively in Gallina.