I've never done Hindley-Milner type inference before, and I just took a look at Poly. It's nice to see the solve function there, looking nice and simple like I hoped. XD It seems Algorithm W just treats the program as a graph of type equality constraints, and it does substitutions and such until it runs out of equations to process, at which point it's collected a full map of type variable bindings. I hope that makes sense.
