[GHC] #9123: Emit quantified Coercible constraints in GeneralizedNewtypeDeriving

[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 goldfire):

 If we wanted to do this (and I'm waiting for Simon to say that we don't),
 the quantified constraint would be only an output from the constraint
 solver, not an input. The constraint solver works over a tree of
 constraints, where (roughly) interior nodes are givens (which can bring
 skolems into scope for their descendants) and leaves are wanteds. When
 inferring, we build up the tree of constraints and then simplify it to
 another tree that logically entails the first one. When we can simplify no
 more, we (roughly) look at the tree. If it's the kind of tree we like to
 quantify over (`Eq a`: yes. `Int ~ Bool`: no. An implication: no, today),
 convert it back to a normal constraint and quantify.

 To infer quantified constraints, all we have to do is change what trees we
 like to quantify over.

 Some of the action is in `TcSimplify.approximateWC` which looks to find
 simple (i.e. non-implication) constraints to quantify over. It will have
 to be adapted to sometimes return implication constraints. Then, the code
 in `TcDerivInfer.simplifyDeriv` will have to be taught to handle the
 implication constraints. I don't think it will be all that invasive, but
 we might find that we're accepting more programs than we like. See Note
 [Exotic derived instance contexts] in TcDerivInfer.

 Perhaps this helps start you off...

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