Move error-ids to MkCore (from PrelRules)
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index 39bf3d8..effd245 100644 (file)
@@ -10,28 +10,35 @@ module Simplify ( simplTopBinds, simplExpr ) where
 
 import DynFlags
 import SimplMonad
-import Type hiding      ( substTy, extendTvSubst )
+import Type hiding      ( substTy, extendTvSubst, substTyVar )
 import SimplEnv
 import SimplUtils
-import MkId            ( rUNTIME_ERROR_ID )
+import FamInstEnv      ( FamInstEnv )
 import Id
+import MkId            ( seqId, realWorldPrimId )
+import MkCore          ( mkImpossibleExpr )
 import Var
 import IdInfo
+import Name            ( mkSystemVarName, isExternalName )
 import Coercion
+import OptCoercion     ( optCoercion )
 import FamInstEnv       ( topNormaliseType )
-import DataCon          ( dataConRepStrictness, dataConUnivTyVars )
+import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness )
+import CoreMonad       ( SimplifierSwitch(..), Tick(..) )
 import CoreSyn
-import NewDemand        ( isStrictDmd, splitStrictSig )
+import Demand           ( isStrictDmd, splitStrictSig )
 import PprCore          ( pprParendExpr, pprCoreExpr )
-import CoreUnfold       ( mkUnfolding, callSiteInline, CallCtxt(..) )
+import CoreUnfold       ( mkUnfolding, mkCoreUnfolding, mkInlineRule, 
+                          exprIsConApp_maybe, callSiteInline, CallCtxt(..) )
 import CoreUtils
+import qualified CoreSubst
+import CoreArity       ( exprArity )
 import Rules            ( lookupRule, getRules )
-import BasicTypes       ( isMarkedStrict )
-import CostCentre       ( currentCCS )
+import BasicTypes       ( isMarkedStrict, Arity )
+import CostCentre       ( currentCCS, pushCCisNop )
 import TysPrim          ( realWorldStatePrimTy )
-import PrelInfo         ( realWorldPrimId )
-import BasicTypes       ( TopLevelFlag(..), isTopLevel,
-                          RecFlag(..), isNonRuleLoopBreaker )
+import BasicTypes       ( TopLevelFlag(..), isTopLevel, RecFlag(..) )
+import MonadUtils      ( foldlM, mapAccumLM )
 import Maybes           ( orElse )
 import Data.List        ( mapAccumL )
 import Outputable
@@ -199,7 +206,7 @@ expansion at a let RHS can concentrate solely on the PAP case.
 %************************************************************************
 
 \begin{code}
-simplTopBinds :: SimplEnv -> [InBind] -> SimplM [OutBind]
+simplTopBinds :: SimplEnv -> [InBind] -> SimplM SimplEnv
 
 simplTopBinds env0 binds0
   = do  {       -- Put all the top-level binders into scope at the start
@@ -208,11 +215,10 @@ simplTopBinds env0 binds0
                 -- It's rather as if the top-level binders were imported.
         ; env1 <- simplRecBndrs env0 (bindersOfBinds binds0)
         ; dflags <- getDOptsSmpl
-        ; let dump_flag = dopt Opt_D_dump_inlinings dflags ||
-                          dopt Opt_D_dump_rule_firings dflags
+        ; let dump_flag = dopt Opt_D_verbose_core2core dflags
         ; env2 <- simpl_binds dump_flag env1 binds0
         ; freeTick SimplifierDone
-        ; return (getFloats env2) }
+        ; return env2 }
   where
         -- We need to track the zapped top-level binders, because
         -- they should have their fragile IdInfo zapped (notably occurrence info)
@@ -330,15 +336,14 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                 -- See Note [Floating and type abstraction] in SimplUtils
 
         -- Simplify the RHS
-        ; (body_env1, body1) <- simplExprF body_env body mkBoringStop
-
+        ; (body_env1, body1) <- simplExprF body_env body mkRhsStop
         -- ANF-ise a constructor or PAP rhs
-        ; (body_env2, body2) <- prepareRhs body_env1 body1
+        ; (body_env2, body2) <- prepareRhs top_lvl body_env1 bndr1 body1
 
         ; (env', rhs')
             <-  if not (doFloatFromRhs top_lvl is_rec False body2 body_env2)
-                then                            -- No floating, just wrap up!
-                     do { rhs' <- mkLam tvs' (wrapFloats body_env2 body2)
+                then                            -- No floating, revert to body1
+                     do { rhs' <- mkLam env tvs' (wrapFloats body_env1 body1)
                         ; return (env, rhs') }
 
                 else if null tvs then           -- Simple floating
@@ -348,8 +353,8 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                 else                            -- Do type-abstraction first
                      do { tick LetFloatFromLet
                         ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
-                        ; rhs' <- mkLam tvs' body3
-                        ; let env' = foldl (addPolyBind top_lvl) env poly_binds
+                        ; rhs' <- mkLam env tvs' body3
+                        ; env' <- foldlM (addPolyBind top_lvl) env poly_binds
                         ; return (env', rhs') }
 
         ; completeBind env' top_lvl bndr bndr1 rhs' }
@@ -365,18 +370,22 @@ simplNonRecX :: SimplEnv
              -> SimplM SimplEnv
 
 simplNonRecX env bndr new_rhs
+  | isDeadBinder bndr  -- Not uncommon; e.g. case (a,b) of b { (p,q) -> p }
+  = return env         --               Here b is dead, and we avoid creating
+  | otherwise          --               the binding b = (a,b)
   = do  { (env', bndr') <- simplBinder env bndr
-        ; completeNonRecX env' (isStrictId bndr) bndr bndr' new_rhs }
+        ; completeNonRecX NotTopLevel env' (isStrictId bndr) bndr bndr' new_rhs }
+               -- simplNonRecX is only used for NotTopLevel things
 
-completeNonRecX :: SimplEnv
+completeNonRecX :: TopLevelFlag -> SimplEnv
                 -> Bool
                 -> InId                 -- Old binder
                 -> OutId                -- New binder
                 -> OutExpr              -- Simplified RHS
                 -> SimplM SimplEnv
 
-completeNonRecX env is_strict old_bndr new_bndr new_rhs
-  = do  { (env1, rhs1) <- prepareRhs (zapFloats env) new_rhs
+completeNonRecX top_lvl env is_strict old_bndr new_bndr new_rhs
+  = do  { (env1, rhs1) <- prepareRhs top_lvl (zapFloats env) new_bndr new_rhs
         ; (env2, rhs2) <-
                 if doFloatFromRhs NotTopLevel NonRecursive is_strict rhs1 env1
                 then do { tick LetFloatFromLet
@@ -427,36 +436,42 @@ Here we want to make e1,e2 trivial and get
 That's what the 'go' loop in prepareRhs does
 
 \begin{code}
-prepareRhs :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
+prepareRhs :: TopLevelFlag -> SimplEnv -> OutId -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Adds new floats to the env iff that allows us to return a good RHS
-prepareRhs env (Cast rhs co)    -- Note [Float coercions]
+prepareRhs top_lvl env id (Cast rhs co)    -- Note [Float coercions]
   | (ty1, _ty2) <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
   , not (isUnLiftedType ty1)            -- see Note [Float coercions (unlifted)]
-  = do  { (env', rhs') <- makeTrivial env rhs
+  = do  { (env', rhs') <- makeTrivialWithInfo top_lvl env sanitised_info rhs
         ; return (env', Cast rhs' co) }
+  where
+    sanitised_info = vanillaIdInfo `setStrictnessInfo` strictnessInfo info
+                                   `setDemandInfo`     demandInfo info
+    info = idInfo id
 
-prepareRhs env0 rhs0
-  = do  { (_is_val, env1, rhs1) <- go 0 env0 rhs0
+prepareRhs top_lvl env0 _ rhs0
+  = do  { (_is_exp, env1, rhs1) <- go 0 env0 rhs0
         ; return (env1, rhs1) }
   where
     go n_val_args env (Cast rhs co)
-        = do { (is_val, env', rhs') <- go n_val_args env rhs
-             ; return (is_val, env', Cast rhs' co) }
+        = do { (is_exp, env', rhs') <- go n_val_args env rhs
+             ; return (is_exp, env', Cast rhs' co) }
     go n_val_args env (App fun (Type ty))
-        = do { (is_val, env', rhs') <- go n_val_args env fun
-             ; return (is_val, env', App rhs' (Type ty)) }
+        = do { (is_exp, env', rhs') <- go n_val_args env fun
+             ; return (is_exp, env', App rhs' (Type ty)) }
     go n_val_args env (App fun arg)
-        = do { (is_val, env', fun') <- go (n_val_args+1) env fun
-             ; case is_val of
-                True -> do { (env'', arg') <- makeTrivial env' arg
+        = do { (is_exp, env', fun') <- go (n_val_args+1) env fun
+             ; case is_exp of
+                True -> do { (env'', arg') <- makeTrivial top_lvl env' arg
                            ; return (True, env'', App fun' arg') }
                 False -> return (False, env, App fun arg) }
     go n_val_args env (Var fun)
-        = return (is_val, env, Var fun)
+        = return (is_exp, env, Var fun)
         where
-          is_val = n_val_args > 0       -- There is at least one arg
-                                        -- ...and the fun a constructor or PAP
-                 && (isDataConWorkId fun || n_val_args < idArity fun)
+          is_exp = isExpandableApp fun n_val_args   -- The fun a constructor or PAP
+                       -- See Note [CONLIKE pragma] in BasicTypes
+                       -- The definition of is_exp should match that in
+                       -- OccurAnal.occAnalApp
+
     go _ env other
         = return (False, env, other)
 \end{code}
@@ -484,6 +499,17 @@ and lead to further optimisation.  Example:
           go n = case x of { T m -> go (n-m) }
                 -- This case should optimise
 
+Note [Preserve strictness when floating coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In the Note [Float coercions] transformation, keep the strictness info.
+Eg
+       f = e `cast` co    -- f has strictness SSL
+When we transform to
+        f' = e            -- f' also has strictness SSL
+        f = f' `cast` co   -- f still has strictness SSL
+
+Its not wrong to drop it on the floor, but better to keep it.
+
 Note [Float coercions (unlifted)]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 BUT don't do [Float coercions] if 'e' has an unlifted type.
@@ -502,28 +528,68 @@ These strange casts can happen as a result of case-of-case
 
 
 \begin{code}
-makeTrivial :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
+makeTrivial :: TopLevelFlag -> SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Binds the expression to a variable, if it's not trivial, returning the variable
-makeTrivial env expr
-  | exprIsTrivial expr
+makeTrivial top_lvl env expr = makeTrivialWithInfo top_lvl env vanillaIdInfo expr
+
+makeTrivialWithInfo :: TopLevelFlag -> SimplEnv -> IdInfo 
+                    -> OutExpr -> SimplM (SimplEnv, OutExpr)
+-- Propagate strictness and demand info to the new binder
+-- Note [Preserve strictness when floating coercions]
+-- Returned SimplEnv has same substitution as incoming one
+makeTrivialWithInfo top_lvl env info expr
+  | exprIsTrivial expr                                 -- Already trivial
+  || not (bindingOk top_lvl expr expr_ty)      -- Cannot trivialise
+                                               --   See Note [Cannot trivialise]
   = return (env, expr)
   | otherwise           -- See Note [Take care] below
-  = do  { var <- newId (fsLit "a") (exprType expr)
-        ; env' <- completeNonRecX env False var var expr
---       pprTrace "makeTrivial" (vcat [ppr var <+> ppr (exprArity (substExpr env' (Var var)))
---                                    , ppr expr
---                                    , ppr (substExpr env' (Var var))
---                                    , ppr (idArity (fromJust (lookupInScope (seInScope env') var))) ]) $
-       ; return (env', substExpr env' (Var var)) }
-       -- The substitution is needed becase we're constructing a new binding
+  = do  { uniq <- getUniqueM
+        ; let name = mkSystemVarName uniq (fsLit "a")
+              var = mkLocalIdWithInfo name expr_ty info
+        ; env' <- completeNonRecX top_lvl env False var var expr
+       ; expr' <- simplVar env' var
+        ; return (env', expr') }
+       -- The simplVar is needed becase we're constructing a new binding
        --     a = rhs
        -- And if rhs is of form (rhs1 |> co), then we might get
        --     a1 = rhs1
        --     a = a1 |> co
        -- and now a's RHS is trivial and can be substituted out, and that
        -- is what completeNonRecX will do
+       -- To put it another way, it's as if we'd simplified
+       --    let var = e in var
+  where
+    expr_ty = exprType expr
+
+bindingOk :: TopLevelFlag -> CoreExpr -> Type -> Bool
+-- True iff we can have a binding of this expression at this level
+-- Precondition: the type is the type of the expression
+bindingOk top_lvl _ expr_ty
+  | isTopLevel top_lvl = not (isUnLiftedType expr_ty) 
+  | otherwise          = True
 \end{code}
 
+Note [Cannot trivialise]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider tih
+   f :: Int -> Addr#
+   
+   foo :: Bar
+   foo = Bar (f 3)
+
+Then we can't ANF-ise foo, even though we'd like to, because
+we can't make a top-level binding for the Addr# (f 3). And if
+so we don't want to turn it into
+   foo = let x = f 3 in Bar x
+because we'll just end up inlining x back, and that makes the
+simplifier loop.  Better not to ANF-ise it at all.
+
+A case in point is literal strings (a MachStr is not regarded as
+trivial):
+
+   foo = Ptr "blob"#
+
+We don't want to ANF-ise this.
 
 %************************************************************************
 %*                                                                      *
@@ -561,29 +627,24 @@ completeBind :: SimplEnv
 --      * or by adding to the floats in the envt
 
 completeBind env top_lvl old_bndr new_bndr new_rhs
-  | postInlineUnconditionally env top_lvl new_bndr occ_info new_rhs unfolding
-                -- Inline and discard the binding
-  = do  { tick (PostInlineUnconditionally old_bndr)
-        ; -- pprTrace "postInlineUnconditionally" (ppr old_bndr <+> ppr new_bndr <+> ppr new_rhs) $
-          return (extendIdSubst env old_bndr (DoneEx new_rhs)) }
-        -- Use the substitution to make quite, quite sure that the
-        -- substitution will happen, since we are going to discard the binding
+  = do { let old_info = idInfo old_bndr
+             old_unf  = unfoldingInfo old_info
+             occ_info = occInfo old_info
 
-  | otherwise
-  = return (addNonRecWithUnf env new_bndr new_rhs unfolding wkr)
-  where
-    unfolding | omit_unfolding = NoUnfolding
-             | otherwise      = mkUnfolding  (isTopLevel top_lvl) new_rhs
-    old_info    = idInfo old_bndr
-    occ_info    = occInfo old_info
-    wkr                = substWorker env (workerInfo old_info)
-    omit_unfolding = isNonRuleLoopBreaker occ_info 
-                  --       or not (activeInline env old_bndr)
-                  -- Do *not* trim the unfolding in SimplGently, else
-                  -- the specialiser can't see it!
-
------------------
-addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplEnv
+       ; new_unfolding <- simplUnfolding env top_lvl old_bndr occ_info new_rhs old_unf
+
+       ; if postInlineUnconditionally env top_lvl new_bndr occ_info new_rhs new_unfolding
+                       -- Inline and discard the binding
+         then do  { tick (PostInlineUnconditionally old_bndr)
+                  ; -- pprTrace "postInlineUnconditionally" (ppr old_bndr <+> equals <+> ppr new_rhs) $
+                     return (extendIdSubst env old_bndr (DoneEx new_rhs)) }
+               -- Use the substitution to make quite, quite sure that the
+               -- substitution will happen, since we are going to discard the binding
+
+         else return (addNonRecWithUnf env new_bndr new_rhs new_unfolding) }
+
+------------------------------
+addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplM SimplEnv
 -- Add a new binding to the environment, complete with its unfolding
 -- but *do not* do postInlineUnconditionally, because we have already
 -- processed some of the scope of the binding
@@ -596,71 +657,136 @@ addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplEnv
 -- opportunity to inline 'y' too.
 
 addPolyBind top_lvl env (NonRec poly_id rhs)
-  = addNonRecWithUnf env poly_id rhs unfolding NoWorker
-  where
-    unfolding | not (activeInline env poly_id) = NoUnfolding
-             | otherwise                      = mkUnfolding (isTopLevel top_lvl) rhs
-               -- addNonRecWithInfo adds the new binding in the
-               -- proper way (ie complete with unfolding etc),
-               -- and extends the in-scope set
+  = do { unfolding <- simplUnfolding env top_lvl poly_id NoOccInfo rhs noUnfolding
+                       -- Assumes that poly_id did not have an INLINE prag
+                       -- which is perhaps wrong.  ToDo: think about this
+        ; return (addNonRecWithUnf env poly_id rhs unfolding) }
 
-addPolyBind _ env bind@(Rec _) = extendFloats env bind
+addPolyBind _ env bind@(Rec _) = return (extendFloats env bind)
                -- Hack: letrecs are more awkward, so we extend "by steam"
                -- without adding unfoldings etc.  At worst this leads to
                -- more simplifier iterations
 
------------------
+------------------------------
 addNonRecWithUnf :: SimplEnv
-                 -> OutId -> OutExpr        -- New binder and RHS
-                 -> Unfolding -> WorkerInfo -- and unfolding
-                 -> SimplEnv
--- Add suitable IdInfo to the Id, add the binding to the floats, and extend the in-scope set
-addNonRecWithUnf env new_bndr rhs unfolding wkr
-  = ASSERT( isId new_bndr )
+                -> OutId -> OutExpr    -- New binder and RHS
+                -> Unfolding           -- New unfolding
+                -> SimplEnv
+addNonRecWithUnf env new_bndr new_rhs new_unfolding
+  = let new_arity = exprArity new_rhs
+       old_arity = idArity new_bndr
+        info1 = idInfo new_bndr `setArityInfo` new_arity
+       
+              -- Unfolding info: Note [Setting the new unfolding]
+       info2 = info1 `setUnfoldingInfo` new_unfolding
+
+        -- Demand info: Note [Setting the demand info]
+        info3 | isEvaldUnfolding new_unfolding = zapDemandInfo info2 `orElse` info2
+              | otherwise                      = info2
+
+        final_id = new_bndr `setIdInfo` info3
+       dmd_arity = length $ fst $ splitStrictSig $ idStrictness new_bndr
+    in
+    ASSERT( isId new_bndr )
     WARN( new_arity < old_arity || new_arity < dmd_arity, 
-          (ppr final_id <+> ppr old_arity <+> ppr new_arity <+> ppr dmd_arity) $$ ppr rhs )
-    final_id `seq`      -- This seq forces the Id, and hence its IdInfo,
-                       -- and hence any inner substitutions
-    addNonRec env final_id rhs
-       -- The addNonRec adds it to the in-scope set too
+          (ptext (sLit "Arity decrease:") <+> (ppr final_id <+> ppr old_arity
+               <+> ppr new_arity <+> ppr dmd_arity) $$ ppr new_rhs) )
+       -- Note [Arity decrease]
+
+    final_id `seq`   -- This seq forces the Id, and hence its IdInfo,
+                    -- and hence any inner substitutions
+           -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
+    addNonRec env final_id new_rhs
+               -- The addNonRec adds it to the in-scope set too
+
+------------------------------
+simplUnfolding :: SimplEnv-> TopLevelFlag
+              -> Id
+              -> OccInfo -> OutExpr
+              -> Unfolding -> SimplM Unfolding
+-- Note [Setting the new unfolding]
+simplUnfolding env _ _ _ _ (DFunUnfolding ar con ops)
+  = return (DFunUnfolding ar con ops')
   where
-       dmd_arity = length $ fst $ splitStrictSig $ idNewStrictness new_bndr
-       old_arity = idArity new_bndr
+    ops' = map (substExpr (text "simplUnfolding") env) ops
+
+simplUnfolding env top_lvl id _ _ 
+    (CoreUnfolding { uf_tmpl = expr, uf_arity = arity
+                   , uf_src = src, uf_guidance = guide })
+  | isInlineRuleSource src
+  = do { expr' <- simplExpr rule_env expr
+       ; let src' = CoreSubst.substUnfoldingSource (mkCoreSubst (text "inline-unf") env) src
+       ; return (mkCoreUnfolding (isTopLevel top_lvl) src' expr' arity guide) }
+               -- See Note [Top-level flag on inline rules] in CoreUnfold
+  where
+    act      = idInlineActivation id
+    rule_env = updMode (updModeForInlineRules act) env
+                      -- See Note [Simplifying gently inside InlineRules] in SimplUtils
+
+simplUnfolding _ top_lvl id _occ_info new_rhs _
+  = return (mkUnfolding (isTopLevel top_lvl) (isBottomingId id) new_rhs)
+  -- We make an  unfolding *even for loop-breakers*.
+  -- Reason: (a) It might be useful to know that they are WHNF
+  --        (b) In TidyPgm we currently assume that, if we want to
+  --            expose the unfolding then indeed we *have* an unfolding
+  --            to expose.  (We could instead use the RHS, but currently
+  --            we don't.)  The simple thing is always to have one.
+\end{code}
 
-        --      Arity info
-       new_arity = exprArity rhs
-        new_bndr_info = idInfo new_bndr `setArityInfo` new_arity
-
-        --      Unfolding info
-        -- Add the unfolding *only* for non-loop-breakers
-        -- Making loop breakers not have an unfolding at all
-        -- means that we can avoid tests in exprIsConApp, for example.
-        -- This is important: if exprIsConApp says 'yes' for a recursive
-        -- thing, then we can get into an infinite loop
-
-        --      Demand info
-        -- If the unfolding is a value, the demand info may
-        -- go pear-shaped, so we nuke it.  Example:
-        --      let x = (a,b) in
-        --      case x of (p,q) -> h p q x
-        -- Here x is certainly demanded. But after we've nuked
-        -- the case, we'll get just
-        --      let x = (a,b) in h a b x
-        -- and now x is not demanded (I'm assuming h is lazy)
-        -- This really happens.  Similarly
-        --      let f = \x -> e in ...f..f...
-        -- After inlining f at some of its call sites the original binding may
-        -- (for example) be no longer strictly demanded.
-        -- The solution here is a bit ad hoc...
-        info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
-                                  `setWorkerInfo`    wkr
-
-        final_info | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
-                   | otherwise                  = info_w_unf
+Note [Arity decrease]
+~~~~~~~~~~~~~~~~~~~~~
+Generally speaking the arity of a binding should not decrease.  But it *can* 
+legitimately happen becuase of RULES.  Eg
+       f = g Int
+where g has arity 2, will have arity 2.  But if there's a rewrite rule
+       g Int --> h
+where h has arity 1, then f's arity will decrease.  Here's a real-life example,
+which is in the output of Specialise:
+
+     Rec {
+       $dm {Arity 2} = \d.\x. op d
+       {-# RULES forall d. $dm Int d = $s$dm #-}
        
-        final_id = new_bndr `setIdInfo` final_info
-\end{code}
+       dInt = MkD .... opInt ...
+       opInt {Arity 1} = $dm dInt
+
+       $s$dm {Arity 0} = \x. op dInt }
+
+Here opInt has arity 1; but when we apply the rule its arity drops to 0.
+That's why Specialise goes to a little trouble to pin the right arity
+on specialised functions too.
+
+Note [Setting the new unfolding]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* If there's an INLINE pragma, we simplify the RHS gently.  Maybe we
+  should do nothing at all, but simplifying gently might get rid of 
+  more crap.
 
+* If not, we make an unfolding from the new RHS.  But *only* for
+  non-loop-breakers. Making loop breakers not have an unfolding at all
+  means that we can avoid tests in exprIsConApp, for example.  This is
+  important: if exprIsConApp says 'yes' for a recursive thing, then we
+  can get into an infinite loop
+
+If there's an InlineRule on a loop breaker, we hang on to the inlining.
+It's pretty dodgy, but the user did say 'INLINE'.  May need to revisit
+this choice.
+
+Note [Setting the demand info]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the unfolding is a value, the demand info may
+go pear-shaped, so we nuke it.  Example:
+     let x = (a,b) in
+     case x of (p,q) -> h p q x
+Here x is certainly demanded. But after we've nuked
+the case, we'll get just
+     let x = (a,b) in h a b x
+and now x is not demanded (I'm assuming h is lazy)
+This really happens.  Similarly
+     let f = \x -> e in ...f..f...
+After inlining f at some of its call sites the original binding may
+(for example) be no longer strictly demanded.
+The solution here is a bit ad hoc...
 
 
 %************************************************************************
@@ -731,7 +857,7 @@ simplExprF env e cont
 
 simplExprF' :: SimplEnv -> InExpr -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
-simplExprF' env (Var v)        cont = simplVar env v cont
+simplExprF' env (Var v)        cont = simplVarF env v cont
 simplExprF' env (Lit lit)      cont = rebuild env (Lit lit) cont
 simplExprF' env (Note n expr)  cont = simplNote env n expr cont
 simplExprF' env (Cast body co) cont = simplCast env body co cont
@@ -751,14 +877,14 @@ simplExprF' env expr@(Lam _ _) cont
     n_params = length bndrs
     (bndrs, body) = collectBinders expr
     zap | n_args >= n_params = \b -> b
-        | otherwise          = \b -> if isTyVar b then b
+        | otherwise          = \b -> if isTyCoVar b then b
                                      else zapLamIdInfo b
         -- NB: we count all the args incl type args
         -- so we must count all the binders (incl type lambdas)
 
 simplExprF' env (Type ty) cont
   = ASSERT( contIsRhsOrArg cont )
-    do  { ty' <- simplType env ty
+    do  { ty' <- simplCoercion env ty
         ; rebuild env (Type ty') cont }
 
 simplExprF' env (Case scrut bndr _ alts) cont
@@ -790,9 +916,18 @@ simplType :: SimplEnv -> InType -> SimplM OutType
         -- Kept monadic just so we can do the seqType
 simplType env ty
   = -- pprTrace "simplType" (ppr ty $$ ppr (seTvSubst env)) $
-    seqType new_ty   `seq`   return new_ty
+    seqType new_ty `seq` return new_ty
   where
     new_ty = substTy env ty
+
+---------------------------------
+simplCoercion :: SimplEnv -> InType -> SimplM OutType
+-- The InType isn't *necessarily* a coercion, but it might be
+-- (in a type application, say) and optCoercion is a no-op on types
+simplCoercion env co
+  = seqType new_co `seq` return new_co
+  where 
+    new_co = optCoercion (getTvSubst env) co
 \end{code}
 
 
@@ -812,7 +947,7 @@ rebuild env expr cont0
       Stop {}                      -> return (env, expr)
       CoerceIt co cont             -> rebuild env (mkCoerce co expr) cont
       Select _ bndr alts se cont   -> rebuildCase (se `setFloats` env) expr bndr alts cont
-      StrictArg fun _ info cont    -> rebuildCall env (fun `App` expr) info cont
+      StrictArg info _ cont        -> rebuildCall env (info `addArgTo` expr) cont
       StrictBind b bs body se cont -> do { env' <- simplNonRecX (se `setFloats` env) b expr
                                          ; simplLam env' bs body cont }
       ApplyTo _ arg se cont        -> do { arg' <- simplExpr (se `setInScope` env) arg
@@ -830,7 +965,7 @@ rebuild env expr cont0
 simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
           -> SimplM (SimplEnv, OutExpr)
 simplCast env body co0 cont0
-  = do  { co1 <- simplType env co0
+  = do  { co1 <- simplCoercion env co0
         ; simplExprF env body (addCoerce co1 cont0) }
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
@@ -842,8 +977,8 @@ simplCast env body co0 cont0
          | (_l1, t1) <- coercionKind co2
                --      e |> (g1 :: S1~L) |> (g2 :: L~T1)
                 -- ==>
-                --      e,                       if T1=T2
-                --      e |> (g1 . g2 :: T1~T2)  otherwise
+                --      e,                       if S1=T1
+                --      e |> (g1 . g2 :: S1~T1)  otherwise
                 --
                 -- For example, in the initial form of a worker
                 -- we may find  (coerce T (coerce S (\x.e))) y
@@ -854,14 +989,19 @@ simplCast env body co0 cont0
 
        add_coerce co (s1s2, _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
                 -- (f |> g) ty  --->   (f ty) |> (g @ ty)
-                -- This implements the PushT rule from the paper
+                -- This implements the PushT and PushC rules from the paper
          | Just (tyvar,_) <- splitForAllTy_maybe s1s2
-         , not (isCoVar tyvar)
-         = ApplyTo dup (Type ty') (zapSubstEnv env) (addCoerce (mkInstCoercion co ty') cont)
+         = let 
+             (new_arg_ty, new_cast)
+               | isCoVar tyvar = (new_arg_co, mkCselRCoercion co)       -- PushC rule
+               | otherwise     = (ty',        mkInstCoercion co ty')    -- PushT rule
+           in 
+           ApplyTo dup (Type new_arg_ty) (zapSubstEnv arg_se) (addCoerce new_cast cont)
          where
            ty' = substTy (arg_se `setInScope` env) arg_ty
-
-        -- ToDo: the PushC rule is not implemented at all
+          new_arg_co = mkCsel1Coercion co  `mkTransCoercion`
+                              ty'           `mkTransCoercion`
+                        mkSymCoercion (mkCsel2Coercion co)
 
        add_coerce co (s1s2, _t1t2) (ApplyTo dup arg arg_se cont)
          | not (isTypeArg arg)  -- This implements the Push rule from the paper
@@ -880,14 +1020,14 @@ simplCast env body co0 cont0
                 -- But it isn't a common case.
                 --
                 -- Example of use: Trac #995
-         = ApplyTo dup new_arg (zapSubstEnv env) (addCoerce co2 cont)
+         = ApplyTo dup new_arg (zapSubstEnv arg_se) (addCoerce co2 cont)
          where
            -- we split coercion t1->t2 ~ s1->s2 into t1 ~ s1 and
            -- t2 ~ s2 with left and right on the curried form:
            --    (->) t1 t2 ~ (->) s1 s2
            [co1, co2] = decomposeCo 2 co
            new_arg    = mkCoerce (mkSymCoercion co1) arg'
-           arg'       = substExpr (arg_se `setInScope` env) arg
+           arg'       = substExpr (text "move-cast") (arg_se `setInScope` env) arg
 
        add_coerce co _ cont = CoerceIt co cont
 \end{code}
@@ -914,12 +1054,12 @@ simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
 simplLam env bndrs body cont
   = do  { (env', bndrs') <- simplLamBndrs env bndrs
         ; body' <- simplExpr env' body
-        ; new_lam <- mkLam bndrs' body'
+        ; new_lam <- mkLam env' bndrs' body'
         ; rebuild env' new_lam cont }
 
 ------------------
 simplNonRecE :: SimplEnv
-             -> InId                    -- The binder
+             -> InBndr                  -- The binder
              -> (InExpr, SimplEnv)      -- Rhs of binding (or arg of lambda)
              -> ([InBndr], InExpr)      -- Body of the let/lambda
                                         --      \xs.e
@@ -941,7 +1081,7 @@ simplNonRecE :: SimplEnv
        -- First deal with type applications and type lets
        --   (/\a. e) (Type ty)   and   (let a = Type ty in e)
 simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
-  = ASSERT( isTyVar bndr )
+  = ASSERT( isTyCoVar bndr )
     do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
        ; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
 
@@ -955,7 +1095,7 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
                      (StrictBind bndr bndrs body env cont) }
 
   | otherwise
-  = ASSERT( not (isTyVar bndr) )
+  = ASSERT( not (isTyCoVar bndr) )
     do  { (env1, bndr1) <- simplNonRecBndr env bndr
         ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
         ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
@@ -975,40 +1115,42 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
 simplNote :: SimplEnv -> Note -> CoreExpr -> SimplCont
           -> SimplM (SimplEnv, OutExpr)
 simplNote env (SCC cc) e cont
+  | pushCCisNop cc (getEnclosingCC env)  -- scc "f" (...(scc "f" e)...) 
+  = simplExprF env e cont               -- ==>  scc "f" (...e...)
+  | otherwise
   = do  { e' <- simplExpr (setEnclosingCC env currentCCS) e
         ; rebuild env (mkSCC cc e') cont }
 
--- See notes with SimplMonad.inlineMode
-simplNote env InlineMe e cont
-  | Just (inside, outside) <- splitInlineCont cont  -- Boring boring continuation; see notes above
-  = do  {                       -- Don't inline inside an INLINE expression
-          e' <- simplExprC (setMode inlineMode env) e inside
-        ; rebuild env (mkInlineMe e') outside }
-
-  | otherwise   -- Dissolve the InlineMe note if there's
-                -- an interesting context of any kind to combine with
-                -- (even a type application -- anything except Stop)
-  = simplExprF env e cont
-
-simplNote env (CoreNote s) e cont = do
-    e' <- simplExpr env e
-    rebuild env (Note (CoreNote s) e') cont
+simplNote env (CoreNote s) e cont
+  = do { e' <- simplExpr env e
+       ; rebuild env (Note (CoreNote s) e') cont }
 \end{code}
 
 
 %************************************************************************
 %*                                                                      *
-\subsection{Dealing with calls}
+                     Variables
 %*                                                                      *
 %************************************************************************
 
 \begin{code}
-simplVar :: SimplEnv -> Id -> SimplCont -> SimplM (SimplEnv, OutExpr)
-simplVar env var cont
+simplVar :: SimplEnv -> InVar -> SimplM OutExpr
+-- Look up an InVar in the environment
+simplVar env var
+  | isTyCoVar var 
+  = return (Type (substTyVar env var))
+  | otherwise
+  = case substId env var of
+        DoneId var1      -> return (Var var1)
+        DoneEx e         -> return e
+        ContEx tvs ids e -> simplExpr (setSubstEnv env tvs ids) e
+
+simplVarF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplEnv, OutExpr)
+simplVarF env var cont
   = case substId env var of
         DoneEx e         -> simplExprF (zapSubstEnv env) e cont
         ContEx tvs ids e -> simplExprF (setSubstEnv env tvs ids) e cont
-        DoneId var1      -> completeCall (zapSubstEnv env) var1 cont
+        DoneId var1      -> completeCall env var1 cont
                 -- Note [zapSubstEnv]
                 -- The template is already simplified, so don't re-substitute.
                 -- This is VITAL.  Consider
@@ -1024,94 +1166,50 @@ simplVar env var cont
 
 completeCall :: SimplEnv -> Id -> SimplCont -> SimplM (SimplEnv, OutExpr)
 completeCall env var cont
-  = do  { dflags <- getDOptsSmpl
-        ; let   (args,call_cont) = contArgs cont
+  = do  {   ------------- Try inlining ----------------
+          dflags <- getDOptsSmpl
+        ; let  (lone_variable, arg_infos, call_cont) = contArgs cont
                 -- The args are OutExprs, obtained by *lazily* substituting
                 -- in the args found in cont.  These args are only examined
                 -- to limited depth (unless a rule fires).  But we must do
                 -- the substitution; rule matching on un-simplified args would
                 -- be bogus
 
-        ------------- First try rules ----------------
-        -- Do this before trying inlining.  Some functions have
-        -- rules *and* are strict; in this case, we don't want to
-        -- inline the wrapper of the non-specialised thing; better
-        -- to call the specialised thing instead.
-        --
-        -- We used to use the black-listing mechanism to ensure that inlining of
-        -- the wrapper didn't occur for things that have specialisations till a
-        -- later phase, so but now we just try RULES first
-        --
-        -- Note [Rules for recursive functions]
-        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-        -- You might think that we shouldn't apply rules for a loop breaker:
-        -- doing so might give rise to an infinite loop, because a RULE is
-        -- rather like an extra equation for the function:
-        --      RULE:           f (g x) y = x+y
-        --      Eqn:            f a     y = a-y
-        --
-        -- But it's too drastic to disable rules for loop breakers.
-        -- Even the foldr/build rule would be disabled, because foldr
-        -- is recursive, and hence a loop breaker:
-        --      foldr k z (build g) = g k z
-        -- So it's up to the programmer: rules can cause divergence
-        ; rule_base <- getSimplRules
-        ; let   in_scope   = getInScope env
-               rules      = getRules rule_base var
-                maybe_rule = case activeRule dflags env of
-                                Nothing     -> Nothing  -- No rules apply
-                                Just act_fn -> lookupRule act_fn in_scope
-                                                          var args rules 
-        ; case maybe_rule of {
-            Just (rule, rule_rhs) -> do
-                tick (RuleFired (ru_name rule))
-                (if dopt Opt_D_dump_rule_firings dflags then
-                   pprTrace "Rule fired" (vcat [
-                        text "Rule:" <+> ftext (ru_name rule),
-                        text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
-                        text "After: " <+> pprCoreExpr rule_rhs,
-                        text "Cont:  " <+> ppr call_cont])
-                 else
-                        id)             $
-                 simplExprF env rule_rhs (dropArgs (ruleArity rule) cont)
-                 -- The ruleArity says how many args the rule consumed
-
-          ; Nothing -> do       -- No rules
-
-        ------------- Next try inlining ----------------
-        { let   arg_infos = [interestingArg arg | arg <- args, isValArg arg]
-                n_val_args = length arg_infos
-                interesting_cont = interestingCallContext call_cont
-                active_inline = activeInline env var
-                maybe_inline  = callSiteInline dflags active_inline var
-                                               (null args) arg_infos interesting_cont
+               n_val_args = length arg_infos
+               interesting_cont = interestingCallContext call_cont
+               unfolding    = activeUnfolding env var
+               maybe_inline = callSiteInline dflags var unfolding
+                                             lone_variable arg_infos interesting_cont
         ; case maybe_inline of {
-            Just unfolding      -- There is an inlining!
+            Just expr      -- There is an inlining!
               ->  do { tick (UnfoldingDone var)
-                     ; (if dopt Opt_D_dump_inlinings dflags then
-                           pprTrace ("Inlining done" ++ showSDoc (ppr var)) (vcat [
-                                text "Before:" <+> ppr var <+> sep (map pprParendExpr args),
-                                text "Inlined fn: " <+> nest 2 (ppr unfolding),
-                                text "Cont:  " <+> ppr call_cont])
-                         else
-                                id)
-                       simplExprF env unfolding cont }
-
-            ; Nothing ->                -- No inlining!
-
-        ------------- No inlining! ----------------
-        -- Next, look for rules or specialisations that match
-        --
-        rebuildCall env (Var var)
-                    (mkArgInfo var n_val_args call_cont) cont
-    }}}}
+                     ; trace_inline dflags expr cont $
+                       simplExprF (zapSubstEnv env) expr cont }
+
+            ; Nothing -> do               -- No inlining!
+
+        { rule_base <- getSimplRules
+        ; let info = mkArgInfo var (getRules rule_base var) n_val_args call_cont
+        ; rebuildCall env info cont
+    }}}
+  where
+    trace_inline dflags unfolding cont stuff
+      | not (dopt Opt_D_dump_inlinings dflags) = stuff
+      | not (dopt Opt_D_verbose_core2core dflags) 
+      = if isExternalName (idName var) then 
+         pprTrace "Inlining done:" (ppr var) stuff
+        else stuff
+      | otherwise
+      = pprTrace ("Inlining done: " ++ showSDoc (ppr var))
+           (vcat [text "Inlined fn: " <+> nest 2 (ppr unfolding),
+                  text "Cont:  " <+> ppr cont])
+           stuff
 
 rebuildCall :: SimplEnv
-            -> OutExpr       -- Function 
             -> ArgInfo
             -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
-rebuildCall env fun (ArgInfo { ai_strs = [] }) cont
+rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_strs = [] }) cont
   -- When we run out of strictness args, it means
   -- that the call is definitely bottom; see SimplUtils.mkArgInfo
   -- Then we want to discard the entire strict continuation.  E.g.
@@ -1123,25 +1221,26 @@ rebuildCall env fun (ArgInfo { ai_strs = [] }) cont
   -- the continuation, leaving just the bottoming expression.  But the
   -- type might not be right, so we may have to add a coerce.
   | not (contIsTrivial cont)     -- Only do this if there is a non-trivial
-  = return (env, mk_coerce fun)  -- contination to discard, else we do it
+  = return (env, mk_coerce res)  -- contination to discard, else we do it
   where                          -- again and again!
-    fun_ty  = exprType fun
-    cont_ty = contResultType env fun_ty cont
-    co      = mkUnsafeCoercion fun_ty cont_ty
-    mk_coerce expr | cont_ty `coreEqType` fun_ty = expr
+    res     = mkApps (Var fun) (reverse rev_args)
+    res_ty  = exprType res
+    cont_ty = contResultType env res_ty cont
+    co      = mkUnsafeCoercion res_ty cont_ty
+    mk_coerce expr | cont_ty `coreEqType` res_ty = expr
                    | otherwise = mkCoerce co expr
 
-rebuildCall env fun info (ApplyTo _ (Type arg_ty) se cont)
-  = do  { ty' <- simplType (se `setInScope` env) arg_ty
-        ; rebuildCall env (fun `App` Type ty') info cont }
+rebuildCall env info (ApplyTo _ (Type arg_ty) se cont)
+  = do  { ty' <- simplCoercion (se `setInScope` env) arg_ty
+        ; rebuildCall env (info `addArgTo` Type ty') cont }
 
-rebuildCall env fun 
-           (ArgInfo { ai_rules = has_rules, ai_strs = str:strs, ai_discs = disc:discs })
-           (ApplyTo _ arg arg_se cont)
+rebuildCall env info@(ArgInfo { ai_encl = encl_rules
+                              , ai_strs = str:strs, ai_discs = disc:discs })
+            (ApplyTo _ arg arg_se cont)
   | str                -- Strict argument
   = -- pprTrace "Strict Arg" (ppr arg $$ ppr (seIdSubst env) $$ ppr (seInScope env)) $
     simplExprF (arg_se `setFloats` env) arg
-               (StrictArg fun cci arg_info' cont)
+               (StrictArg info' cci cont)
                 -- Note [Shadowing]
 
   | otherwise                           -- Lazy argument
@@ -1151,16 +1250,40 @@ rebuildCall env fun
         -- floating a demanded let.
   = do  { arg' <- simplExprC (arg_se `setInScope` env) arg
                              (mkLazyArgStop cci)
-        ; rebuildCall env (fun `App` arg') arg_info' cont }
+        ; rebuildCall env (addArgTo info' arg') cont }
   where
-    arg_info' = ArgInfo { ai_rules = has_rules, ai_strs = strs, ai_discs = discs }
-    cci | has_rules || disc > 0 = ArgCtxt has_rules disc  -- Be keener here
-        | otherwise             = BoringCtxt              -- Nothing interesting
-
-rebuildCall env fun _ cont
-  = rebuild env fun cont
+    info' = info { ai_strs = strs, ai_discs = discs }
+    cci | encl_rules || disc > 0 = ArgCtxt encl_rules  -- Be keener here
+        | otherwise              = BoringCtxt          -- Nothing interesting
+
+rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_rules = rules }) cont
+  = do {  -- We've accumulated a simplified call in <fun,rev_args> 
+          -- so try rewrite rules; see Note [RULEs apply to simplified arguments]
+         -- See also Note [Rules for recursive functions]
+       ; let args = reverse rev_args
+              env' = zapSubstEnv env
+       ; mb_rule <- tryRules env rules fun args cont
+       ; case mb_rule of {
+            Just (n_args, rule_rhs) -> simplExprF env' rule_rhs $
+                                        pushArgs env' (drop n_args args) cont ;
+                 -- n_args says how many args the rule consumed
+           ; Nothing -> rebuild env (mkApps (Var fun) args) cont      -- No rules
+    } }
 \end{code}
 
+Note [RULES apply to simplified arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very desirable to try RULES once the arguments have been simplified, because
+doing so ensures that rule cascades work in one pass.  Consider
+   {-# RULES g (h x) = k x
+            f (k x) = x #-}
+   ...f (g (h x))...
+Then we want to rewrite (g (h x)) to (k x) and only then try f's rules. If
+we match f's rules against the un-simplified RHS, it won't match.  This 
+makes a particularly big difference when superclass selectors are involved:
+       op ($p1 ($p2 (df d)))
+We want all this to unravel in one sweeep.
+
 Note [Shadowing]
 ~~~~~~~~~~~~~~~~
 This part of the simplifier may break the no-shadowing invariant
@@ -1185,38 +1308,193 @@ to get the effect that finding (error "foo") in a strict arg position will
 discard the entire application and replace it with (error "foo").  Getting
 all this at once is TOO HARD!
 
+
+%************************************************************************
+%*                                                                      *
+                Rewrite rules
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+tryRules :: SimplEnv -> [CoreRule]
+         -> Id -> [OutExpr] -> SimplCont 
+        -> SimplM (Maybe (Arity, CoreExpr))         -- The arity is the number of
+                                                    -- args consumed by the rule
+tryRules env rules fn args call_cont
+  | null rules
+  = return Nothing
+  | otherwise
+  = do { dflags <- getDOptsSmpl
+       ; case activeRule dflags env of {
+           Nothing     -> return Nothing  ; -- No rules apply
+           Just act_fn -> 
+         case lookupRule act_fn (activeUnfInRule env) (getInScope env) fn args rules of {
+           Nothing               -> return Nothing ;   -- No rule matches
+           Just (rule, rule_rhs) ->
+
+             do { tick (RuleFired (ru_name rule))
+                ; trace_dump dflags rule rule_rhs $
+                  return (Just (ruleArity rule, rule_rhs)) }}}}
+  where
+    trace_dump dflags rule rule_rhs stuff
+      | not (dopt Opt_D_dump_rule_firings dflags) = stuff
+      | not (dopt Opt_D_verbose_core2core dflags) 
+
+      = pprTrace "Rule fired:" (ftext (ru_name rule)) stuff
+      | otherwise
+      = pprTrace "Rule fired"
+           (vcat [text "Rule:" <+> ftext (ru_name rule),
+                 text "Before:" <+> ppr fn <+> sep (map pprParendExpr args),
+                 text "After: " <+> pprCoreExpr rule_rhs,
+                 text "Cont:  " <+> ppr call_cont])
+           stuff
+\end{code}
+
+Note [Rules for recursive functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might think that we shouldn't apply rules for a loop breaker:
+doing so might give rise to an infinite loop, because a RULE is
+rather like an extra equation for the function:
+     RULE:           f (g x) y = x+y
+     Eqn:            f a     y = a-y
+
+But it's too drastic to disable rules for loop breakers.
+Even the foldr/build rule would be disabled, because foldr
+is recursive, and hence a loop breaker:
+     foldr k z (build g) = g k z
+So it's up to the programmer: rules can cause divergence
+
+
 %************************************************************************
 %*                                                                      *
                 Rebuilding a cse expression
 %*                                                                      *
 %************************************************************************
 
-Blob of helper functions for the "case-of-something-else" situation.
+Note [Case elimination]
+~~~~~~~~~~~~~~~~~~~~~~~
+The case-elimination transformation discards redundant case expressions.
+Start with a simple situation:
+
+        case x# of      ===>   e[x#/y#]
+          y# -> e
+
+(when x#, y# are of primitive type, of course).  We can't (in general)
+do this for algebraic cases, because we might turn bottom into
+non-bottom!
+
+The code in SimplUtils.prepareAlts has the effect of generalise this
+idea to look for a case where we're scrutinising a variable, and we
+know that only the default case can match.  For example:
+
+        case x of
+          0#      -> ...
+          DEFAULT -> ...(case x of
+                         0#      -> ...
+                         DEFAULT -> ...) ...
+
+Here the inner case is first trimmed to have only one alternative, the
+DEFAULT, after which it's an instance of the previous case.  This
+really only shows up in eliminating error-checking code.
+
+We also make sure that we deal with this very common case:
+
+        case e of
+          x -> ...x...
+
+Here we are using the case as a strict let; if x is used only once
+then we want to inline it.  We have to be careful that this doesn't
+make the program terminate when it would have diverged before, so we
+check that
+        - e is already evaluated (it may so if e is a variable)
+        - x is used strictly, or
+
+Lastly, the code in SimplUtils.mkCase combines identical RHSs.  So
+
+        case e of       ===> case e of DEFAULT -> r
+           True  -> r
+           False -> r
+
+Now again the case may be elminated by the CaseElim transformation.
+
+
+Further notes about case elimination
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:       test :: Integer -> IO ()
+                test = print
+
+Turns out that this compiles to:
+    Print.test
+      = \ eta :: Integer
+          eta1 :: State# RealWorld ->
+          case PrelNum.< eta PrelNum.zeroInteger of wild { __DEFAULT ->
+          case hPutStr stdout
+                 (PrelNum.jtos eta ($w[] @ Char))
+                 eta1
+          of wild1 { (# new_s, a4 #) -> PrelIO.lvl23 new_s  }}
+
+Notice the strange '<' which has no effect at all. This is a funny one.
+It started like this:
+
+f x y = if x < 0 then jtos x
+          else if y==0 then "" else jtos x
+
+At a particular call site we have (f v 1).  So we inline to get
+
+        if v < 0 then jtos x
+        else if 1==0 then "" else jtos x
+
+Now simplify the 1==0 conditional:
+
+        if v<0 then jtos v else jtos v
+
+Now common-up the two branches of the case:
+
+        case (v<0) of DEFAULT -> jtos v
+
+Why don't we drop the case?  Because it's strict in v.  It's technically
+wrong to drop even unnecessary evaluations, and in practice they
+may be a result of 'seq' so we *definitely* don't want to drop those.
+I don't really know how to improve this situation.
 
 \begin{code}
 ---------------------------------------------------------
 --      Eliminate the case if possible
 
-rebuildCase :: SimplEnv
-            -> OutExpr          -- Scrutinee
-            -> InId             -- Case binder
-            -> [InAlt]          -- Alternatives (inceasing order)
-            -> SimplCont
-            -> SimplM (SimplEnv, OutExpr)
+rebuildCase, reallyRebuildCase
+   :: SimplEnv
+   -> OutExpr          -- Scrutinee
+   -> InId             -- Case binder
+   -> [InAlt]          -- Alternatives (inceasing order)
+   -> SimplCont
+   -> SimplM (SimplEnv, OutExpr)
 
 --------------------------------------------------
 --      1. Eliminate the case if there's a known constructor
 --------------------------------------------------
 
 rebuildCase env scrut case_bndr alts cont
-  | Just (con,args) <- exprIsConApp_maybe scrut
-        -- Works when the scrutinee is a variable with a known unfolding
-        -- as well as when it's an explicit constructor application
-  = knownCon env scrut (DataAlt con) args case_bndr alts cont
-
   | Lit lit <- scrut    -- No need for same treatment as constructors
                         -- because literals are inlined more vigorously
-  = knownCon env scrut (LitAlt lit) [] case_bndr alts cont
+  = do  { tick (KnownBranch case_bndr)
+        ; case findAlt (LitAlt lit) alts of
+           Nothing           -> missingAlt env case_bndr alts cont
+           Just (_, bs, rhs) -> simple_rhs bs rhs }
+
+  | Just (con, ty_args, other_args) <- exprIsConApp_maybe (activeUnfInRule env) scrut
+        -- Works when the scrutinee is a variable with a known unfolding
+        -- as well as when it's an explicit constructor application
+  = do  { tick (KnownBranch case_bndr)
+        ; case findAlt (DataAlt con) alts of
+           Nothing  -> missingAlt env case_bndr alts cont
+            Just (DEFAULT, bs, rhs) -> simple_rhs bs rhs
+           Just (_, bs, rhs)       -> knownCon env scrut con ty_args other_args 
+                                                case_bndr bs rhs cont
+       }
+  where
+    simple_rhs bs rhs = ASSERT( null bs ) 
+                        do { env' <- simplNonRecX env case_bndr scrut
+                          ; simplExprF env' rhs cont }
 
 
 --------------------------------------------------
@@ -1225,7 +1503,7 @@ rebuildCase env scrut case_bndr alts cont
 
 rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
   -- See if we can get rid of the case altogether
-  -- See the extensive notes on case-elimination above
+  -- See Note [Case eliminiation] 
   -- mkCase made sure that if all the alternatives are equal,
   -- then there is now only one (DEFAULT) rhs
  | all isDeadBinder bndrs       -- bndrs are [InId]
@@ -1257,18 +1535,39 @@ rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
   where
         -- The case binder is going to be evaluated later,
         -- and the scrutinee is a simple variable
-    var_demanded_later (Var v) = isStrictDmd (idNewDemandInfo case_bndr)
+    var_demanded_later (Var v) = isStrictDmd (idDemandInfo case_bndr)
                                  && not (isTickBoxOp v)
                                     -- ugly hack; covering this case is what
                                     -- exprOkForSpeculation was intended for.
     var_demanded_later _       = False
 
+--------------------------------------------------
+--      3. Try seq rules; see Note [User-defined RULES for seq] in MkId
+--------------------------------------------------
+
+rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
+  | all isDeadBinder (case_bndr : bndrs)  -- So this is just 'seq'
+  = do { let rhs' = substExpr (text "rebuild-case") env rhs
+             out_args = [Type (substTy env (idType case_bndr)), 
+                        Type (exprType rhs'), scrut, rhs']
+                     -- Lazily evaluated, so we don't do most of this
+
+       ; rule_base <- getSimplRules
+       ; mb_rule <- tryRules env (getRules rule_base seqId) seqId out_args cont
+       ; case mb_rule of 
+           Just (n_args, res) -> simplExprF (zapSubstEnv env) 
+                                           (mkApps res (drop n_args out_args))
+                                            cont
+          Nothing -> reallyRebuildCase env scrut case_bndr alts cont }
+
+rebuildCase env scrut case_bndr alts cont
+  = reallyRebuildCase env scrut case_bndr alts cont
 
 --------------------------------------------------
 --      3. Catch-all case
 --------------------------------------------------
 
-rebuildCase env scrut case_bndr alts cont
+reallyRebuildCase env scrut case_bndr alts cont
   = do  {       -- Prepare the continuation;
                 -- The new subst_env is in place
           (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont
@@ -1277,21 +1576,13 @@ rebuildCase env scrut case_bndr alts cont
         ; (scrut', case_bndr', alts') <- simplAlts env' scrut case_bndr alts dup_cont
 
        -- Check for empty alternatives
-       ; if null alts' then
-               -- This isn't strictly an error, although it is unusual. 
-               -- It's possible that the simplifer might "see" that 
-               -- an inner case has no accessible alternatives before 
-               -- it "sees" that the entire branch of an outer case is 
-               -- inaccessible.  So we simply put an error case here instead.
-           pprTrace "mkCase: null alts" (ppr case_bndr <+> ppr scrut) $
-           let res_ty' = contResultType env' (substTy env' (coreAltsType alts)) dup_cont
-               lit = mkStringLit "Impossible alternative"
-           in return (env', mkApps (Var rUNTIME_ERROR_ID) [Type res_ty', lit])
-
+       ; if null alts' then missingAlt env case_bndr alts cont
          else do
-       { case_expr <- mkCase scrut' case_bndr' alts'
+        { dflags <- getDOptsSmpl
+        ; case_expr <- mkCase dflags scrut' case_bndr' alts'
 
-       -- Notice that rebuild gets the in-scope set from env, not alt_env
+       -- Notice that rebuild gets the in-scope set from env', not alt_env
+       -- (which in any case is only build in simplAlts)
        -- The case binder *not* scope over the whole returned case-expression
        ; rebuild env' case_expr nodup_cont } }
 \end{code}
@@ -1301,78 +1592,15 @@ try to eliminate uses of v in the RHSs in favour of case_bndr; that
 way, there's a chance that v will now only be used once, and hence
 inlined.
 
-Note [no-case-of-case]
-~~~~~~~~~~~~~~~~~~~~~~
-We *used* to suppress the binder-swap in case expressoins when 
--fno-case-of-case is on.  Old remarks:
-    "This happens in the first simplifier pass,
-    and enhances full laziness.  Here's the bad case:
-            f = \ y -> ...(case x of I# v -> ...(case x of ...) ... )
-    If we eliminate the inner case, we trap it inside the I# v -> arm,
-    which might prevent some full laziness happening.  I've seen this
-    in action in spectral/cichelli/Prog.hs:
-             [(m,n) | m <- [1..max], n <- [1..max]]
-    Hence the check for NoCaseOfCase."
-However, now the full-laziness pass itself reverses the binder-swap, so this
-check is no longer necessary.
-
-Note [Suppressing the case binder-swap]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There is another situation when it might make sense to suppress the
-case-expression binde-swap. If we have
-
-    case x of w1 { DEFAULT -> case x of w2 { A -> e1; B -> e2 }
-                   ...other cases .... }
-
-We'll perform the binder-swap for the outer case, giving
-
-    case x of w1 { DEFAULT -> case w1 of w2 { A -> e1; B -> e2 }
-                   ...other cases .... }
-
-But there is no point in doing it for the inner case, because w1 can't
-be inlined anyway.  Furthermore, doing the case-swapping involves
-zapping w2's occurrence info (see paragraphs that follow), and that
-forces us to bind w2 when doing case merging.  So we get
-
-    case x of w1 { A -> let w2 = w1 in e1
-                   B -> let w2 = w1 in e2
-                   ...other cases .... }
-
-This is plain silly in the common case where w2 is dead.
-
-Even so, I can't see a good way to implement this idea.  I tried
-not doing the binder-swap if the scrutinee was already evaluated
-but that failed big-time:
-
-        data T = MkT !Int
-
-        case v of w  { MkT x ->
-        case x of x1 { I# y1 ->
-        case x of x2 { I# y2 -> ...
-
-Notice that because MkT is strict, x is marked "evaluated".  But to
-eliminate the last case, we must either make sure that x (as well as
-x1) has unfolding MkT y1.  THe straightforward thing to do is to do
-the binder-swap.  So this whole note is a no-op.
+Historical note: we use to do the "case binder swap" in the Simplifier
+so there were additional complications if the scrutinee was a variable.
+Now the binder-swap stuff is done in the occurrence analyer; see
+OccurAnal Note [Binder swap].
 
 Note [zapOccInfo]
 ~~~~~~~~~~~~~~~~~
-If we replace the scrutinee, v, by tbe case binder, then we have to nuke
-any occurrence info (eg IAmDead) in the case binder, because the
-case-binder now effectively occurs whenever v does.  AND we have to do
-the same for the pattern-bound variables!  Example:
-
-        (case x of { (a,b) -> a }) (case x of { (p,q) -> q })
-
-Here, b and p are dead.  But when we move the argment inside the first
-case RHS, and eliminate the second case, we get
-
-        case x of { (a,b) -> a b }
-
-Urk! b is alive!  Reason: the scrutinee was a variable, and case elimination
-happened.
-
-Indeed, this can happen anytime the case binder isn't dead:
+If the case binder is not dead, then neither are the pattern bound
+variables:  
         case <any> of x { (a,b) ->
         case x of { (p,q) -> p } }
 Here (a,b) both look dead, but come alive after the inner case is eliminated.
@@ -1381,9 +1609,13 @@ The point is that we bring into the envt a binding
 after the outer case, and that makes (a,b) alive.  At least we do unless
 the case binder is guaranteed dead.
 
+In practice, the scrutinee is almost always a variable, so we pretty
+much always zap the OccInfo of the binders.  It doesn't matter much though.
+
+
 Note [Case of cast]
 ~~~~~~~~~~~~~~~~~~~
-Consider        case (v `cast` co) of x { I# ->
+Consider        case (v `cast` co) of x { I# y ->
                 ... (case (v `cast` co) of {...}) ...
 We'd like to eliminate the inner case.  We can get this neatly by
 arranging that inside the outer case we add the unfolding
@@ -1404,10 +1636,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.
-
-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
@@ -1416,193 +1669,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.)
-
-Note [Case elimination]
-~~~~~~~~~~~~~~~~~~~~~~~
-The case-elimination transformation discards redundant case expressions.
-Start with a simple situation:
-
-        case x# of      ===>   e[x#/y#]
-          y# -> e
-
-(when x#, y# are of primitive type, of course).  We can't (in general)
-do this for algebraic cases, because we might turn bottom into
-non-bottom!
-
-The code in SimplUtils.prepareAlts has the effect of generalise this
-idea to look for a case where we're scrutinising a variable, and we
-know that only the default case can match.  For example:
-
-        case x of
-          0#      -> ...
-          DEFAULT -> ...(case x of
-                         0#      -> ...
-                         DEFAULT -> ...) ...
-
-Here the inner case is first trimmed to have only one alternative, the
-DEFAULT, after which it's an instance of the previous case.  This
-really only shows up in eliminating error-checking code.
-
-We also make sure that we deal with this very common case:
-
-        case e of
-          x -> ...x...
-
-Here we are using the case as a strict let; if x is used only once
-then we want to inline it.  We have to be careful that this doesn't
-make the program terminate when it would have diverged before, so we
-check that
-        - e is already evaluated (it may so if e is a variable)
-        - x is used strictly, or
-
-Lastly, the code in SimplUtils.mkCase combines identical RHSs.  So
-
-        case e of       ===> case e of DEFAULT -> r
-           True  -> r
-           False -> r
-
-Now again the case may be elminated by the CaseElim transformation.
-
-
-Further notes about case elimination
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:       test :: Integer -> IO ()
-                test = print
-
-Turns out that this compiles to:
-    Print.test
-      = \ eta :: Integer
-          eta1 :: State# RealWorld ->
-          case PrelNum.< eta PrelNum.zeroInteger of wild { __DEFAULT ->
-          case hPutStr stdout
-                 (PrelNum.jtos eta ($w[] @ Char))
-                 eta1
-          of wild1 { (# new_s, a4 #) -> PrelIO.lvl23 new_s  }}
-
-Notice the strange '<' which has no effect at all. This is a funny one.
-It started like this:
-
-f x y = if x < 0 then jtos x
-          else if y==0 then "" else jtos x
-
-At a particular call site we have (f v 1).  So we inline to get
-
-        if v < 0 then jtos x
-        else if 1==0 then "" else jtos x
-
-Now simplify the 1==0 conditional:
-
-        if v<0 then jtos v else jtos v
-
-Now common-up the two branches of the case:
-
-        case (v<0) of DEFAULT -> jtos v
-
-Why don't we drop the case?  Because it's strict in v.  It's technically
-wrong to drop even unnecessary evaluations, and in practice they
-may be a result of 'seq' so we *definitely* don't want to drop those.
-I don't really know how to improve this situation.
-
-
-\begin{code}
-simplCaseBinder :: SimplEnv -> OutExpr -> OutId -> [InAlt]
-                -> SimplM (SimplEnv, OutExpr, OutId)
-simplCaseBinder env0 scrut0 case_bndr0 alts
-  = do  { (env1, case_bndr1) <- simplBinder env0 case_bndr0
-
-        ; fam_envs <- getFamEnvs
-        ; (env2, scrut2, case_bndr2) <- improve_seq fam_envs env1 scrut0
-                                                case_bndr0 case_bndr1 alts
-                        -- Note [Improving seq]
-
-        ; let (env3, case_bndr3) = improve_case_bndr env2 scrut2 case_bndr2
-                        -- Note [Case of cast]
-
-        ; return (env3, scrut2, case_bndr3) }
-  where
-
-    improve_seq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
-        | 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)
-                    env2 = extendIdSubst env case_bndr rhs
-              ; return (env2, scrut `Cast` co, case_bndr2) }
-
-    improve_seq _ env scrut _ case_bndr1 _
-        = return (env, scrut, case_bndr1)
-
-
-    improve_case_bndr env scrut case_bndr
-        -- See Note [no-case-of-case]
-       --  | switchIsOn (getSwitchChecker env) NoCaseOfCase
-       --  = (env, case_bndr)
-
-        | otherwise     -- Failed try; see Note [Suppressing the case binder-swap]
-                        --     not (isEvaldUnfolding (idUnfolding v))
-        = case scrut of
-            Var v -> (modifyInScope env1 v case_bndr', case_bndr')
-                -- Note about using modifyInScope for v here
-                -- We could extend the substitution instead, but it would be
-                -- a hack because then the substitution wouldn't be idempotent
-                -- any more (v is an OutId).  And this does just as well.
-
-            Cast (Var v) co -> (addBinderUnfolding env1 v rhs, case_bndr')
-                            where
-                                rhs = Cast (Var case_bndr') (mkSymCoercion co)
-
-            _ -> (env, case_bndr)
-        where
-          case_bndr' = zapOccInfo case_bndr
-          env1       = modifyInScope env case_bndr case_bndr'
-
-
-zapOccInfo :: InId -> InId      -- See Note [zapOccInfo]
-zapOccInfo b = b `setIdOccInfo` NoOccInfo
-\end{code}
-
-
-simplAlts does two things:
-
-1.  Eliminate alternatives that cannot match, including the
-    DEFAULT alternative.
-
-2.  If the DEFAULT alternative can match only one possible constructor,
-    then make that constructor explicit.
-    e.g.
-        case e of x { DEFAULT -> rhs }
-     ===>
-        case e of x { (a,b) -> rhs }
-    where the type is a single constructor type.  This gives better code
-    when rhs also scrutinises x or e.
-
-Here "cannot match" includes knowledge from GADTs
-
-It's a good idea do do this stuff before simplifying the alternatives, to
-avoid simplifying alternatives we know can't happen, and to come up with
-the list of constructors that are handled, to put into the IdInfo of the
-case binder, for use when simplifying the alternatives.
-
-Eliminating the default alternative in (1) isn't so obvious, but it can
-happen:
-
-data Colour = Red | Green | Blue
-
-f x = case x of
-        Red -> ..
-        Green -> ..
-        DEFAULT -> h x
-
-h y = case y of
-        Blue -> ..
-        DEFAULT -> [ case y of ... ]
-
-If we inline h into f, the default case of the inlined h can't happen.
-If we don't notice this, we may end up filtering out *all* the cases
-of the inner case y, which give us nowhere to go!
-
+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}
 simplAlts :: SimplEnv
@@ -1612,18 +1681,41 @@ simplAlts :: SimplEnv
          -> SimplCont
           -> SimplM (OutExpr, OutId, [OutAlt])  -- Includes the continuation
 -- Like simplExpr, this just returns the simplified alternatives;
--- it not return an environment
+-- it does not return an environment
 
 simplAlts env scrut case_bndr alts cont'
-  = -- pprTrace "simplAlts" (ppr alts $$ ppr (seIdSubst env)) $
-    do  { let alt_env = zapFloats env
-        ; (alt_env', scrut', case_bndr') <- simplCaseBinder alt_env scrut case_bndr alts
+  = -- pprTrace "simplAlts" (ppr alts $$ ppr (seTvSubst env)) $
+    do  { let env0 = zapFloats env
 
-        ; (imposs_deflt_cons, in_alts) <- prepareAlts alt_env' scrut case_bndr' alts
+        ; (env1, case_bndr1) <- simplBinder env0 case_bndr
+
+        ; fam_envs <- getFamEnvs
+       ; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env1 scrut 
+                                                      case_bndr case_bndr1 alts
+
+        ; (imposs_deflt_cons, in_alts) <- prepareAlts scrut' case_bndr' alts
 
         ; alts' <- mapM (simplAlt alt_env' imposs_deflt_cons case_bndr' cont') in_alts
         ; return (scrut', case_bndr', alts') }
 
+
+------------------------------------
+improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
+          -> OutExpr -> InId -> OutId -> [InAlt]
+          -> SimplM (SimplEnv, OutExpr, OutId)
+-- Note [Improving seq]
+improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
+  | 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)
+              env2 = extendIdSubst env case_bndr rhs
+        ; return (env2, scrut `Cast` co, case_bndr2) }
+
+improveSeq _ env scrut _ case_bndr1 _
+  = return (env, scrut, case_bndr1)
+
+
 ------------------------------------
 simplAlt :: SimplEnv
          -> [AltCon]    -- These constructors can't be present when
@@ -1676,7 +1768,7 @@ simplAlt env _ case_bndr' cont' (DataAlt con, vs, rhs)
         = go vs the_strs
         where
           go [] [] = []
-          go (v:vs') strs | isTyVar v = v : go vs' strs
+          go (v:vs') strs | isTyCoVar v = v : go vs' strs
           go (v:vs') (str:strs)
             | isMarkedStrict str = evald_v  : go vs' strs
             | otherwise          = zapped_v : go vs' strs
@@ -1685,6 +1777,7 @@ simplAlt env _ case_bndr' cont' (DataAlt con, vs, rhs)
               evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
           go _ _ = pprPanic "cat_evals" (ppr con $$ ppr vs $$ ppr the_strs)
 
+       -- See Note [zapOccInfo]
         -- zap_occ_info: if the case binder is alive, then we add the unfolding
         --      case_bndr = C vs
         -- to the envt; so vs are now very much alive
@@ -1692,16 +1785,23 @@ simplAlt env _ case_bndr' cont' (DataAlt con, vs, rhs)
         --        case e of t { (a,b) -> ...(case t of (p,q) -> p)... }
         --   ==>  case e of t { (a,b) -> ...(a)... }
         -- Look, Ma, a is alive now.
-    zap_occ_info | isDeadBinder case_bndr' = \ident -> ident
-                 | otherwise               = zapOccInfo
+    zap_occ_info = zapCasePatIdOcc case_bndr'
 
 addBinderUnfolding :: SimplEnv -> Id -> CoreExpr -> SimplEnv
 addBinderUnfolding env bndr rhs
-  = modifyInScope env bndr (bndr `setIdUnfolding` mkUnfolding False rhs)
+  = modifyInScope env (bndr `setIdUnfolding` mkUnfolding False False rhs)
 
 addBinderOtherCon :: SimplEnv -> Id -> [AltCon] -> SimplEnv
 addBinderOtherCon env bndr cons
-  = modifyInScope env bndr (bndr `setIdUnfolding` mkOtherCon cons)
+  = modifyInScope env (bndr `setIdUnfolding` mkOtherCon cons)
+
+zapCasePatIdOcc :: Id -> Id -> Id
+-- Consider  case e of b { (a,b) -> ... }
+-- Then if we bind b to (a,b) in "...", and b is not dead,
+-- then we must zap the deadness info on a,b
+zapCasePatIdOcc case_bndr
+  | isDeadBinder case_bndr = \ pat_id -> pat_id
+  | otherwise             = \ pat_id -> zapIdOccInfo pat_id
 \end{code}
 
 
@@ -1725,75 +1825,72 @@ and then
 All this should happen in one sweep.
 
 \begin{code}
-knownCon :: SimplEnv -> OutExpr -> AltCon
-        -> [OutExpr]           -- Args *including* the universal args
-         -> InId -> [InAlt] -> SimplCont
+knownCon :: SimplEnv           
+         -> OutExpr                            -- The scrutinee
+         -> DataCon -> [OutType] -> [OutExpr]  -- The scrutinee (in pieces)
+         -> InId -> [InBndr] -> InExpr         -- The alternative
+         -> SimplCont
          -> SimplM (SimplEnv, OutExpr)
 
-knownCon env scrut con args bndr alts cont
-  = do  { tick (KnownBranch bndr)
-        ; knownAlt env scrut args bndr (findAlt con alts) cont }
-
-knownAlt :: SimplEnv -> OutExpr -> [OutExpr]
-         -> InId -> (AltCon, [CoreBndr], InExpr) -> SimplCont
-         -> SimplM (SimplEnv, OutExpr)
-knownAlt env scrut _ bndr (DEFAULT, bs, rhs) cont
-  = ASSERT( null bs )
-    do  { env' <- simplNonRecX env bndr scrut
-                -- This might give rise to a binding with non-atomic args
-                -- like x = Node (f x) (g x)
-                -- but simplNonRecX will atomic-ify it
-        ; simplExprF env' rhs cont }
-
-knownAlt env scrut _ bndr (LitAlt _, bs, rhs) cont
-  = ASSERT( null bs )
-    do  { env' <- simplNonRecX env bndr scrut
-        ; simplExprF env' rhs cont }
-
-knownAlt env scrut the_args bndr (DataAlt dc, bs, rhs) cont
-  = do  { let dead_bndr  = isDeadBinder bndr    -- bndr is an InId
-              n_drop_tys = length (dataConUnivTyVars dc)
-        ; env' <- bind_args env dead_bndr bs (drop n_drop_tys the_args)
-        ; let
-                -- It's useful to bind bndr to scrut, rather than to a fresh
-                -- binding      x = Con arg1 .. argn
-                -- because very often the scrut is a variable, so we avoid
-                -- creating, and then subsequently eliminating, a let-binding
-                -- BUT, if scrut is a not a variable, we must be careful
-                -- about duplicating the arg redexes; in that case, make
-                -- a new con-app from the args
-                bndr_rhs  = case scrut of
-                                Var _ -> scrut
-                                _     -> con_app
-                con_app = mkConApp dc (take n_drop_tys the_args ++ con_args)
-                con_args = [substExpr env' (varToCoreExpr b) | b <- bs]
-                                -- args are aready OutExprs, but bs are InIds
-
-        ; env'' <- simplNonRecX env' bndr bndr_rhs
-        ; -- pprTrace "knownCon2" (ppr bs $$ ppr rhs $$ ppr (seIdSubst env'')) $
-          simplExprF env'' rhs cont }
+knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
+  = do  { env'  <- bind_args env bs dc_args
+        ; env'' <- bind_case_bndr env'
+        ; simplExprF env'' rhs cont }
   where
-    -- Ugh!
-    bind_args env' _ [] _  = return env'
+    zap_occ = zapCasePatIdOcc bndr    -- bndr is an InId
 
-    bind_args env' dead_bndr (b:bs') (Type ty : args)
-      = ASSERT( isTyVar b )
-        bind_args (extendTvSubst env' b ty) dead_bndr bs' args
+                  -- Ugh!
+    bind_args env' [] _  = return env'
 
-    bind_args env' dead_bndr (b:bs') (arg : args)
+    bind_args env' (b:bs') (Type ty : args)
+      = ASSERT( isTyCoVar b )
+        bind_args (extendTvSubst env' b ty) bs' args
+
+    bind_args env' (b:bs') (arg : args)
       = ASSERT( isId b )
-        do { let b' = if dead_bndr then b else zapOccInfo b
+        do { let b' = zap_occ b
              -- Note that the binder might be "dead", because it doesn't
              -- occur in the RHS; and simplNonRecX may therefore discard
              -- it via postInlineUnconditionally.
              -- Nevertheless we must keep it if the case-binder is alive,
              -- because it may be used in the con_app.  See Note [zapOccInfo]
            ; env'' <- simplNonRecX env' b' arg
-           ; bind_args env'' dead_bndr bs' args }
+           ; bind_args env'' bs' args }
 
-    bind_args _ _ _ _ =
-      pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr the_args $$
+    bind_args _ _ _ =
+      pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr dc_args $$
                              text "scrut:" <+> ppr scrut
+
+       -- It's useful to bind bndr to scrut, rather than to a fresh
+       -- binding      x = Con arg1 .. argn
+       -- because very often the scrut is a variable, so we avoid
+       -- creating, and then subsequently eliminating, a let-binding
+       -- BUT, if scrut is a not a variable, we must be careful
+       -- about duplicating the arg redexes; in that case, make
+       -- a new con-app from the args
+    bind_case_bndr env
+      | isDeadBinder bndr   = return env
+      | exprIsTrivial scrut = return (extendIdSubst env bndr (DoneEx scrut))
+      | otherwise           = do { dc_args <- mapM (simplVar env) bs
+                                        -- dc_ty_args are aready OutTypes, 
+                                        -- but bs are InBndrs
+                                ; let con_app = Var (dataConWorkId dc) 
+                                                `mkTyApps` dc_ty_args      
+                                                `mkApps`   dc_args
+                                ; simplNonRecX env bndr con_app }
+  
+-------------------
+missingAlt :: SimplEnv -> Id -> [InAlt] -> SimplCont -> SimplM (SimplEnv, OutExpr)
+               -- This isn't strictly an error, although it is unusual. 
+               -- It's possible that the simplifer might "see" that 
+               -- an inner case has no accessible alternatives before 
+               -- it "sees" that the entire branch of an outer case is 
+               -- inaccessible.  So we simply put an error case here instead.
+missingAlt env case_bndr alts cont
+  = WARN( True, ptext (sLit "missingAlt") <+> ppr case_bndr )
+    return (env, mkImpossibleExpr res_ty)
+  where
+    res_ty = contResultType env (substTy env (coreAltsType alts)) cont
 \end{code}
 
 
@@ -1832,11 +1929,13 @@ mkDupableCont env (CoerceIt ty cont)
 
 mkDupableCont env cont@(StrictBind {})
   =  return (env, mkBoringStop, cont)
-        -- See Note [Duplicating strict continuations]
+        -- See Note [Duplicating StrictBind]
 
-mkDupableCont env cont@(StrictArg {})
-  =  return (env, mkBoringStop, cont)
-        -- See Note [Duplicating strict continuations]
+mkDupableCont env (StrictArg info cci cont)
+        -- See Note [Duplicating StrictArg]
+  = do { (env', dup, nodup) <- mkDupableCont env cont
+       ; (env'', args')     <- mapAccumLM (makeTrivial NotTopLevel) env' (ai_args info)
+       ; return (env'', StrictArg (info { ai_args = args' }) cci dup, nodup) }
 
 mkDupableCont env (ApplyTo _ arg se cont)
   =     -- e.g.         [...hole...] (...arg...)
@@ -1845,7 +1944,7 @@ mkDupableCont env (ApplyTo _ arg se cont)
         --              in [...hole...] a
     do  { (env', dup_cont, nodup_cont) <- mkDupableCont env cont
         ; arg' <- simplExpr (se `setInScope` env') arg
-        ; (env'', arg'') <- makeTrivial env' arg'
+        ; (env'', arg'') <- makeTrivial NotTopLevel env' arg'
         ; let app_cont = ApplyTo OkToDup arg'' (zapSubstEnv env'') dup_cont
         ; return (env'', app_cont, nodup_cont) }
 
@@ -1905,14 +2004,33 @@ mkDupableAlts env case_bndr' the_alts
 
 mkDupableAlt :: SimplEnv -> OutId -> (AltCon, [CoreBndr], CoreExpr)
               -> SimplM (SimplEnv, (AltCon, [CoreBndr], CoreExpr))
-mkDupableAlt env case_bndr' (con, bndrs', rhs')
+mkDupableAlt env case_bndr (con, bndrs', rhs')
   | exprIsDupable rhs'  -- Note [Small alternative rhs]
   = return (env, (con, bndrs', rhs'))
   | otherwise
-  = do  { let rhs_ty'     = exprType rhs'
-              used_bndrs' = filter abstract_over (case_bndr' : bndrs')
+  = do  { let rhs_ty'  = exprType rhs'
+             scrut_ty = idType case_bndr
+             case_bndr_w_unf   
+                = case con of 
+                     DEFAULT    -> case_bndr                                   
+                     DataAlt dc -> setIdUnfolding case_bndr unf
+                         where
+                                -- See Note [Case binders and join points]
+                            unf = mkInlineRule rhs Nothing
+                            rhs = mkConApp dc (map Type (tyConAppArgs scrut_ty)
+                                               ++ varsToCoreExprs bndrs')
+
+                     LitAlt {} -> WARN( True, ptext (sLit "mkDupableAlt")
+                                               <+> ppr case_bndr <+> ppr con )
+                                  case_bndr
+                          -- The case binder is alive but trivial, so why has 
+                          -- it not been substituted away?
+
+              used_bndrs' | isDeadBinder case_bndr = filter abstract_over bndrs'
+                         | otherwise              = bndrs' ++ [case_bndr_w_unf]
+             
               abstract_over bndr
-                  | isTyVar bndr = True -- Abstract over all type variables just in case
+                  | isTyCoVar bndr = True -- Abstract over all type variables just in case
                   | otherwise    = not (isDeadBinder bndr)
                         -- The deadness info on the new Ids is preserved by simplBinders
 
@@ -1935,10 +2053,52 @@ mkDupableAlt env case_bndr' (con, bndrs', rhs')
                 join_rhs  = mkLams really_final_bndrs rhs'
                 join_call = mkApps (Var join_bndr) final_args
 
-        ; return (addPolyBind NotTopLevel env (NonRec join_bndr join_rhs), (con, bndrs', join_call)) }
+       ; env' <- addPolyBind NotTopLevel env (NonRec join_bndr join_rhs)
+        ; return (env', (con, bndrs', join_call)) }
                 -- See Note [Duplicated env]
 \end{code}
 
+Note [Case binders and join points]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this 
+   case (case .. ) of c {
+     I# c# -> ....c....
+
+If we make a join point with c but not c# we get
+  $j = \c -> ....c....
+
+But if later inlining scrutines the c, thus
+
+  $j = \c -> ... case c of { I# y -> ... } ...
+
+we won't see that 'c' has already been scrutinised.  This actually
+happens in the 'tabulate' function in wave4main, and makes a significant
+difference to allocation.
+
+An alternative plan is this:
+
+   $j = \c# -> let c = I# c# in ...c....
+
+but that is bad if 'c' is *not* later scrutinised.  
+
+So instead we do both: we pass 'c' and 'c#' , and record in c's inlining
+(an InlineRule) that it's really I# c#, thus
+   
+   $j = \c# -> \c[=I# c#] -> ...c....
+
+Absence analysis may later discard 'c'.
+
+NB: take great care when doing strictness analysis; 
+    see Note [Lamba-bound unfoldings] in DmdAnal.
+
+Also note that we can still end up passing stuff that isn't used.  Before
+strictness analysis we have
+   let $j x y c{=(x,y)} = (h c, ...)
+   in ...
+After strictness analysis we see that h is strict, we end up with
+   let $j x y c{=(x,y)} = ($wh x y, ...)
+and c is unused.
+   
 Note [Duplicated env]
 ~~~~~~~~~~~~~~~~~~~~~
 Some of the alternatives are simplified, but have not been turned into a join point
@@ -1948,7 +2108,7 @@ we'd lose that when zapping the subst-env.  We could have a per-alt subst-env,
 but zapping it (as we do in mkDupableCont, the Select case) is safe, and
 at worst delays the join-point inlining.
 
-Note [Small alterantive rhs]
+Note [Small alternative rhs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It is worth checking for a small RHS because otherwise we
 get extra let bindings that may cause an extra iteration of the simplifier to
@@ -2017,32 +2177,71 @@ It's a bit silly to add the realWorld dummy arg in this case, making
            True -> $j s
 (the \v alone is enough to make CPR happy) but I think it's rare
 
-Note [Duplicating strict continuations]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Do *not* duplicate StrictBind and StritArg continuations.  We gain
-nothing by propagating them into the expressions, and we do lose a
-lot.  Here's an example:
-        && (case x of { T -> F; F -> T }) E
+Note [Duplicating StrictArg]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The original plan had (where E is a big argument)
+e.g.    f E [..hole..]
+        ==>     let $j = \a -> f E a
+                in $j [..hole..]
+
+But this is terrible! Here's an example:
+        && E (case x of { T -> F; F -> T })
 Now, && is strict so we end up simplifying the case with
 an ArgOf continuation.  If we let-bind it, we get
-
-        let $j = \v -> && v E
+        let $j = \v -> && E v
         in simplExpr (case x of { T -> F; F -> T })
                      (ArgOf (\r -> $j r)
 And after simplifying more we get
-
-        let $j = \v -> && v E
+        let $j = \v -> && E v
         in case x of { T -> $j F; F -> $j T }
 Which is a Very Bad Thing
 
+What we do now is this
+       f E [..hole..]
+       ==>     let a = E
+               in f a [..hole..]
+Now if the thing in the hole is a case expression (which is when
+we'll call mkDupableCont), we'll push the function call into the
+branches, which is what we want.  Now RULES for f may fire, and
+call-pattern specialisation.  Here's an example from Trac #3116
+     go (n+1) (case l of
+                1  -> bs'
+                _  -> Chunk p fpc (o+1) (l-1) bs')
+If we can push the call for 'go' inside the case, we get
+call-pattern specialisation for 'go', which is *crucial* for 
+this program.
+
+Here is the (&&) example: 
+        && E (case x of { T -> F; F -> T })
+  ==>   let a = E in 
+        case x of { T -> && a F; F -> && a T }
+Much better!
+
+Notice that 
+  * Arguments to f *after* the strict one are handled by 
+    the ApplyTo case of mkDupableCont.  Eg
+       f [..hole..] E
+
+  * We can only do the let-binding of E because the function
+    part of a StrictArg continuation is an explicit syntax
+    tree.  In earlier versions we represented it as a function
+    (CoreExpr -> CoreEpxr) which we couldn't take apart.
+
+Do *not* duplicate StrictBind and StritArg continuations.  We gain
+nothing by propagating them into the expressions, and we do lose a
+lot.  
+
+The desire not to duplicate is the entire reason that
+mkDupableCont returns a pair of continuations.
+
+Note [Duplicating StrictBind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Unlike StrictArg, there doesn't seem anything to gain from
+duplicating a StrictBind continuation, so we don't.
+
 The desire not to duplicate is the entire reason that
 mkDupableCont returns a pair of continuations.
 
-The original plan had:
-e.g.    (...strict-fn...) [...hole...]
-        ==>
-                let $j = \a -> ...strict-fn...
-                in $j [...hole...]
 
 Note [Single-alternative cases]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~