TaPLを読んだものの、雰囲気でしか理解できません。MLで書かれたコードを意味もわからずパクるくらいしか出来ることがないので、独自研究で色々やってみます。
https://kuis-isle3sw.github.io/IoPLMaterials/textbook/chap04-5.html
Glispは構造的部分型付けを採用するため、単一化アルゴリズムにおける代入（Substitution）は $\sigma = [\alpha \mapsto \tau]$ の形式ではなく、$\sigma = [\alpha \mapsto [\tau_{lower}, \tau_{upper}]]$ の形で、型変数が取りうる型の下限と上限を範囲指定します。
同様に、制約（Constraints）は等式だけではなく不等式を扱います。（現状のアルゴリズムは等式 $\alpha = X$を2つの不等式 $(\alpha \leq X) \land (\alpha \geq X)$として扱っていますが、Glispの型の内包関係はもしかしたら反対称的ではないかもしれません。）そして、左辺に含まれる型変数が動く範囲が、右辺に含まれる型変数によって表されるよう単一化を試みます。つまり、不等式の左右を入れ替えて単一化をした場合、異なった代入が返されます。
上記のHindley-Milnerの単一化アルゴリズムは、不正な制約集合にはエラーを返します。しかし、漠然と型付けに失敗したと表示されるより、どの項がどう適合しなかったかを具体的に教えてくれたほうが便利です。Glispの戦略は、不正な制約のうちできるだけ有効な部分制約を抽出するとともに、不正あるいは不定となる制約は、$X \leq \top$や$X \geq \bot$のように自明な制約に読み替えて単一化を試みます。こうすることで、左辺に登場する型変数すべてについて、何らかの型付け範囲を代入に合成し、代入を左辺に適用したときに型変数が置換されず残されるのを防ぎます。
代入に関しても、例えば$\alpha \mapsto [Int, Bool]$のように（整数型は真偽型の部分型ではないので）不正な範囲を取る場合、下限を上限にコピーすることで正規化します。
コーディングの単純化のため、代入を順序付きの置換リストではなく、型変数 $\alpha$ から型の下限・上限のペア $\tau_l \times \tau_u$ への部分関数と考えます。代入$\sigma$を拡張するたび、終域（元となった制約における右辺）に含まれる型変数を単一化し、終域から型変数を取り除くようにします。これは、(. id id)が$\alpha \rightarrow \alpha$ではなく$\alpha_1 \rightarrow \alpha_2$のように推論されるのを防ぐためです。
RangedUnifier.addConsts で行っているアルゴリズムを下に示します。