単一化の際に型の出現検査をする

一つの型変数 = なんかの型 を考えたときに、「左辺の型変数」が右辺に含まれていないかどうか、を判定する

含まれている場合、どうごにょっても無理になるので、型に不整合があると判断し、処理を中断する

無理な例

一つの型変数 == なんかの型 という等式を考えている

CVar 1 は型変数

この等式を満たすような型 CVar 1 は存在しない

なぜなら絶対に右辺のほうが大きな型になるから

「左辺の型変数」が右辺に含まれていない、というのが条件になる

右辺が型変数を含まない型の場合も問答無用で結果はFalseになる

関数の例

上の例に合わせるなら 左辺 -> 右辺 -> 結果

返り値はbool

第一引数が、 Int になっているのは TVar のidを Int にしているから

参考