archives

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.