I am pretty new to type inference and was wondering if there are any good extensions or papers out there for HM that allows allowing more than one error.
I might be missing something but if there is a unification error, can the type-checker proceed given that the type contexts are "poisoned"?
You can recover from unification errors (including occurs check failures) by ignoring all or part of the offending unification, and you can recover from "unknown identifier" errors by typing the identifier with a fresh type variable. It's easy enough to arrange not to "poison" your type context, even if you decide to partially process a particular unification.
To be a little more concrete, if you're implementing some version of Algorithm J, then roughly speaking the program text entirely determines a recursively constructed sequence of "instructions" to transform a type context. The only "instructions" that can fail are looking up the polytype of an unknown identifier in [Var] and the unification step in [App]. Everything else (instantiation of a polytype in [Var], creating fresh type variables in [App] and [Abs], generalizing a monotype to a polytype in [Let], or augmenting the type context in [Abs] and [Let]) cannot possibly fail, assuming the type context representation is not actually corrupted.
The unification "instruction" will typically be implemented as a recursion that matches up primitive type constructors (function arrows (->), pairs, lists, or whatever other primitive types you've included) before binding a sequence of type variables to monotypes. Depending on how you represent the results of unification, you'll probably find that simply pruning the recursion at any type constructor mismatches (attempts to unify functions and pairs, etc.) and skipping any attempted bindings that fail an occurs check will leave your type context in a valid state, so type checking can continue and potentially generate other informative errors.
