1

（这是多态变体和 let%bind 类型错误的扩展/蒸馏）

考虑以下代码：

版本 1：

let x : [> `Error1 ] = (`Error1 : [> `Error1 ])
let y : [> `Error1 | `Error2 ] = x

版本 2：

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])
let y : [> `Error1 | `Error2 ] = x

版本 1 类型检查，但版本 2 失败（我正在使用 4.09.0 编译）：

File "test.ml", line 2, characters 33-34:
2 | let y : [> `Error1 | `Error2 ] = x
                                     ^
Error: This expression has type [ `Error1 ]
       but an expression was expected of type [> `Error1 | `Error2 ]
       The first variant type does not allow tag(s) `Error2

请注意，此错误发生在 的定义中y，但两种情况下的签名x相同！怎么y能看到里面的定义x呢？是否有x比其签名更多的类型检查信息？

4

1 回答 1

3

简而言之，显式类型注释不是类型签名。特别是，在

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

的类型x是[ `Error1 ]。

问题的根源在于显式类型注释中的统一类型变量可以与具体类型统一。

你的问题的一个更简单的例子是

let f: 'a -> 'a = fun x -> x + 1

在这里，'a -> 'a注释与实际类型统一，int->int因此此代码类型检查。如果要使类型变量'a具有通用性，则需要通过添加显式通用量化来更加明确

let f: 'a. 'a -> 'a = fun x -> x + 1

Error: This definition has type int -> int which is less general than
'a. 'a -> 'a

使用隐式行变量的代码也会发生同样的现象：

let x : [> `Error1 ] = (`Error1 : [ `Error1 ])

此注解不保证 is 的类型，x只[> `Error1]保证可以与[> `Error1]. 并且由于类型[ `Error1 ]可以与 统一[> `Error1 ]，因此没有理由引发错误。

和以前一样，如果你想避免这个问题，你需要明确哪些变量在你的注释中被普遍量化：

let x : 'row. ([> `Error1 ] as 'row) = (`Error1 : [ `Error1 ])

Error: This expression has type [ `Error1 ]
      but an expression was expected of type [> `Error1 ]
      The second variant type is bound to the universal type variable 'a,
      it cannot be closed
于 2020-06-03T15:28:57.710 回答