Note [User-defined RULES for seq]
Roman found situations where he had
case (f n) of _ -> e
where he knew that f (which was strict in n) would terminate if n did.
Notice that the result of (f n) is discarded. So it makes sense to
transform to
case n of _ -> e
Rather than attempt some general analysis to support this, I've added
enough support that you can do this using a rewrite rule:
RULE "f/seq" forall n. seq (f n) = seq n
You write that rule. When GHC sees a case expression that discards
its result, it mentally transforms it to a call to 'seq' and looks for
a RULE. (This is done in GHC.Core.Opt.Simplify.trySeqRules.) As usual, the
correctness of the rule is up to you.
VERY IMPORTANT: to make this work, we give the RULE an arity of 1, not 2.
If we wrote
RULE "f/seq" forall n e. seq (f n) e = seq n e
with rule arity 2, then two bad things would happen:
- The magical desugaring done in Note [seqId magic] item (b)
for saturated application of 'seq' would turn the LHS into
a case expression!
- The code in GHC.Core.Opt.Simplify.rebuildCase would need to actually supply
the value argument, which turns out to be awkward.
See also: Note [User-defined RULES for seq] in GHC.Core.Opt.Simplify. References 1
- seqId magic GHC.Types.Id.Make
Referenced by 4
- User-defined RULES for seq GHC.Core.Opt.Simplify.Iteration
- GHC.Core.Opt.Simplify.Iteration call site
- Unfold compulsory unfoldings in RULE LHSs GHC.Core.SimpleOpt
- seqId magic GHC.Types.Id.Make