I'm getting a few detailed responses :) Unfortunately, I'm getting conflicting answers. I'm having trouble wrapping my head around why App+Abs couldn't be equivalent to Let in the absence of the value restriction.
If you look at the [Abs] rule, you will see in the premise "x : tau". Here, by definition, tau is non qualified. It represents a unique type. It's necessary monomorphic. Concretely, it means x will be bound to a type variable in the type environment and this type variable will uniquely be unified.
On the other hand, the premise for [Let] is e0 : sigma, x : sigma. Contrary to tau, sigma is qualified (polymorphic). So, it can be unified to a different type variable in different expressions.
I completely understand why it fails you. The way qualifier affects the unification process is quite complicated. I finally understood it only after having to write my own rules when I was implementing a type checker for my master thesis.
If you don't mind the formalism, read carefully the Wikipedia article paying particular attention to how tau and sigma are defined and to the paragraph about free and bound type variables. If you want something more practical, look at the Peyton Jones book I gave a link to in this thread. Part 9.5 is the important part but it's difficult to get without having read the whole chapter (eventually chapter 8 too). It 's still complex but far less abrupt than the Wikipedia article.
If the SPJ book is the one about implementing functional languages, then I've got a copy on my laptop I can peruse when I get home from work.
This causes difficulties because the set of free type variables needs to be calculated in order for generalisation to produce safe type schemes, and that is tough to do for an unknown set of expressions.
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.