The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

> I wouldn't call the last definition "more permissive," because certain 
> uses of it fail to type-check, where uses of both previous versions 
> _would_ type-check. The problem is that you are forced to "go up a 
> universe" relative to the universes of the constructor's arguments, 
> which is a general reason that you'd want to use parameters instead 
> where possible.
> 
> To see the problem, try [Check (pair 0 (pair 0 0))] (assuming [Set 
> Implicit Arguments] is on) with all of the definitions (where your last 
> definition is fixed). The first two check out, but the last one has a 
> universe inconsistency.

Aah, thanks for pointing that out. Should have noticed that.
Interesting. Why do the two definitions cause different universe
constraints? 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; is there an easy example? Or a reference I should read?

Edsko