#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): As you point out, the last two instance always overlap looking only at the instance heads. So I think you'd still need `{-# OVERLAPPING #-}`. Previously, Simon was worried that the equality constraints would always be redundant. I think that's still true in your examples, but with a key twist: the equality constraints can be used for improvement during type checking. That may indeed be correct. As a practical matter though, I can't imagine how to implement them. And, given the fact that we have many ways of expressing these ideas already, without quantified equality constraints, (for example, your `ElimElem` could be implemented as a closed type family), I'm not yet motivated to start thinking about how to write a solver than can deal with these. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler