= Occurs check
The <occurs check> tests whether a <type variable> occurs inside the expression proposed as its replacement during <type unification>. After discarding a trivial <equation> such as $\alpha=\alpha$, solving $\alpha=\tau$ by a <type substitution> requires that $\alpha$ not occur in $\tau$. Thus $\alpha=\mathrm{int}\to\beta$ is permitted when $\alpha$ and $\beta$ are distinct, but $\alpha=\alpha\to\beta$ is rejected in our finite <simple type> grammar.
There is a short reason for the rejection. If a finite replacement $T$ for $\alpha$ existed, with replacement $B$ for $\beta$, the <equation> would become $T=T\to B$. The right side's <abstract syntax tree> has one new arrow node plus the nodes of $T$ and $B$, so it has strictly more nodes than $T$. Equal finite type expressions cannot have different sizes. <Recursive types> are a different design: they explicitly describe self-reference and specify how it interacts with <typing judgments>.
Back to article page
