Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier
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.