# 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?

• is this related to occurs check in gprolog (preventing infinite loops)? – seteropere Apr 25 '14 at 8:05
• @seteropere: I think so. As far as I know, the name comes from Prolog. – beta Apr 25 '14 at 13:37
• It's essentially the same unification algorithm as the one in prolog. – Andrej Bauer Apr 26 '14 at 22:30

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 -> x x ;; - : ('a -> 'b as 'a) -> 'b = <fun>  This says that fun x -> 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.