Правильная форма letrec в системе типа Hindley-Milner?

У меня возникли проблемы с пониманием определения letrec для системы HM, которое приведено в Википедии, здесь: https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

Для меня правило грубо переводится по следующему алгоритму:

выводить типы на все в разделе определения letrec
- присваивать переменные временного типа каждому определенному идентификатору
- рекурсивно обрабатывать все определения с временными типами
- в парах, унифицируйте результаты с исходными временными переменными
закрыть (с forall) выводимые типы, добавить их в базу (контекст) и вывести типы выражения с ней

У меня возникают проблемы с такой программой:

letrec
 p = (+)     --has type Uint -> Uint -> Uint
 x = (letrec
       test = p 5 5
     in test)
in x

Поведение, которое я наблюдаю, выглядит следующим образом:

определение p получает временный тип a
определение x также получает некоторый временный тип, но теперь из нашей области
in x, определение test получает временный тип t
p получает временный тип a из области действия, используя правило HM для переменной
(f 5) обрабатывается по правилу HM для приложения, итоговый тип - b (и унификация, которая (a объединяется с Uint -> b)
((p 5) 5) обрабатывается по тому же правилу, что приводит к большему количеству унификаций и типу c, a теперь в результате объединяется с Uint -> Uint -> c
теперь тест закрывается, чтобы ввести forall c.c
переменная test in test получает экземпляр типа (или forall c.c) со свежими переменными, в соответствии с правилом HM для переменной, в результате чего test :: d (который унифицирован с test::t справа)
в результате x эффективно набирает d (или t, в зависимости от настроения унификации)

Проблема: x должен, очевидно, иметь тип Uint, но я не вижу, чтобы эти двое могли объединяться для создания типа. Существует потеря информации, когда тип test закрывается, и экземпляр снова появляется, что я не уверен, как преодолеть или подключиться к подстановкам/унификации.

Любая идея, как алгоритм должен быть исправлен для корректной печати x::Uint? Или это свойство системы HM и просто не будет вводить такой случай (что я сомневаюсь)?

Обратите внимание, что это было бы вполне нормально со стандартным let, но я не хотел обфускать пример с помощью рекурсивных определений, которые невозможно обработать с помощью let.

Заранее спасибо

Ответ 1