一致替换的目标
合一中的替换把变量统一地换成项，而不是只改某一处字符。例如，f(X, a) 与 f(b, Y) 可以用 X = b、Y = a 变成同一个项；同一变量的所有出现必须遵守这份替换。
在有限的一阶项问题中，最一般合一子保留尚未被约束的自由度，其他解可以继续实例化得到。算法寻找的是约束允许的通用解，而不是随意选一个碰巧匹配的具体值。
参考：[1]
拆解结构并传播条件
类型推断可以把两个函数类型相等，拆成参数类型相等和结果类型相等。找到某变量的替换后，还要把它传播到剩余约束，继续处理直到没有未解决的等式，或发现冲突。
不同基本类型不能因为名字接近就合一，构造子或参数个数不符也会导致结构性失败。合一解决给定的等式约束，并不代表所有更丰富的类型系统都能用同一套规则推断。
参考：[1]
有限项与循环项的区别
若变量 X 必须等于 f(X)，就没有有限展开的一阶项解。出现检查在绑定变量之前检查它是否已出现在目标项中，避免偷偷把有限类型约束改成无限递归结构。
SWI-Prolog 明确区分这种检查与默认可建立循环项的合一行为。其 unify_with_occurs_check 阻止新建这种循环；已有循环项的处理还有实现边界，因此跨系统程序不能假设所有“合一”具有完全相同语义。
参考：[2]