Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why does GHC produce an equality constraint error rather than a type match error here?

Following up from this question, I'm not sure why these two code snippets produce completely different errors:

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'.

What is the rule giving rise to this behavior?

It's not very readable, even to someone familiar with standard Haskell; the equality constraint (a ~ b) requires a language extension.

Note that, as chi pointed out, the mere presence of a constraint triggers the constraint error:

class C a

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

(An empty constraint, () => a -> b, gives the match not the constraint error.)

like image 861
Christian Conkle Avatar asked Nov 13 '14 23:11

Christian Conkle


1 Answers

I don't think there's a shorter answer than digging into GHC internals to understand why.

If you run GHC with the -ddump-tc-trace switch, you can get quite a lengthy log of the typechecking process. In particular, if you run it on this code:

f :: a -> b
f x = x

class C a

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

you can see that typechecking a vs b, and typechecking c vs d progresses exactly the same way in both cases, culminating in the following two unsolved constraints (output is from GHC 7.8.2):

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

By following the rabbit hole a bit more in TcErrors, you can see that for equalities on skolems, tryReporters eventually gets to creating the error message via misMatchOrCND, which has an explicit special case for empty contexts:

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)
like image 128
Cactus Avatar answered Oct 14 '22 15:10

Cactus