[GHC] #12074: RULE too complicated to desugar

[GHC]

#12074: RULE too complicated to desugar
-------------------------------------+-------------------------------------
        Reporter:  crockeea          |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  warning at compile-time            |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 You are asking for something quite trikcy, and I'm not altogether
 surprised it fails.

 Let's step through it.  You are asking that whenever GHC sees  a call
 {{{
 ...(f @(Foo ty) d1 d2)...
 }}}
 where `d1 :: C2 (Foo ty)` and `d2 :: C2 (Bar (Foo ty))`, you want it to be
 replace with a call to the specialised function
 {{{
 ...($sf @ty d3)...
 }}}
 where `$sf :: (C1 q) => Foo q -> Foo q` and `d3 :: C2 ty`.

 The binding for `$sf` is no problem.  The problem is: what rewrite rule
 can rewrite the call to `f` into the call for `$sf`.  In particular, where
 does the rewrite rule get hold of a dictionary for `d3`?  The only thing
 we can do is to unpick the dictionary applications on the LHS.  For
 example, simplifying the signature for `f` to
 {{{
 f :: C2 (Bar r) => r -> r
 }}}
 with HEAD we get the specialisation rule
 {{{
 "SPEC f" [ALWAYS]
     forall (@ q_a1Im) ($dC1_a1In :: C1 q_a1Im).
       f @ (Foo q_a1Im)
         (T12074.$fC2Bar @ (Foo q_a1Im) (T12074.$fC2Foo @ q_a1Im
 $dC1_a1In))
       = T12074.f_$sf @ q_a1Im $dC1_a1In
 }}}
 Notice the rather deeply-nested form of the LHS, which makes it hard ot
 match.  But we need all that nesting to extract `$dC1_a1In` which is
 what's needed on the RHS (`d3` in the above).

 Now in the actual example you give, even HEAD fails with
 {{{
     RULE left-hand side too complicated to desugar
       Optimised lhs: let {
                        $dC2_a1HS :: C2 (Foo q)
                        [LclId]
                        $dC2_a1HS = T12074.$fC2Foo @ q $dC1_a1HQ } in
                      f @ (Foo q) $dC2_a1HS (T12074.$fC2Bar @ (Foo q)
 $dC2_a1HS)
 }}}
 That `let` is defeating it!  We could perhaps inline the `let` to get an
 LHS like
 {{{
   f @ (Foo q)
       (T12074.$fC2Foo @ q $dC1_a1HQ)
       (T12074.$fC2Bar @ (Foo q) (T12074.$fC2Foo @ q $dC1_a1HQ))
 }}}
 But we only need to bind `$dC1_a1H1` (needed on the RHS) once.  So we
 could make do with the simpler LHS
 {{{
   f @ (Foo q)
       (T12074.$fC2Foo @ q $dC1_a1HQ)
       _
 }}}
 where `_` is just a wildcard match.  That's be a better outcome.  But it's
 not obvious how to achieve it.  We want to pick just one of the several
 occurrences of `$dC1_a1HQ`, turn the rest into wildcards.

 There's an interesting graph algorithm in here, a kind of minimum-cover
 algorithm. But someone else will have to work on it.

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