[GHC] #14338: Simplifier fails with "Simplifier ticks exhausted"

[GHC]

#14338: Simplifier fails with "Simplifier ticks exhausted"
-------------------------------------+-------------------------------------
        Reporter:  dredozubov        |                Owner:  bgamari
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:  8.4.1
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
Operating System:  Linux             |         Architecture:  x86_64
 Type of failure:  Compile-time      |  (amd64)
  crash or panic                     |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Going from 1,500 to 75,000 ticks is stunning.  Thank you for locating the
 offenting patch.

 I spent some while digging.  Here's what I learned

 * Discarding `(case e of co -> blah)` is indeed unsound, unless we know
 that `e` terminates, so Richard's patch in #11230 is right.

 * But his patch does not say why the remaining "optimisation" (which works
 for superclass selectors over a `Coercible` dictionary) is sound.  And
 indeed, it is not; in Core I could produce a bottoming `Coercible`
 dictionary.  This "optimsation" in `CoreOpt` is all in service of `Note
 [Getting the map/coerce RULE to work]`, and I'm not sure how important
 that is.

 * I was also perplexed that in the case of #11230 the coericon involved
 seemed to be dead.  The code is
 {{{
 testPhantom :: Phantom Char -> Phantom Bool
 testPhantom x = id x
 }}}
   which should generate something like
 {{{
 data Wag x = MkWag ()
 type role Wag phantom

 testPhantom x = let co :: Wag Char ~ Wag Bool = error "blah"
                 in id @(PhantomChar) x |> co
 }}}
   so that coercion `co` certainly isn't dead!  But what happens is this.
 We actually generate
 {{{
 testPhantom x = let co :: Char ~# Bool = error "blah"
                 in id @(PhantomChar) x |> mkSubCo (Wag co)
 }}}
   where the `mkSubCo` turns a nominal coercion `Char ~# Bool` into a
 representational one.  Rather than just generate `SubCo` always, it pushes
 the sub inwards.  Because of the role of `Wag`, we then want to turn the
 nominal `co` into a phantom version, via `downgradeRole`.  But (currently)
 that dicards `co` (retaining only its kind) -- see `Coecion.toPhantomCo`
 -- so now `co` appears to be dead.  This seems wrong to me; the (nominal-
 equality) evidence really is needed and should really still be free in the
 result.

 That's one set of issues. Now, returning to this ticket:

 * The perf changes in this ticket are presumably because of `HEq_sc`
 selections, as reported in #13032.
 * And here the evidence really is not needed!
 * And hence it's really wrong to force the dictionary; that makes the
 function stricter (in its dictionary argument) than it should be.  (As
 well as less efficient.)

 Solution: do not generate all these speculative "given" bindings in the
 first place.  Instead, in the desugarer, figure out which given bindings
 are needed, and only emit those ones.  That will generate less code  --
 perhaps a lot less in some exotic programs -- and be better all round.

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