+Note [seqId magic]
+~~~~~~~~~~~~~~~~~~
+'GHC.Prim.seq' is special in several ways.
+
+a) Its second arg can have an unboxed type
+ x `seq` (v +# w)
+
+b) Its fixity is set in LoadIface.ghcPrimIface
+
+c) It has quite a bit of desugaring magic.
+ See DsUtils.lhs Note [Desugaring seq (1)] and (2) and (3)
+
+d) There is some special rule handing: Note [User-defined RULES for seq]
+
+e) See Note [Typing rule for seq] in TcExpr.
+
+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) 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.
+
+To make this work, we need to be careful that the magical desugaring
+done in 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.
+
+Note [Built-in RULES for seq]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We also have the following built-in rule for seq
+
+ seq (x `cast` co) y = seq x y
+
+This eliminates unnecessary casts and also allows other seq rules to
+match more often. Notably,
+
+ seq (f x `cast` co) y --> seq (f x) y
+
+and now a user-defined rule for seq (see Note [User-defined RULES for seq])
+may fire.
+
+