
#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): If I had to guess, I would guess that there is no entirely satisfactory general solution to this problem. Given `type role F representational` (or `type role F nominal`) and forall a b. `C a b => Coercible (F a) (F b)`, and seeking `Coercible (F a) (F b)` I very much doubt that there's a single optimal way to determine whether to reduce the wanted to `C` or to `Coercible a b` (or `a ~ b`). To be consistent with how this is handled for other classes, we "should" just reject the constraint altogether, as overlapping. But that would be sad, and I do suspect we can do better, at least for some special cases. For example, if we're given `forall a b. Coercible (F a) (F b)`, we want to think of that as improving the type role of `F`'s parameter from whatever it may be to phantom. Similarly, if we're given `forall a b. Coercible a b => Coercible (F a) (F b)`, we want to think of that as improving the type role of `F`s parameter to representational, if it would otherwise be nominal. Adding such special cases to the constraint solver would certainly be a horribly ugly hack, but I don't really know what else we can do. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15639#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler