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.