[GHC] #9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving (was: Need for higher kinded roles)

[GHC]

#9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  7.8.2
  checker)                           |             Keywords:  Roles,
      Resolution:                    |  QuantifiedConstraints
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:  quantified-
                                     |  constraints/T9123{,a}
      Blocked By:  15290             |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Ah, quite right. Since we have "higher kinded roles" currently (in some
 sense) due to `QuantifiedConstraints`, I'll change the title of this
 ticket to reflect its new goal.

 Speaking of which, let's talk about what it would take to actually
 accomplish this. I've been inclined to try implementing this myself, but
 every time I get started, I quickly get lost in the weeds. Assuming that
 #15290 were fixed, what would it take to train the constraint solver to
 spit out quantified `Coercible` constraints? My understanding of GHC's
 constraint solver (which, admittedly, is quite limited) is that it will
 //never// emit a quantified constraint under any circumstances. Would we
 have to change this invariant somewhere? Also, would we be feeding a
 constraint like `forall p q. Coercible p q => Coercible (m p) (m q)` as an
 input to the constraint solver? Or would it only be an output?

 I'm afraid I don't really know where to look to answer these questions, so
 advice would be greatly appreciated.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9123#comment:60>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler