This is the promise of the chapter, delivered. The program let id = \x. x in let const = \x. \y. x in const (id 5) true has no type annotation anywhere, yet the checker works out that id is polymorphic (forall a. a -> a), that const is forall a b. a -> b -> a, that id 5 is Int, and that const applied to an Int and a Bool returns the Int - so the whole program has type Int. Every mechanism you built carries some of that weight: fresh variables, unification, substitution threading, generalization at each let, and instantiation at each use.

The rejection matters just as much. \x. if x then x else 1 looks plausible until you follow the constraints: using x as a condition forces it to Bool, but then the then branch returns that same Bool where the else branch says the result is Int, and the two cannot agree - cannot unify Bool with Int. A checker that accepted it would let a Bool flow where an Int is needed at runtime. You now have a complete Hindley-Milner inference engine for the functional core: literals, variables, let, if, functions, application, and full let-polymorphism, inferring the principal type of any program in that fragment. The remaining chapters widen the language it accepts and sharpen the errors it reports.