I can try to explain why HM type inference and unification are related. If you take just the lambda calculus where you have: 1) Lambdas that bind variables 2

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