尝试在 Haskell 中使用存在类型时出现编译错误

Question

我收到如下错误消息：

Linear.hs:215:27:
    Couldn't match expected type `forall v1.
                                  Ident v1 =>
                                  SubstT v1 (GenericLL (a v1 c)) n x'
                with actual type `forall v1. Ident v1 => SubstT v1 a0 m0 b0'
    Expected type: (forall v1.
                    Ident v1 =>
                    SubstT v1 (GenericLL (a v1 c)) n x)
                   -> n x
      Actual type: (forall v1. Ident v1 => SubstT v1 a0 m0 b0) -> m0 b0
    In the first argument of `flattenImpl', namely `runSubstT'
    In the expression: flattenImpl runSubstT

实际类型似乎比预期类型更通用。那么这种错误消息的可能原因是什么？该消息是否具有误导性或我阅读不正确？

我要做的是传递一个存在量化的函数runSubstT，其类型是：

runSubstT :: (Monad m) => (forall v. (Ident v) => SubstT v a m b) -> m b

我还将对 GHC 编译器如何对存在量化类型执行类型匹配进行一些很好的描述。

Answer 1

我有一个猜测，但在您发布足够的代码以重现错误之前，我无法确定。我的猜测，基于看这个：

runSubstT :: (Monad m) => (forall v. (Ident v) => SubstT v a m b) -> m b

是否使第二种类型“a”依赖于第一种存在类型“v”可能是一个问题。预期类型：

forall v1。 Ident v1 => SubstT v1 (GenericLL (a v1 c)) n x'

将第二种类型替换为 (GenericLL (a v1 c))，它依赖于第一个存在类型“v1”。这可能是冲突的根源，但没有代码我无法跟踪类型检查器的登录。