Unwanted universe constraints?
Closed this issue · 1 comments
alxest commented
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 commented
It seems this was fixed in paco.