[GHC] #10829: Simplification in the RHS of rules

[GHC]

#10829: Simplification in the RHS of rules
-------------------------------------+-------------------------------------
              Reporter:  afarmer     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:  7.10.3
             Component:  Compiler    |           Version:  7.10.2
              Keywords:              |  Operating System:  Unknown/Multiple
          Architecture:              |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
             Test Case:              |        Blocked By:
              Blocking:              |   Related Tickets:  10528
Differential Revisions:              |
-------------------------------------+-------------------------------------
 HERMIT users depend on RULES to specify equational properties.

 7.10.2 performed both inlining and simplification in both sides of the
 rules, meaning they can't really be used for this. This breaks most HERMIT
 use cases. Note that this behavior was a change from 7.8 and prior, due to
 this commit:

 https://git.haskell.org/ghc.git/commitdiff/8af219adb914b292d0f8c737fe0a1e3f7fb19cf3

 The following commit disables the inlining/simplification in the LHS of
 rules, which fixes half the problem, but it has yet to be merged and
 released (attached to ticket #10528):

 https://git.haskell.org/ghc.git/commitdiff/bc4b64ca5b99bff6b3d5051b57cb2bc52bd4c841

 This ticket is to ask that inlining/simplification also be disabled in the
 RHS of rules.

 As an example of what is happening, we are seeing rules like this:

 {{{
 repH :: [a] -> [a] -> [a]

 {-# RULES "repH ++" [~] forall xs ys. repH (xs ++ ys) = repH xs . repH ys
 #-}
 }}}

 get to HERMIT as:

 {{{
 "repH ++" forall xs ys. repH (xs ++ ys) = let f = repH xs
                                               g = repH ys
                                           in \ z -> f (g z)
 }}}

 In this case it is just an unfolding of composition, but some rules get
 rather gross on the RHS. The extra junk makes equational reasoning with
 these rules very fiddly and sort of breaks the correspondence with the
 source-level code. For instance, it is almost impossible to apply these
 right-to-left, which is a common thing to do when performing equational
 reasoning.

 Some possible solutions:

 1. Don't inline/apply rules in the RHS at all (just like the LHS).

 2. Don't inline/apply rules in the RHS of rules marked with the
 NeverActive notation (rules intended for HERMIT use are generally marked
 NeverActive). Since NeverActive rules are not applied by GHC anyway, this
 should actually save compile-time work and not affect real programs/rules.

 Would either of those be acceptable/possible? Option 1 would be ideal,
 because it would match the behavior of 7.8 (AFAICT). Option 2 would be
 sufficient, however.

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