# Question about let syntax in type systems

• As far as I can tell that section is just poorly written. What you should get out of it is that HM can only generalize let bound functions, and that this change (or some change) is necessary because type inference (and type checking) are undecidable in the polymorphic lambda calculus. If you've understood that, I wouldn't put any more effort into deciphering what the author of that section intended. – Derek Elkins Jan 23 at 22:24