Re: [GHC] #12734: Missed use of solved dictionaries leads to context stack overflow

24 Oct 2016

      #12734: Missed use of solved dictionaries leads to context stack overflow
-------------------------------------+-------------------------------------
        Reporter:  danilo2           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 OK I know what is going on.  With the cut-down example above, when
 checking the cod for `test_ghc_err` we are faced with
 {{{
     [W] Con m (TStk t lrs)

        where  m := KT A '[Type] IO
               bind := Expr Net '[Type]
               t := Net
               lrs := '[Type]
 }}}
 The `:=` are unifications that can take place pretty eagerly.

 Now let's try solving that wanted constraint
 {{{
     [W] Con m (TStk t lrs)

 = (Type synonym)
     [W] Con m (Stack lrs (Layer4 bind))

 = (inline lrs)
     [W] Con m (Stack '[Type] (Layer4 bind))

 --> instance decl for (Con m (Stack (l :' ls) t))
     [W] Con m (Stack '[] bind)
     [W] Con m (Layer4 bind Type)

 The first of these rapidly reduces to (Monad m).  The second is harder:

     [W] Con m (Layer4 bind Type)

 --> instance decl for (Con m (Layer4 expr Type)
     [W] bind ~ Expr t0 lrs0          -- C1
     [W] Con m (TStk t0 lrs0)         -- C2

     where t0, lrs0 are fresh unification variables.

 If we simplify (C1), using the fact that bind := Expr Net '[Type]
 we get

     t0 := Net
     lrs0 := lrs

 And now we have (C2):
     [W] Con m (TStk Net lrs)

 which is the very same thing we start with.  So we can
 "tie the knot" via the `inert_solved_dicts` and we are done.
 }}}
 This makes essential use of GHC's ability to solve a set of constraints
 with a ''recursive'' dictionary binding.

 So what goes wrong?

 * If we fail to prioritise C1 over C2, we'll embark on simplifying C2, not
 spotting the loop.  Result: an infinite regress.

 * We do prioritise equality constraints

 * But C1, namely `bind ~ Expr t0 lrs0` is actually a ''class'' constraint,
 not an equality.  It has a built-in reduction to the homogeneous-equality
 class constraint `bind ~~ Expr t0 lrs0`; and that in turn has a built-in
 reduction to the true equality constraint `bind ~# Expr t0 lrs0`.

 So a solution that works is to prioritise the two equality-class
 constraints `t1 ~ t2` and `t1 ~~ t2` just as we do equality constraints.
 That's a good thing to do anyway.

 But I'm concerned that it does not truly solve the problem.  Two worries:

 * To "tie the knot" we rely on saying "I've see this goal before".  But to
 be sure of that we should rewrite `inert_solved_dicts` with the current
 substitution, and currently we don't do that.  Maybe we should.  It's more
 work but we might in exchange sometimes get more sharing.

 * What if we have a class constraint `(C t1 t2)` where C has a perhaps-
 distant superclass `(s1 ~ s2)`.  Then should we prioritise the `(C t1 t2)`
 constraint?  But the superclass might not even be revealed until we do
 some reduction on `(C t1 t2)`.  This way lies madness.  I think wes should
 not even attempt to do this.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12734#comment:10
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler