haskell - HindleyMilnerと制約を使用して再帰式を推測する

Question

次の式のタイプを推測しようとしています。

let rec fix f = f (fix f)

タイプを指定する必要があります(a -> a) -> a

ボトムアップアルゴリズム（ヒンドリーミルナー型推論アルゴリズムの一般化で説明）を使用した後、以下にルールを追加します。

           a1, c1 |-BU e1 : t1     B = fresh var
---------------------------------------------------------
a1\x, c1 U {t' == B | x : t' in A} |-BU let rec x = e1 : t

私は次のタイプが残っています：t1 -> t2

および次の制約：

t0 = fix
t1 = f
t2 = f (fix f)
t3 = f
t4 = fix f
t5 = fix
t6 = f

t3 = t1
t3 = t4 -> t2
t5 = t0
t5 = t6 -> t4
t6 = t1

タイプが残っているように、これらの制約をどのように解決できるかわかりません(a -> a) -> a。私が間違っているのを誰かが見るのは明らかだと思います。

完全なソースコードはこちら

Answer 1

t7最初にあるべきではありませんfix fか？これらは制約を与えます:

t7 = t2
t0 = t1 -> t7

t4 = t2そこから、それを推測できるはずですt0 = (t2 -> t2) -> t2。