Unification is the heart of inference - the operation that makes two types equal by solving for their unknowns. Today you build its first two cases - two ground types, and a variable meeting a type it must become.
Unify two base types, and bind a variable to whatever type it is unified against.
Unification answers a sharper question than Equal did. Equal asks “are these
two types the same?”; unification asks “what would make them the same?” and returns
the substitution that does it, or fails if nothing can. It is the engine that lets a
lambda parameter start as an unknown a and become Int the moment it is used where
an Int is required.
Today covers the two base cases. When both sides are the same ground type, they are
already equal, so unification succeeds having learned nothing - the empty
substitution. When they are different ground types, Int and Bool, nothing can
reconcile them and unification fails; that failure is the argument-mismatch error
from chapter two, now expressed as unification. The interesting case is a variable
meeting a type: since a stands for an unknown, you make the two equal simply by
deciding a is that type, and record { a -> Int }. It works from either side,
because unification is symmetric. One case is still missing, and it is the one that
keeps unification from looping forever - that is next.
// unify makes two types equal, returning the substitution that does it.func unify(a, b Type) (Subst, error) {switch {case bothBaseAndEqual(a, b): return Subst{}, nilcase isVar(a): return Subst{a.(TVar).Id: b}, nil // bind a to bcase isVar(b): return Subst{b.(TVar).Id: a}, nil // bind b to a}return nil, fmt.Errorf("cannot unify %s with %s", a, b)}