Macro typechecker: improve treatment of equalities

The solver didn't handle equalities properly, as it didn't account for
the result of unification. Now, we try to unify, and if the unifier
makes no progress we make the constraint into an inert constraint.