A compiler can infer types by assigning unknown type variables to expressions and turning typing requirements into type constraints.

Suppose a function is written without annotations:

fun f(x) = x + 1

Give $x$ an unknown type $\alpha$. The typing rule for addition requires both operands to be integers, producing

$$\alpha=\text{Int}.$$

The function therefore has inferred type

$$\text{Int}\to\text{Int}.$$

Function application generates a structural constraint. If $e_1$ has unknown type $T_1$, $e_2$ has type $T_2$, and the application receives fresh result type $\beta$, then typing requires

$$T_1=T_2\to\beta.$$

A complete expression accumulates many such equations. They are then solved using first-order unification over the type-expression constructors.

For

fun f -> fun x -> f x

fresh variables lead to the requirement that the type of f be $\alpha\to\beta$, giving the function type

$$(\alpha\to\beta)\to\alpha\to\beta.$$

Constraint generation separates syntax-directed collection of requirements from the general equation-solving algorithm. That factorization lets the same unification machinery serve type inference and other symbolic tasks.