Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the mgu and match.

Let's talk about the TAp case (full implementation in the article):

-- Substitutions are from a type variable to a type
type Subst  = [(Tyvar, Type)]


-- Calculate most general unifier 's' so that:
-- prop&gt; apply s t1 = apply s t2
mgu :: Monad m =&gt; Ty.Type -&gt; Ty.Type -&gt; m Subst
mgu (TAp l r) (TAp l' r') = do s1 &lt;- mgu l l'
                               s2 &lt;- mgu (apply s1 r) (apply s1 r')
                               return (s2 @@ s1)              -- &lt;=== THIS
-- ...snip...


-- Matching of t1 and t2 finds a substitution 's' so that:
-- prop&gt; apply s t1 = t2
match :: Monad m =&gt; Type -&gt; Type -&gt; m Subst
match (TAp l r) (TAp l' r') = do sl &lt;- match l l'
                                 sr &lt;- match r r'
                                 merge sl sr                  -- &lt;=== THIS
-- ...snip...


-- Substitution composition such that:
-- prop&gt; apply (s1 @@ s2) = apply s1 . apply s2
(@@)       :: Subst -&gt; Subst -&gt; Subst
s1 @@ s2    = [ (u, apply s1 t) | (u,t) &lt;- s2 ] ++ s1


-- A `symmetric' composition of substitutions such that:
-- prop&gt; apply (s1++s2) = apply (s2++s1)
merge :: Monad m =&gt; Subst -&gt; Subst -&gt; m Subst
merge s1 s2 = if agree then return (s1 ++ s2) else fail "merge fails"
  where agree = all (\v -&gt; apply s1 (Ty.TVar v) == apply s2 (Ty.TVar v))
                    (map fst s1 `intersect` map fst s2)


match is used only for matching predicates, mgu is used more often e.g. for actual type inference.

I can't wrap my head on why in the mgu the substitution composition is sequential and in match a symmetric composition is used. Why's that?

Furthermore, would it make a difference if I'd change the ordering of unification, so mgu would read:

mgu (TAp l r) (TAp l' r') = do s1 &lt;- mgu r r'
                               s2 &lt;- mgu (apply s1 l) (apply s1 l')
                               return (s2 @@ s1)
Ok, so I figured it out the next day. It's all dead simple as it came out.

Let's use an example – type applications z a a and z a b where z :: * -&gt; * -&gt; *. The unification will yield that (without further context) z a a is the most general type for both giving substitution {b↦a}. On the other hand, z a a cannot be matched to z a b, as they are simply different.

So now let's dissect the implementations. The mgu x@(TAp l r) y@(TAp l' r') first compares l and l' giving a substitution s1 &lt;- mgu l l'. The s1 is a knowledge of how part of x and y are different. With that knowledge, we can investigate further; that's why we use apply in s2 &lt;- mgu (apply s1 l) (apply s1 l') which gives us next premises on how different x and y are. So the summary is to compose the knowledge: s2 @@ s1 (ordering is as in function composition, e.g. g (f (x)) can be written as (g ∘ f) (x)).

I believe (without a proof though) that it's possible to just use s2 &lt;- mgu r r' and then try to combine s1 with s2 though some kind of recursion would be required. Also, I believe it's possible to match r with r' first and then match l with l'; the ordering is just to make error messages more obvious (order of reading in a file).

The match x@(TAp l r) y@(TAp l' r') is different. We must not approve the first example: z a a vs z a b. In order to do that we need to:


note that a from x would need to become a from y
note that a from x would need to become b from y
tell that the above two premises are contradictory


That's the reason to yielding strange substitutions like {a↦a} which is semantically equivalent to {} but allows for taking #1 into account.
The symmetric composition takes this additional information. It doesn't put apply in the second sub-matching (match (apply s1 r) (apply s1 r')) since applying a substitution would make us lose information about contradictory premises.