Comment by ReleaseCandidat

Type checking (type inference) is the usual application of unification in programming languages (compilers or interpreters). Pattern matching does not need unification, because, as mentioned in the beginning of post, the "matching" is done one the left side only (no variables to "match" on the right side).