poulet4 has many libraries of functions and lemmas parameterized by a Type of an unspecified universe level, such as those for maps, monads, lists, etc. Furthermore p4light syntax and semantics are parameterized by a tags_t : Type.
Occasionally bizarre universe errors occur that may be avoided by making these definitions universe polymorphic or restricting them to Set.
I found it is not as simple as writing Set Universe Polymorphism in all of these files: I believe it will require explicit universe annotations.
For example for pull request #434 I attempted to write a general monadic sequence operation for InOut.t (P4cub/Syntax/AST.v) as
Definition seq {A B : Set} {m : Set -> Set} `{Monad m} (io : InOut.t (m A) (m B)) : m (InOut.t A B) :=
let* inns := sequence io.inn in
let^ outs := seqeunce io.out in
{| inn:=inns; outs:=outs |}.
InOut.t lives in Set but Monad and sequence require a Type but they should be universe agnostic.
poulet4has many libraries of functions and lemmas parameterized by aTypeof an unspecified universe level, such as those for maps, monads, lists, etc. Furthermorep4lightsyntax and semantics are parameterized by atags_t : Type.Occasionally bizarre universe errors occur that may be avoided by making these definitions universe polymorphic or restricting them to
Set.I found it is not as simple as writing
Set Universe Polymorphismin all of these files: I believe it will require explicit universe annotations.For example for pull request #434 I attempted to write a general monadic sequence operation for
InOut.t(P4cub/Syntax/AST.v) asInOut.tlives inSetbutMonadandsequencerequire aTypebut they should be universe agnostic.