Comment by neel_k

If you have a bound on the size of the largest type in your program, then HM type inference is linear in the size of the program text.

The intuition is that you never need to backtrack, so boolean formulae (ie, SAT) offer no help in expressing the type inference problem. That is, if you think of HM as generating a set of constraints, then what HM type inference is doing is producing a conjunction of equality constraints which you then solve using the unification algorithm.