haskell - 为什么 GHC 会在这里产生等式约束错误而不是类型匹配错误？

Question

跟进 this question ，我不确定为什么这两个代码片段会产生完全不同的错误:

f :: a -> b
f x = x
-- Couldn't match expected type `b' with actual type `a'
-- In the expression: x

g :: Monad m => a -> m b
g x = return x
-- Could not deduce (a ~ b) from the context (Monad m)
-- In the first argument of `return', namely `x'.

导致这种行为的规则是什么？

即使对于熟悉标准 Haskell 的人来说，它也不是很易读；等式约束 (a ~ b)需要语言扩展。

请注意，正如 chi 指出的那样，仅存在约束就会触发约束错误:

class C a

h :: C a => a -> b
h x = x
-- Could not deduce...

(空约束 () => a -> b 给出匹配而不是约束错误。)

Answer 1

我认为没有比深入研究 GHC 内部结构来理解原因更简短的答案了。

如果您使用 -ddump-tc-trace 运行 GHC switch，你可以获得相当长的类型检查过程的日志。特别是，如果您在此代码上运行它:

f :: a -> b
f x = x

class C a

h :: C c => c -> d
h x = x

你可以看到类型检查 a对比 b , 和类型检查 c对比 d在这两种情况下都以完全相同的方式进行，最终导致以下两个 Unresolved 约束(输出来自 GHC 7.8.2):

tryReporters { [[W] cobox_aJH :: c ~ d (CNonCanonical)]
...
tryReporters { [[W] cobox_aJK :: a ~ b (CNonCanonical)]

在 TcErrors 中多关注兔子洞，您可以看到对于 skolem 上的等式， tryReporters最终通过 misMatchOrCND 创建错误消息，它对空上下文有一个明确的特殊情况:

misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc
-- If oriented then ty1 is actual, ty2 is expected
misMatchOrCND ctxt ct oriented ty1 ty2
  | null givens ||
    (isRigid ty1 && isRigid ty2) ||
    isGivenCt ct
       -- If the equality is unconditionally insoluble
       -- or there is no context, don't report the context
  = misMatchMsg oriented ty1 ty2
  | otherwise
  = couldNotDeduce givens ([mkTcEqPred ty1 ty2], orig)