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.
与恶龙缠斗过久,自身亦成为恶龙；凝视深渊过久,深渊将回以凝视…
