+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.
+
+
+Note [lazyId magic]
+~~~~~~~~~~~~~~~~~~~
+ lazy :: forall a?. a? -> a? (i.e. works for unboxed types too)
+
+Used to lazify pseq: pseq a b = a `seq` lazy b
+
+Also, no strictness: by being a built-in Id, all the info about lazyId comes from here,
+not from GHC.Base.hi. This is important, because the strictness
+analyser will spot it as strict!
+
+Also no unfolding in lazyId: it gets "inlined" by a HACK in CorePrep.
+It's very important to do this inlining *after* unfoldings are exposed
+in the interface file. Otherwise, the unfolding for (say) pseq in the
+interface file will not mention 'lazy', so if we inline 'pseq' we'll totally
+miss the very thing that 'lazy' was there for in the first place.
+See Trac #3259 for a real world example.
+
+lazyId is defined in GHC.Base, so we don't *have* to inline it. If it
+appears un-applied, we'll end up just calling it.
+
+-------------------------------------------------------------