型推論器を作る(3) 単相の型推論②出現チェック

前回のunifyでは、型のコピーを取りました。その型のコピーがもしも、自分自身の型だったら、型が循環して場合に寄ってはコンパイラが止まらなくなってしまうかもしれません。
そこで、型をコピーする前に型が自分の中に含まれていないかをチェックします。
それが、occurs checkです。

  let rec occurs (tvr: tv ref) (t:t):unit =
    match t with
    | TVar tvr' when tvr == tvr' -> failwith "occurs check"
    | TVar({contents = Link t}) -> occurs tvr t
    | TArrow(t1,t2) -> occurs tvr t1; occurs tvr t2
    | _ -> () 

実装は上記のように簡単です。型tの中身が型変数でかつ自分自身なら例外を投げます。
Linkならその中身をチェックし直します。
関数の型なら再帰的にチェックします。

この作成した出現チェック関数をunifyに組み込めば、出現チェックがうまく動作するようになります。

    | (TVar({contents=Unbound _} as tv), t)
    | (t, TVar({contents=Unbound _} as tv)) ->
      occurs tv t';
      tv := Link t