Hindley-Milner 类型系统中 letrec 的正确形式？

Question

对我来说，规则大致转化为以下算法：

推断 letrec 定义部分中所有内容的类型
1. 为每个定义的标识符分配临时类型变量
2. 递归处理所有具有临时类型的定义
3. 成对，将结果与原来的临时变量统一
关闭（使用forall）推断类型，将它们添加到基础（上下文）并用它推断表达式部分的类型

我在使用这样的程序时遇到了问题：

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

我观察到的行为如下：

p 的定义获得临时类型 a
x 的定义也得到一些临时类型，但现在不在我们的范围内
在 x 中，test 的定义得到一个临时类型 t
p 从作用域中获取临时类型 a，对变量使用 HM 规则
(f 5) 被 HM 规则处理为应用程序，结果类型为 b（以及 (a 与 Uint -> b 统一的统一）
((p 5) 5) 由相同的规则处理，导致更多的统一和类型 c，a 现在结果与 Uint -> Uint -> c
现在，测试结束以输入 forall c.c
in test 的变量测试获取具有新变量的类型实例（或 forall c.c），根据变量的 HM 规则，导致 test :: d （与 [ 统一=33=] 马上）
结果 x 有效地键入 d（或 t，取决于统一的心情）

问题：x 显然应该有类型 Uint，但我看不出这两个可以统一产生类型。当 test 的类型关闭并再次实例化时会丢失信息，我不确定如何克服或连接 substitutions/unifications。

知道应该如何更正算法以正确生成 x::Uint 打字吗？或者这是一个属性的 HM 系统，它根本不会输入这种情况（我怀疑）？

请注意，这对于标准 let 来说完全没问题，但我不想用 let 无法处理的递归定义来混淆示例。

提前致谢

Answer 1

回答我自己的问题：

Wiki 上的定义是错误的，尽管它至少在某种程度上可以用于类型检查。

向 HM 系统添加递归的最简单和正确的方法是使用 fix 谓词，定义 fix f = f (fix f) 和类型 forall a. (a->a) -> a。相互递归由双定点等处理

Haskell 解决问题的方法（在 https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b#binding-groups 中描述）是（粗略地）为所有函数推导一个不完整的类型，然后再次运行推导以针对每个函数检查它们其他.

Correct form of letrec in Hindley-Milner type system?