My approach to the typing error reporting is quite compatible with the Prolog codegen. What I do: for each AST node which produce one or more type equations I record the location data (cache it and give it an index), and then issue a Prolog term like this: with_location(Id, Term), for each of the terms generated by this location.

with_location semantics is simple, but may depend on the presence of a backtracking. If it's a plain Hindley-Milner, there is no backtracking, and it simply do call/1(Term), continue if true, store Id and the failed term with all the current bindings and fail/0() if false.

If there is a backtracking, I store a stack of location ids and failure reasons instead, but this required patching the Prolog execution engine a little bit (luckily, I'm using my own Prolog for this).

Now, the next step is to decipher the failed term. Most of the equations are in a trivial form: equals(A, B), so I simply report that prolog_to_type(A) failed to unify with prolog_to_type(B). For the other (rare) kinds of equations I define custom pretty-printing rules.