[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
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:  10528             |  Differential Revisions:
-------------------------------------+-------------------------------------
Description changed by afarmer:

Old description:

> 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.

New description:

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