We could split type inference in its subparts
For example, one with the gathering of the typing relation, and one for the type variable equations, one aspect for unification.
For example, one with the gathering of the typing relation, and one for the type variable equations, one aspect for unification.