The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> - Require Import A B. succeeds
> - Require Import B A. fails

That sounds like a bug, you can open an issue on github with 
reproduction instructions and we will look into it.


> globalization of polymorphic reference <ID> would forget universes.

Unfortunately various tactics and commands do not support or badly 
support universe polymorphism. This error means some function hasn't 
been adapted. It should probably be an anomaly.
Depending on what exactly is failing it may be possible for us to fix 
it, or it could be beyond our current manpower.

Gaëtan Gilbert

On 07/09/2018 15:59, Christian Doczkal wrote:
> Hello,
>
> I got back to investigating universe inconsistencies, and I realize that
> I still don't quite understand the mechanics. So here are two more
> questions:
>
> 1) I have two modules, say A and B such that:
> - Require Import A B. succeeds
> - Require Import B A. fails
>
> So what is happening to the universe constraints upon Require Import
> that makes this order sensitive? In would have expected that either
> order yields the union of the constraints imposed by A and B. In this
> particular case, A contains universe polymorphic instances of classes
> that are common ancestors of A and B.
>
> 2) While experimenting with making more and more things universe
> polymorphic, I encountered an error message I don't understand:
>
> globalization of polymorphic reference <ID> would forget universes.
>
> This seems to be undocumented, so what is the problem here? (e.g., is
> there a minimal example triggering this message?)
>
> Best,
> Christian
>
> On 06/09/18 18:38, Christian Doczkal wrote:
> > Hello,
> >
> > On 06/09/18 13:55, Jan-Oliver Kaiser wrote:
> >
> > > You can print entire modules using [Print] or [Print Module] in case of 
> > > ambiguities.
> >
> > Thank you, I simply hadn't thought of that. Pretty useful.
> >
> > > 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.
> >
> > This I find very interesting. Could someone with insight into the
> > algorithm comment on which kind of type checking problems are more
> > likely to trigger an error message providing a full cycle?
> >
> > Other than that, has anyone played with dumping the output of print
> > universes plus the constraint that is reported as inconsistent into some
> > external tool that finds irreducible infeasible subsets for the
> > underlying ILP? (Does there even exist open source software finding these?)
> >
> > Best,
> > Christian