Allow RULES for seq, and exploit them
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) e = seq n e 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 Simplify.rebuildCase.) As usual, the correctness of the rule is up to you. This patch implements the extra stuff. I have not documented it explicitly in the user manual yet... let's see how useful it is first. The patch looks bigger than it is, because a) Comments; see esp MkId Note [seqId magic] b) Some refactoring. Notably, I moved the special desugaring for seq from MkCore back into DsUtils where it properly belongs. (It's really a desugaring thing, not a CoreSyn invariant.) c) Annoyingly, in a RULE left-hand side we need to be careful that the magical desugaring done in MkId Note [seqId magic] item (c) is *not* done on the LHS of a rule. Or rather, we arrange to un-do it, in DsBinds.decomposeRuleLhs.