Note [Simplifying rules]

When simplifying a rule LHS, refrain from /any/ inlining or applying
of other RULES. Doing anything to the LHS is plain confusing, because
it means that what the rule matches is not what the user
wrote. c.f. #10595, and #10528.

* sm_inline, sm_rules: inlining (or applying rules) on rule LHSs risks
  introducing Ticks into the LHS, which makes matching
  trickier. #10665, #10745.

  Doing this to either side confounds tools like HERMIT, which seek to reason
  about and apply the RULES as originally written. See #10829.

  See also Note [Do not expose strictness if sm_inline=False]

* sm_eta_expand: the template (LHS) of a rule must only mention coercion
  /variables/ not arbitrary coercions.  See Note [Casts in the template] in
  GHC.Core.Rules.  Eta expansion can create new coercions; so we switch
  it off.

There is, however, one case where we are pretty much /forced/ to transform the
LHS of a rule: postInlineUnconditionally. For instance, in the case of

    let f = g @Int in f

We very much want to inline f into the body of the let. However, to do so (and
be able to safely drop f's binding) we must inline into all occurrences of f,
including those in the LHS of rules.

This can cause somewhat surprising results; for instance, in #18162 we found
that a rule template contained ticks in its arguments, because
postInlineUnconditionally substituted in a trivial expression that contains
ticks. See Note [Tick annotations in RULE matching] in GHC.Core.Rules for
details.