Failed definition: cannot ensure subtype

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).

You could make Content universe polymorphic

Gaëtan Gilbert