Prettier errors with bindings in scope and solved corresponding types

[nachivpn]

Let the unifier continue unification in spite of failing to unify a constraint, and collect the problematic constraints separately. Printing the errors with "relevant bindings" and solved types (to the extent possible) could lead to a lot more readable errors.