Simplification in the RHS of rules
HERMIT users depend on RULES to specify equational properties.
- 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 (closed)):
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:
- Don't inline/apply rules in the RHS at all (just like the LHS).
- 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.