unification with occurs check