Re: [GHC] #11379: Solver hits iteration limit in code without recursive constraints

18 Jan 2016

      #11379: Solver hits iteration limit in code without recursive constraints
-------------------------------------+-------------------------------------
        Reporter:  bgamari           |                Owner:  simonpj
            Type:  bug               |               Status:  merge
        Priority:  highest           |            Milestone:  8.0.1
       Component:  Compiler (Type    |              Version:  8.0.1-rc1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Compile-time      |  Unknown/Multiple
  performance bug                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * status:  new => merge

Comment:

 Actually this ticket #11is fixed by the following commit.  I forgot to
 mention it in the list of fixes in the commit message.  The important bit
 of the patch for #11379 is the new function `TcSMonad.mkShadowCt`,
 explained by `Note [Keep CDictCan shadows as CDictCan]`.

 Let's merge this.

 {{{
 commit 9308c736d43b92bf8634babf565048e66e071bd8
 Author: Simon Peyton Jones 
 Date:   Sat Jan 16 00:37:15 2016 +0000

     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/11379#comment:6
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler