Eratta 3.2 Type Unification

Glossary ;

Type Unification

The method by which two type expressions are "unified".  The type
expressions are matched along their structure. Where a type variable
appears in one expression it then "unified" to represent the corresponding
structure element of the other expression, be it another variable or
subexpression. All variable assignments must remain consistent in both
structures.  Unification fails if the two expressions cannot be aligned,
either by having dissimilar structure, or by having instance conflicts,
such as a variable needs to represent both "xs:string" and "xs:integer".  
For a full explanation of type unification, please see [Ref].

[Ref] Hancock, "Polymorphic Type Checking", in Simon L. Peyton Jones,
"Implementation of Functional Programming Languages", Section 8, 
Prentice-Hall International, 1987