Universe inconsistency when paired with RelationAlgebra

[YaZko]

A lot of universe inconsistencies have crept in the ctree library, and (at least) one root of it seems to come from interactions between the itree library and @damien-pous 's relation-algebra library.

One somewhat minimal example triggering it is the following:

From RelationAlgebra Require Import
  kat_tac
  srel.

From ITree Require Import
  Core.KTree
  Interp.TranslateFacts
  Basics.Monad
  Core.ITreeDefinition.

#[global] Instance Eq1_ITree {E} : Eq1 (itree E) := fun a => eutt eq.

Where Eq1 seem to be the culprit, but I have a hard time understanding why the RelationAlgebra imports are relevant to this inconsistency, since the set of failing constraints provided is between definitions of itrees and extlib only.

I'm gonna try to deep dive into this, but if anybody has insights or advices, anything's welcome!

[YaZko]

Making Eq1 universe polymorphic moves the cursor ever so slightly, the example above goes through, but not the following:

From RelationAlgebra Require Import
  kat_tac
  srel.

From ITree Require Import
  Core.KTreeFacts
  Interp.TranslateFacts.

Digging into this one seems to pin the responsibility on the Kleisli typeclass this time, but generalizing it as follow:

Definition Kleisli@{c d} (m : Type@{c} -> Type@{d}) (a : Type@{d}) (b : Type@{c}) : Type@{max(d+1,c)} := a -> m b.

is insufficient to solve these imports, it only moves the problem to:

Error: Universe inconsistency. Cannot enforce sum.u0 < ITree.Basics.CategoryOps.137 because ITree.Basics.CategoryOps.137 <= ITree.Basics.CategoryOps.2 = sum.u0.

Still, relation-algebra's responsibility in all of this remains mysterious so far...

[Lysxia]

By binary search in TranslateFacts the culprit seems to be the statement (not the proof) of this Proper theorem:

Instance eq_itree_apply_IFun {E F : Type -> Type} {T : Type}
  : Proper (respectful_eq_itree ==> eq_itree eq ==> eq_itree eq)
           (@apply_IFun (itree E) (itree F) T).

There seems to be some conflict between the ways the two libraries use relations. I still don't know a good way to debug this. Maybe we should do like relation-algebra and explicitly name some universes and fix the universe of all occurrences of Type to one of them, instead of letting Coq generate a new universe for every Type and unify them after the fact. With much fewer universes, it should be clear where the inequalities are coming from.

[YaZko]

Hey Li-yao,

Yes Damien mentioned to me that he had to specialise universes once to dodge universe inconsistencies --- this is completely backward to me, I don't quite foresee how it helps. But at least doing so might help pinning down the current issue as you suggest.

I also asked on Zulip (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/On.20the.20art.20of.20fixing.20the.20universe) and got pointed out by Paolo that the core issue has to do with template polymorphic definitions, and that eta-expansion can dodge this bullet --- a situation they encountered in stdpp (https://gitlab.mpi-sws.org/iris/stdpp/-/issues/80).

I need to ingest all that to understand better I must say.

[YaZko]

I'm not sure it helps much, but I have inlined most of ext-lib's dependencies (as well as made Eq1 and Kleisli universe polymorphic) to try to at least focus on only two libs right now.

The first inconsistency now appears with:

From RelationAlgebra Require Import
  kat_tac
  srel.

From ITree Require Import
     Basics.CategoryTheory
     Basics.CategoryKleisli.

By visibly overly constraining the sum type constructor from the standard library --- which seems to match Paolo's suggestion that it's all because of Template Polymorphic definitions from the standard library. I still need to understand what eta-expansion might save the day in the middle of all that...

And frustratingly, inlining CategoryKleisli solves the issue...

[mattam82]

Usually it comes from a partially applied type constructor somewhere, e.g. SomeClass sum. You could try to use Jason Gross's bug minimizer @JasonGross to find the faulty definition.

[mattam82]

One way to debug this is to look at the graph and find if one of sum's universes is bounded from above by another universe, this quickly leads to inconsistencies.

[857b]

I depend on parts of the ITree library (mostly ITree and ITreeFacts), and I ran into issues related to bounds on template universes (of sum and prod in particular).
There are already upper bounds on template universes in ExtLib, but they are not blocking for me currently.
The issues seem to come mostly from Function.v.
I had to patch the ITree library (https://github.com/857b/InteractionTrees/tree/fix_template_universes).
Unfortunately, I was not able to fix my issues without adding explicit Constraints.
Without those lines, some tactics in CategoryKleisliFacts.v unify some universes.
Also, even with my patch, it is not possible to require the whole development simultaneously:

Fail From ITree Require
  Basics.CategoryRelations
  Core.KTreeFacts
  Eq.SimUpToTaus.

[YaZko]

Thanks for bumping this issue and your take on it Benjamin.!

With Sébastien Michelland we had to simply work with a local polymorphic version of Sum in an other development depending on itrees (https://gitlab.inria.fr/sebmiche/itree-ai/-/blob/icfp24-artifact/theories/Util/Psum.v), and so far in ctrees I still have given up and unplug universe checks in a file...

One thing that makes me slightly lazy about this issue at the moment (I mean, additionally to it being an hell hole), is that my understanding is that @mattam82 is about to deliver a complete reimplementation of universes in Coq 9.0 if I understood correctly, which I (naively) assume will impact how to resolve the question.

[Chobbes]

By binary search in TranslateFacts the culprit seems to be the statement (not the proof) of this Proper theorem:

Instance eq_itree_apply_IFun {E F : Type -> Type} {T : Type}
  : Proper (respectful_eq_itree ==> eq_itree eq ==> eq_itree eq)
           (@apply_IFun (itree E) (itree F) T).

There seems to be some conflict between the ways the two libraries use relations. I still don't know a good way to debug this. Maybe we should do like relation-algebra and explicitly name some universes and fix the universe of all occurrences of Type to one of them, instead of letting Coq generate a new universe for every Type and unify them after the fact. With much fewer universes, it should be clear where the inequalities are coming from.

Not sure if this is at all helpful, but when working on Vellvm I've run into this exact universe inconsistency as well. Defining my own TranslateFacts locally with this Proper instance removed resolves the problem.

Is there a better way to solve this issue in general? I really don't want to copy bits of itrees piecemeal if I can avoid it 😬.

[Lysxia]

I haven't made any breakthrough in dealing with universes since then :/