Mmmh I see. Thanks for your answer.

I spent hours to understand how ([< `A | `B of 'a ] 'a) was transformed
into ([< `B of 'a ] as 'a) and I did not saw the influence of the
polymorphism in the type-checking.

Thanks again.

On 05/28/2013 10:13 AM, Leo White wrote:
>> 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