Вывод рекурсивных выражений с использованием Хиндли Милнера и ограничений

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,