The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Edsko de Vries wrote:
> [different universes for:]
>
>   Inductive prod (A B : Type) : Type :=
>     | pair : A -> B -> prod A B.
>
> [vs.]
>
>   Inductive prod (A : Type) (B : Type) : Type :=
>     | pair : A -> B -> prod A B.
>   

Wow, that is really weird. I had been assuming that these two 
definitions would desugar to the same internal AST. At least one of them 
had the behavior I expected. ;-)

The two ways of building universe constraints at least seem provably 
equivalent from the user's point of view.

> Slightly different again:
>
>   Inductive prod : Type -> Type -> Type :=
>     | pair : forall (A : Type) (B : Type), prod A B.
>   
>   Set Printing Universes.
>   Print prod.
>   Print Universes.
>
> We get
>
>   Inductive prod
>                 : Type (* Top.1 *) ->
>                   Type (* Top.2 *) -> Type (* max((Top.4)+1, (Top.5)+1) *) :=
>       pair : forall (A : Type (* Top.4 *)) (B : Type (* Top.5 *)), prod A B
>   
>   Top.5 <= Top.2
>   Top.4 <= Top.1
>
> Which is more permissive again.

Your new definition doesn't match up with the old ones, since your pairs 
contain no data. ;-) But I think adding the data wouldn't have an 
interesting effect on the universe constraints.

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.