Comment author: @garrigue

For principality reasons, in general it is not correct to unify argument types in the upper bound. It is of course correct in some cases, but detecting them is non-trivial: it amounts to checking an equivalence between two quantified logical formulae. I tried once, but this was really too much work to be worth it.
The specific case you describe here is simpler than the general one, since it would be sufficient to check that a type variable only occurs as argument of a single variant type, but this is still some work.

Comment author: @lpw25

I think the first example is the only one that is actually confusing because you start with two types which have no conjunctions and, even though the types can unify, you end up with a conjunction.

Would it not be safe (and easy to implement) to attempt unification when faced with two types which do not have any conjunctions (e.g. [< Foo of 'a] and [< Foo of int]) and then only fallback to a conjunction (e.g. [< `Foo of 'a & int]) if the unification fails?

Comment author: @lpw25

Would it not be safe (and easy to implement) to attempt unification when faced with two types which do not have any conjunctions (e.g. [< Foo of 'a] and [< Foo of int]) and then only fallback to a conjunction (e.g. [< `Foo of 'a & int]) if the unification fails?

Actually, I guess that would be less general since it would not allow:

# let f (x : [< `A of 'b | `B of string]) (y : 'b) = x;;
val f : ([< `A of 'b | `B of string ] as 'a) -> 'b -> 'a = <fun>

# let g (x : [< `A of int | `B of string]) (y : float) = f x y;;
val g : ([< `A of int & float | `B of string ] as 'a) -> float -> 'a = <fun>

# let h (x : [`B of string]) (y : float) = g x y;;
val h : [ `B of string ] -> float -> [ `B of string ] = <fun>