Non-transitivity of type unification

We know type unification is not transitive in general

a ~ b /\ b ~ c does not imply a ~ c

And it's easy to find examples that don't unify

a |-> Int; b |-> b; c |-> Bool
a |-> (Int, a'); b |-> (Int, Bool); c |-> (c', Bool)

In all the examples I can make up, there's two outer types that don't unify, and a piggy in the middle that is either strictly more general than the outers (bare b) or strictly subsumed (Int, Bool).

For some (malicious) testing, I want an example where each three pairings of types unify, but the three types together do not. That is

a ~ b /\ b ~ c /\ a ~ c but not mgu(a, b) ~ c

Can anybody concoct such an example?
Or point me to something showing it's impossible.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

repeated type vars

OK cracked it

a |-> (Int, a'); b |-> (b', b'); c |-> (c', Bool)

a ~ b, mgu |-> (Int, Int)
b ~ c, mgu |-> (Bool, Bool)
a ~ c, mgu |-> (Int, Bool)

None of those mgus unify.

Are there any examples not relying on repeated type vars?

Probably need type vars?

Offhand, it seems like you'd need to have repeated type var. If you had a conflict between concrete type constructors in some part of the type, that conflict would exhibit with the pair that introduced those constructors.