如何阅读ghci类型错误？

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 只出现在元组的第二个元素中。

我猜第二个错误来自于先前的liftFunc应用中将a匹配到x，而现在我们正在尝试在第二个应用中将其与b匹配，但这不太对。这样说对吗？

如何正确阅读这些错误消息，并且“无法匹配类型..与..”和“期望类型：..实际类型：..”消息中提到的变量之间的关系是什么？

- egdmitry

---

我的猜想（虽然不够专业，不打算将其作为答案）是GHC首先尝试统一类型变量以使一切都具有良好的类型，此时它发现所有的'a'、'b'和'x'必须相同；然后再检查这三个变量中是否有任何一个是刚性的，不能彼此统一，从而得出这种看似随机的匹配结果。 - Ørjan Johansen

Answer 1

您正在正确地阅读类型错误：

1. GHC 正在推断/检查表达式 `liftFunc t` 的类型 2. 它发现这个应用 `liftFunc` 的返回类型将是 `f x` 3. 它发现这个表达式的期望类型应该是 `f a` 4. 这要求 `f x` 和 `f a` 是相同的类型；GHC 在试图证明它们相同时崩溃了，因为它需要 `x` 和 `b` 是相同的东西

“期望类型”和“实际类型”与其所讨论的表达式的类型有关（即“在调用 `liftFunc` 的返回类型中…”）。但是，“无法匹配类型 'x' 和 'b'”是告诉您它已经注意到不可能的事情，当尝试将期望类型与实际类型匹配时，因此它不一定会直接报告两者不匹配。

这可能是不直观的，但它是有效的。因为 `liftFunc` 在 `liftTup` 中具有单态类型，在两种类型 `a` 和 `b` 的值上应用它，类型检查器推断出 `x`、`a` 和 `b` 必须全部相等。所以 `x ~ b`（`~` 是 Haskell 中写类型相等的方式）确实是必须成立的，这样才能使表达式具有良好的类型，而通过观察 `x` 和 `b` 都是“刚性类型变量”（必须保持独立的普遍量化）无法统一来建立这一点确实会导致出现类型错误。

我猜测类型检查器已经进行了一些分析，得出了一组成对约束条件，包括 `f x ~ f a`、`f x ~ f b`、`x ~ a`、`x ~ b` 和 `a ~ b`，然后开始证明它们。也许 `x ~ b` 只是它尝试的第一个约束条件。或者它不得不证明 `x ~ a`，由于没有直接证明的方法，而且唯一可用的信息是 `a ~ b`，因此它尝试应用它来推导出 `x ~ b`，然后在没有办法证明它（并且循环检查阻止它应用 `b ~ a` 以回到 `x ~ a`）的情况下失败。总之，大致就是这样。我相当确定 `x ~ b` 只是它在尝试检查 `liftFunc t` 过程中注意到的第一件不可能的事情。

- Ben

Answer 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必须是相同的类型。但是没有办法证明这一点，因此会出现类型错误。

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

- user2407038