How do I add type annotations to interior locations in an abstract syntax tree?.... i.e. the type it [algorithm] infers is the type of the whole program, I would also like the types of any internal let-rec definitions so I can label my AST.

I had exactly the same problem: type reconstruction and the annotation of all sub-terms with their inferred types. Even if the overall type inference fails, the user can still see what the type checker was able to infer before the error. Here is the solution http://okmij.org/ftp/Computation/FLOLAC/TEvalNR.hs There is a bit of the explanation here: http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf