Lambda the Ultimate

This is not the best place for a query like this (in my opinion) though I'm not quite sure of a better place. comp.lang.functional is certainly a possibility. Checking out the Getting Started page offers many possibilities. It, however, doesn't mention "Programming Languages: Application and Interpretation" which is probably closest to what you want.

Perhaps you'd like the following, less canonical explanation of type
inference and type reconstruction, from simply-typed lambda-calculus
to let-polymorphism:

http://okmij.org/ftp/Computation/Computation.html#teval

It was presented at the summer school FLOLAC. Chung-chieh Shan and I
wanted to emphasize type inference as abstract interpretation, and
polymorphism as inlining. The complete Haskell code for the
progression of various interpreters and type-checkers is available
from the above page.

The Wikipedia article actually isn't a bad starting point.

Your basic HM-style inference strategy works bottom-up. You design your language so that every literal has a unique type. You define some functions that are near the "bottom" of the system (add, subtract, etc.) and you define rules for those: "if add takes two ints then it return int". Basically, for each syntactic structure of the language you define a "type rule" for the gazintas and the gazoutas. These rules take the form "well, if I know the following things, then I can conclude the following other things". The type inference implementation is merely a capturing of those rules in source code. Generally you'll need some form of unification, but that's just linking things together.

For something like ML, that's about it. Some formal work is required to make sure that your type system is sound and complete, but that's not the question you seem to be asking.

Perhaps the reason that there isn't a simple tutorial is that things go downhill quickly from there. Want to define +/- over ints and floats but not strings? Great. Now you need a constraint system and a solver. Want to deal with subtypes? Now you need a solver that handles inequalities and you need to worry about contravariance. Want to do both in the same language? Now you either need a really talented psychiatrist or you need to hire Oleg. :-) Want a language that does polymorphic inference with mutability and unboxing? Now you need either the psychiatrist or Swaroop Sridhar. Aspirin is also good here. Dependent types? Really cool, but they have known to cause cranial explosions in otherwise mathematically inclined computer scientists (since his head is intact, one may infer from this that Benjamin Pierce is either not a computer scientist or not entirely human, but he's still a nice guy).

What I'm trying to get at here is that the most basic HM-style inference is pretty simple, but inference gets complicated very quickly as seemingly innocuous things get added to the language. Of course, if Joe the Language Plumber wanted to design something exactly like ML, he'ld just use ML, so each language carries its own new inference challenges. BitC is (we think) a present extreme. Of the ~30,000 lines in the BitC front end, almost 9,000 are taken up by the type inference mechanism and the constraint solver. It would probably be smaller if it weren't written in C++, but there was this reductio problem...

Lisp isn't a good candidate for HM-style type inference, for a couple of reasons. First, LISP is dynamically typed, so HM-style inference doesn't apply straightforwardly. Second, many of the things that smell like types in lisp aren't simple to describe. For example, lisp lists are heterogeneous. One way to think of this in terms of static types is that there are a whole lot of places in lisp where the constraints on what type a given symbol must be aren't constraining enough to generate a unique answer. And there really isn't anything in LISP that is mathematically analogous to sum types (unions) or product types (roughly: structures) in ML.

While BitC gives an example of one way to impose static types on LISP, it's a result achieved at considerable complexity, it's strictly static (so there are some things LISP does that it can't express) and it's inference mechanism is too complicated to serve as a learning tool. Another thing to look at if you are interested in lisp-like languages would be typed scheme, but I have no sense of how simple or complicated that inference engine might be.

One thing you might consider is looking over the Hugs implementation for haskell, which is readily available and not overwhelmingly complicated.

The Book: Types and Programming Languages by Benjamin C. Pierce has the best section on HM style typechecking that I have seen. More great stuff in that book also.

I personally found the Typing Haskell in Haskell paper useful for my discovery of HM type-inference, since a complete version of a type-checker is built progressively, in a readable and testable form (that is, in Haskell). The type-checker is built for a subset of Haskell 98 which is powerful enough to be useful as a basis for future extensions and yet understandable. I think it might be helpful to you as well.

Since you're programming in haskell, you might find this interesting

Practical type inference for arbitrary-rank types

While the paper is about higher-rank types, it includes a tutorial on implementing HM type inference using a cool monad to keep track of unification variables (and unify them). There is an associated implementation.

I believe the Nice programming language has substantial advances in type inference over basic HM implementations from ML era. (I haven't been following Haskel though. Might have the same thing.) Back when I was studying type inference there was a hard nut around higher order polymorphism that seems to have yielded ground at least practically. Google Bonniot (Nice language guy) for clues.

http://lucacardelli.name/Papers/BasicTypechecking.pdf
I learned by reading Luca Cardelli's paper. It has working code in the appendix. It's in Modula-2, but you should be able to understand it if you know Pascal or C.