Type inference

Remarks

Example: in the Curry-style simply typed lambda calculus with type variables, take $t = \lambda f.\, \lambda x.\, f\, x$ and the empty context. Give $f$ the type $\alpha$ and $x$ the type $\beta$; the application $f\, x$ forces $\alpha = \beta \to \gamma$. So $t$ has the principal type $(\beta \to \gamma) \to \beta \to \gamma$, and each other type, such as $(\mathsf{b} \to \mathsf{b}) \to \mathsf{b} \to \mathsf{b}$, is a substitution instance of it. For this calculus the constraints are equations between types, and first-order unification solves them, so inference is decidable.

Non-example: the term $\lambda x.\, x\, x$ has no type in the simply typed calculus. Inference reaches the equation $\alpha = \alpha \to \beta$, which fails the occurs check of unification, and the algorithm reports that there is no type.

Type inference differs from type checking, which is the problem of deciding $\Gamma \vdash t : \tau$ for a given $\tau$. For the Curry-style System F, J. B. Wells proved that both problems are undecidable.