[GHC] #15639: Surprising failure combining QuantifiedConstraints with Coercible

[GHC]

#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