Jeremy Yallop <j.d.yallop@sms.ed.ac.uk> a écrit :

» I have two polymorphic variant types, as follows:
» 
»    type f = [`A | `B of f]
»    type g = [f | `C]
» 
» Next, I have a function from f to g:
» 
»    let s1 : f -> g = function
»      | `A -> `A
»      | `B b -> b
» 
» Sadly, the compiler rejects this:
» 
»      Characters 57-58:
»        | `B b -> b;;
»                  ^
»    This expression has type f but is here used with type g
»    The first variant type does not allow tag(s) `C
» 
» The error message seems odd.  Why should it matter that g has more tags 
» than f, since every value of f is a value of g (by definition)?

f is indeed a subtype of g, but to forget the precise type of b (that is, forget the information that it cannot contain the tag `C), you have to use explicit coercion, i. e. :

  let s1 : f -> g = function
     | `A -> `A
     | `B b -> (b :> g)