F*中的应用函子:类型检查错误

Question

作为一个实验，当我试图熟悉F*时，我尝试实现一个应用函子。我被一个奇怪的类型检查错误困住了。我还不确定这是由于类型检查中的某些特性/逻辑所致，而我并没有意识到，或者这是由真正的bug引起的。

下面是代码中给我带来麻烦的部分：

module Test

noeq type test : Type -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

以下是相应的错误：

Test(7,24-7,25): (Error 54) Test.test 'a is not a subtype of the expected type Test.test 'a (see also Test(7,12-7,13))
1 error was reported (see above)

有人能告诉我我错过了什么吗？类型统一的行为是否受子类型的影响？或者这种类型检查是否应该是编译器的错误呢？

Answer 1

我相信有一个宇宙不平等约束的诱因，而你并没有强制。

以下代码将键入代码：

noeq type test : Type0 -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

注意我在第一行中添加的0。

这是因为这说明第一个Type0所处的宇宙比Type (我相信它本身意味着任何宇宙)都低。在你的例子中，F*不知道如何比较这两种类型的宇宙，因此失败了。

如果你写了noeq type test : Type -> Type0，你会看到一个稍微好一点的错误信息：“未能解决诱因的宇宙不等式”。所以我把错误信息归咎于这里。

如果解释不够精确，我道歉，我不是PL人.：)