[emillon]

I was not totally right in the my "uncle" comment. It has to do with the value restriction in the sense that it is where the distinction occurs (lambdas are never genezalized ; let-bindings are generalized for values), but the original HM system (without refs) indeed made this distinction.

I believe that if you don't do it and generalize everywhere, unification of types is harder or even impossible because everything has a type scheme.

This would look a lot like System F, for which type inference is undecidable, for example.