The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

Hey Christian,

You can print entire modules using [Print] or [Print Module] in case of 
ambiguities. With [Set Printing Universes] enabled you can at least 
search for particular universes quickly within a module. (There's one 
annoying thing here which is that submodules are not automatically 
expanded. Maybe there is an option for that that I don't know?)

Apart from that, [Set Printing Universes] should *sometimes* show the 
full universe cycle when an inconsistency occurs, but it depends very 
much on the particular error that appears.

Regarding the actual inconsistency: One quick way of eliminating a 
particular egregious class of inconsistencies is to look for partial 
applications of template-polymorphic types (such as datatypes from the 
standard library). These partial applications restrict all future uses 
of the partially-applied type and can very easily lead to hard-to-find 
inconsistencies. An example would be a type classes such as [FMap] with 
an instance [FMap list]. Together with another definition that mixes 
[FMap] and [list] and introduces the opposite universe constraint of the 
[FMap] instance for [list], this can lead to inconsistencies.

If you do find any such partial applications, try to see if the universe 
cycle includes any of the relevant universes. Or, equivalently, start 
with the universes in the cycle—attainable by massaging the failing 
definition with explicit universes until you get the right *kind* of 
universe error—and see if any of them are related to the standard 
library or your own template-polymorphic inductive types and work 
backwards from there to find partial applications of such types.

Sadly even this process can take a long time.

Best,
Janno


On 9/6/18 1:01 PM, Christian Doczkal wrote:
> Hello,
>
> I already had used "Set Printing Universes". As far as I can tell, the
> only thing "Set Printing Universes" does is cause "Print/Check term." to
> print the universe levels of all occurrences of "Type" occurring in a
> particular definition as well as the constraints enforced by a
> particular definition.
>
> I have a constraint system with thousands of constraints arising from
> hundreds of definitions and I would like to know which constraints
> contribute to the inconsistency and which definitions/lemmas give rise
> to a given constraint.
>
> For instance, Print Universes might mention
> "Coq.Relations.Relation_Definitions.1" which I could correctly guess is
> the first argument of "relation":
>
> relation =
> fun A : Type@{Coq.Relations.Relation_Definitions.1} => A -> A -> Prop
>       : Type@{Coq.Relations.Relation_Definitions.1} ->
>         Type@{max(Coq.Relations.Relation_Definitions.1,Set+1)}
>
> But its not always that easy to guess the definitions introducing a
> particular universe index and even harder to guess which definition or
> lemma enforces a given constraint.
>
> Best,
> Christian
>
>
> On 05/09/18 20:42, Gaëtan Gilbert wrote:
> > 1) yes
> >
> > 2) and 3)
> > if you enable printing of universes (Set Printing Universes. in
> > coqtop/proof general/etc, some GUI toggle in coqide) universe
> > inconsistencies should print that information
> >
> > Gaëtan Gilbert
> >
> > On 05/09/2018 17:57, Christian Doczkal wrote:
> > > 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