I can try to explain why HM type inference and unification are related.<p>If you take just the lambda calculus where you have:<p>1) Lambdas that bind variables<p>2) Usages of bound variables<p>3) Function applications<p>The inference rules for the first 2 are simple &amp; straight-forward and require no unification.<p>For 1 (lambdas) - you create a fresh type variable (e.g: &#x27;a&#x27;) for the parameter type and infer the lambda body (e.g: &#x27;T&#x27;), and the lambda&#x27;s type is then &#x27;a -&gt; T&#x27;. While inferring the lambda body, you also pass the information that the parameter bound by the lambda has-type &#x27;a&#x27;.<p>For 2 (variable usage), you just use the known type information that was passed down by the lambda inference.<p>For 3 (application), you need unification. Function application is between two subexpressions (e.g: &#x27;f&#x27; and &#x27;x&#x27;). You infer both of these recursively, and get 2 types (e.g: &#x27;fType&#x27; and &#x27;xType&#x27;).  But you also know that &#x27;fType&#x27; must look like: &#x27;xType -&gt; resType&#x27; because it&#x27;s being applied to &#x27;x&#x27;. You also know that &#x27;resType&#x27; is the result of the entire application. So you have to unify &#x27;fType&#x27; with &#x27;xType -&gt; resType&#x27;.<p>This is why inference relates to unification: You have 2 sources of information for &#x27;fType&#x27; and &#x27;xType&#x27; -- the recursive inference AND the fact they&#x27;re being applied together.<p>This unification, by the way, is the only way that type information is learned for parameter types. If all parameter types are always specified (as in, e.g: C++) then formally, there&#x27;s no type inference at all. So what C++ calls &quot;local type inference&quot; is formally just type checking.