Unwanted universe constraints?

[alxest]

I am facing a universe issue and want to report it. Below is the minimal reproducible code. (Compiles with Coq 8.12.2 / itree 3.2.0 / paco 4.0.2)

Require Import Coq.Relations.Relation_Definitions.
From Paco Require Import paco.
Variable f: (forall R, relation R -> Prop) -> (forall R, relation R -> Prop).
Goal forall R (RR: relation R), (gpaco2 f (cpn2 f) bot2 bot2 R RR). Proof. gcofix CIH. Abort.
From ITree Require Import InterpFacts.
Goal forall R (RR: relation R), (gpaco2 f (cpn2 f) bot2 bot2 R RR). Proof. Fail gcofix CIH. Abort.

I think the problem is that InterpFacts -- interp_translate lemma introduces universe constraints that affect Paco. Specifically, the following lines are added:

rel2.u0 <= Coq.Relations.Relation_Definitions.1
rel2.u1 <= Coq.Relations.Relation_Definitions.1

.

In the above example (and my development), just using R -> R -> Prop instead of relation R was sufficient to avoid the problem. But it would be good if we can remove such constraints?

[Lysxia]

It seems this was fixed in paco.