## 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

### 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.