[GHC] #9117: Coercible constraint solver misses one

[GHC]

#9117: Coercible constraint solver misses one
-------------------------------------+-------------------------------------
              Reporter:  goldfire    |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.2
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:  Phab:D546   |
-------------------------------------+-------------------------------------

Comment (by Richard Eisenberg <eir@…>):

 In [changeset:"0cc47eb90805f3e166ac4d3991e66d3346ca05e7/ghc"]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="0cc47eb90805f3e166ac4d3991e66d3346ca05e7"
 Rewrite `Coercible` solver

 Summary:
 This is a rewrite of the algorithm to solve for Coercible "instances".

 A preliminary form of these ideas is at
 https://ghc.haskell.org/trac/ghc/wiki/Design/NewCoercibleSolver

 The basic idea here is that the `EqPred` constructor of `PredTree`
 now is parameterised by a new type `EqRel` (where
 `data EqRel = NomEq | ReprEq`). Thus, every equality constraint can
 now talk about nominal equality (the usual case) or representational
 equality (the `Coercible` case).

 This is a change from the previous
 behavior where `Coercible` was just considered a regular class with
 a special case in `matchClassInst`.

 Because of this change, representational equalities are now
 canonicalized just like nominal ones, allowing more equalities
 to be solved -- in particular, the case at the top of #9117.

 A knock-on effect is that the flattener must be aware of the
 choice of equality relation, because the inert set now stores
 both representational inert equalities alongside the nominal
 inert equalities. Of course, we can use representational equalities
 to rewrite only within another representational equality --
 thus the parameterization of the flattener.

 A nice side effect of this change is that I've introduced a new
 type `CtFlavour`, which tracks G vs. W vs. D, removing some ugliness
 in the flattener.

 This commit includes some refactoring as discussed on D546.
 It also removes the ability of Deriveds to rewrite Deriveds.

 This fixes bugs #9117 and #8984.

 Reviewers: simonpj, austin, nomeata

 Subscribers: carter, thomie

 Differential Revision: https://phabricator.haskell.org/D546

 GHC Trac Issues: #9117, #8984
 }}}

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