Move error-ids to MkCore (from PrelRules)
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index aaeec2e..effd245 100644 (file)
@@ -4,44 +4,45 @@
 \section[Simplify]{The main module of the simplifier}
 
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
 module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
 import DynFlags
 import SimplMonad
-import Type hiding      ( substTy, extendTvSubst )
+import Type hiding      ( substTy, extendTvSubst, substTyVar )
 import SimplEnv
 import SimplUtils
+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 )
+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 Rules            ( lookupRule )
-import BasicTypes       ( isMarkedStrict )
-import CostCentre       ( currentCCS )
+import qualified CoreSubst
+import CoreArity       ( exprArity )
+import Rules            ( lookupRule, getRules )
+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
-import Util
+import FastString
 \end{code}
 
 
@@ -205,20 +206,19 @@ 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 env binds
+simplTopBinds env0 binds0
   = do  {       -- Put all the top-level binders into scope at the start
                 -- so that if a transformation rule has unexpectedly brought
                 -- anything into scope, then we don't get a complaint about that.
                 -- It's rather as if the top-level binders were imported.
-        ; env <- simplRecBndrs env (bindersOfBinds binds)
+        ; env1 <- simplRecBndrs env0 (bindersOfBinds binds0)
         ; dflags <- getDOptsSmpl
-        ; let dump_flag = dopt Opt_D_dump_inlinings dflags ||
-                          dopt Opt_D_dump_rule_firings dflags
-        ; env' <- simpl_binds dump_flag env binds
+        ; let dump_flag = dopt Opt_D_verbose_core2core dflags
+        ; env2 <- simpl_binds dump_flag env1 binds0
         ; freeTick SimplifierDone
-        ; return (getFloats env') }
+        ; return env2 }
   where
         -- We need to track the zapped top-level binders, because
         -- they should have their fragile IdInfo zapped (notably occurrence info)
@@ -227,13 +227,13 @@ simplTopBinds env binds
         -- The dump-flag emits a trace for each top-level binding, which
         -- helps to locate the tracing for inlining and rule firing
     simpl_binds :: Bool -> SimplEnv -> [InBind] -> SimplM SimplEnv
-    simpl_binds dump env []           = return env
-    simpl_binds dump env (bind:binds) = do { env' <- trace dump bind $
+    simpl_binds _    env []           = return env
+    simpl_binds dump env (bind:binds) = do { env' <- trace_bind dump bind $
                                                      simpl_bind env bind
                                            ; simpl_binds dump env' binds }
 
-    trace True  bind = pprTrace "SimplBind" (ppr (bindersOf bind))
-    trace False bind = \x -> x
+    trace_bind True  bind = pprTrace "SimplBind" (ppr (bindersOf bind))
+    trace_bind False _    = \x -> x
 
     simpl_bind env (Rec pairs)  = simplRecBind      env  TopLevel pairs
     simpl_bind env (NonRec b r) = simplRecOrTopPair env' TopLevel b b' r
@@ -255,12 +255,12 @@ simplRecBind is used for
 simplRecBind :: SimplEnv -> TopLevelFlag
              -> [(InId, InExpr)]
              -> SimplM SimplEnv
-simplRecBind env top_lvl pairs
-  = do  { let (env_with_info, triples) = mapAccumL add_rules env pairs
-        ; env' <- go (zapFloats env_with_info) triples
-        ; return (env `addRecFloats` env') }
-        -- addFloats adds the floats from env',
-        -- *and* updates env with the in-scope set from env'
+simplRecBind env0 top_lvl pairs0
+  = do  { let (env_with_info, triples) = mapAccumL add_rules env0 pairs0
+        ; env1 <- go (zapFloats env_with_info) triples
+        ; return (env0 `addRecFloats` env1) }
+        -- addFloats adds the floats from env1,
+        -- _and_ updates env0 with the in-scope set from env1
   where
     add_rules :: SimplEnv -> (InBndr,InExpr) -> (SimplEnv, (InBndr, OutBndr, InExpr))
         -- Add the (substituted) rules to the binder
@@ -271,8 +271,8 @@ simplRecBind env top_lvl pairs
     go env [] = return env
 
     go env ((old_bndr, new_bndr, rhs) : pairs)
-        = do { env <- simplRecOrTopPair env top_lvl old_bndr new_bndr rhs
-             ; go env pairs }
+        = do { env' <- simplRecOrTopPair env top_lvl old_bndr new_bndr rhs
+             ; go env' pairs }
 \end{code}
 
 simplOrTopPair is used for
@@ -322,23 +322,28 @@ simplLazyBind :: SimplEnv
 
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
   = do  { let   rhs_env     = rhs_se `setInScope` env
-                (tvs, body) = collectTyBinders rhs
-        ; (body_env, tvs') <- simplBinders rhs_env tvs
-                -- See Note [Floating and type abstraction]
-                -- in SimplUtils
+               (tvs, body) = case collectTyBinders rhs of
+                               (tvs, body) | not_lam body -> (tvs,body)
+                                           | otherwise    -> ([], rhs)
+               not_lam (Lam _ _) = False
+               not_lam _         = True
+                       -- Do not do the "abstract tyyvar" thing if there's
+                       -- a lambda inside, becuase it defeats eta-reduction
+                       --    f = /\a. \x. g a x  
+                       -- should eta-reduce
 
-        -- Simplify the RHS; note the mkRhsStop, which tells
-        -- the simplifier that this is the RHS of a let.
-        ; let rhs_cont = mkRhsStop (applyTys (idType bndr1) (mkTyVarTys tvs'))
-        ; (body_env1, body1) <- simplExprF body_env body rhs_cont
+        ; (body_env, tvs') <- simplBinders rhs_env tvs
+                -- See Note [Floating and type abstraction] in SimplUtils
 
+        -- Simplify the RHS
+        ; (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,9 @@ 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
-                        ; return (extendFloats env poly_binds, rhs') }
+                        ; rhs' <- mkLam env tvs' body3
+                        ; env' <- foldlM (addPolyBind top_lvl) env poly_binds
+                        ; return (env', rhs') }
 
         ; completeBind env' top_lvl bndr bndr1 rhs' }
 \end{code}
@@ -364,21 +370,24 @@ simplNonRecX :: SimplEnv
              -> SimplM SimplEnv
 
 simplNonRecX env bndr new_rhs
-  = do  { (env, bndr') <- simplBinder env bndr
-        ; completeNonRecX env NotTopLevel NonRecursive
-                          (isStrictId bndr) bndr bndr' new_rhs }
-
-completeNonRecX :: SimplEnv
-                -> TopLevelFlag -> RecFlag -> Bool
+  | 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 NotTopLevel env' (isStrictId bndr) bndr bndr' new_rhs }
+               -- simplNonRecX is only used for NotTopLevel things
+
+completeNonRecX :: TopLevelFlag -> SimplEnv
+                -> Bool
                 -> InId                 -- Old binder
                 -> OutId                -- New binder
                 -> OutExpr              -- Simplified RHS
                 -> SimplM SimplEnv
 
-completeNonRecX env top_lvl is_rec 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 top_lvl is_rec is_strict rhs1 env1
+                if doFloatFromRhs NotTopLevel NonRecursive is_strict rhs1 env1
                 then do { tick LetFloatFromLet
                         ; return (addFloats env env1, rhs1) }   -- Add the floats to the main env
                 else return (env, wrapFloats env1 rhs1)         -- Wrap the floats around the RHS
@@ -427,37 +436,43 @@ 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]
-  | (ty1, ty2) <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
+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 env rhs
-  = do  { (is_val, env', rhs') <- go 0 env rhs
-        ; return (env', rhs') }
+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)
-    go n_val_args env other
+          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,18 +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 NotTopLevel NonRecursive
-                                 False var var expr
-        ; return (env, substExpr env (Var var)) }
+  = 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.
 
 %************************************************************************
 %*                                                                      *
@@ -551,62 +627,166 @@ 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
-
-  |  otherwise
-  = let
-        --      Arity info
-        new_bndr_info = idInfo new_bndr `setArityInfo` exprArity new_rhs
-
-        --      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`    worker_info
-
-        final_info | loop_breaker               = new_bndr_info
-                   | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
-                   | otherwise                  = info_w_unf
-
-        final_id = new_bndr `setIdInfo` final_info
+  = do { let old_info = idInfo old_bndr
+             old_unf  = unfoldingInfo old_info
+             occ_info = occInfo old_info
+
+       ; 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
+-- We still want the unfolding though.  Consider
+--     let 
+--           x = /\a. let y = ... in Just y
+--     in body
+-- Then we float the y-binding out (via abstractFloats and addPolyBind)
+-- but 'x' may well then be inlined in 'body' in which case we'd like the 
+-- opportunity to inline 'y' too.
+
+addPolyBind top_lvl env (NonRec poly_id rhs)
+  = 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 _) = 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           -- 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
-                -- These seqs forces the Id, and hence its IdInfo,
-                -- and hence any inner substitutions
-    final_id                                    `seq`
-    -- pprTrace "Binding" (ppr final_id <+> ppr unfolding) $
-    return (addNonRec env final_id new_rhs)
+    ASSERT( isId new_bndr )
+    WARN( new_arity < old_arity || new_arity < dmd_arity, 
+          (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
-    unfolding    = mkUnfolding (isTopLevel top_lvl) new_rhs
-    worker_info  = substWorker env (workerInfo old_info)
-    loop_breaker = isNonRuleLoopBreaker occ_info
-    old_info     = idInfo old_bndr
-    occ_info     = occInfo old_info
+    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}
 
+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 #-}
+       
+       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...
 
 
 %************************************************************************
@@ -655,14 +835,7 @@ might do the same again.
 
 \begin{code}
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
-simplExpr env expr = simplExprC env expr (mkBoringStop expr_ty')
-                   where
-                     expr_ty' = substTy env (exprType expr)
-        -- The type in the Stop continuation, expr_ty', is usually not used
-        -- It's only needed when discarding continuations after finding
-        -- a function that returns bottom.
-        -- Hence the lazy substitution
-
+simplExpr env expr = simplExprC env expr mkBoringStop
 
 simplExprC :: SimplEnv -> CoreExpr -> SimplCont -> SimplM CoreExpr
         -- Simplify an expression, given a continuation
@@ -682,7 +855,9 @@ simplExprF env e cont
   = -- pprTrace "simplExprF" (ppr e $$ ppr cont $$ ppr (seTvSubst env) $$ ppr (seIdSubst env) {- $$ ppr (seFloats env) -} ) $
     simplExprF' env e cont
 
-simplExprF' env (Var v)        cont = simplVar env v cont
+simplExprF' :: SimplEnv -> InExpr -> SimplCont
+            -> SimplM (SimplEnv, OutExpr)
+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
@@ -702,17 +877,17 @@ 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 case_ty alts) cont
+simplExprF' env (Case scrut bndr _ alts) cont
   | not (switchIsOn (getSwitchChecker env) NoCaseOfCase)
   =     -- Simplify the scrutinee with a Select continuation
     simplExprF env scrut (Select NoDup bndr alts env cont)
@@ -723,16 +898,15 @@ simplExprF' env (Case scrut bndr case_ty alts) cont
     do  { case_expr' <- simplExprC env scrut case_cont
         ; rebuild env case_expr' cont }
   where
-    case_cont = Select NoDup bndr alts env (mkBoringStop case_ty')
-    case_ty'  = substTy env case_ty     -- c.f. defn of simplExpr
+    case_cont = Select NoDup bndr alts env mkBoringStop
 
 simplExprF' env (Let (Rec pairs) body) cont
-  = do  { env <- simplRecBndrs env (map fst pairs)
+  = do  { env' <- simplRecBndrs env (map fst pairs)
                 -- NB: bndrs' don't have unfoldings or rules
                 -- We add them as we go down
 
-        ; env <- simplRecBind env NotTopLevel pairs
-        ; simplExprF env body cont }
+        ; env'' <- simplRecBind env' NotTopLevel pairs
+        ; simplExprF env'' body cont }
 
 simplExprF' env (Let (NonRec bndr rhs) body) cont
   = simplNonRecE env bndr (rhs, env) ([], body) cont
@@ -742,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}
 
 
@@ -758,13 +941,13 @@ simplType env ty
 rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM (SimplEnv, OutExpr)
 -- At this point the substitution in the SimplEnv should be irrelevant
 -- only the in-scope set and floats should matter
-rebuild env expr cont
-  = -- pprTrace "rebuild" (ppr expr $$ ppr cont $$ ppr (seFloats env)) $
-    case cont of
+rebuild env expr cont0
+  = -- pprTrace "rebuild" (ppr expr $$ ppr cont0 $$ ppr (seFloats env)) $
+    case cont0 of
       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 ty _ info cont -> rebuildCall env (fun `App` expr) (funResultTy ty) 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
@@ -781,21 +964,21 @@ rebuild env expr cont
 \begin{code}
 simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
           -> SimplM (SimplEnv, OutExpr)
-simplCast env body co cont
-  = do  { co' <- simplType env co
-        ; simplExprF env body (addCoerce co' cont) }
+simplCast env body co0 cont0
+  = do  { co1 <- simplCoercion env co0
+        ; simplExprF env body (addCoerce co1 cont0) }
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
 
-       add_coerce co (s1, k1) cont      -- co :: ty~ty
+       add_coerce _co (s1, k1) cont     -- co :: ty~ty
          | s1 `coreEqType` k1 = cont    -- is a no-op
 
-       add_coerce co1 (s1, k2) (CoerceIt co2 cont)
-         | (l1, t1) <- coercionKind co2
-                --      coerce T1 S1 (coerce S1 K1 e)
+       add_coerce co1 (s1, _k2) (CoerceIt co2 cont)
+         | (_l1, t1) <- coercionKind co2
+               --      e |> (g1 :: S1~L) |> (g2 :: L~T1)
                 -- ==>
-                --      e,                      if T1=K1
-                --      coerce T1 K1 e,         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
@@ -804,26 +987,31 @@ simplCast env body co cont
          , s1 `coreEqType` t1  = cont            -- The coerces cancel out
          | otherwise           = CoerceIt (mkTransCoercion co1 co2) cont
 
-       add_coerce co (s1s2, t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
-                -- (f `cast` g) ty  --->   (f ty) `cast` (g @ ty)
-                -- This implements the PushT rule from the paper
+       add_coerce co (s1s2, _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
+                -- (f |> g) ty  --->   (f ty) |> (g @ ty)
+                -- 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 arg_ty
+           ty' = substTy (arg_se `setInScope` env) arg_ty
+          new_arg_co = mkCsel1Coercion co  `mkTransCoercion`
+                              ty'           `mkTransCoercion`
+                        mkSymCoercion (mkCsel2Coercion co)
 
-        -- ToDo: the PushC rule is not implemented at all
-
-       add_coerce co (s1s2, t1t2) (ApplyTo dup arg arg_se cont)
+       add_coerce co (s1s2, _t1t2) (ApplyTo dup arg arg_se cont)
          | not (isTypeArg arg)  -- This implements the Push rule from the paper
          , isFunTy s1s2   -- t1t2 must be a function type, becuase it's applied
-                -- co : s1s2 :=: t1t2
-                --      (coerce (T1->T2) (S1->S2) F) E
+                --      (e |> (g :: s1s2 ~ t1->t2)) f
                 -- ===>
-                --      coerce T2 S2 (F (coerce S1 T1 E))
+                --      (e (f |> (arg g :: t1~s1))
+               --      |> (res g :: s2->t2)
                 --
-                -- t1t2 must be a function type, T1->T2, because it's applied
+                -- t1t2 must be a function type, t1->t2, because it's applied
                 -- to something but s1s2 might conceivably not be
                 --
                 -- When we build the ApplyTo we can't mix the out-types
@@ -832,14 +1020,14 @@ simplCast env body co cont
                 -- 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
+           -- 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 arg
+           arg'       = substExpr (text "move-cast") (arg_se `setInScope` env) arg
 
        add_coerce co _ cont = CoerceIt co cont
 \end{code}
@@ -857,30 +1045,23 @@ simplLam :: SimplEnv -> [InId] -> InExpr -> SimplCont
 
 simplLam env [] body cont = simplExprF env body cont
 
-        -- Type-beta reduction
-simplLam env (bndr:bndrs) body (ApplyTo _ (Type ty_arg) arg_se cont)
-  = ASSERT( isTyVar bndr )
-    do  { tick (BetaReduction bndr)
-        ; ty_arg' <- simplType (arg_se `setInScope` env) ty_arg
-        ; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
-
-        -- Ordinary beta reduction
+        -- Beta reduction
 simplLam env (bndr:bndrs) body (ApplyTo _ arg arg_se cont)
   = do  { tick (BetaReduction bndr)
         ; simplNonRecE env bndr (arg, arg_se) (bndrs, body) cont }
 
         -- Not enough args, so there are real lambdas left to put in the result
 simplLam env bndrs body cont
-  = do  { (env, bndrs') <- simplLamBndrs env bndrs
-        ; body' <- simplExpr env body
-        ; new_lam <- mkLam bndrs' body'
-        ; rebuild env new_lam cont }
+  = do  { (env', bndrs') <- simplLamBndrs env bndrs
+        ; body' <- simplExpr env' 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)
-             -> ([InId], InExpr)        -- Body of the let/lambda
+             -> ([InBndr], InExpr)      -- Body of the let/lambda
                                         --      \xs.e
              -> SimplCont
              -> SimplM (SimplEnv, OutExpr)
@@ -897,6 +1078,13 @@ simplNonRecE :: SimplEnv
 -- Why?  Because of the binder-occ-info-zapping done before
 --       the call to simplLam in simplExprF (Lam ...)
 
+       -- 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( isTyCoVar bndr )
+    do { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
+       ; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
+
 simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
   | preInlineUnconditionally env NotTopLevel bndr rhs
   = do  { tick (PreInlineUnconditionally bndr)
@@ -907,7 +1095,8 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
                      (StrictBind bndr bndrs body env cont) }
 
   | otherwise
-  = do  { (env1, bndr1) <- simplNonRecBndr env 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
         ; simplLam env3 bndrs body cont }
@@ -923,40 +1112,45 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
 \begin{code}
 -- Hack alert: we only distinguish subsumed cost centre stacks for the
 -- purposes of inlining.  All other CCCSs are mapped to currentCCS.
+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 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
@@ -970,94 +1164,52 @@ simplVar env var cont
 ---------------------------------------------------------
 --      Dealing with a call site
 
+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
-        ; rules <- getRules
-        ; let   in_scope   = getInScope env
-                maybe_rule = case activeRule dflags env of
-                                Nothing     -> Nothing  -- No rules apply
-                                Just act_fn -> lookupRule act_fn in_scope
-                                                          rules var args
-        ; 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) (idType 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 -> OutType       -- Function and its type
             -> ArgInfo
             -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
-rebuildCall env fun fun_ty (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.
@@ -1069,24 +1221,26 @@ rebuildCall env fun fun_ty (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!
-    cont_ty = contResultType cont
-    co      = mkUnsafeCoercion fun_ty cont_ty
-    mk_coerce expr | cont_ty `coreEqType` fun_ty = fun
-                   | otherwise = mkCoerce co fun
-
-rebuildCall env fun fun_ty info (ApplyTo _ (Type arg_ty) se cont)
-  = do  { ty' <- simplType (se `setInScope` env) arg_ty
-        ; rebuildCall env (fun `App` Type ty') (applyTy fun_ty ty') info cont }
-
-rebuildCall env fun fun_ty
-           (ArgInfo { ai_rules = has_rules, ai_strs = str:strs, ai_discs = disc:discs })
-           (ApplyTo _ arg arg_se cont)
-  | str || isStrictType arg_ty          -- Strict argument
+    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 info (ApplyTo _ (Type arg_ty) se cont)
+  = do  { ty' <- simplCoercion (se `setInScope` env) arg_ty
+        ; rebuildCall env (info `addArgTo` Type ty') 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 fun_ty cci arg_info' cont)
+               (StrictArg info' cci cont)
                 -- Note [Shadowing]
 
   | otherwise                           -- Lazy argument
@@ -1095,18 +1249,41 @@ rebuildCall env fun fun_ty
         -- have to be very careful about bogus strictness through
         -- floating a demanded let.
   = do  { arg' <- simplExprC (arg_se `setInScope` env) arg
-                             (mkLazyArgStop arg_ty cci)
-        ; rebuildCall env (fun `App` arg') res_ty arg_info' cont }
+                             (mkLazyArgStop cci)
+        ; rebuildCall env (addArgTo info' arg') cont }
   where
-    (arg_ty, res_ty) = splitFunTy fun_ty
-    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 fun_ty info 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
@@ -1131,224 +1308,68 @@ 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!
 
+
 %************************************************************************
 %*                                                                      *
-                Rebuilding a cse expression
+                Rewrite rules
 %*                                                                      *
 %************************************************************************
 
-Blob of helper functions for the "case-of-something-else" situation.
-
 \begin{code}
----------------------------------------------------------
---      Eliminate the case if possible
-
-rebuildCase :: 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
-
-
---------------------------------------------------
---      2. Eliminate the case if scrutinee is evaluated
---------------------------------------------------
-
-rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
-  -- See if we can get rid of the case altogether
-  -- See the extensive notes on case-elimination above
-  -- mkCase made sure that if all the alternatives are equal,
-  -- then there is now only one (DEFAULT) rhs
- | all isDeadBinder bndrs       -- bndrs are [InId]
-
-        -- Check that the scrutinee can be let-bound instead of case-bound
- , exprOkForSpeculation scrut
-                -- OK not to evaluate it
-                -- This includes things like (==# a# b#)::Bool
-                -- so that we simplify
-                --      case ==# a# b# of { True -> x; False -> x }
-                -- to just
-                --      x
-                -- This particular example shows up in default methods for
-                -- comparision operations (e.g. in (>=) for Int.Int32)
-        || exprIsHNF scrut                      -- It's already evaluated
-        || var_demanded_later scrut             -- It'll be demanded later
-
---      || not opt_SimplPedanticBottoms)        -- Or we don't care!
---      We used to allow improving termination by discarding cases, unless -fpedantic-bottoms was on,
---      but that breaks badly for the dataToTag# primop, which relies on a case to evaluate
---      its argument:  case x of { y -> dataToTag# y }
---      Here we must *not* discard the case, because dataToTag# just fetches the tag from
---      the info pointer.  So we'll be pedantic all the time, and see if that gives any
---      other problems
---      Also we don't want to discard 'seq's
-  = do  { tick (CaseElim case_bndr)
-        ; env <- simplNonRecX env case_bndr scrut
-        ; simplExprF env rhs cont }
+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
-        -- 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)
-                                 && not (isTickBoxOp v)
-                                    -- ugly hack; covering this case is what
-                                    -- exprOkForSpeculation was intended for.
-    var_demanded_later other   = False
-
-
---------------------------------------------------
---      3. Catch-all case
---------------------------------------------------
-
-rebuildCase 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
-
-        -- Simplify the alternatives
-        ; (scrut', case_bndr', alts') <- simplAlts env scrut case_bndr alts dup_cont
-        ; let res_ty' = contResultType dup_cont
-        ; case_expr <- mkCase scrut' case_bndr' res_ty' alts'
-
-        -- Notice that rebuildDone returns the in-scope set from env, not alt_env
-        -- The case binder *not* scope over the whole returned case-expression
-        ; rebuild env case_expr nodup_cont }
+    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}
 
-simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
-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]
-~~~~~~~~~~~~~~~~~~~~~~
-There is a time we *don't* want to do that, namely when
--fno-case-of-case is on.  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.
-
-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.
-
-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:
-        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.
-The point is that we bring into the envt a binding
-        let x = (a,b)
-after the outer case, and that makes (a,b) alive.  At least we do unless
-the case binder is guaranteed dead.
-
-Note [Case of cast]
-~~~~~~~~~~~~~~~~~~~
-Consider        case (v `cast` co) of x { I# ->
-                ... (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
-        v |-> x `cast` (sym co)
-to v.  Then we should inline v at the inner case, cancel the casts, and away we go
-
-Note [Improving seq]
-~~~~~~~~~~~~~~~~~~~
-Consider
-        type family F :: * -> *
-        type instance F Int = Int
-
-        ... case e of x { DEFAULT -> rhs } ...
-
-where x::F Int.  Then we'd like to rewrite (F Int) to Int, getting
-
-        case e `cast` co of x'::Int
-           I# x# -> let x = x' `cast` sym co
-                    in rhs
+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
 
-so that 'rhs' can take advantage of the form of x'.  Notice that Note
-[Case of cast] may then apply to the result.
+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
 
-This showed up in Roman's experiments.  Example:
-  foo :: F Int -> Int -> Int
-  foo t n = t `seq` bar n
-     where
-       bar 0 = 0
-       bar n = bar (n - case t of TI i -> i)
-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.)
+%************************************************************************
+%*                                                                      *
+                Rebuilding a cse expression
+%*                                                                      *
+%************************************************************************
 
 Note [Case elimination]
 ~~~~~~~~~~~~~~~~~~~~~~~
@@ -1436,123 +1457,265 @@ 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 env scrut case_bndr alts
-  = do  { (env1, case_bndr1) <- simplBinder env case_bndr
+---------------------------------------------------------
+--      Eliminate the case if possible
 
-        ; fam_envs <- getFamEnvs
-        ; (env2, scrut2, case_bndr2) <- improve_seq fam_envs env1 scrut
-                                                case_bndr case_bndr1 alts
-                        -- Note [Improving seq]
+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
+--------------------------------------------------
 
-        ; let (env3, case_bndr3) = improve_case_bndr env2 scrut2 case_bndr2
-                        -- Note [Case of cast]
+rebuildCase env scrut case_bndr alts cont
+  | Lit lit <- scrut    -- No need for same treatment as constructors
+                        -- because literals are inlined more vigorously
+  = 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 }
 
-        ; return (env3, scrut2, case_bndr3) }
+  | 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 }
 
-    improve_seq fam_envs env1 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 env1 case_bndr rhs
-              ; return (env2, scrut `Cast` co, case_bndr2) }
 
-    improve_seq fam_envs env1 scrut case_bndr case_bndr1 alts
-        = return (env1, scrut, case_bndr1)
+--------------------------------------------------
+--      2. Eliminate the case if scrutinee is evaluated
+--------------------------------------------------
 
+rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
+  -- See if we can get rid of the case altogether
+  -- 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]
 
-    improve_case_bndr env scrut case_bndr
-        | switchIsOn (getSwitchChecker env) NoCaseOfCase
-                -- See Note [no-case-of-case]
-        = (env, case_bndr)
+        -- Check that the scrutinee can be let-bound instead of case-bound
+ , exprOkForSpeculation scrut
+                -- OK not to evaluate it
+                -- This includes things like (==# a# b#)::Bool
+                -- so that we simplify
+                --      case ==# a# b# of { True -> x; False -> x }
+                -- to just
+                --      x
+                -- This particular example shows up in default methods for
+                -- comparision operations (e.g. in (>=) for Int.Int32)
+        || exprIsHNF scrut                      -- It's already evaluated
+        || var_demanded_later scrut             -- It'll be demanded later
+
+--      || not opt_SimplPedanticBottoms)        -- Or we don't care!
+--      We used to allow improving termination by discarding cases, unless -fpedantic-bottoms was on,
+--      but that breaks badly for the dataToTag# primop, which relies on a case to evaluate
+--      its argument:  case x of { y -> dataToTag# y }
+--      Here we must *not* discard the case, because dataToTag# just fetches the tag from
+--      the info pointer.  So we'll be pedantic all the time, and see if that gives any
+--      other problems
+--      Also we don't want to discard 'seq's
+  = do  { tick (CaseElim case_bndr)
+        ; env' <- simplNonRecX env case_bndr scrut
+        ; simplExprF env' 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 (idDemandInfo case_bndr)
+                                 && not (isTickBoxOp v)
+                                    -- ugly hack; covering this case is what
+                                    -- exprOkForSpeculation was intended for.
+    var_demanded_later _       = False
 
-        | 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.
+--------------------------------------------------
+--      3. Try seq rules; see Note [User-defined RULES for seq] in MkId
+--------------------------------------------------
 
-            Cast (Var v) co -> (addBinderUnfolding env1 v rhs, case_bndr')
-                            where
-                                rhs = Cast (Var case_bndr') (mkSymCoercion co)
+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 }
 
-            other -> (env, case_bndr)
-        where
-          case_bndr' = zapOccInfo case_bndr
-          env1       = modifyInScope env case_bndr case_bndr'
+rebuildCase env scrut case_bndr alts cont
+  = reallyRebuildCase env scrut case_bndr alts cont
 
+--------------------------------------------------
+--      3. Catch-all case
+--------------------------------------------------
+
+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
 
-zapOccInfo :: InId -> InId      -- See Note [zapOccInfo]
-zapOccInfo b = b `setIdOccInfo` NoOccInfo
+        -- Simplify the alternatives
+        ; (scrut', case_bndr', alts') <- simplAlts env' scrut case_bndr alts dup_cont
+
+       -- Check for empty alternatives
+       ; if null alts' then missingAlt env case_bndr alts cont
+         else do
+        { dflags <- getDOptsSmpl
+        ; case_expr <- mkCase dflags scrut' case_bndr' alts'
+
+       -- 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}
 
+simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
+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.
 
-simplAlts does two things:
+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].
 
-1.  Eliminate alternatives that cannot match, including the
-    DEFAULT alternative.
+Note [zapOccInfo]
+~~~~~~~~~~~~~~~~~
+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.
+The point is that we bring into the envt a binding
+        let x = (a,b)
+after the outer case, and that makes (a,b) alive.  At least we do unless
+the case binder is guaranteed dead.
 
-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.
+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.
 
-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.
+Note [Case of cast]
+~~~~~~~~~~~~~~~~~~~
+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
+        v |-> x `cast` (sym co)
+to v.  Then we should inline v at the inner case, cancel the casts, and away we go
 
-Eliminating the default alternative in (1) isn't so obvious, but it can
-happen:
+Note [Improving seq]
+~~~~~~~~~~~~~~~~~~~
+Consider
+        type family F :: * -> *
+        type instance F Int = Int
 
-data Colour = Red | Green | Blue
+        ... case e of x { DEFAULT -> rhs } ...
 
-f x = case x of
-        Red -> ..
-        Green -> ..
-        DEFAULT -> h x
+where x::F Int.  Then we'd like to rewrite (F Int) to Int, getting
 
-h y = case y of
-        Blue -> ..
-        DEFAULT -> [ case y of ... ]
+        case e `cast` co of x'::Int
+           I# x# -> let x = x' `cast` sym co
+                    in rhs
 
-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!
+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
+       bar 0 = 0
+       bar n = bar (n - case t of TI i -> i)
+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.)
 
 \begin{code}
 simplAlts :: SimplEnv
           -> OutExpr
           -> InId                       -- Case binder
-          -> [InAlt] -> SimplCont
+          -> [InAlt]                   -- Non-empty
+         -> 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
 
-        ; alts' <- mapM (simplAlt alt_env imposs_deflt_cons case_bndr' cont') in_alts
+        ; 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
@@ -1569,26 +1732,27 @@ simplAlt env imposs_deflt_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
         ; rhs' <- simplExprC env' rhs cont'
         ; return (DEFAULT, [], rhs') }
 
-simplAlt env imposs_deflt_cons case_bndr' cont' (LitAlt lit, bndrs, rhs)
+simplAlt env _ case_bndr' cont' (LitAlt lit, bndrs, rhs)
   = ASSERT( null bndrs )
     do  { let env' = addBinderUnfolding env case_bndr' (Lit lit)
         ; rhs' <- simplExprC env' rhs cont'
         ; return (LitAlt lit, [], rhs') }
 
-simplAlt env imposs_deflt_cons case_bndr' cont' (DataAlt con, vs, rhs)
+simplAlt env _ case_bndr' cont' (DataAlt con, vs, rhs)
   = do  {       -- Deal with the pattern-bound variables
                 -- Mark the ones that are in ! positions in the
                 -- data constructor as certainly-evaluated.
                 -- NB: simplLamBinders preserves this eval info
-          let vs_with_evals = add_evals vs (dataConRepStrictness con)
-        ; (env, vs') <- simplLamBndrs env vs_with_evals
+          let vs_with_evals = add_evals (dataConRepStrictness con)
+        ; (env', vs') <- simplLamBndrs env vs_with_evals
 
                 -- Bind the case-binder to (con args)
         ; let inst_tys' = tyConAppArgs (idType case_bndr')
               con_args  = map Type inst_tys' ++ varsToCoreExprs vs'
-              env'      = addBinderUnfolding env case_bndr' (mkConApp con con_args)
+              env''     = addBinderUnfolding env' case_bndr'
+                                             (mkConApp con con_args)
 
-        ; rhs' <- simplExprC env' rhs cont'
+        ; rhs' <- simplExprC env'' rhs cont'
         ; return (DataAlt con, vs', rhs') }
   where
         -- add_evals records the evaluated-ness of the bound variables of
@@ -1600,19 +1764,20 @@ simplAlt env imposs_deflt_cons case_bndr' cont' (DataAlt con, vs, rhs)
         -- We really must record that b is already evaluated so that we don't
         -- go and re-evaluate it when constructing the result.
         -- See Note [Data-con worker strictness] in MkId.lhs
-    add_evals vs strs
-        = go vs strs
+    add_evals the_strs
+        = go vs the_strs
         where
           go [] [] = []
-          go (v:vs) strs | isTyVar v = v : go vs strs
-          go (v:vs) (str:strs)
-            | isMarkedStrict str = evald_v  : go vs strs
-            | otherwise          = zapped_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
             where
               zapped_v = zap_occ_info v
               evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
-          go _ _ = pprPanic "cat_evals" (ppr con $$ ppr vs $$ ppr strs)
+          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
@@ -1620,16 +1785,23 @@ simplAlt env imposs_deflt_cons 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' = \id -> id
-                 | 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}
 
 
@@ -1653,70 +1825,72 @@ and then
 All this should happen in one sweep.
 
 \begin{code}
-knownCon :: SimplEnv -> OutExpr -> AltCon -> [OutExpr]
-         -> 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 env scrut args 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 args bndr (LitAlt lit, bs, rhs) cont
-  = ASSERT( null bs )
-    do  { env <- simplNonRecX env bndr scrut
-        ; simplExprF env rhs cont }
-
-knownAlt env scrut 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 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 v -> scrut
-                                other -> con_app
-                con_app = mkConApp dc (take n_drop_tys 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 dead_bndr [] _  = 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
-                    -- 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 _ _ _ _ =
-      pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr args $$
+        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'' bs' 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}
 
 
@@ -1735,8 +1909,8 @@ prepareCaseCont :: SimplEnv
                         -- continunation)
 
         -- No need to make it duplicatable if there's only one alternative
-prepareCaseCont env [alt] cont = return (env, cont, mkBoringStop (contResultType cont))
-prepareCaseCont env alts  cont = mkDupableCont env cont
+prepareCaseCont env [_] cont = return (env, cont, mkBoringStop)
+prepareCaseCont env _   cont = mkDupableCont env cont
 \end{code}
 
 \begin{code}
@@ -1745,41 +1919,43 @@ mkDupableCont :: SimplEnv -> SimplCont
 
 mkDupableCont env cont
   | contIsDupable cont
-  = return (env, cont, mkBoringStop (contResultType cont))
+  = return (env, cont, mkBoringStop)
 
-mkDupableCont env (Stop {}) = panic "mkDupableCont"     -- Handled by previous eqn
+mkDupableCont _   (Stop {}) = panic "mkDupableCont"     -- Handled by previous eqn
 
 mkDupableCont env (CoerceIt ty cont)
-  = do  { (env, dup, nodup) <- mkDupableCont env cont
-        ; return (env, CoerceIt ty dup, nodup) }
+  = do  { (env', dup, nodup) <- mkDupableCont env cont
+        ; return (env', CoerceIt ty dup, nodup) }
 
-mkDupableCont env cont@(StrictBind bndr _ _ se _)
-  =  return (env, mkBoringStop (substTy se (idType bndr)), cont)
-        -- See Note [Duplicating strict continuations]
+mkDupableCont env cont@(StrictBind {})
+  =  return (env, mkBoringStop, cont)
+        -- See Note [Duplicating StrictBind]
 
-mkDupableCont env cont@(StrictArg _ fun_ty _ _ _)
-  =  return (env, mkBoringStop (funArgTy fun_ty), 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...)
         --      ==>
         --              let a = ...arg...
         --              in [...hole...] a
-    do  { (env, dup_cont, nodup_cont) <- mkDupableCont env cont
-        ; arg <- simplExpr (se `setInScope` env) arg
-        ; (env, arg) <- makeTrivial env arg
-        ; let app_cont = ApplyTo OkToDup arg (zapSubstEnv env) dup_cont
-        ; return (env, app_cont, nodup_cont) }
+    do  { (env', dup_cont, nodup_cont) <- mkDupableCont env cont
+        ; arg' <- simplExpr (se `setInScope` env') arg
+        ; (env'', arg'') <- makeTrivial NotTopLevel env' arg'
+        ; let app_cont = ApplyTo OkToDup arg'' (zapSubstEnv env'') dup_cont
+        ; return (env'', app_cont, nodup_cont) }
 
-mkDupableCont env cont@(Select _ case_bndr [(_,bs,rhs)] se case_cont)
+mkDupableCont env cont@(Select _ case_bndr [(_, bs, _rhs)] _ _)
 --  See Note [Single-alternative case]
 --  | not (exprIsDupable rhs && contIsDupable case_cont)
 --  | not (isDeadBinder case_bndr)
-  | all isDeadBinder bs         -- InIds
-  = return (env, mkBoringStop scrut_ty, cont)
-  where
-    scrut_ty = substTy se (idType case_bndr)
+  | all isDeadBinder bs  -- InIds
+    && not (isUnLiftedType (idType case_bndr))
+    -- Note [Single-alternative-unlifted]
+  = return (env, mkBoringStop, cont)
 
 mkDupableCont env (Select _ case_bndr alts se cont)
   =     -- e.g.         (case [...hole...] of { pi -> ei })
@@ -1787,14 +1963,14 @@ mkDupableCont env (Select _ case_bndr alts se cont)
         --              let ji = \xij -> ei
         --              in case [...hole...] of { pi -> ji xij }
     do  { tick (CaseOfCase case_bndr)
-        ; (env, dup_cont, nodup_cont) <- mkDupableCont env cont
+        ; (env', dup_cont, nodup_cont) <- mkDupableCont env cont
                 -- NB: call mkDupableCont here, *not* prepareCaseCont
                 -- We must make a duplicable continuation, whereas prepareCaseCont
                 -- doesn't when there is a single case branch
 
-        ; let alt_env = se `setInScope` env
-        ; (alt_env, case_bndr') <- simplBinder alt_env case_bndr
-        ; alts' <- mapM (simplAlt alt_env [] case_bndr' dup_cont) alts
+        ; let alt_env = se `setInScope` env'
+        ; (alt_env', case_bndr') <- simplBinder alt_env case_bndr
+        ; alts' <- mapM (simplAlt alt_env' [] case_bndr' dup_cont) alts
         -- Safe to say that there are no handled-cons for the DEFAULT case
                 -- NB: simplBinder does not zap deadness occ-info, so
                 -- a dead case_bndr' will still advertise its deadness
@@ -1807,10 +1983,9 @@ mkDupableCont env (Select _ case_bndr alts se cont)
         -- NB: we don't use alt_env further; it has the substEnv for
         --     the alternatives, and we don't want that
 
-        ; (env, alts') <- mkDupableAlts env case_bndr' alts'
-        ; return (env,  -- Note [Duplicated env]
-                  Select OkToDup case_bndr' alts' (zapSubstEnv env)
-                         (mkBoringStop (contResultType dup_cont)),
+        ; (env'', alts'') <- mkDupableAlts env' case_bndr' alts'
+        ; return (env'',  -- Note [Duplicated env]
+                  Select OkToDup case_bndr' alts'' (zapSubstEnv env'') mkBoringStop,
                   nodup_cont) }
 
 
@@ -1818,33 +1993,54 @@ mkDupableAlts :: SimplEnv -> OutId -> [InAlt]
               -> SimplM (SimplEnv, [InAlt])
 -- Absorbs the continuation into the new alternatives
 
-mkDupableAlts env case_bndr' alts
-  = go env alts
+mkDupableAlts env case_bndr' the_alts
+  = go env the_alts
   where
-    go env [] = return (env, [])
-    go env (alt:alts)
-        = do { (env, alt') <- mkDupableAlt env case_bndr' alt
-     ; (env, alts') <- go env alts
-             ; return (env, alt' : alts' ) }
-
-mkDupableAlt env case_bndr' (con, bndrs', rhs')
+    go env0 [] = return (env0, [])
+    go env0 (alt:alts)
+        = do { (env1, alt') <- mkDupableAlt env0 case_bndr' alt
+             ; (env2, alts') <- go env1 alts
+             ; return (env2, alt' : alts' ) }
+
+mkDupableAlt :: SimplEnv -> OutId -> (AltCon, [CoreBndr], CoreExpr)
+              -> SimplM (SimplEnv, (AltCon, [CoreBndr], CoreExpr))
+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
 
         ; (final_bndrs', final_args)    -- Note [Join point abstraction]
                 <- if (any isId used_bndrs')
                    then return (used_bndrs', varsToCoreExprs used_bndrs')
-                    else do { rw_id <- newId FSLIT("w") realWorldStatePrimTy
+                    else do { rw_id <- newId (fsLit "w") realWorldStatePrimTy
                             ; return ([rw_id], [Var realWorldPrimId]) }
 
-        ; join_bndr <- newId FSLIT("$j") (mkPiTypes final_bndrs' rhs_ty')
+        ; join_bndr <- newId (fsLit "$j") (mkPiTypes final_bndrs' rhs_ty')
                 -- Note [Funky mkPiTypes]
 
         ; let   -- We make the lambdas into one-shot-lambdas.  The
@@ -1857,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 (addNonRec env 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
@@ -1870,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
@@ -1939,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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2026,3 +2303,37 @@ Other choices:
      When x is inlined into its full context, we find that it was a bad
      idea to have pushed the outer case inside the (...) case.
 
+Note [Single-alternative-unlifted]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here's another single-alternative where we really want to do case-of-case:
+
+data Mk1 = Mk1 Int#
+data Mk1 = Mk2 Int#
+
+M1.f =
+    \r [x_s74 y_s6X]
+        case
+            case y_s6X of tpl_s7m {
+              M1.Mk1 ipv_s70 -> ipv_s70;
+              M1.Mk2 ipv_s72 -> ipv_s72;
+            }
+        of
+        wild_s7c
+        { __DEFAULT ->
+              case
+                  case x_s74 of tpl_s7n {
+                    M1.Mk1 ipv_s77 -> ipv_s77;
+                    M1.Mk2 ipv_s79 -> ipv_s79;
+                  }
+              of
+              wild1_s7b
+              { __DEFAULT -> ==# [wild1_s7b wild_s7c];
+              };
+        };
+
+So the outer case is doing *nothing at all*, other than serving as a
+join-point.  In this case we really want to do case-of-case and decide
+whether to use a real join point or just duplicate the continuation.
+
+Hence: check whether the case binder's type is unlifted, because then
+the outer case is *not* a seq.