Occurs Check

type-theory

Definition

Occurs Check

The occurs check is the unification test that rejects binding a variable to an expression that already contains that variable.

Formally, a proposed substitution

$$\alpha \mapsto \tau$$

is rejected when

$$\alpha \in \mathrm{ftv}(\tau ).$$

In type inference, this prevents infinite types such as $\alpha =\alpha \to \beta$.