Comments only, relating to Roman's new built-in rule for seq

compiler/basicTypes/MkId.lhs

@@ -942,13 +942,15 @@ seqId = pcMiscPrelId seqName ty info
     [x,y] = mkTemplateLocals [alphaTy, openBetaTy]
     rhs = mkLams [alphaTyVar,openBetaTyVar,x,y] (Case (Var x) x openBetaTy [(DEFAULT, [], Var y)])
 
+    -- See Note [Built-in RULES for seq]
     seq_cast_rule = BuiltinRule { ru_name  = fsLit "seq of cast"
                                 , ru_fn    = seqName
                                 , ru_nargs = 4
                                 , ru_try   = match_seq_of_cast
                                 }
 
-match_seq_of_cast :: [CoreExpr] -> Maybe CoreExpr     -- Note [RULES for seq]
+match_seq_of_cast :: [CoreExpr] -> Maybe CoreExpr
+    -- See Note [Built-in RULES for seq]
 match_seq_of_cast [Type _, Type res_ty, Cast scrut co, expr]
   = Just (Var seqId `mkApps` [Type (fst (coercionKind co)), Type res_ty,
                               scrut, expr])
@@ -974,10 +976,10 @@ 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 [RULES for seq]
+d) There is some special rule handing: Note [User-defined RULES for seq]
 
-Note [RULES for seq]
-~~~~~~~~~~~~~~~~~~~~
+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.
@@ -999,12 +1001,20 @@ 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.
 
-We also have the following builtin rule:
+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.
+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]
 ~~~~~~~~~~~~~~~~~~~

compiler/simplCore/Simplify.lhs

@@ -1450,7 +1450,7 @@ rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
 
 rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
   | all isDeadBinder (case_bndr : bndrs)  -- So this is just 'seq'
-  = 	-- For this case, see Note [RULES for seq] in MkId
+  = 	-- For this case, see Note [User-defined RULES for seq] in MkId
     do { let rhs' = substExpr env rhs
              out_args = [Type (substTy env (idType case_bndr)), 
 	     	         Type (exprType rhs'), scrut, rhs']
@@ -1539,13 +1539,31 @@ where x::F Int.  Then we'd like to rewrite (F Int) to Int, getting
            I# x# -> let x = x' `cast` sym co
                     in rhs
 
-so that 'rhs' can take advantage of the form of x'.  Notice that Note
-[Case of cast] may then apply to the result. We only do this if x is actually
-used in the rhs. There is no point in adding the cast if this is really just a
-seq and doing so would interfere with seq rules (Note [RULES for seq]), in
-particular with the one that removes casts.
-
-This showed up in Roman's experiments.  Example:
+so that 'rhs' can take advantage of the form of x'.  
+
+Notice that Note [Case of cast] may then apply to the result. 
+
+Nota Bene: We only do the [Improving seq] transformation if the 
+case binder 'x' is actually used in the rhs; that is, if the case 
+is *not* a *pure* seq.  
+  a) There is no point in adding the cast to a pure seq.
+  b) There is a good reason not to: doing so would interfere 
+     with seq rules (Note [Built-in RULES for seq] in MkId).
+     In particular, this [Improving seq] thing *adds* a cast
+     while [Built-in RULES for seq] *removes* one, so they
+     just flip-flop.
+
+You might worry about 
+   case v of x { __DEFAULT ->
+      ... case (v `cast` co) of y { I# -> ... }}
+This is a pure seq (since x is unused), so [Improving seq] won't happen.
+But it's ok: the simplifier will replace 'v' by 'x' in the rhs to get
+   case v of x { __DEFAULT ->
+      ... case (x `cast` co) of y { I# -> ... }}
+Now the outer case is not a pure seq, so [Improving seq] will happen,
+and then the inner case will disappear.
+
+The need for [Improving seq] showed up in Roman's experiments.  Example:
   foo :: F Int -> Int -> Int
   foo t n = t `seq` bar n
      where
@@ -1554,11 +1572,9 @@ This showed up in Roman's experiments.  Example:
 Here we'd like to avoid repeated evaluating t inside the loop, by
 taking advantage of the `seq`.
 
-At one point I did transformation in LiberateCase, but it's more robust here.
-(Otherwise, there's a danger that we'll simply drop the 'seq' altogether, before
-LiberateCase gets to see it.)
-
-
+At one point I did transformation in LiberateCase, but it's more
+robust here.  (Otherwise, there's a danger that we'll simply drop the
+'seq' altogether, before LiberateCase gets to see it.)
 
 
 \begin{code}
@@ -1567,7 +1583,7 @@ improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
 	   -> SimplM (SimplEnv, OutExpr, OutId)
 -- Note [Improving seq]
 improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
-  | not (isDeadBinder case_bndr)
+  | not (isDeadBinder case_bndr)	-- Not a pure seq!  See the Note!
   , Just (co, ty2) <- topNormaliseType fam_envs (idType case_bndr1)
   = do { case_bndr2 <- newId (fsLit "nt") ty2
         ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCoercion co)