search

vellvm / ctrees

An itree-like data-structure to additionally support internal non-determinism
MIT License
13 stars 2 forks source link

Universe inconsistency with ITree.Events.StateFacts #8

Open elefthei opened 2 years ago

elefthei commented 2 years ago

We tried to solve this with @euisuny and @YaZko but I had to leave. Making a note here that

From ITree Require Import
     Events.StateFacts.

From CTree Require Import
     Bisim.

Gives a universe inconsistency error

Error: Universe inconsistency. Cannot enforce Coq.Relations.Relation_Definitions.1 <= RelationAlgebra.monoid.1 because RelationAlgebra.monoid.1 <= Coq.Lists.List.1 <= MonadFix.MonadFix.u0 < Coq.Relations.Relation_Definitions.1.

YaZko commented 2 years ago

Yes, thanks for recording this!

If I am not mistaken, Bisim is only a vessel for the issue, I think (but am not sure) that the problem has to do with the use of the RelationAlgebra library that we make in Trans.v to work in the Kleene Algebra against a model where the equality is equ.

Note that this is the exact same issue as in examples/Yield/Lang.v where we shamefully killed universe checks for now rather than dealing with it.