The Coq mailing list

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

Hi, 

It may be worthwhile to add that, at least the last time I ran into this 
issue, Coq applied some heuristics/approximations when introducing new 
universe constraints. A universe inconsistency on import is likely the result 
of the heuristics introducing imprecise constraints along one path in a 
parallelized development. These heuristics will backtrack and introduce 
weaker constraints on failure. Hence, there are a few things one can do:

- try linearizing the file dependency structure until the inconsistencies 
disappear or appear at the some definition/lemma.
- if the inconsistencies disappear, one can try to look for differences in 
the universe constraints. This is easier if one introduces a few explicit 
universes and uses them in key definitions. 
- once one has located the spot where needlessly strong constraints (usually 
U = V for some U and V) are enforced, one can precede said lemma/definition 
with a "Contraint" command ruling out the equality (e.g., Contraint U < V) to 
force backtracking within the definition/lemma. Afterwards, the desired 
parallel structure can be reestablished.

I hope this helps!

Best,
Christian

On 11/30/19 3:15 AM, Jason Gross wrote:
> If you `Set Printing Universes` before you do the Require Import, you will 
> get more info, often enough to figure out which file they're in.  If you 
> then print the file (with printing universes on), you can figure out which 
> definition the universes come from (figuring out where the constraints come 
> from is much harder, unfortunately).
> 
> On Fri, Nov 29, 2019, 20:08 Brett Gilio 
> <brettg AT posteo.net
>  
> <mailto:brettg AT posteo.net>>
>  wrote:
> 
>     Vadim Zaliva 
> <vzaliva AT cmu.edu
>  
> <mailto:vzaliva AT cmu.edu>>
>  writes:
> 
>     > I have `Require Import` which fails with the "universe inconsistency" 
> error. There is no more detail besides this message. Any hints on how one 
> can debug this?
>     >
>     > Vadim
>     > 
>     > --
>     > Vadim Zaliva
>     > A button for name playback in email signature
>     > 
>     > CMU ECE Ph.D. candidate
>     > Mobile/Signal/WhatsApp: +1(510)220-1060
>     >
> 
>     Hello Vadim,
> 
>     Can I see an example of what you are trying to achieve? Sometimes a
>     universe inconsistency error can point to an error with logic in the 
> import.
> 
>     -- 
>     Brett M. Gilio
>     https://git.sr.ht/~brettgilio/
>