如何读取 ghci 类型错误？

Posted 2023-03-28

【中文标题】如何读取 ghci 类型错误？

【英文标题】：How to read ghci type errors?

【发布时间】：2014-06-02 02:05:22

【问题描述】：

我一直在尝试this question的答案中的一个小例子：

liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
liftTup liftFunc (t, v) = (liftFunc t, liftFunc v)

这显然需要forall 量词才能工作，但我正在尝试理解错误消息的语法，以便能够在将来遇到类似问题时知道什么是错误的。所以对于这个我得到：

monad.hs:112:28-37: Couldn't match type `x' with `b' …
      `x' is a rigid type variable bound by
          the type signature for
            liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
          at /Users/user/monad.hs:111:12
      `b' is a rigid type variable bound by
          the type signature for
            liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
          at /Users/user/monad.hs:111:12
    Expected type: f a
      Actual type: f x
    In the return type of a call of `liftFunc'
    In the expression: liftFunc t
    In the expression: (liftFunc t, liftFunc v)
monad.hs:112:40-49: Couldn't match type `a' with `b' …
      `a' is a rigid type variable bound by
          the type signature for
            liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
          at /Users/user/monad.hs:111:12
      `b' is a rigid type variable bound by
          the type signature for
            liftTup :: (x -> f x) -> (a, b) -> (f a, f b)
          at /Users/user/monad.hs:111:12
    Expected type: f b
      Actual type: f x
    In the return type of a call of `liftFunc'
    In the expression: liftFunc v
    In the expression: (liftFunc t, liftFunc v)

据我所知，第一个错误与第一次将liftFunc 应用于t 有关，因此它尝试将f x 与f a 匹配。但是b 和这个有什么关系呢？ b 只出现在元组的第二个元素中。

我猜第二个错误是因为a 在之前的liftFunc 应用程序中与x 匹配，而现在我们正试图将它与第二个应用程序中的b 匹配，但这并没有不太行。是这样吗？

阅读这些错误消息的正确方法是什么？“无法将类型..与..匹配”中提到的变量与“预期类型：..实际类型：..”消息中提到的变量之间的关系是什么？

【问题讨论】：

我的猜测（这是未受过足够教育的，我不会给出答案），是 GHC first 尝试统一类型变量以使所有内容都可以很好地键入，此时点它发现所有a、b和x必须相同；并且只有 then 检查三个变量中的任何一个是否是刚性的并且不能相互统一，从而给出这种看起来随机的罪魁祸首。

【参考方案1】：

您正在正确读取类型错误：

GHC 正在尝试推断/检查表达式liftFunc t 的类型 发现liftFunc这个应用程序的返回类型是f x 发现这个表达式的预期类型应该是f a 这要求f x和f a是同一类型； GHC 在试图证明这一点时失败了，因为它要求 x 和 b 是同一件事

“预期类型”和“实际类型”与紧随其后谈论的表达式的类型有关（“在对liftFunc 的调用的返回类型中...”）。但是“无法将类型'x'与'b'匹配”告诉你它注意到的事情是不可能的，当试图将预期类型与实际类型匹配时，所以它不一定会直接报告那个两者不匹配。

这可能不直观，但它是有效的。因为liftFunc 有一个单态类型within liftTup，并且它适用于a 和b 这两种类型的值，所以类型检查器推断出x，a，和b 必须全部相等。所以x ~ b（~ 是用 Haskell 编写的类型相等性）确实是必须保持的东西才能成为一个类型良好的表达式，并确定它不能统一（通过观察 x 和b 都是必须保持独立普遍量化的“刚性类型变量”）确实确定存在类型错误。

我的猜测是类型检查器已经做了一些分析，得出了一组成对约束，包括f x ~ f a、f x ~ f b、x ~ a、x ~ b和@ 987654345@，然后开始证明它们。也许x ~ b 是它尝试的第一个。或者它可能必须证明x ~ a，并且没有直接的方法来证明这一点，并且唯一可用的其他信息是a ~ b，它试图应用它来推导x ~ b，然后没有办法证明这一点（和一个循环检查阻止它应用b ~ a 以再次返回x ~ a）它在那时失败。无论如何，沿着这些路线。我很漂亮x ~ b 只是它碰巧注意到的第一件事是在尝试检查liftFunc t 的过程中是不可能的。

【参考方案2】：

这些错误非常能描述您的问题。但是阅读 ghc 错误消息有时很困难，因为它们包含太多信息。

Couldn't match type x with b 表示它期望x 和b 是同一类型，但它无法证明这一点。另一个错误也是如此。所以从这两个错误一起来看，你知道编译器需要a==b==x，但这不是你写的。

但是你还不知道为什么它实际上确实期望这个。第一条错误消息如下：

Expected type: f a
  Actual type: f x
In the return type of a call of `liftFunc'

您声称liftunc 的类型是x -> f x。但是您还声称liftFunc t 的类型为f a。由此，编译器可以推断出a 和x 必须是相同类型的唯一 事物。但是没有办法证明，因此，类型错误。

第二个错误是将完全相同的逻辑应用于元组的第二个参数。