## 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 |