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.