[GHC] #11408: Delicate solve order

[GHC]

#11408: Delicate solve order
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by Simon Peyton Jones <simonpj@…>):

 In [changeset:"9308c736d43b92bf8634babf565048e66e071bd8/ghc"
 9308c736/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="9308c736d43b92bf8634babf565048e66e071bd8"
 Fix a number of subtle solver bugs

 As a result of some other unrelated changes I found that
 IndTypesPerf was failing, and opened Trac #11408.  There's
 a test in indexed-types/should-compile/T11408.

 The bug was that a type like
  forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
 is in fact unambiguous, but it's a bit subtle to prove
 that it is unambiguous.

 In investigating, Dimitrios and I found several subtle
 bugs in the constraint solver, fixed by this patch

 * canRewrite was missing a Derived/Derived case.  This was
   lost by accident in Richard's big kind-equality patch.

 * Interact.interactTyVarEq would discard [D] a ~ ty if there
   was a [W] a ~ ty in the inert set.  But that is wrong because
   the former can rewrite things that the latter cannot.
   Fix: a new function eqCanDischarge

 * In TcSMonad.addInertEq, the process was outright wrong for
   a Given/Wanted in the (GWModel) case.  We were adding a new
   Derived without kicking out things that it could rewrite.
   Now the code is simpler (no special GWModel case), and works
   correctly.

 * The special case in kickOutRewritable for [W] fsk ~ ty,
   turns out not to be needed.  (We emit a [D] fsk ~ ty which
   will do the job.

 I improved comments and documentation, esp in TcSMonad.
 }}}

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