Oleg has a nice article on how to implement OCaml-style type inference. It's a more sophisticated approach than just Algorithm W: http://okmij.org/ftp/ML/generalization.html
For me, this article was the one where it "clicked": http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval . Summary: type inference is just "evaluating" the program/expression, but the result is a type instead of a value. Each time you evaluate a function call, use unification to bind the arguments rather than pattern matching. Another way to understand it: pattern matching only works "one way", whereas unification wo…
Damas-Milner type inference uses an "occurs check" to prevent the type equation solver from unifying a type variable with a compound type expression containing the same variable. The "obviously correct" way to perform this check is eagerly - as soon as possible.
However, performance-wise, delaying the occurs check can speed up the inference process - and this is exactly what OCaml does. The downside is that the resulting algorithm is quite involved, because the solver can now run into type expressions containing cycles, so naively recursively walking type expressions can cause an infinite loop.