Tuple constraints don't work right

Consider this program:

{-# LANGUAGE RankNTypes, ConstraintKinds, KindSignatures, DataKinds, TypeFamilies #-}
module Wrong where

import GHC.Prim

data Proxy (c :: Constraint)

class Deferrable (c :: Constraint) where
  defer :: Proxy c -> (c => a) -> a

deferPair :: (Deferrable c1, Deferrable c2) =>
                  Proxy (c1,c2) -> ((c1,c2) => a) -> a
deferPair = undefined

instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where
    -- defer p f = deferPair p f     -- Succeeds
    defer = deferPair                -- Fails

The first (commented-out) definition of defer in the instance declaration succeeds; but the second fails with an utterly bogus message

ConstraintBug.hs:27:13:
    Could not deduce (c1 ~ (c1, c2))
    from the context (Deferrable c1, Deferrable c2)

The reason is that when type-checking the method defintion we try to unify

     ((c1,c2) => a) ~ ((gamma1, gamma2) => alpha)

where

• the LHS comes from instantiating the signature (c => a) (from the class decl) with (c1,c2)/c from the instance.
• the RHS comes from instantiating the type of deferPair with fresh unification variables.

The difficulty is that in the type of deferPair, the concrete syntax

  deferPair :: ...((c1,c2) => a)...

is really just syntactic sugar for

  deferPair :: ...(c1 => c2 => a)...

i.e. curried. But the function in the instantiated signature really has one constraint argument, a pair, not two.

It's not clear how to fix this. It would actually be more consistent if

f :: (Eq a, Show a) => blah

really did take a pair of dictionaries, rather than two curried dictionaries. But that would be a pretty big change, forced by a corner case.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture