I’m trying to construct a Content
by wrapping a Content
as its constructor’s argument:
Parameter Bag : Type -> Set.
Parameter wrap : forall {A}, A -> Bag A.
Variant Content :=
Content_Unit
| Content_Bag {A} (bag : Bag A).
Fail Definition wrappedUnit : Content :=
Content_Bag (wrap Content_Unit).
but Coq doesn’t like it:
The command has indeed failed with message:
The term “wrap Content_Unit” has type “Bag Content” while it is expected to have type
“Bag ?A” (unable to find a well-typed instantiation for “?A”: cannot ensure that “Type@{max(Set,Top.6+1)}” is a
subtype of “Type@{Top.6}”).
Is there a valid way to write such wrapped definition?
Solution: Polymorphic Universes
Polymorphic Variant Content :=
Content_Unit
| Content_Bag {A} (bag : Bag A).