From: Jacques Le Normand <rathereasy@gmail.com>

> let a be a polymorphic variant type of the form  ([`C1 of t1 | `C2 of t2 |
> .. | `Cn of tn] as 'a)
> let b be a polymorphic variant type of the form ([`C1 of t1['b/'a] | `C2 of
> t2['b/'a] | ... | `Cn of tn['b/'a] | Cp of tp] as 'b)
> where ['b/'a] represents substitution. In other words, b has one more
> constructor than a. Is a always a subtype of b?

Yes, but only if 'a appears only in covariant positions inside
t1...tn. And you will need "double coercions" (i.e. coercions with
explicit source and target types) to enforce this subtyping.

Jacques Garrigue