Occurs check in type inference I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with.

Constraints generation is presented in this table:



So, given the term λx.x x, we get the following two constraints, as far as I can see:


[λx.x x] = [x] → [x x] (from λ.x x)
[x] = [x] → [x x] (from x x)


Ok, onto the unification algorithm, described in the following manner:



Apart from the use of the word “identifier”, this looks easy enough. (Apparantly the author uses “identifier” since he first assigns a name such as 1⃣  to a term like [λx.x x] – I guess these boxed numbers are identifiers...)

Ok, so our stack of constraints is

{[λx.x x] = [x] → [x x], [x] = [x] → [x x]}


and our set of substitutions is empty. The first constraint can simply be added to the set of substitutions, which is now

{[λx.x x] ↦ [x] → [x x]}


We then replace each occurrence of [λx.x x] with [x] → [x x], but there are none, so our job in this step is done.

In the next step, the remaining constraint gets the same treatment: we simply add it to the set of substitutions, which then becomes

{[λx.x x] ↦ [x] → [x x], [x] ↦ [x] → [x x]}


But our job in this step is not done, we also need to recursively update all occurrences of [x] with [x] → [x x], so we get

{[λx.x x] ↦ [x] → [x x], [x] → [x x] ↦ [x] → [x x]}


Doing this again gives us

{[λx.x x] ↦ [x] → [x x], [x] → [x x] → [x x] ↦ [x] → [x x]}


… and so on, never terminating.

Is this understanding of the problem the “occurs check” solves correct? Is this what would have happened in a type inference algorithm such as Hindley-Milner if there wasn't an explicit occurs check?
Yes, the occurs check is there so that the algorithm is guaranteed to terminate. Without it, when we deal with an equation $X = T$ in which $X$ may occur, substituting $T$ for $X$ everywhere does not get rid of $X$, and so we can run in circles, as your example shows.

There is a way to avoid this by allowing arbitrary recursive types. If we have an equation $X = T$ then we may replace $X$ everywhere by the type $\mathsf{fix} \,X \,.\, T$, i.e., a canonical solution to the equation $X = T$. Ocaml will do this for you if you run it with -rectypes:

$ ocaml -rectypes
        OCaml version 4.01.0

# fun x -&gt; x x ;;
- : ('a -&gt; 'b as 'a) -&gt; 'b = &lt;fun&gt;


This says that fun x -&gt; x x has the type $A \to B$ where $A = A \to B$.

By the way, you can find an implementation of the algorithm in my PL Zoo, see solve in the language Poly.