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

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 ,则可以获得相当长的类型检查过程日志.特别是,如果您在此代码上运行它:

f :: a -> b
f x = x

class C a

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

你可以看到在两种情况下,类型检查avs b和类型检查c与d进展完全相同,最终导致以下两个未解决的约束(输出来自GHC 7.8.2):

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

通过更多地关注兔子洞TcErrors,你可以看到,对于skolems的平等,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)