#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