In unification, there is a "occur-check". Such as $X = a \, X$ fails to find a substitution for $X$ since it appears on right hand side too. The first-order unification, higher-order unification all have occur-check.
the paper nominal unification described a kind of unification based on nominal concepts. But I did not mention "occur-check" at all.
So, I am thinking why? does it has occur-check?