#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/8af219adb914b292d0f8c737fe0a1e3f7...
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/bc4b64ca5b99bff6b3d5051b57cb2bc52...
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/8af219adb914b292d0f8c737fe0a1e3f7... 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/bc4b64ca5b99bff6b3d5051b57cb2bc52... 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