Just to note one error in I.2.1:

> ... whereas unification without the occur check is linear on the size of the smallest of the terms being unified.

This claim is incorrect, it goes far beyond what is possible. To see its incorrectness consider the unification problem X = Y. And just for illustrative purposes, think of them both as being very big and evolved. Now, consider a related unification problem Z-Z = X-Y with Z just a variable. According to above claim, the cost would be now independent of X and Y which cannot be.