Type inference for HM is actually exponential, due to generalization for let-polymorphism. You're probably thinking of inference for a language with just simpl

Type inference for HM is actually exponential, due to generalization for let-polymorphism. You're probably thinking of inference for a language with just simple types.