The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a -> [> 'a b ] », it does compile but I don't
know why the previous code doesn't.

Does somebody have any hints ?

Your f function expects an argument of type:

  ([< `A | `B of 'a ] as 'a)

whilst (M.b (M.a ())) has type:

  [`B of [`A]]

If you try to unify these two types, you have to unify 'a with both [`A]
and [`B of [`A]]. These types can't be unified since they are both
closed and are not equal.

If you change the definitions of M.a and M.b as you described, then (M.b
(M.a ())) has type:

  [> `B of [> `A]]

If you try to unify this with the type of f's argument, you unify 'a
with [> `A] and [> `B of [> `A]]. These types can be unified because
they are both open and are not incompatible.

Note that you can use subtyping to give the original (M.b (M.a ())) the
type:

  ([`A | `B of 'a] as 'a)

which *is* unifiable with the argument type of f:

  f (M.b (M.a ()) :> [`A | `B of 'a] as 'a)

Regards,

Leo