Type unification
= Type unification
<Type unification> finds a <type substitution> making specified type expressions equal, or reports incompatible constraints. In our <simple type> grammar, matching two <function types> reduces to matching their argument types and their result types. Distinct base types `int` and `bool` fail to match; solving a <type variable> against a nontrivial type expression uses the <occurs check>.
// Target: computer-science.bigb