Occurs check in type inference
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.