AST with type variables
Hindley-Milner: watch unification solve type constraints step by step
Hindley-Milner collects equality constraints between type variables, then solves via Robinson unification. Let-polymorphism generalizes variables not bound by lambdas, giving ML-style parametric polymorphism.
Hindley-Milner type inference is sound and complete: if a type exists, it will be found. The algorithm runs in nearly-linear time via union-find. The "self-apply" example (λx.x x) has no type in simple HM — it requires recursive types.