Unification is a vital process in the implementation of Hindley-Damas-Milner type inference. In the original paper it is mentioned in passing as assumed knowledge, so here is an explanation of unification in with a little help from the HM type theory.
