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.