#15639: Surprising failure combining QuantifiedConstraints with Coercible -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:10 simonpj]:
The best thing is to avoid overlap.
This is a very good general principle (and the reason I was concerned about bundling implication constraints with quantified constraints). But I think the special case of `Coercible` deserves some special consideration. Overlap is very often (perhaps usually) unavoidable when using quantified constraints with `Coercible`. There's just no way to hide the global mechanism. So I think it pays to consider how we can refine the overlap rules to make these constraints as useful as possible. I ''conjecture'' that we will get strictly or almost strictly better results by applying quantified constraints before and between built-in rules (other than symmetry, which I imagine does some global canonicalization). We seem to already do something special to allow things to work as expected when pattern matching on `Coercion`s to locally reveal `Coercible` instances. Can we do something similar for quantified constraints? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler