Until now every lambda spelled out its parameter type, so there was nothing to discover. Take the annotation away and the checker has to invent a placeholder - a fresh type variable - stand it in for the parameter, and infer the body with that placeholder in scope. For the identity \x. x, the body is just x, whose type is the placeholder a, so the whole thing is a -> a: a function from some type to the same type, exactly the polymorphic identity you would hope for. \x. \y. x nests the trick twice and comes out a -> b -> a.

This lesson also quietly upgrades the engine’s plumbing. Inference now threads a substitution alongside the type it returns, because the body may refine the parameter’s placeholder as it goes, and that discovery has to flow back out to the arrow. The public Infer stays the same shape - give it an environment and an expression, get a type - and it applies the final substitution before handing the type back. Two small conveniences keep the output stable. Infer resets the fresh-variable supply at the start of each top-level call, so the ids a program uses do not depend on what ran before it (which matters the moment an error message names a variable). And because substitution can leave gaps in those ids, a small Show renames the variables in a finished type to a, b, c in the order they first appear, so \x. x reads back as a -> a every time. The parameter of \x. x never gets refined, so it stays fully general; the next two lessons are where using the parameter starts pinning it down.