Universe inconsistency

[alxest]

I am trying to use interaction tree in my project and I encountered an universe inconsistency error.
I am reporting this issue because I am not sure if the problematic constraint is an essential one.

Here is a minimized example.

From ITree Require Export
     ITree ITreeFacts.
Require Import List.
Set Printing Universes.

Record my_mod: Type := mk {
  datatype: Type;
}.
Definition my_mods_uses_List (ms: my_mod) (mms: list my_mod): Prop := In ms mms.
Variant void1 : Type -> Type := .
Definition boo: my_mod := mk (itree void1 unit).

It fails to compile with the following error message.
(Note: If you do not import ITreeFacts, it compiles.)

Error:
The term "itree void1 unit" has type
 "Type@{max(Set,ITree.Core.ITreeDefinition.2,ITree.Core.ITreeDefinition.3,itreeF.u1+1)}"
while it is expected to have type "Type@{my_mod.u0}"
(universe inconsistency: Cannot enforce ITree.Core.ITreeDefinition.3 <= my_mod.u0 because
my_mod.u0 < Coq.Lists.List.1 <= MonadFix.MonadFix.u0 = ITree.Core.ITreeDefinition.3).

What is interesting here is that InteractionTrees repository does not import MonadFix at all.
If these universe constraints are not essential and you can remove them, it will make my life easier.

I tested it in version: coq 8.10.1 // ext-lib 0.11.1 // itree 3.1.0 // paco 4.0.0

Also, interestingly, my colleague @kim-yoonseung tested the same code in older version of itree, and he says it compiled without an error.
The version he used is as follows: coq 8.9.1 // ext-lib 0.10.2 // itree 2.0.0 // paco 4.0.0

---

I would like to ask for some general advice when dealing with universe inconsistencies. (it seems you have a lot of experience with it :D)

1. Finding the root cause of an error.
   Coq's messages (Print Universes, Set Printing Universes) are not very satisfactory in at least two ways:

   • I can't find where the constraints are introduced. (So I am trying similar things like this)
   • The error message does not give a full cycle. For an instance, in the above error message, actually the constraint MonadFix.MonadFix.u0 = ITree.Core.ITreeDefinition.3 does not appear directly in Print Universes. It is established by transitivity.

2. Solving the problem.
   I tried to put Set Universe Polymorphism only in the problematic cases but it was hard localize the use of universe polymorphism -- it enforced me to change some other monomorphic definitions to polymorphic ones. I didn't want to have too much headache with it, so I put Set Universe Polymorphism everywhere, and it was also annoying. Universe polymorphic definitions does not work well with Set sort, so I had to wrap existing Set definitions to Type, which was not feasible because my project depends on a large codebase that I can't modify.
   Now I am considering another approach -- just copy-pasting the problematic monomorphic code (e.g., List) as much as needed, instead of polymorphism.

Thanks for reading this!

[Lysxia]

Thanks for reporting this issue!

It does look like something that should be allowed, but I'm also unsure how to fix it.

I believe part of the problem is the list of types, which adds a constraint on the universe of the list type. One solution might be to make the type of lists universe polymorphic, but this is tricky of course because it is in the standard library, and I'm not sure the switch would be painless for everyone. If your situation allows it, you could try defining your own type of lists when the intent is for them to contain types as opposed to regular data.

Perhaps ITree could avoid using some types from the standard library internally to avoid adding its own universe constraints, I'll need to investigate this more.

For working with universes in general, I'm in the same boat as you are :) I also don't get much out of the Printing Universes option, so my not-magical approach has been to painstakingly minimize the code causing the universe inconsistency.

[alxest]

@Lysxia Thanks for your reply!

• I had an experiment in my codebase and it seems to work.
  I defined PList by copy-pasting Coq.Lists.List and putting universe polymorphism on it (only two lines diff). Then, I replaced the problematic occurrences of List.map/List.In(only two occurrences) with this new one. If interested, you can see the commit here: snu-sf/CompCertM@524b53b

  • Coq.Init.Datatypes.list, and functions in Coq.Lists.List lives in different universes. I only needed to copy-paste the latter.
  • I additionally defined some monomorphization lemmas for smooth interaction with existing proofs.

  I think this is a temporary hacking, though, and in the long term, I would like this to be removed; either by waiting for universe polymorphism to settle in stdlib -- actually they put it and rolled back it 7 years ago -- or doing some work in extlib/interaction trees.

• For working in universes in general, thanks for sharing your experience. I will definitely let you know if I get a magic bullet someday.

[alxest]

I have come to know a useful command when doing universe-aware programming and would like to share it.
A Gallina command Constraint i < j (you can use = and <= too) tries to add universe constraints.
For the recent few univ inconsistencies I faced, I put appropriate constraints into libraries that I use, and it made my debugging much easier. (It clarifies who is to blame -- the library or me -- effectively enabling binary search)

• It can also be used to enforce absence of a constraint, like: Let __marker__ := tt. Constraint j <= i. Reset __marker__. This enforces absence of i < j.
• If the command fails, it gives useful debug information. (the problematic cycle)

[minkiminki]

I have the same problem, and I tried to fix it by making some definitions in ExtLib polymorphic: https://github.com/minkiminki/coq-ext-lib/tree/poly

For example, the below code works well with my ExtLib fix, but not for the original ExtLib.
Definition failure := Some (@existT _ (fun X => X) (itree void1 unit)).

I have no experience with ExtLib, so I'm not sure if this fix will make other problems.