Quantified constraints do not work with equality constraints

Feeling abusive toward GHC this morning, I tried this:

class C a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b
foo Dict x = x

I thought it wouldn't work, and I was right:

    • Class ‘~’ does not support user-specified instances
    • In the quantified constraint ‘forall (a :: k) (b :: k).
                                    C a b =>
                                    a ~ b’
      In the type signature:
        foo :: (forall a b. C a b => a ~ b) => Dict (C a b) -> a -> b

Good. But then I tried something more devious:

class C a b
class a ~ b => D a b

data Dict c where
  Dict :: c => Dict c

foo :: (forall a b. C a b => D a b) => Dict (C a b) -> a -> b
foo Dict x = x

This also fails, with Couldn't match expected type ‘b’ with actual type ‘a’.

I'm fine with the second case failing (because I think anything else would be very challenging), but the error message is unfortunate. According to the semantics of class constraints and quantified constraints, this case should be accepted. So if we reject it, we should have a good reason -- like we offer in the first case. Essentially, we need to explain that any logical entailment of an equality constraint simply doesn't hold in the presence of a quantified constraint. I neither know a good pithy way of explaining that to users nor how to detect when to do so.

Trac metadata

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