UNDO: Add -fpass-case-bndr-to-join-points
[ghc-hetmet.git] / compiler / simplCore / Simplify.lhs
index aaeec2e..eba2728 100644 (file)
@@ -4,13 +4,6 @@
 \section[Simplify]{The main module of the simplifier}
 
 \begin{code}
 \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"
 module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
@@ -20,6 +13,8 @@ import SimplMonad
 import Type hiding      ( substTy, extendTvSubst )
 import SimplEnv
 import SimplUtils
 import Type hiding      ( substTy, extendTvSubst )
 import SimplEnv
 import SimplUtils
+import MkId            ( rUNTIME_ERROR_ID )
+import FamInstEnv      ( FamInstEnv )
 import Id
 import Var
 import IdInfo
 import Id
 import Var
 import IdInfo
@@ -27,11 +22,11 @@ import Coercion
 import FamInstEnv       ( topNormaliseType )
 import DataCon          ( dataConRepStrictness, dataConUnivTyVars )
 import CoreSyn
 import FamInstEnv       ( topNormaliseType )
 import DataCon          ( dataConRepStrictness, dataConUnivTyVars )
 import CoreSyn
-import NewDemand        ( isStrictDmd )
+import NewDemand        ( isStrictDmd, splitStrictSig )
 import PprCore          ( pprParendExpr, pprCoreExpr )
 import CoreUnfold       ( mkUnfolding, callSiteInline, CallCtxt(..) )
 import CoreUtils
 import PprCore          ( pprParendExpr, pprCoreExpr )
 import CoreUnfold       ( mkUnfolding, callSiteInline, CallCtxt(..) )
 import CoreUtils
-import Rules            ( lookupRule )
+import Rules            ( lookupRule, getRules )
 import BasicTypes       ( isMarkedStrict )
 import CostCentre       ( currentCCS )
 import TysPrim          ( realWorldStatePrimTy )
 import BasicTypes       ( isMarkedStrict )
 import CostCentre       ( currentCCS )
 import TysPrim          ( realWorldStatePrimTy )
@@ -41,7 +36,7 @@ import BasicTypes       ( TopLevelFlag(..), isTopLevel,
 import Maybes           ( orElse )
 import Data.List        ( mapAccumL )
 import Outputable
 import Maybes           ( orElse )
 import Data.List        ( mapAccumL )
 import Outputable
-import Util
+import FastString
 \end{code}
 
 
 \end{code}
 
 
@@ -207,18 +202,18 @@ expansion at a let RHS can concentrate solely on the PAP case.
 \begin{code}
 simplTopBinds :: SimplEnv -> [InBind] -> SimplM [OutBind]
 
 \begin{code}
 simplTopBinds :: SimplEnv -> [InBind] -> SimplM [OutBind]
 
-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.
   = 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
         ; 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
+        ; env2 <- simpl_binds dump_flag env1 binds0
         ; freeTick SimplifierDone
         ; freeTick SimplifierDone
-        ; return (getFloats env') }
+        ; return (getFloats env2) }
   where
         -- We need to track the zapped top-level binders, because
         -- they should have their fragile IdInfo zapped (notably occurrence info)
   where
         -- We need to track the zapped top-level binders, because
         -- they should have their fragile IdInfo zapped (notably occurrence info)
@@ -227,13 +222,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
         -- 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 }
 
                                                      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
 
     simpl_bind env (Rec pairs)  = simplRecBind      env  TopLevel pairs
     simpl_bind env (NonRec b r) = simplRecOrTopPair env' TopLevel b b' r
@@ -255,12 +250,12 @@ simplRecBind is used for
 simplRecBind :: SimplEnv -> TopLevelFlag
              -> [(InId, InExpr)]
              -> SimplM SimplEnv
 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
   where
     add_rules :: SimplEnv -> (InBndr,InExpr) -> (SimplEnv, (InBndr, OutBndr, InExpr))
         -- Add the (substituted) rules to the binder
@@ -271,8 +266,8 @@ simplRecBind env top_lvl pairs
     go env [] = return env
 
     go env ((old_bndr, new_bndr, rhs) : 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
 \end{code}
 
 simplOrTopPair is used for
@@ -322,15 +317,21 @@ simplLazyBind :: SimplEnv
 
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
   = do  { let   rhs_env     = rhs_se `setInScope` env
 
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
   = do  { let   rhs_env     = rhs_se `setInScope` env
-                (tvs, body) = collectTyBinders rhs
+               (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
+
         ; (body_env, tvs') <- simplBinders rhs_env tvs
         ; (body_env, tvs') <- simplBinders rhs_env tvs
-                -- See Note [Floating and type abstraction]
-                -- in SimplUtils
+                -- See Note [Floating and type abstraction] in SimplUtils
 
 
-        -- 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
+        -- Simplify the RHS
+        ; (body_env1, body1) <- simplExprF body_env body mkBoringStop
 
         -- ANF-ise a constructor or PAP rhs
         ; (body_env2, body2) <- prepareRhs body_env1 body1
 
         -- ANF-ise a constructor or PAP rhs
         ; (body_env2, body2) <- prepareRhs body_env1 body1
@@ -349,7 +350,8 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                      do { tick LetFloatFromLet
                         ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
                         ; rhs' <- mkLam tvs' body3
                      do { tick LetFloatFromLet
                         ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
                         ; rhs' <- mkLam tvs' body3
-                        ; return (extendFloats env poly_binds, rhs') }
+                        ; let env' = foldl (addPolyBind top_lvl) env poly_binds
+                        ; return (env', rhs') }
 
         ; completeBind env' top_lvl bndr bndr1 rhs' }
 \end{code}
 
         ; completeBind env' top_lvl bndr bndr1 rhs' }
 \end{code}
@@ -364,21 +366,23 @@ simplNonRecX :: SimplEnv
              -> SimplM SimplEnv
 
 simplNonRecX env bndr new_rhs
              -> SimplM SimplEnv
 
 simplNonRecX env bndr new_rhs
-  = do  { (env, bndr') <- simplBinder env bndr
-        ; completeNonRecX env NotTopLevel NonRecursive
-                          (isStrictId bndr) bndr bndr' new_rhs }
+  | isDeadBinder bndr  -- Not uncommon; e.g. case (a,b) of b { (p,q) -> p }
+  = return env         --               Here b is dead, and we avoid creating
+  | otherwise          --               the binding b = (a,b)
+  = do  { (env', bndr') <- simplBinder env bndr
+        ; completeNonRecX env' (isStrictId bndr) bndr bndr' new_rhs }
 
 completeNonRecX :: SimplEnv
 
 completeNonRecX :: SimplEnv
-                -> TopLevelFlag -> RecFlag -> Bool
+                -> Bool
                 -> InId                 -- Old binder
                 -> OutId                -- New binder
                 -> OutExpr              -- Simplified RHS
                 -> SimplM SimplEnv
 
                 -> 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
+completeNonRecX env is_strict old_bndr new_bndr new_rhs
   = do  { (env1, rhs1) <- prepareRhs (zapFloats env) new_rhs
         ; (env2, rhs2) <-
   = do  { (env1, rhs1) <- prepareRhs (zapFloats env) 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
                 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
@@ -430,14 +434,14 @@ That's what the 'go' loop in prepareRhs does
 prepareRhs :: SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
 -- Adds new floats to the env iff that allows us to return a good RHS
 prepareRhs env (Cast rhs co)    -- Note [Float coercions]
 prepareRhs :: SimplEnv -> 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
+  | (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
         ; return (env', Cast rhs' co) }
 
   , not (isUnLiftedType ty1)            -- see Note [Float coercions (unlifted)]
   = do  { (env', rhs') <- makeTrivial env rhs
         ; return (env', Cast rhs' co) }
 
-prepareRhs env rhs
-  = do  { (is_val, env', rhs') <- go 0 env rhs
-        ; return (env', rhs') }
+prepareRhs env0 rhs0
+  = do  { (_is_val, 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
   where
     go n_val_args env (Cast rhs co)
         = do { (is_val, env', rhs') <- go n_val_args env rhs
@@ -457,7 +461,7 @@ prepareRhs env rhs
           is_val = n_val_args > 0       -- There is at least one arg
                                         -- ...and the fun a constructor or PAP
                  && (isDataConWorkId fun || n_val_args < idArity fun)
           is_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
+    go _ env other
         = return (False, env, other)
 \end{code}
 
         = return (False, env, other)
 \end{code}
 
@@ -508,10 +512,20 @@ makeTrivial env expr
   | exprIsTrivial expr
   = return (env, expr)
   | otherwise           -- See Note [Take care] below
   | exprIsTrivial expr
   = 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  { var <- newId (fsLit "a") (exprType expr)
+        ; env' <- completeNonRecX env False var var expr
+--       pprTrace "makeTrivial" (vcat [ppr var <+> ppr (exprArity (substExpr env' (Var var)))
+--                                    , ppr expr
+--                                    , ppr (substExpr env' (Var var))
+--                                    , ppr (idArity (fromJust (lookupInScope (seInScope env') var))) ]) $
+       ; return (env', substExpr env' (Var var)) }
+       -- The substitution is needed becase we're constructing a new binding
+       --     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
 \end{code}
 
 
 \end{code}
 
 
@@ -559,10 +573,67 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
         -- Use the substitution to make quite, quite sure that the
         -- substitution will happen, since we are going to discard the binding
 
         -- Use the substitution to make quite, quite sure that the
         -- substitution will happen, since we are going to discard the binding
 
-  |  otherwise
-  = let
+  | otherwise
+  = return (addNonRecWithUnf env new_bndr new_rhs unfolding wkr)
+  where
+    unfolding | omit_unfolding = NoUnfolding
+             | otherwise      = mkUnfolding  (isTopLevel top_lvl) new_rhs
+    old_info    = idInfo old_bndr
+    occ_info    = occInfo old_info
+    wkr                = substWorker env (workerInfo old_info)
+    omit_unfolding = isNonRuleLoopBreaker occ_info 
+                  --       or not (activeInline env old_bndr)
+                  -- Do *not* trim the unfolding in SimplGently, else
+                  -- the specialiser can't see it!
+
+-----------------
+addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplEnv
+-- 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)
+  = addNonRecWithUnf env poly_id rhs unfolding NoWorker
+  where
+    unfolding | not (activeInline env poly_id) = NoUnfolding
+             | otherwise                      = mkUnfolding (isTopLevel top_lvl) rhs
+               -- addNonRecWithInfo adds the new binding in the
+               -- proper way (ie complete with unfolding etc),
+               -- and extends the in-scope set
+
+addPolyBind _ env bind@(Rec _) = extendFloats env bind
+               -- Hack: letrecs are more awkward, so we extend "by steam"
+               -- without adding unfoldings etc.  At worst this leads to
+               -- more simplifier iterations
+
+-----------------
+addNonRecWithUnf :: SimplEnv
+                 -> OutId -> OutExpr        -- New binder and RHS
+                 -> Unfolding -> WorkerInfo -- and unfolding
+                 -> SimplEnv
+-- Add suitable IdInfo to the Id, add the binding to the floats, and extend the in-scope set
+addNonRecWithUnf env new_bndr rhs unfolding wkr
+  = ASSERT( isId new_bndr )
+    WARN( new_arity < old_arity || new_arity < dmd_arity, 
+          (ppr final_id <+> ppr old_arity <+> ppr new_arity <+> ppr dmd_arity) $$ ppr rhs )
+    final_id `seq`      -- This seq forces the Id, and hence its IdInfo,
+                       -- and hence any inner substitutions
+    addNonRec env final_id rhs
+       -- The addNonRec adds it to the in-scope set too
+  where
+       dmd_arity = length $ fst $ splitStrictSig $ idNewStrictness new_bndr
+       old_arity = idArity new_bndr
+
         --      Arity info
         --      Arity info
-        new_bndr_info = idInfo new_bndr `setArityInfo` exprArity new_rhs
+       new_arity = exprArity rhs
+        new_bndr_info = idInfo new_bndr `setArityInfo` new_arity
 
         --      Unfolding info
         -- Add the unfolding *only* for non-loop-breakers
 
         --      Unfolding info
         -- Add the unfolding *only* for non-loop-breakers
@@ -586,25 +657,12 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
         -- (for example) be no longer strictly demanded.
         -- The solution here is a bit ad hoc...
         info_w_unf = new_bndr_info `setUnfoldingInfo` unfolding
         -- (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
+                                  `setWorkerInfo`    wkr
 
 
-        final_info | loop_breaker               = new_bndr_info
-                   | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
+        final_info | isEvaldUnfolding unfolding = zapDemandInfo info_w_unf `orElse` info_w_unf
                    | otherwise                  = info_w_unf
                    | otherwise                  = info_w_unf
-
+       
         final_id = new_bndr `setIdInfo` final_info
         final_id = new_bndr `setIdInfo` final_info
-    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)
-  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
 \end{code}
 
 
 \end{code}
 
 
@@ -655,14 +713,7 @@ might do the same again.
 
 \begin{code}
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
 
 \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
 
 simplExprC :: SimplEnv -> CoreExpr -> SimplCont -> SimplM CoreExpr
         -- Simplify an expression, given a continuation
@@ -682,6 +733,8 @@ simplExprF env e cont
   = -- pprTrace "simplExprF" (ppr e $$ ppr cont $$ ppr (seTvSubst env) $$ ppr (seIdSubst env) {- $$ ppr (seFloats env) -} ) $
     simplExprF' env e cont
 
   = -- pprTrace "simplExprF" (ppr e $$ ppr cont $$ ppr (seTvSubst env) $$ ppr (seIdSubst env) {- $$ ppr (seFloats env) -} ) $
     simplExprF' env e cont
 
+simplExprF' :: SimplEnv -> InExpr -> SimplCont
+            -> SimplM (SimplEnv, OutExpr)
 simplExprF' env (Var v)        cont = simplVar 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 (Var v)        cont = simplVar env v cont
 simplExprF' env (Lit lit)      cont = rebuild env (Lit lit) cont
 simplExprF' env (Note n expr)  cont = simplNote env n expr cont
@@ -712,7 +765,7 @@ simplExprF' env (Type ty) cont
     do  { ty' <- simplType env ty
         ; rebuild env (Type ty') cont }
 
     do  { ty' <- simplType 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)
   | not (switchIsOn (getSwitchChecker env) NoCaseOfCase)
   =     -- Simplify the scrutinee with a Select continuation
     simplExprF env scrut (Select NoDup bndr alts env cont)
@@ -723,16 +776,15 @@ simplExprF' env (Case scrut bndr case_ty alts) cont
     do  { case_expr' <- simplExprC env scrut case_cont
         ; rebuild env case_expr' cont }
   where
     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
 
 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
 
                 -- 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
 
 simplExprF' env (Let (NonRec bndr rhs) body) cont
   = simplNonRecE env bndr (rhs, env) ([], body) cont
@@ -758,13 +810,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 :: 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
       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 fun _ info cont    -> rebuildCall env (fun `App` expr) info 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
       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 +833,21 @@ rebuild env expr cont
 \begin{code}
 simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
           -> SimplM (SimplEnv, OutExpr)
 \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 <- simplType env co0
+        ; simplExprF env body (addCoerce co1 cont0) }
   where
        addCoerce co cont = add_coerce co (coercionKind co) cont
 
   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
 
          | 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 T1=T2
+                --      e |> (g1 . g2 :: T1~T2)  otherwise
                 --
                 -- For example, in the initial form of a worker
                 -- we may find  (coerce T (coerce S (\x.e))) y
                 --
                 -- For example, in the initial form of a worker
                 -- we may find  (coerce T (coerce S (\x.e))) y
@@ -804,26 +856,26 @@ simplCast env body co cont
          , s1 `coreEqType` t1  = cont            -- The coerces cancel out
          | otherwise           = CoerceIt (mkTransCoercion co1 co2) 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)
+       add_coerce co (s1s2, _t1t2) (ApplyTo dup (Type arg_ty) arg_se cont)
+                -- (f |> g) ty  --->   (f ty) |> (g @ ty)
                 -- This implements the PushT rule from the paper
          | Just (tyvar,_) <- splitForAllTy_maybe s1s2
          , not (isCoVar tyvar)
          = ApplyTo dup (Type ty') (zapSubstEnv env) (addCoerce (mkInstCoercion co ty') cont)
          where
                 -- This implements the PushT rule from the paper
          | Just (tyvar,_) <- splitForAllTy_maybe s1s2
          , not (isCoVar tyvar)
          = ApplyTo dup (Type ty') (zapSubstEnv env) (addCoerce (mkInstCoercion co ty') cont)
          where
-           ty' = substTy arg_se arg_ty
+           ty' = substTy (arg_se `setInScope` env) arg_ty
 
         -- ToDo: the PushC rule is not implemented at all
 
 
         -- 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
          | 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
                 -- to something but s1s2 might conceivably not be
                 --
                 -- When we build the ApplyTo we can't mix the out-types
@@ -834,12 +886,12 @@ simplCast env body co cont
                 -- Example of use: Trac #995
          = ApplyTo dup new_arg (zapSubstEnv env) (addCoerce co2 cont)
          where
                 -- Example of use: Trac #995
          = ApplyTo dup new_arg (zapSubstEnv env) (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'
            [co1, co2] = decomposeCo 2 co
            new_arg    = mkCoerce (mkSymCoercion co1) arg'
-           arg'       = substExpr arg_se arg
+           arg'       = substExpr (arg_se `setInScope` env) arg
 
        add_coerce co _ cont = CoerceIt co cont
 \end{code}
 
        add_coerce co _ cont = CoerceIt co cont
 \end{code}
@@ -857,30 +909,23 @@ simplLam :: SimplEnv -> [InId] -> InExpr -> SimplCont
 
 simplLam env [] body cont = simplExprF env body cont
 
 
 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
 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
+  = do  { (env', bndrs') <- simplLamBndrs env bndrs
+        ; body' <- simplExpr env' body
         ; new_lam <- mkLam bndrs' body'
         ; new_lam <- mkLam bndrs' body'
-        ; rebuild env new_lam cont }
+        ; rebuild env' new_lam cont }
 
 ------------------
 simplNonRecE :: SimplEnv
              -> InId                    -- The binder
              -> (InExpr, SimplEnv)      -- Rhs of binding (or arg of lambda)
 
 ------------------
 simplNonRecE :: SimplEnv
              -> InId                    -- 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)
                                         --      \xs.e
              -> SimplCont
              -> SimplM (SimplEnv, OutExpr)
@@ -897,6 +942,13 @@ simplNonRecE :: SimplEnv
 -- Why?  Because of the binder-occ-info-zapping done before
 --       the call to simplLam in simplExprF (Lam ...)
 
 -- 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( isTyVar 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)
 simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
   | preInlineUnconditionally env NotTopLevel bndr rhs
   = do  { tick (PreInlineUnconditionally bndr)
@@ -907,7 +959,8 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
                      (StrictBind bndr bndrs body env cont) }
 
   | otherwise
                      (StrictBind bndr bndrs body env cont) }
 
   | otherwise
-  = do  { (env1, bndr1) <- simplNonRecBndr env bndr
+  = ASSERT( not (isTyVar 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 }
         ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
         ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
         ; simplLam env3 bndrs body cont }
@@ -923,6 +976,8 @@ 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.
 \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
   = do  { e' <- simplExpr (setEnclosingCC env currentCCS) e
         ; rebuild env (mkSCC cc e') cont }
 simplNote env (SCC cc) e cont
   = do  { e' <- simplExpr (setEnclosingCC env currentCCS) e
         ; rebuild env (mkSCC cc e') cont }
@@ -952,6 +1007,7 @@ simplNote env (CoreNote s) e cont = do
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
+simplVar :: SimplEnv -> Id -> SimplCont -> SimplM (SimplEnv, OutExpr)
 simplVar env var cont
   = case substId env var of
         DoneEx e         -> simplExprF (zapSubstEnv env) e cont
 simplVar env var cont
   = case substId env var of
         DoneEx e         -> simplExprF (zapSubstEnv env) e cont
@@ -970,6 +1026,7 @@ simplVar env var cont
 ---------------------------------------------------------
 --      Dealing with a call site
 
 ---------------------------------------------------------
 --      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
 completeCall env var cont
   = do  { dflags <- getDOptsSmpl
         ; let   (args,call_cont) = contArgs cont
@@ -1002,12 +1059,13 @@ completeCall env var cont
         -- 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
         -- 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
+        ; rule_base <- getSimplRules
         ; let   in_scope   = getInScope env
         ; let   in_scope   = getInScope env
+               rules      = getRules rule_base var
                 maybe_rule = case activeRule dflags env of
                                 Nothing     -> Nothing  -- No rules apply
                                 Just act_fn -> lookupRule act_fn in_scope
                 maybe_rule = case activeRule dflags env of
                                 Nothing     -> Nothing  -- No rules apply
                                 Just act_fn -> lookupRule act_fn in_scope
-                                                          rules var args
+                                                          var args rules 
         ; case maybe_rule of {
             Just (rule, rule_rhs) -> do
                 tick (RuleFired (ru_name rule))
         ; case maybe_rule of {
             Just (rule, rule_rhs) -> do
                 tick (RuleFired (ru_name rule))
@@ -1048,16 +1106,16 @@ completeCall env var cont
         ------------- No inlining! ----------------
         -- Next, look for rules or specialisations that match
         --
         ------------- No inlining! ----------------
         -- Next, look for rules or specialisations that match
         --
-        rebuildCall env (Var var) (idType var)
+        rebuildCall env (Var var)
                     (mkArgInfo var n_val_args call_cont) cont
     }}}}
 
 rebuildCall :: SimplEnv
                     (mkArgInfo var n_val_args call_cont) cont
     }}}}
 
 rebuildCall :: SimplEnv
-            -> OutExpr -> OutType       -- Function and its type
+            -> OutExpr       -- Function 
             -> ArgInfo
             -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
             -> ArgInfo
             -> SimplCont
             -> SimplM (SimplEnv, OutExpr)
-rebuildCall env fun fun_ty (ArgInfo { ai_strs = [] }) cont
+rebuildCall env fun (ArgInfo { 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.
   -- 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.
@@ -1071,22 +1129,23 @@ rebuildCall env fun fun_ty (ArgInfo { ai_strs = [] }) cont
   | not (contIsTrivial cont)     -- Only do this if there is a non-trivial
   = return (env, mk_coerce fun)  -- contination to discard, else we do it
   where                          -- again and again!
   | not (contIsTrivial cont)     -- Only do this if there is a non-trivial
   = return (env, mk_coerce fun)  -- contination to discard, else we do it
   where                          -- again and again!
-    cont_ty = contResultType cont
+    fun_ty  = exprType fun
+    cont_ty = contResultType env fun_ty cont
     co      = mkUnsafeCoercion fun_ty cont_ty
     co      = mkUnsafeCoercion fun_ty cont_ty
-    mk_coerce expr | cont_ty `coreEqType` fun_ty = fun
-                   | otherwise = mkCoerce co fun
+    mk_coerce expr | cont_ty `coreEqType` fun_ty = expr
+                   | otherwise = mkCoerce co expr
 
 
-rebuildCall env fun fun_ty info (ApplyTo _ (Type arg_ty) se cont)
+rebuildCall env fun info (ApplyTo _ (Type arg_ty) se cont)
   = do  { ty' <- simplType (se `setInScope` env) arg_ty
   = do  { ty' <- simplType (se `setInScope` env) arg_ty
-        ; rebuildCall env (fun `App` Type ty') (applyTy fun_ty ty') info cont }
+        ; rebuildCall env (fun `App` Type ty') info cont }
 
 
-rebuildCall env fun fun_ty
+rebuildCall env fun 
            (ArgInfo { ai_rules = has_rules, ai_strs = str:strs, ai_discs = disc:discs })
            (ApplyTo _ arg arg_se cont)
            (ArgInfo { ai_rules = has_rules, ai_strs = str:strs, ai_discs = disc:discs })
            (ApplyTo _ arg arg_se cont)
-  | str || isStrictType arg_ty          -- Strict argument
+  | str                -- Strict argument
   = -- pprTrace "Strict Arg" (ppr arg $$ ppr (seIdSubst env) $$ ppr (seInScope env)) $
     simplExprF (arg_se `setFloats` env) arg
   = -- 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 fun cci arg_info' cont)
                 -- Note [Shadowing]
 
   | otherwise                           -- Lazy argument
                 -- Note [Shadowing]
 
   | otherwise                           -- Lazy argument
@@ -1095,15 +1154,14 @@ 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
         -- 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 (fun `App` arg') arg_info' cont }
   where
   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
 
     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
+rebuildCall env fun _ cont
   = rebuild env fun cont
 \end{code}
 
   = rebuild env fun cont
 \end{code}
 
@@ -1137,7 +1195,91 @@ all this at once is TOO HARD!
 %*                                                                      *
 %************************************************************************
 
 %*                                                                      *
 %************************************************************************
 
-Blob of helper functions for the "case-of-something-else" situation.
+Note [Case elimination]
+~~~~~~~~~~~~~~~~~~~~~~~
+The case-elimination transformation discards redundant case expressions.
+Start with a simple situation:
+
+        case x# of      ===>   e[x#/y#]
+          y# -> e
+
+(when x#, y# are of primitive type, of course).  We can't (in general)
+do this for algebraic cases, because we might turn bottom into
+non-bottom!
+
+The code in SimplUtils.prepareAlts has the effect of generalise this
+idea to look for a case where we're scrutinising a variable, and we
+know that only the default case can match.  For example:
+
+        case x of
+          0#      -> ...
+          DEFAULT -> ...(case x of
+                         0#      -> ...
+                         DEFAULT -> ...) ...
+
+Here the inner case is first trimmed to have only one alternative, the
+DEFAULT, after which it's an instance of the previous case.  This
+really only shows up in eliminating error-checking code.
+
+We also make sure that we deal with this very common case:
+
+        case e of
+          x -> ...x...
+
+Here we are using the case as a strict let; if x is used only once
+then we want to inline it.  We have to be careful that this doesn't
+make the program terminate when it would have diverged before, so we
+check that
+        - e is already evaluated (it may so if e is a variable)
+        - x is used strictly, or
+
+Lastly, the code in SimplUtils.mkCase combines identical RHSs.  So
+
+        case e of       ===> case e of DEFAULT -> r
+           True  -> r
+           False -> r
+
+Now again the case may be elminated by the CaseElim transformation.
+
+
+Further notes about case elimination
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider:       test :: Integer -> IO ()
+                test = print
+
+Turns out that this compiles to:
+    Print.test
+      = \ eta :: Integer
+          eta1 :: State# RealWorld ->
+          case PrelNum.< eta PrelNum.zeroInteger of wild { __DEFAULT ->
+          case hPutStr stdout
+                 (PrelNum.jtos eta ($w[] @ Char))
+                 eta1
+          of wild1 { (# new_s, a4 #) -> PrelIO.lvl23 new_s  }}
+
+Notice the strange '<' which has no effect at all. This is a funny one.
+It started like this:
+
+f x y = if x < 0 then jtos x
+          else if y==0 then "" else jtos x
+
+At a particular call site we have (f v 1).  So we inline to get
+
+        if v < 0 then jtos x
+        else if 1==0 then "" else jtos x
+
+Now simplify the 1==0 conditional:
+
+        if v<0 then jtos v else jtos v
+
+Now common-up the two branches of the case:
+
+        case (v<0) of DEFAULT -> jtos v
+
+Why don't we drop the case?  Because it's strict in v.  It's technically
+wrong to drop even unnecessary evaluations, and in practice they
+may be a result of 'seq' so we *definitely* don't want to drop those.
+I don't really know how to improve this situation.
 
 \begin{code}
 ---------------------------------------------------------
 
 \begin{code}
 ---------------------------------------------------------
@@ -1169,9 +1311,9 @@ rebuildCase env scrut case_bndr alts cont
 --      2. Eliminate the case if scrutinee is evaluated
 --------------------------------------------------
 
 --      2. Eliminate the case if scrutinee is evaluated
 --------------------------------------------------
 
-rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
+rebuildCase env scrut case_bndr [(_, bndrs, rhs)] cont
   -- See if we can get rid of the case altogether
   -- See if we can get rid of the case altogether
-  -- See the extensive notes on case-elimination above
+  -- See Note [Case eliminiation] 
   -- mkCase made sure that if all the alternatives are equal,
   -- then there is now only one (DEFAULT) rhs
  | all isDeadBinder bndrs       -- bndrs are [InId]
   -- mkCase made sure that if all the alternatives are equal,
   -- then there is now only one (DEFAULT) rhs
  | all isDeadBinder bndrs       -- bndrs are [InId]
@@ -1198,8 +1340,8 @@ rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
 --      other problems
 --      Also we don't want to discard 'seq's
   = do  { tick (CaseElim case_bndr)
 --      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 }
+        ; 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
   where
         -- The case binder is going to be evaluated later,
         -- and the scrutinee is a simple variable
@@ -1207,7 +1349,7 @@ rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
                                  && not (isTickBoxOp v)
                                     -- ugly hack; covering this case is what
                                     -- exprOkForSpeculation was intended for.
                                  && not (isTickBoxOp v)
                                     -- ugly hack; covering this case is what
                                     -- exprOkForSpeculation was intended for.
-    var_demanded_later other   = False
+    var_demanded_later _       = False
 
 
 --------------------------------------------------
 
 
 --------------------------------------------------
@@ -1217,16 +1359,29 @@ rebuildCase env scrut case_bndr [(con,bndrs,rhs)] cont
 rebuildCase env scrut case_bndr alts cont
   = do  {       -- Prepare the continuation;
                 -- The new subst_env is in place
 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
+          (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont
 
         -- Simplify the alternatives
 
         -- 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 }
+        ; (scrut', case_bndr', alts') <- simplAlts env' scrut case_bndr alts dup_cont
+
+       -- Check for empty alternatives
+       ; if null alts' then
+               -- This isn't strictly an error, although it is unusual. 
+               -- It's possible that the simplifer might "see" that 
+               -- an inner case has no accessible alternatives before 
+               -- it "sees" that the entire branch of an outer case is 
+               -- inaccessible.  So we simply put an error case here instead.
+           pprTrace "mkCase: null alts" (ppr case_bndr <+> ppr scrut) $
+           let res_ty' = contResultType env' (substTy env' (coreAltsType alts)) dup_cont
+               lit = mkStringLit "Impossible alternative"
+           in return (env', mkApps (Var rUNTIME_ERROR_ID) [Type res_ty', lit])
+
+         else do
+       { case_expr <- mkCase scrut' case_bndr' alts'
+
+       -- Notice that rebuild gets 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 } }
 \end{code}
 
 simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
 \end{code}
 
 simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
@@ -1234,75 +1389,15 @@ try to eliminate uses of v in the RHSs in favour of case_bndr; that
 way, there's a chance that v will now only be used once, and hence
 inlined.
 
 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.
+Historical note: we use to do the "case binder swap" in the Simplifier
+so there were additional complications if the scrutinee was a variable.
+Now the binder-swap stuff is done in the occurrence analyer; see
+OccurAnal Note [Binder swap].
 
 Note [zapOccInfo]
 ~~~~~~~~~~~~~~~~~
 
 Note [zapOccInfo]
 ~~~~~~~~~~~~~~~~~
-If we replace the scrutinee, v, by tbe case binder, then we have to nuke
-any occurrence info (eg IAmDead) in the case binder, because the
-case-binder now effectively occurs whenever v does.  AND we have to do
-the same for the pattern-bound variables!  Example:
-
-        (case x of { (a,b) -> a }) (case x of { (p,q) -> q })
-
-Here, b and p are dead.  But when we move the argment inside the first
-case RHS, and eliminate the second case, we get
-
-        case x of { (a,b) -> a b }
-
-Urk! b is alive!  Reason: the scrutinee was a variable, and case elimination
-happened.
-
-Indeed, this can happen anytime the case binder isn't dead:
+If the case binder is not dead, then neither are the pattern bound
+variables:  
         case <any> of x { (a,b) ->
         case x of { (p,q) -> p } }
 Here (a,b) both look dead, but come alive after the inner case is eliminated.
         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.
@@ -1311,15 +1406,6 @@ The point is that we bring into the envt a binding
 after the outer case, and that makes (a,b) alive.  At least we do unless
 the case binder is guaranteed dead.
 
 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
 Note [Improving seq]
 ~~~~~~~~~~~~~~~~~~~
 Consider
@@ -1350,125 +1436,82 @@ 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.)
 
 (Otherwise, there's a danger that we'll simply drop the 'seq' altogether, before
 LiberateCase gets to see it.)
 
-Note [Case elimination]
-~~~~~~~~~~~~~~~~~~~~~~~
-The case-elimination transformation discards redundant case expressions.
-Start with a simple situation:
-
-        case x# of      ===>   e[x#/y#]
-          y# -> e
 
 
-(when x#, y# are of primitive type, of course).  We can't (in general)
-do this for algebraic cases, because we might turn bottom into
-non-bottom!
-
-The code in SimplUtils.prepareAlts has the effect of generalise this
-idea to look for a case where we're scrutinising a variable, and we
-know that only the default case can match.  For example:
-
-        case x of
-          0#      -> ...
-          DEFAULT -> ...(case x of
-                         0#      -> ...
-                         DEFAULT -> ...) ...
-
-Here the inner case is first trimmed to have only one alternative, the
-DEFAULT, after which it's an instance of the previous case.  This
-really only shows up in eliminating error-checking code.
-
-We also make sure that we deal with this very common case:
-
-        case e of
-          x -> ...x...
-
-Here we are using the case as a strict let; if x is used only once
-then we want to inline it.  We have to be careful that this doesn't
-make the program terminate when it would have diverged before, so we
-check that
-        - e is already evaluated (it may so if e is a variable)
-        - x is used strictly, or
-
-Lastly, the code in SimplUtils.mkCase combines identical RHSs.  So
-
-        case e of       ===> case e of DEFAULT -> r
-           True  -> r
-           False -> r
-
-Now again the case may be elminated by the CaseElim transformation.
-
-
-Further notes about case elimination
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider:       test :: Integer -> IO ()
-                test = print
+Historical note [no-case-of-case]
+~~~~~~~~~~~~~~~~~~~~~~
+We *used* to suppress the binder-swap in case expressoins when 
+-fno-case-of-case is on.  Old remarks:
+    "This happens in the first simplifier pass,
+    and enhances full laziness.  Here's the bad case:
+            f = \ y -> ...(case x of I# v -> ...(case x of ...) ... )
+    If we eliminate the inner case, we trap it inside the I# v -> arm,
+    which might prevent some full laziness happening.  I've seen this
+    in action in spectral/cichelli/Prog.hs:
+             [(m,n) | m <- [1..max], n <- [1..max]]
+    Hence the check for NoCaseOfCase."
+However, now the full-laziness pass itself reverses the binder-swap, so this
+check is no longer necessary.
+
+Historical 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
 
 
-Turns out that this compiles to:
-    Print.test
-      = \ eta :: Integer
-          eta1 :: State# RealWorld ->
-          case PrelNum.< eta PrelNum.zeroInteger of wild { __DEFAULT ->
-          case hPutStr stdout
-                 (PrelNum.jtos eta ($w[] @ Char))
-                 eta1
-          of wild1 { (# new_s, a4 #) -> PrelIO.lvl23 new_s  }}
+    case x of w1 { DEFAULT -> case x of w2 { A -> e1; B -> e2 }
+                   ...other cases .... }
 
 
-Notice the strange '<' which has no effect at all. This is a funny one.
-It started like this:
+We'll perform the binder-swap for the outer case, giving
 
 
-f x y = if x < 0 then jtos x
-          else if y==0 then "" else jtos x
+    case x of w1 { DEFAULT -> case w1 of w2 { A -> e1; B -> e2 }
+                   ...other cases .... }
 
 
-At a particular call site we have (f v 1).  So we inline to get
+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
 
 
-        if v < 0 then jtos x
-        else if 1==0 then "" else jtos x
+    case x of w1 { A -> let w2 = w1 in e1
+                   B -> let w2 = w1 in e2
+                   ...other cases .... }
 
 
-Now simplify the 1==0 conditional:
+This is plain silly in the common case where w2 is dead.
 
 
-        if v<0 then jtos v else jtos v
+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:
 
 
-Now common-up the two branches of the case:
+        data T = MkT !Int
 
 
-        case (v<0) of DEFAULT -> jtos v
+        case v of w  { MkT x ->
+        case x of x1 { I# y1 ->
+        case x of x2 { I# y2 -> ...
 
 
-Why don't we drop the case?  Because it's strict in v.  It's technically
-wrong to drop even unnecessary evaluations, and in practice they
-may be a result of 'seq' so we *definitely* don't want to drop those.
-I don't really know how to improve this situation.
+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.
 
 
 \begin{code}
 
 
 \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
-
-        ; fam_envs <- getFamEnvs
-        ; (env2, scrut2, case_bndr2) <- improve_seq fam_envs env1 scrut
-                                                case_bndr case_bndr1 alts
-                        -- Note [Improving seq]
-
-        ; let (env3, case_bndr3) = improve_case_bndr env2 scrut2 case_bndr2
-                        -- Note [Case of cast]
-
-        ; return (env3, scrut2, case_bndr3) }
-  where
-
-    improve_seq fam_envs 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)
-
-
+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,_,_)]
+  | 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)
+
+{-
     improve_case_bndr env scrut case_bndr
     improve_case_bndr env scrut case_bndr
-        | switchIsOn (getSwitchChecker env) NoCaseOfCase
-                -- See Note [no-case-of-case]
-        = (env, case_bndr)
+        -- See Note [no-case-of-case]
+       --  | switchIsOn (getSwitchChecker env) NoCaseOfCase
+       --  = (env, case_bndr)
 
         | otherwise     -- Failed try; see Note [Suppressing the case binder-swap]
                         --     not (isEvaldUnfolding (idUnfolding v))
 
         | otherwise     -- Failed try; see Note [Suppressing the case binder-swap]
                         --     not (isEvaldUnfolding (idUnfolding v))
@@ -1483,14 +1526,11 @@ simplCaseBinder env scrut case_bndr alts
                             where
                                 rhs = Cast (Var case_bndr') (mkSymCoercion co)
 
                             where
                                 rhs = Cast (Var case_bndr') (mkSymCoercion co)
 
-            other -> (env, case_bndr)
+            _ -> (env, case_bndr)
         where
         where
-          case_bndr' = zapOccInfo case_bndr
+          case_bndr' = zapIdOccInfo case_bndr
           env1       = modifyInScope env case_bndr case_bndr'
           env1       = modifyInScope env case_bndr case_bndr'
-
-
-zapOccInfo :: InId -> InId      -- See Note [zapOccInfo]
-zapOccInfo b = b `setIdOccInfo` NoOccInfo
+-}
 \end{code}
 
 
 \end{code}
 
 
@@ -1538,19 +1578,25 @@ of the inner case y, which give us nowhere to go!
 simplAlts :: SimplEnv
           -> OutExpr
           -> InId                       -- Case binder
 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
 
 simplAlts env scrut case_bndr alts cont'
   = -- pprTrace "simplAlts" (ppr alts $$ ppr (seIdSubst env)) $
           -> SimplM (OutExpr, OutId, [OutAlt])  -- Includes the continuation
 -- Like simplExpr, this just returns the simplified alternatives;
 -- it 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
+    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 alt_env' scrut' case_bndr' alts
+
+        ; alts' <- mapM (simplAlt alt_env' imposs_deflt_cons case_bndr' cont') in_alts
         ; return (scrut', case_bndr', alts') }
 
 ------------------------------------
         ; return (scrut', case_bndr', alts') }
 
 ------------------------------------
@@ -1569,26 +1615,27 @@ simplAlt env imposs_deflt_cons case_bndr' cont' (DEFAULT, bndrs, rhs)
         ; rhs' <- simplExprC env' rhs cont'
         ; return (DEFAULT, [], 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') }
 
   = 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
   = 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'
 
                 -- 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
         ; return (DataAlt con, vs', rhs') }
   where
         -- add_evals records the evaluated-ness of the bound variables of
@@ -1600,19 +1647,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
         -- 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 [] [] = []
         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 | isTyVar 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
             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
         -- 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 +1668,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.
         --        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
 
 addBinderUnfolding :: SimplEnv -> Id -> CoreExpr -> SimplEnv
 addBinderUnfolding env bndr rhs
-  = modifyInScope env bndr (bndr `setIdUnfolding` mkUnfolding False rhs)
+  = modifyInScope env (bndr `setIdUnfolding` mkUnfolding False rhs)
 
 addBinderOtherCon :: SimplEnv -> Id -> [AltCon] -> SimplEnv
 addBinderOtherCon env bndr cons
 
 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}
 
 
 \end{code}
 
 
@@ -1653,7 +1708,8 @@ and then
 All this should happen in one sweep.
 
 \begin{code}
 All this should happen in one sweep.
 
 \begin{code}
-knownCon :: SimplEnv -> OutExpr -> AltCon -> [OutExpr]
+knownCon :: SimplEnv -> OutExpr -> AltCon
+        -> [OutExpr]           -- Args *including* the universal args
          -> InId -> [InAlt] -> SimplCont
          -> SimplM (SimplEnv, OutExpr)
 
          -> InId -> [InAlt] -> SimplCont
          -> SimplM (SimplEnv, OutExpr)
 
@@ -1661,23 +1717,25 @@ knownCon env scrut con args bndr alts cont
   = do  { tick (KnownBranch bndr)
         ; knownAlt env scrut args bndr (findAlt con alts) cont }
 
   = do  { tick (KnownBranch bndr)
         ; knownAlt env scrut args bndr (findAlt con alts) cont }
 
-knownAlt env scrut args bndr (DEFAULT, bs, rhs) cont
+knownAlt :: SimplEnv -> OutExpr -> [OutExpr]
+         -> InId -> (AltCon, [CoreBndr], InExpr) -> SimplCont
+         -> SimplM (SimplEnv, OutExpr)
+knownAlt env scrut _ bndr (DEFAULT, bs, rhs) cont
   = ASSERT( null bs )
   = ASSERT( null bs )
-    do  { env <- simplNonRecX env bndr scrut
+    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
                 -- 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 }
+        ; simplExprF env' rhs cont }
 
 
-knownAlt env scrut args bndr (LitAlt lit, bs, rhs) cont
+knownAlt env scrut _ bndr (LitAlt _, bs, rhs) cont
   = ASSERT( null bs )
   = ASSERT( null bs )
-    do  { env <- simplNonRecX env bndr scrut
-        ; simplExprF env rhs cont }
+    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)
+knownAlt env scrut the_args bndr (DataAlt dc, bs, rhs) cont
+  = do  { let n_drop_tys = length (dataConUnivTyVars dc)
+        ; env' <- bind_args env bs (drop n_drop_tys the_args)
         ; let
                 -- It's useful to bind bndr to scrut, rather than to a fresh
                 -- binding      x = Con arg1 .. argn
         ; let
                 -- It's useful to bind bndr to scrut, rather than to a fresh
                 -- binding      x = Con arg1 .. argn
@@ -1687,35 +1745,37 @@ knownAlt env scrut args bndr (DataAlt dc, bs, rhs) cont
                 -- about duplicating the arg redexes; in that case, make
                 -- a new con-app from the args
                 bndr_rhs  = case scrut of
                 -- 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]
+                                Var _ -> scrut
+                                _     -> con_app
+                con_app = mkConApp dc (take n_drop_tys the_args ++ con_args)
+                con_args = [substExpr env' (varToCoreExpr b) | b <- bs]
                                 -- args are aready OutExprs, but bs are InIds
 
                                 -- 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 }
+        ; env'' <- simplNonRecX env' bndr bndr_rhs
+        ; simplExprF env'' rhs cont }
   where
   where
-    -- Ugh!
-    bind_args env dead_bndr [] _  = return env
+    zap_occ = zapCasePatIdOcc bndr    -- bndr is an InId
+
+                  -- Ugh!
+    bind_args env' [] _  = return env'
 
 
-    bind_args env dead_bndr (b:bs) (Type ty : args)
+    bind_args env' (b:bs') (Type ty : args)
       = ASSERT( isTyVar b )
       = ASSERT( isTyVar b )
-        bind_args (extendTvSubst env b ty) dead_bndr bs args
+        bind_args (extendTvSubst env' b ty) bs' args
 
 
-    bind_args env dead_bndr (b:bs) (arg : args)
+    bind_args env' (b:bs') (arg : args)
       = ASSERT( isId b )
       = 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 the_args $$
                              text "scrut:" <+> ppr scrut
 \end{code}
 
                              text "scrut:" <+> ppr scrut
 \end{code}
 
@@ -1735,8 +1795,8 @@ prepareCaseCont :: SimplEnv
                         -- continunation)
 
         -- No need to make it duplicatable if there's only one alternative
                         -- 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}
 \end{code}
 
 \begin{code}
@@ -1745,20 +1805,20 @@ mkDupableCont :: SimplEnv -> SimplCont
 
 mkDupableCont env cont
   | contIsDupable cont
 
 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)
 
 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)
+mkDupableCont env cont@(StrictBind {})
+  =  return (env, mkBoringStop, cont)
         -- See Note [Duplicating strict continuations]
 
         -- See Note [Duplicating strict continuations]
 
-mkDupableCont env cont@(StrictArg _ fun_ty _ _ _)
-  =  return (env, mkBoringStop (funArgTy fun_ty), cont)
+mkDupableCont env cont@(StrictArg {})
+  =  return (env, mkBoringStop, cont)
         -- See Note [Duplicating strict continuations]
 
 mkDupableCont env (ApplyTo _ arg se cont)
         -- See Note [Duplicating strict continuations]
 
 mkDupableCont env (ApplyTo _ arg se cont)
@@ -1766,20 +1826,20 @@ mkDupableCont env (ApplyTo _ arg se cont)
         --      ==>
         --              let a = ...arg...
         --              in [...hole...] a
         --      ==>
         --              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 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)
 --  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 })
 
 mkDupableCont env (Select _ case_bndr alts se cont)
   =     -- e.g.         (case [...hole...] of { pi -> ei })
@@ -1787,14 +1847,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)
         --              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
 
                 -- 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
         -- 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 +1867,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
 
         -- 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) }
 
 
                   nodup_cont) }
 
 
@@ -1818,15 +1877,17 @@ mkDupableAlts :: SimplEnv -> OutId -> [InAlt]
               -> SimplM (SimplEnv, [InAlt])
 -- Absorbs the continuation into the new alternatives
 
               -> 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
   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' ) }
-
+    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'))
 mkDupableAlt env case_bndr' (con, bndrs', rhs')
   | exprIsDupable rhs'  -- Note [Small alternative rhs]
   = return (env, (con, bndrs', rhs'))
@@ -1841,10 +1902,10 @@ mkDupableAlt env case_bndr' (con, bndrs', rhs')
         ; (final_bndrs', final_args)    -- Note [Join point abstraction]
                 <- if (any isId used_bndrs')
                    then return (used_bndrs', varsToCoreExprs used_bndrs')
         ; (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]) }
 
                             ; 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
                 -- Note [Funky mkPiTypes]
 
         ; let   -- We make the lambdas into one-shot-lambdas.  The
@@ -1857,7 +1918,7 @@ mkDupableAlt env case_bndr' (con, bndrs', rhs')
                 join_rhs  = mkLams really_final_bndrs rhs'
                 join_call = mkApps (Var join_bndr) final_args
 
                 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)) }
+        ; return (addPolyBind NotTopLevel env (NonRec join_bndr join_rhs), (con, bndrs', join_call)) }
                 -- See Note [Duplicated env]
 \end{code}
 
                 -- See Note [Duplicated env]
 \end{code}
 
@@ -2026,3 +2087,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.
 
      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.