The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hello everyone,

We have a large development where we have generic structures and some
concrete instances for them. One of these is for relations (X -> Y ->
Prop) with (X,Y : Set).

Now I was trying to generalize this to all instances with (X,Y : Type).
This leads to a universe inconsistency thousands of lines down the road.
I would hope that this is merely a problem of making certain things
universe polymorphic, but I don't manage to come up with a minimal
example reproducing the problem.

At first, I only got the rather uninformative "Universe Inconsistency"
error when trying to load two separately compiled parts of the library.

With some trial and error I got to the point where I have statement that
type checks before the generalized instances are imported and fails to
type check afterwards. This gives me an Error of the form:

"... cannot ensure that "Type@{foo.2}" is a subtype of Type@{bar.3}"

I can use "Print Universes" before and after the Import, but that yields
thousands of constraints and even the diff is not too enlightening.

If I understand the universe mechanism and the error message correctly,
this actually means that assuming "foo.2 <= bar.3" is inconsistent with
the current collection of universe constraints. So here are some questions:

1) Is my understanding correct?

2) If yes, is there a way to obtain a minimal (or at least sufficiently
small) subset of the current collection of constraints, proving that
"foo.2 <= bar.3" cannot be consistently added.

3) What other things can I do to shed some light onto what is happening?

Any help would be appreciated.

Best,
Christian