The Coq mailing list

[Ben Sherman <sherman AT csail.mit.edu>]

Hi Gregory,

I've experienced similar issues. In particular, I had issues with `prod`, 
where I was occasionally not using it in a fully applied manner, so it in 
fact didn't end up being universe-polymorphic, and then I had universe 
inconsistencies as a result. In particular, it affected using typeclass-based 
rewriting (i.e., CRelationClasses/CMorphisms), because `iffT` is defined 
using `prod`. So one non-polymorphic use of `prod` broke behavior of `iffT`, 
even though `iffT` has a fully applied use of `prod`.

One option to fix this, which I don't particularly like, is to make sure that 
*every* use of `prod` is "fully applied", that is, that it instantiates 
arguments to `prod` with universe-polymorphic types.

The other option, which I took, is to just redefine `prod` with universe 
polymorphism, and use that instead:
https://github.com/bmsherman/topology/blob/master/src/StdLib.v

The reason why I like this approach is because it makes it easier to reason 
about universes. That is, it can make it so definitions have fewer universe 
constraints. For any definition using template-polymorphic `prod` (even if it 
is fully applied), you'll get universe constraints that look something like

Univ < Coq.Init.Datatypes.19
Univ < Coq.Init.Datatypes.20

where `Coq.Init.Datatypes.[19-20]` are the two universes for the arguments to 
the template-polymorphic `prod` definition in the standard library. I think 
that these constraints aren't really a worry, because we can just let 
`Coq.Init.Datatypes.[19-20]` be arbitrarily big. But I guess that when `prod` 
isn't fully applied, you can get lower bounds on these universe levels, too, 
which is an issue.

Anyway, I like never having to look at constraints like the one above in the 
first place; it makes it easier to figure out what's going on with universes. 
So I suggest the seemingly radical option of redefining `prod` (or whatever 
datatype it is for you) in a universe-polymorphic manner.

(There's a feature request for more documentation on template polymorphism in 
the Coq bug tracker:
https://coq.inria.fr/bugs/show_bug.cgi?id=4860)

Ben