The Coq mailing list

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

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
>