[project @ 2001-11-16 15:42:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / simplCore / SimplUtils.lhs
index 22d1357..e894bc0 100644 (file)
@@ -5,44 +5,46 @@
 
 \begin{code}
 module SimplUtils (
-       simplBinder, simplBinders, simplIds,
-       transformRhs,
-       mkCase, findAlt, findDefault,
+       simplBinder, simplBinders, simplRecBndrs, 
+       simplLetBndr, simplLamBndrs, 
+       newId, mkLam, mkCase,
 
        -- The continuation type
-       SimplCont(..), DupFlag(..), contIsDupable, contResultType,
-       pushArgs, discardCont, countValArgs, countArgs,
-       analyseCont, discardInline
+       SimplCont(..), DupFlag(..), LetRhsFlag(..), 
+       contIsDupable, contResultType,
+       countValArgs, countArgs, pushContArgs,
+       mkBoringStop, mkStop, contIsRhs, contIsRhsOrArg,
+       getContArgs, interestingCallContext, interestingArg, isStrictType
 
     ) where
 
 #include "HsVersions.h"
 
-import BinderInfo
-import CmdLineOpts     ( opt_SimplDoLambdaEtaExpansion, opt_SimplCaseMerge )
+import CmdLineOpts     ( SimplifierSwitch(..),
+                         opt_SimplDoLambdaEtaExpansion, opt_SimplDoEtaReduction,
+                         opt_SimplCaseMerge, opt_UF_UpdateInPlace
+                       )
 import CoreSyn
-import CoreUnfold      ( isValueUnfolding )
-import CoreFVs         ( exprFreeVars )
-import CoreUtils       ( exprIsTrivial, cheapEqExpr, exprType, exprIsCheap, exprEtaExpandArity, bindNonRec )
-import Subst           ( InScopeSet, mkSubst, substBndrs, substBndr, substIds, lookupIdSubst )
-import Id              ( Id, idType, isId, idName, 
-                         idOccInfo, idUnfolding,
-                         idDemandInfo, mkId, idInfo
+import CoreUtils       ( cheapEqExpr, exprType, 
+                         etaExpand, exprEtaExpandArity, bindNonRec, mkCoerce,
+                         findDefault, exprOkForSpeculation, exprIsValue
+                       )
+import qualified Subst ( simplBndrs, simplBndr, simplLetId, simplLamBndr )
+import Id              ( Id, idType, idInfo, 
+                         mkSysLocal, isDeadBinder, idNewDemandInfo,
+                         idUnfolding, idNewStrictness
                        )
-import IdInfo          ( arityLowerBound, setOccInfo, vanillaIdInfo )
-import Maybes          ( maybeToBool, catMaybes )
-import Name            ( isLocalName, setNameUnique )
+import NewDemand       ( isStrictDmd, isBotRes, splitStrictSig )
 import SimplMonad
-import Type            ( Type, tyVarsOfType, tyVarsOfTypes, mkForAllTys, seqType,
-                         splitTyConApp_maybe, splitAlgTyConApp_maybe, mkTyVarTys, applyTys, splitFunTys, mkFunTys
+import Type            ( Type, seqType, 
+                         splitTyConApp_maybe, tyConAppArgs, mkTyVarTys,
+                         splitRepFunTys, isStrictType
                        )
-import DataCon         ( dataConRepArity )
-import TysPrim         ( statePrimTyCon )
-import Var             ( setVarUnique )
-import VarSet
-import VarEnv          ( SubstEnv, SubstResult(..) )
-import UniqSupply      ( splitUniqSupply, uniqFromSupply )
-import Util            ( zipWithEqual, mapAccumL )
+import OccName         ( UserFS )
+import TyCon           ( tyConDataConsIfAvailable, isAlgTyCon, isNewTyCon )
+import DataCon         ( dataConRepArity, dataConSig, dataConArgTys )
+import Var             ( mkSysTyVar, tyVarKind )
+import Util            ( lengthExceeds, mapAccumL )
 import Outputable
 \end{code}
 
@@ -55,7 +57,11 @@ import Outputable
 
 \begin{code}
 data SimplCont         -- Strict contexts
-  = Stop OutType               -- Type of the result
+  = Stop     OutType           -- Type of the result
+            LetRhsFlag
+            Bool               -- True <=> This is the RHS of a thunk whose type suggests
+                               --          that update-in-place would be possible
+                               --          (This makes the inliner a little keener.)
 
   | CoerceIt OutType                   -- The To-type, simplified
             SimplCont
@@ -64,26 +70,37 @@ data SimplCont              -- Strict contexts
             SimplCont                  -- keen to inline itelf
 
   | ApplyTo  DupFlag 
-            InExpr SubstEnv            -- The argument, as yet unsimplified, 
-            SimplCont                  -- and its subst-env
+            InExpr SimplEnv            -- The argument, as yet unsimplified, 
+            SimplCont                  -- and its environment
 
   | Select   DupFlag 
-            InId [InAlt] SubstEnv      -- The case binder, alts, and subst-env
+            InId [InAlt] SimplEnv      -- The case binder, alts, and subst-env
             SimplCont
 
-  | ArgOf    DupFlag           -- An arbitrary strict context: the argument 
+  | ArgOf    LetRhsFlag                -- An arbitrary strict context: the argument 
                                --      of a strict function, or a primitive-arg fn
                                --      or a PrimOp
-            OutType            -- The type of the expression being sought by the context
+                               -- No DupFlag because we never duplicate it
+            OutType            -- arg_ty: type of the argument itself
+            OutType            -- cont_ty: the type of the expression being sought by the context
                                --      f (error "foo") ==> coerce t (error "foo")
                                -- when f is strict
                                -- We need to know the type t, to which to coerce.
-            (OutExpr -> SimplM OutExprStuff)   -- What to do with the result
+
+            (SimplEnv -> OutExpr -> SimplM FloatsWithExpr)     -- What to do with the result
+                               -- The result expression in the OutExprStuff has type cont_ty
+
+data LetRhsFlag = AnArg                -- It's just an argument not a let RHS
+               | AnRhs         -- It's the RHS of a let (so please float lets out of big lambdas)
+
+instance Outputable LetRhsFlag where
+  ppr AnArg = ptext SLIT("arg")
+  ppr AnRhs = ptext SLIT("rhs")
 
 instance Outputable SimplCont where
-  ppr (Stop _)                      = ptext SLIT("Stop")
+  ppr (Stop _ is_rhs _)             = ptext SLIT("Stop") <> brackets (ppr is_rhs)
   ppr (ApplyTo dup arg se cont)      = (ptext SLIT("ApplyTo") <+> ppr dup <+> ppr arg) $$ ppr cont
-  ppr (ArgOf   dup _ _)             = ptext SLIT("ArgOf...") <+> ppr dup
+  ppr (ArgOf _ _ _ _)               = ptext SLIT("ArgOf...")
   ppr (Select dup bndr alts se cont) = (ptext SLIT("Select") <+> ppr dup <+> ppr bndr) $$ 
                                       (nest 4 (ppr alts)) $$ ppr cont
   ppr (CoerceIt ty cont)            = (ptext SLIT("CoerceIt") <+> ppr ty) $$ ppr cont
@@ -95,34 +112,57 @@ instance Outputable DupFlag where
   ppr OkToDup = ptext SLIT("ok")
   ppr NoDup   = ptext SLIT("nodup")
 
+
+-------------------
+mkBoringStop :: OutType -> SimplCont
+mkBoringStop ty = Stop ty AnArg (canUpdateInPlace ty)
+
+mkStop :: OutType -> LetRhsFlag -> SimplCont
+mkStop ty is_rhs = Stop ty is_rhs (canUpdateInPlace ty)
+
+contIsRhs :: SimplCont -> Bool
+contIsRhs (Stop _ AnRhs _)    = True
+contIsRhs (ArgOf AnRhs _ _ _) = True
+contIsRhs other                      = False
+
+contIsRhsOrArg (Stop _ _ _)    = True
+contIsRhsOrArg (ArgOf _ _ _ _) = True
+contIsRhsOrArg other          = False
+
+-------------------
 contIsDupable :: SimplCont -> Bool
-contIsDupable (Stop _)                  = True
+contIsDupable (Stop _ _ _)                      = True
 contIsDupable (ApplyTo  OkToDup _ _ _)   = True
-contIsDupable (ArgOf    OkToDup _ _)     = True
 contIsDupable (Select   OkToDup _ _ _ _) = True
 contIsDupable (CoerceIt _ cont)          = contIsDupable cont
 contIsDupable (InlinePlease cont)       = contIsDupable cont
 contIsDupable other                     = False
 
-pushArgs :: SubstEnv -> [InExpr] -> SimplCont -> SimplCont
-pushArgs se []         cont = cont
-pushArgs se (arg:args) cont = ApplyTo NoDup arg se (pushArgs se args cont)
+-------------------
+discardableCont :: SimplCont -> Bool
+discardableCont (Stop _ _ _)       = False
+discardableCont (CoerceIt _ cont)   = discardableCont cont
+discardableCont (InlinePlease cont) = discardableCont cont
+discardableCont other              = True
 
 discardCont :: SimplCont       -- A continuation, expecting
            -> SimplCont        -- Replace the continuation with a suitable coerce
-discardCont (Stop to_ty) = Stop to_ty
-discardCont cont        = CoerceIt to_ty (Stop to_ty)
-                        where
-                          to_ty = contResultType cont
+discardCont cont = case cont of
+                    Stop to_ty is_rhs _ -> cont
+                    other               -> CoerceIt to_ty (mkBoringStop to_ty)
+                where
+                  to_ty = contResultType cont
 
+-------------------
 contResultType :: SimplCont -> OutType
-contResultType (Stop to_ty)         = to_ty
-contResultType (ArgOf _ to_ty _)     = to_ty
+contResultType (Stop to_ty _ _)             = to_ty
+contResultType (ArgOf _ _ to_ty _)   = to_ty
 contResultType (ApplyTo _ _ _ cont)  = contResultType cont
 contResultType (CoerceIt _ cont)     = contResultType cont
 contResultType (InlinePlease cont)   = contResultType cont
 contResultType (Select _ _ _ _ cont) = contResultType cont
 
+-------------------
 countValArgs :: SimplCont -> Int
 countValArgs (ApplyTo _ (Type ty) se cont) = countValArgs cont
 countValArgs (ApplyTo _ val_arg   se cont) = 1 + countValArgs cont
@@ -131,11 +171,122 @@ countValArgs other                          = 0
 countArgs :: SimplCont -> Int
 countArgs (ApplyTo _ arg se cont) = 1 + countArgs cont
 countArgs other                          = 0
+
+-------------------
+pushContArgs :: SimplEnv -> [OutArg] -> SimplCont -> SimplCont
+-- Pushes args with the specified environment
+pushContArgs env []           cont = cont
+pushContArgs env (arg : args) cont = ApplyTo NoDup arg env (pushContArgs env args cont)
 \end{code}
 
 
-Comment about analyseCont
-~~~~~~~~~~~~~~~~~~~~~~~~~
+\begin{code}
+getContArgs :: SwitchChecker
+           -> OutId -> SimplCont 
+           -> ([(InExpr, SimplEnv, Bool)],     -- Arguments; the Bool is true for strict args
+               SimplCont,                      -- Remaining continuation
+               Bool)                           -- Whether we came across an InlineCall
+-- getContArgs id k = (args, k', inl)
+--     args are the leading ApplyTo items in k
+--     (i.e. outermost comes first)
+--     augmented with demand info from the functionn
+getContArgs chkr fun orig_cont
+  = let
+               -- Ignore strictness info if the no-case-of-case
+               -- flag is on.  Strictness changes evaluation order
+               -- and that can change full laziness
+       stricts | switchIsOn chkr NoCaseOfCase = vanilla_stricts
+               | otherwise                    = computed_stricts
+    in
+    go [] stricts False orig_cont
+  where
+    ----------------------------
+
+       -- Type argument
+    go acc ss inl (ApplyTo _ arg@(Type _) se cont)
+       = go ((arg,se,False) : acc) ss inl cont
+               -- NB: don't bother to instantiate the function type
+
+       -- Value argument
+    go acc (s:ss) inl (ApplyTo _ arg se cont)
+       = go ((arg,se,s) : acc) ss inl cont
+
+       -- An Inline continuation
+    go acc ss inl (InlinePlease cont)
+       = go acc ss True cont
+
+       -- We're run out of arguments, or else we've run out of demands
+       -- The latter only happens if the result is guaranteed bottom
+       -- This is the case for
+       --      * case (error "hello") of { ... }
+       --      * (error "Hello") arg
+       --      * f (error "Hello") where f is strict
+       --      etc
+    go acc ss inl cont 
+       | null ss && discardableCont cont = (reverse acc, discardCont cont, inl)
+       | otherwise                       = (reverse acc, cont,             inl)
+
+    ----------------------------
+    vanilla_stricts, computed_stricts :: [Bool]
+    vanilla_stricts  = repeat False
+    computed_stricts = zipWith (||) fun_stricts arg_stricts
+
+    ----------------------------
+    (val_arg_tys, _) = splitRepFunTys (idType fun)
+    arg_stricts      = map isStrictType val_arg_tys ++ repeat False
+       -- These argument types are used as a cheap and cheerful way to find
+       -- unboxed arguments, which must be strict.  But it's an InType
+       -- and so there might be a type variable where we expect a function
+       -- type (the substitution hasn't happened yet).  And we don't bother
+       -- doing the type applications for a polymorphic function.
+       -- Hence the split*Rep*FunTys
+
+    ----------------------------
+       -- If fun_stricts is finite, it means the function returns bottom
+       -- after that number of value args have been consumed
+       -- Otherwise it's infinite, extended with False
+    fun_stricts
+      = case splitStrictSig (idNewStrictness fun) of
+         (demands, result_info)
+               | not (demands `lengthExceeds` countValArgs orig_cont)
+               ->      -- Enough args, use the strictness given.
+                       -- For bottoming functions we used to pretend that the arg
+                       -- is lazy, so that we don't treat the arg as an
+                       -- interesting context.  This avoids substituting
+                       -- top-level bindings for (say) strings into 
+                       -- calls to error.  But now we are more careful about
+                       -- inlining lone variables, so its ok (see SimplUtils.analyseCont)
+                  if isBotRes result_info then
+                       map isStrictDmd demands         -- Finite => result is bottom
+                  else
+                       map isStrictDmd demands ++ vanilla_stricts
+
+         other -> vanilla_stricts      -- Not enough args, or no strictness
+
+-------------------
+interestingArg :: OutExpr -> Bool
+       -- An argument is interesting if it has *some* structure
+       -- We are here trying to avoid unfolding a function that
+       -- is applied only to variables that have no unfolding
+       -- (i.e. they are probably lambda bound): f x y z
+       -- There is little point in inlining f here.
+interestingArg (Var v)          = hasSomeUnfolding (idUnfolding v)
+                                       -- Was: isValueUnfolding (idUnfolding v')
+                                       -- But that seems over-pessimistic
+interestingArg (Type _)                 = False
+interestingArg (App fn (Type _)) = interestingArg fn
+interestingArg (Note _ a)       = interestingArg a
+interestingArg other            = True
+       -- Consider     let x = 3 in f x
+       -- The substitution will contain (x -> ContEx 3), and we want to
+       -- to say that x is an interesting argument.
+       -- But consider also (\x. f x y) y
+       -- The substitution will contain (x -> ContEx y), and we want to say
+       -- that x is not interesting (assuming y has no unfolding)
+\end{code}
+
+Comment about interestingCallContext
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We want to avoid inlining an expression where there can't possibly be
 any gain, such as in an argument position.  Hence, if the continuation
 is interesting (eg. a case scrutinee, application etc.) then we
@@ -168,13 +319,9 @@ contIsInteresting looks for case expressions with just a single
 default case.
 
 \begin{code}
-analyseCont :: InScopeSet -> SimplCont
-           -> ([Bool],         -- Arg-info flags; one for each value argument
-               Bool,           -- Context of the result of the call is interesting
-               Bool)           -- There was an InlinePlease 
-
-analyseCont in_scope cont 
-  = case cont of
+interestingCallContext :: Bool                 -- False <=> no args at all
+                      -> Bool          -- False <=> no value args
+                      -> SimplCont -> Bool
        -- The "lone-variable" case is important.  I spent ages
        -- messing about with unsatisfactory varaints, but this is nice.
        -- The idea is that if a variable appear all alone
@@ -182,11 +329,15 @@ analyseCont in_scope cont
        --      as scrutinee of a case          Select
        --      as arg of a strict fn           ArgOf
        -- then we should not inline it (unless there is some other reason,
-       -- e.g. is is the sole occurrence).  
-       -- Why not?  At least in the case-scrutinee situation, turning
-       --      case x of y -> ...
+       -- e.g. is is the sole occurrence).  We achieve this by making
+       -- interestingCallContext return False for a lone variable.
+       --
+       -- Why?  At least in the case-scrutinee situation, turning
+       --      let x = (a,b) in case x of y -> ...
        -- into
-       --      let y = (a,b) in ...
+       --      let x = (a,b) in case (a,b) of y -> ...
+       -- and thence to 
+       --      let x = (a,b) in let y = (a,b) in ...
        -- is bad if the binding for x will remain.
        --
        -- Another example: I discovered that strings
@@ -195,66 +346,34 @@ analyseCont in_scope cont
        --      s = "foo"
        --      f = \x -> ...(error s)...
 
-       -- Fundamentally such contexts should not ecourage inlining becuase
+       -- Fundamentally such contexts should not ecourage inlining because
        -- the context can ``see'' the unfolding of the variable (e.g. case or a RULE)
        -- so there's no gain.
        --
-       -- However, even a type application isn't a lone variable.  Consider
+       -- However, even a type application or coercion isn't a lone variable.
+       -- Consider
        --      case $fMonadST @ RealWorld of { :DMonad a b c -> c }
        -- We had better inline that sucker!  The case won't see through it.
-
-      (Stop _)                   -> boring_result              -- Don't inline a lone variable
-      (Select _ _ _ _ _)         -> boring_result              -- Ditto
-      (ArgOf _ _ _)              -> boring_result              -- Ditto
-      (ApplyTo _ (Type _) _ cont) -> analyse_ty_app cont
-      other                      -> analyse_app cont
+       --
+       -- For now, I'm treating treating a variable applied to types 
+       -- in a *lazy* context "lone". The motivating example was
+       --      f = /\a. \x. BIG
+       --      g = /\a. \y.  h (f a)
+       -- There's no advantage in inlining f here, and perhaps
+       -- a significant disadvantage.  Hence some_val_args in the Stop case
+
+interestingCallContext some_args some_val_args cont
+  = interesting cont
   where
-    boring_result = ([], False, False)
-
-               -- For now, I'm treating not treating a variable applied to types as
-               -- "lone". The motivating example was
-               --      f = /\a. \x. BIG
-               --      g = /\a. \y.  h (f a)
-               -- There's no advantage in inlining f here, and perhaps
-               -- a significant disadvantage.
-    analyse_ty_app (Stop _)                    = boring_result
-    analyse_ty_app (ArgOf _ _ _)               = boring_result
-    analyse_ty_app (Select _ _ _ _ _)          = ([], True, False)     -- See the $fMonadST example above
-    analyse_ty_app (ApplyTo _ (Type _) _ cont) = analyse_ty_app cont
-    analyse_ty_app cont                                = analyse_app cont
-
-    analyse_app (InlinePlease cont)  
-       = case analyse_app cont of
-                (infos, icont, inline) -> (infos, icont, True)
-
-    analyse_app (ApplyTo _ arg subst cont) 
-       | isValArg arg = case analyse_app cont of
-                          (infos, icont, inline) -> (analyse_arg subst arg : infos, icont, inline)
-       | otherwise    = analyse_app cont
-
-    analyse_app cont = ([], interesting_call_context cont, False)
-
-       -- An argument is interesting if it has *some* structure
-       -- We are here trying to avoid unfolding a function that
-       -- is applied only to variables that have no unfolding
-       -- (i.e. they are probably lambda bound): f x y z
-       -- There is little point in inlining f here.
-    analyse_arg :: SubstEnv -> InExpr -> Bool
-    analyse_arg subst (Var v)          = case lookupIdSubst (mkSubst in_scope subst) v of
-                                               DoneId v' _ -> isValueUnfolding (idUnfolding v')
-                                               other       -> False
-    analyse_arg subst (Type _)         = False
-    analyse_arg subst (App fn (Type _)) = analyse_arg subst fn
-    analyse_arg subst (Note _ a)       = analyse_arg subst a
-    analyse_arg subst other            = True
-
-    interesting_call_context (Stop ty)                  = canUpdateInPlace ty
-    interesting_call_context (InlinePlease _)           = True
-    interesting_call_context (Select _ _ _ _ _)          = True
-    interesting_call_context (CoerceIt _ cont)           = interesting_call_context cont
-    interesting_call_context (ApplyTo _ (Type _) _ cont) = interesting_call_context cont
-    interesting_call_context (ApplyTo _ _       _ _)    = True
-    interesting_call_context (ArgOf _ _ _)              = True
+    interesting (InlinePlease _)       = True
+    interesting (Select _ _ _ _ _)     = some_args
+    interesting (ApplyTo _ _ _ _)      = True  -- Can happen if we have (coerce t (f x)) y
+                                               -- Perhaps True is a bit over-keen, but I've
+                                               -- seen (coerce f) x, where f has an INLINE prag,
+                                               -- So we have to give some motivaiton for inlining it
+    interesting (ArgOf _ _ _ _)                 = some_val_args
+    interesting (Stop ty _ upd_in_place) = some_val_args && upd_in_place
+    interesting (CoerceIt _ cont)        = interesting cont
        -- If this call is the arg of a strict function, the context
        -- is a bit interesting.  If we inline here, we may get useful
        -- evaluation information to avoid repeated evals: e.g.
@@ -271,11 +390,8 @@ analyseCont in_scope cont
        -- the context for (f x) is not totally uninteresting.
 
 
-discardInline :: SimplCont -> SimplCont
-discardInline (InlinePlease cont)  = cont
-discardInline (ApplyTo d e s cont) = ApplyTo d e s (discardInline cont)
-discardInline cont                = cont
-
+-------------------
+canUpdateInPlace :: Type -> Bool
 -- Consider   let x = <wurble> in ...
 -- If <wurble> returns an explicit constructor, we might be able
 -- to do update in place.  So we treat even a thunk RHS context
@@ -284,11 +400,16 @@ discardInline cont                   = cont
 -- small arity.  But arity zero isn't good -- we share the single copy
 -- for that case, so no point in sharing.
 
-canUpdateInPlace ty = case splitAlgTyConApp_maybe ty of
-                       Just (_, _, [dc]) -> arity == 1 || arity == 2
-                                         where
-                                            arity = dataConRepArity dc
-                       other -> False
+canUpdateInPlace ty 
+  | not opt_UF_UpdateInPlace = False
+  | otherwise
+  = case splitTyConApp_maybe ty of 
+       Nothing         -> False 
+       Just (tycon, _) -> case tyConDataConsIfAvailable tycon of
+                               [dc]  -> arity == 1 || arity == 2
+                                     where
+                                        arity = dataConRepArity dc
+                               other -> False
 \end{code}
 
 
@@ -299,37 +420,45 @@ canUpdateInPlace ty = case splitAlgTyConApp_maybe ty of
 %*                                                                     *
 %************************************************************************
 
+These functions are in the monad only so that they can be made strict via seq.
+
 \begin{code}
-simplBinders :: [InBinder] -> ([OutBinder] -> SimplM a) -> SimplM a
-simplBinders bndrs thing_inside
-  = getSubst           `thenSmpl` \ subst ->
-    let
-       (subst', bndrs') = substBndrs subst bndrs
+simplBinders :: SimplEnv -> [InBinder] -> SimplM (SimplEnv, [OutBinder])
+simplBinders env bndrs
+  = let
+       (subst', bndrs') = Subst.simplBndrs (getSubst env) bndrs
     in
     seqBndrs bndrs'    `seq`
-    setSubst subst' (thing_inside bndrs')
+    returnSmpl (setSubst env subst', bndrs')
 
-simplBinder :: InBinder -> (OutBinder -> SimplM a) -> SimplM a
-simplBinder bndr thing_inside
-  = getSubst           `thenSmpl` \ subst ->
-    let
-       (subst', bndr') = substBndr subst bndr
+simplBinder :: SimplEnv -> InBinder -> SimplM (SimplEnv, OutBinder)
+simplBinder env bndr
+  = let
+       (subst', bndr') = Subst.simplBndr (getSubst env) bndr
     in
     seqBndr bndr'      `seq`
-    setSubst subst' (thing_inside bndr')
+    returnSmpl (setSubst env subst', bndr')
 
 
--- Same semantics as simplBinders, but a little less 
--- plumbing and hence a little more efficient.
--- Maybe not worth the candle?
-simplIds :: [InBinder] -> ([OutBinder] -> SimplM a) -> SimplM a
-simplIds ids thing_inside
-  = getSubst           `thenSmpl` \ subst ->
-    let
-       (subst', bndrs') = substIds subst ids
+simplLetBndr :: SimplEnv -> InBinder -> SimplM (SimplEnv, OutBinder)
+simplLetBndr env id
+  = let
+       (subst', id') = Subst.simplLetId (getSubst env) id
+    in
+    seqBndr id'                `seq`
+    returnSmpl (setSubst env subst', id')
+
+simplLamBndrs, simplRecBndrs 
+       :: SimplEnv -> [InBinder] -> SimplM (SimplEnv, [OutBinder])
+simplRecBndrs = simplBndrs Subst.simplLetId
+simplLamBndrs = simplBndrs Subst.simplLamBndr
+
+simplBndrs simpl_bndr env bndrs
+  = let
+       (subst', bndrs') = mapAccumL simpl_bndr (getSubst env) bndrs
     in
     seqBndrs bndrs'    `seq`
-    setSubst subst' (thing_inside bndrs')
+    returnSmpl (setSubst env subst', bndrs')
 
 seqBndrs [] = ()
 seqBndrs (b:bs) = seqBndr b `seq` seqBndrs bs
@@ -341,32 +470,130 @@ seqBndr b | isTyVar b = b `seq` ()
 \end{code}
 
 
+\begin{code}
+newId :: UserFS -> Type -> SimplM Id
+newId fs ty = getUniqueSmpl    `thenSmpl` \ uniq ->
+             returnSmpl (mkSysLocal fs uniq ty)
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Rebuilding a lambda}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+mkLam :: SimplEnv -> [OutBinder] -> OutExpr -> SimplCont -> SimplM FloatsWithExpr
+\end{code}
+
+Try three things
+       a) eta reduction, if that gives a trivial expression
+       b) eta expansion [only if there are some value lambdas]
+       c) floating lets out through big lambdas 
+               [only if all tyvar lambdas, and only if this lambda
+                is the RHS of a let]
+
+\begin{code}
+mkLam env bndrs body cont
+ | opt_SimplDoEtaReduction,
+   Just etad_lam <- tryEtaReduce bndrs body
+ = tick (EtaReduction (head bndrs))    `thenSmpl_`
+   returnSmpl (emptyFloats env, etad_lam)
+
+ | opt_SimplDoLambdaEtaExpansion,
+   any isRuntimeVar bndrs
+ = tryEtaExpansion body                `thenSmpl` \ body' ->
+   returnSmpl (emptyFloats env, mkLams bndrs body')
+
+{-     Sept 01: I'm experimenting with getting the
+       full laziness pass to float out past big lambdsa
+ | all isTyVar bndrs,  -- Only for big lambdas
+   contIsRhs cont      -- Only try the rhs type-lambda floating
+                       -- if this is indeed a right-hand side; otherwise
+                       -- we end up floating the thing out, only for float-in
+                       -- to float it right back in again!
+ = tryRhsTyLam env bndrs body          `thenSmpl` \ (floats, body') ->
+   returnSmpl (floats, mkLams bndrs body')
+-}
+
+ | otherwise 
+ = returnSmpl (emptyFloats env, mkLams bndrs body)
+\end{code}
+
+
 %************************************************************************
 %*                                                                     *
-\subsection{Transform a RHS}
+\subsection{Eta expansion and reduction}
 %*                                                                     *
 %************************************************************************
 
-Try (a) eta expansion
-    (b) type-lambda swizzling
+We try for eta reduction here, but *only* if we get all the 
+way to an exprIsTrivial expression.    
+We don't want to remove extra lambdas unless we are going 
+to avoid allocating this thing altogether
 
 \begin{code}
-transformRhs :: InExpr -> SimplM InExpr
-transformRhs rhs 
-  = tryEtaExpansion body               `thenSmpl` \ body' ->
-    mkRhsTyLam tyvars body'
+tryEtaReduce :: [OutBinder] -> OutExpr -> Maybe OutExpr
+tryEtaReduce bndrs body 
+       -- We don't use CoreUtils.etaReduce, because we can be more
+       -- efficient here:
+       --  (a) we already have the binders
+       --  (b) we can do the triviality test before computing the free vars
+       --      [in fact I take the simple path and look for just a variable]
+  = go (reverse bndrs) body
   where
-    (tyvars, body) = collectTyBinders rhs
+    go (b : bs) (App fun arg) | ok_arg b arg = go bs fun       -- Loop round
+    go []       (Var fun)     | ok_fun fun   = Just (Var fun)  -- Success!
+    go _        _                           = Nothing          -- Failure!
+
+    ok_fun fun   = not (fun `elem` bndrs) && 
+                  isEvaldUnfolding (idUnfolding fun)
+       -- The exprIsValue is because eta reduction is not 
+       -- valid in general:  \x. bot  /=  bot
+       -- So we need to be sure that the "fun" is a value.
+    ok_arg b arg = varToCoreExpr b `cheapEqExpr` arg
+\end{code}
+
+
+       Try eta expansion for RHSs
+
+We go for:
+   f = \x1..xn -> N  ==>   f = \x1..xn y1..ym -> N y1..ym
+                                (n >= 0)
+
+where (in both cases) 
+
+       * The xi can include type variables
+
+       * The yi are all value variables
+
+       * N is a NORMAL FORM (i.e. no redexes anywhere)
+         wanting a suitable number of extra args.
+
+We may have to sandwich some coerces between the lambdas
+to make the types work.   exprEtaExpandArity looks through coerces
+when computing arity; and etaExpand adds the coerces as necessary when
+actually computing the expansion.
+
+\begin{code}
+tryEtaExpansion :: OutExpr -> SimplM OutExpr
+-- There is at least one runtime binder in the binders
+tryEtaExpansion body
+  = getUniquesSmpl                     `thenSmpl` \ us ->
+    returnSmpl (etaExpand fun_arity us body (exprType body))
+  where
+    fun_arity = exprEtaExpandArity body
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Local tyvar-lifting}
+\subsection{Floating lets out of big lambdas}
 %*                                                                     *
 %************************************************************************
 
-mkRhsTyLam tries this transformation, when the big lambda appears as
+tryRhsTyLam tries this transformation, when the big lambda appears as
 the RHS of a let(rec) binding:
 
        /\abc -> let(rec) x = e in b
@@ -389,7 +616,7 @@ let-floating.
 This optimisation is CRUCIAL in eliminating the junk introduced by
 desugaring mutually recursive definitions.  Don't eliminate it lightly!
 
-So far as the implemtation is concerned:
+So far as the implementation is concerned:
 
        Invariant: go F e = /\tvs -> F e
        
@@ -431,30 +658,42 @@ as we would normally do.
 
 
 \begin{code}
-mkRhsTyLam tyvars body                 -- Only does something if there's a let
-  | null tyvars || not (worth_it body) -- inside a type lambda, and a WHNF inside that
-  = returnSmpl (mkLams tyvars body)
+{-     Trying to do this in full laziness
+
+tryRhsTyLam :: SimplEnv -> [OutTyVar] -> OutExpr -> SimplM FloatsWithExpr
+-- Call ensures that all the binders are type variables
+
+tryRhsTyLam env tyvars body            -- Only does something if there's a let
+  |  not (all isTyVar tyvars)
+  || not (worth_it body)               -- inside a type lambda, 
+  = returnSmpl (emptyFloats env, body) -- and a WHNF inside that
+
   | otherwise
-  = go (\x -> x) body
+  = go env (\x -> x) body
+
   where
-    worth_it (Let _ e)      = whnf_in_middle e
-    worth_it other                  = False
+    worth_it e@(Let _ _) = whnf_in_middle e
+    worth_it e          = False
+
+    whnf_in_middle (Let (NonRec x rhs) e) | isUnLiftedType (idType x) = False
     whnf_in_middle (Let _ e) = whnf_in_middle e
     whnf_in_middle e        = exprIsCheap e
 
     main_tyvar_set = mkVarSet tyvars
 
-    go fn (Let bind@(NonRec var rhs) body) | exprIsTrivial rhs
-      = go (fn . Let bind) body
+    go env fn (Let bind@(NonRec var rhs) body)
+      | exprIsTrivial rhs
+      = go env (fn . Let bind) body
+
+    go env fn (Let (NonRec var rhs) body)
+      = mk_poly tyvars_here var                                                        `thenSmpl` \ (var', rhs') ->
+       addAuxiliaryBind env (NonRec var' (mkLams tyvars_here (fn rhs)))        $ \ env -> 
+       go env (fn . Let (mk_silly_bind var rhs')) body
 
-    go fn (Let bind@(NonRec var rhs) body)
-      = mk_poly tyvars_here var                                `thenSmpl` \ (var', rhs') ->
-       go (fn . Let (mk_silly_bind var rhs')) body     `thenSmpl` \ body' ->
-       returnSmpl (Let (NonRec var' (mkLams tyvars_here (fn rhs))) body')
       where
-       tyvars_here = tyvars
-               -- varSetElems (main_tyvar_set `intersectVarSet` tyVarsOfType var_ty)
-               -- tyvars_here was an attempt to reduce the number of tyvars
+
+       tyvars_here = varSetElems (main_tyvar_set `intersectVarSet` exprSomeFreeVars isTyVar rhs)
+               -- Abstract only over the type variables free in the rhs
                -- wrt which the new binding is abstracted.  But the naive
                -- approach of abstract wrt the tyvars free in the Id's type
                -- fails. Consider:
@@ -470,273 +709,429 @@ mkRhsTyLam tyvars body                  -- Only does something if there's a let
                -- abstracting wrt *all* the tyvars.  We'll see if that
                -- gives rise to problems.   SLPJ June 98
 
-       var_ty = idType var
-
-    go fn (Let (Rec prs) body)
+    go env fn (Let (Rec prs) body)
        = mapAndUnzipSmpl (mk_poly tyvars_here) vars    `thenSmpl` \ (vars', rhss') ->
         let
-           gn body = fn $ foldr Let body (zipWith mk_silly_bind vars rhss')
+           gn body = fn (foldr Let body (zipWith mk_silly_bind vars rhss'))
+           pairs   = vars' `zip` [mkLams tyvars_here (gn rhs) | rhs <- rhss]
         in
-        go gn body                             `thenSmpl` \ body' ->
-        returnSmpl (Let (Rec (vars' `zip` [mkLams tyvars_here (gn rhs) | rhs <- rhss])) body')
+        addAuxiliaryBind env (Rec pairs)               $ \ env ->
+        go env gn body 
        where
         (vars,rhss) = unzip prs
-        tyvars_here = tyvars
-               -- varSetElems (main_tyvar_set `intersectVarSet` tyVarsOfTypes var_tys)
+        tyvars_here = varSetElems (main_tyvar_set `intersectVarSet` exprsSomeFreeVars isTyVar (map snd prs))
                -- See notes with tyvars_here above
 
-        var_tys     = map idType vars
-
-    go fn body = returnSmpl (mkLams tyvars (fn body))
+    go env fn body = returnSmpl (emptyFloats env, fn body)
 
     mk_poly tyvars_here var
       = getUniqueSmpl          `thenSmpl` \ uniq ->
        let
            poly_name = setNameUnique (idName var) uniq         -- Keep same name
            poly_ty   = mkForAllTys tyvars_here (idType var)    -- But new type of course
+           poly_id   = mkLocalId poly_name poly_ty 
 
-               -- It's crucial to copy the occInfo of the original var, because
-               -- we're looking at occurrence-analysed but as yet unsimplified code!
-               -- In particular, we mustn't lose the loop breakers.
+               -- In the olden days, it was crucial to copy the occInfo of the original var, 
+               -- because we were looking at occurrence-analysed but as yet unsimplified code!
+               -- In particular, we mustn't lose the loop breakers.  BUT NOW we are looking
+               -- at already simplified code, so it doesn't matter
                -- 
                -- It's even right to retain single-occurrence or dead-var info:
                -- Suppose we started with  /\a -> let x = E in B
-               -- where x occurs once in E. Then we transform to:
+               -- where x occurs once in B. Then we transform to:
                --      let x' = /\a -> E in /\a -> let x* = x' a in B
                -- where x* has an INLINE prag on it.  Now, once x* is inlined,
-               -- the occurrences of x' will be just the occurrences originaly
+               -- the occurrences of x' will be just the occurrences originally
                -- pinned on x.
-           poly_info = vanillaIdInfo `setOccInfo` idOccInfo var
-
-           poly_id   = mkId poly_name poly_ty poly_info
        in
        returnSmpl (poly_id, mkTyApps (Var poly_id) (mkTyVarTys tyvars_here))
 
-    mk_silly_bind var rhs = NonRec var rhs
-               -- The Inline note is really important!  If we don't say 
-               -- INLINE on these silly little bindings then look what happens!
+    mk_silly_bind var rhs = NonRec var (Note InlineMe rhs)
                -- Suppose we start with:
                --
-               --      x = let g = /\a -> \x -> f x x
-               --          in 
-               --          /\ b -> let g* = g b in E
+               --      x = /\ a -> let g = G in E
+               --
+               -- Then we'll float to get
+               --
+               --      x = let poly_g = /\ a -> G
+               --          in /\ a -> let g = poly_g a in E
                --
-               -- Then:        * the binding for g gets floated out
-               --              * but then it gets inlined into the rhs of g*
-               --              * then the binding for g* is floated out of the /\b
-               --              * so we're back to square one
-               -- The silly binding for g* must be INLINEd, so that
-               -- we simply substitute for g* throughout.
+               -- But now the occurrence analyser will see just one occurrence
+               -- of poly_g, not inside a lambda, so the simplifier will
+               -- PreInlineUnconditionally poly_g back into g!  Badk to square 1!
+               -- (I used to think that the "don't inline lone occurrences" stuff
+               --  would stop this happening, but since it's the *only* occurrence,
+               --  PreInlineUnconditionally kicks in first!)
+               --
+               -- Solution: put an INLINE note on g's RHS, so that poly_g seems
+               --           to appear many times.  (NB: mkInlineMe eliminates
+               --           such notes on trivial RHSs, so do it manually.)
+-}
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Eta expansion}
+\subsection{Case absorption and identity-case elimination}
 %*                                                                     *
 %************************************************************************
 
-       Try eta expansion for RHSs
+mkCase puts a case expression back together, trying various transformations first.
 
-We go for:
-               \x1..xn -> N    ==>   \x1..xn y1..ym -> N y1..ym
-       AND             
-               N E1..En        ==>   let z1=E1 .. zn=En in \y1..ym -> N z1..zn y1..ym
+\begin{code}
+mkCase :: OutExpr -> [AltCon] -> OutId -> [OutAlt] -> SimplM OutExpr
 
-where (in both cases) N is a NORMAL FORM (i.e. no redexes anywhere)
-wanting a suitable number of extra args.
+mkCase scrut handled_cons case_bndr alts
+  = mkAlts scrut handled_cons case_bndr alts   `thenSmpl` \ better_alts ->
+    mkCase1 scrut case_bndr better_alts
+\end{code}
+
+
+mkAlts tries these things:
+
+1.  If several alternatives are identical, merge them into
+    a single DEFAULT alternative.  I've occasionally seen this 
+    making a big difference:
+
+       case e of               =====>     case e of
+         C _ -> f x                         D v -> ....v....
+         D v -> ....v....                   DEFAULT -> f x
+         DEFAULT -> f x
+
+   The point is that we merge common RHSs, at least for the DEFAULT case.
+   [One could do something more elaborate but I've never seen it needed.]
+   To avoid an expensive test, we just merge branches equal to the *first*
+   alternative; this picks up the common cases
+       a) all branches equal
+       b) some branches equal to the DEFAULT (which occurs first)
+
+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.
+
+3.  Case merging:
+       case e of b {             ==>   case e of b {
+        p1 -> rhs1                      p1 -> rhs1
+        ...                             ...
+        pm -> rhsm                      pm -> rhsm
+        _  -> case b of b' {            pn -> let b'=b in rhsn
+                    pn -> rhsn          ...
+                    ...                 po -> let b'=b in rhso
+                    po -> rhso          _  -> let b'=b in rhsd
+                    _  -> rhsd
+       }  
+    
+    which merges two cases in one case when -- the default alternative of
+    the outer case scrutises the same variable as the outer case This
+    transformation is called Case Merging.  It avoids that the same
+    variable is scrutinised multiple times.
+
+
+The case where transformation (1) showed up was like this (lib/std/PrelCError.lhs):
+
+       x | p `is` 1 -> e1
+         | p `is` 2 -> e2
+       ...etc...
+
+where @is@ was something like
+       
+       p `is` n = p /= (-1) && p == n
+
+This gave rise to a horrible sequence of cases
+
+       case p of
+         (-1) -> $j p
+         1    -> e1
+         DEFAULT -> $j p
+
+and similarly in cascade for all the join points!
 
-NB: the Ei may have unlifted type, but the simplifier (which is applied
-to the result) deals OK with this.
 
-There is no point in looking for a combination of the two, 
-because that would leave use with some lets sandwiched between lambdas;
-that's what the final test in the first equation is for.
 
 \begin{code}
-tryEtaExpansion :: InExpr -> SimplM InExpr
-tryEtaExpansion rhs
-  |  not opt_SimplDoLambdaEtaExpansion
-  || exprIsTrivial rhs                         -- Don't eta-expand a trival RHS
-  || null y_tys                                        -- No useful expansion
-  || not (null x_bndrs || and trivial_args)    -- Not (no x-binders or no z-binds)
-  = returnSmpl rhs
-
-  | otherwise  -- Consider eta expansion
-  = newIds y_tys                                               $ ( \ y_bndrs ->
-    tick (EtaExpansion (head y_bndrs))                         `thenSmpl_`
-    mapAndUnzipSmpl bind_z_arg (args `zip` trivial_args)       `thenSmpl` (\ (maybe_z_binds, z_args) ->
-    returnSmpl (mkLams x_bndrs                         $ 
-               mkLets (catMaybes maybe_z_binds)        $
-               mkLams y_bndrs                          $
-               mkApps (mkApps fun z_args) (map Var y_bndrs))))
+--------------------------------------------------
+--     1. Merge identical branches
+--------------------------------------------------
+mkAlts scrut handled_cons case_bndr alts@((con1,bndrs1,rhs1) : con_alts)
+  | all isDeadBinder bndrs1,                   -- Remember the default 
+    length filtered_alts < length con_alts     -- alternative comes first
+  = tick (AltMerge case_bndr)                  `thenSmpl_`
+    returnSmpl better_alts
   where
-    (x_bndrs, body) = collectValBinders rhs
-    (fun, args)            = collectArgs body
-    trivial_args    = map exprIsTrivial args
-    fun_arity      = exprEtaExpandArity fun
-
-    bind_z_arg (arg, trivial_arg) 
-       | trivial_arg = returnSmpl (Nothing, arg)
-        | otherwise   = newId (exprType arg)   $ \ z ->
-                       returnSmpl (Just (NonRec z arg), Var z)
-
-       -- Note: I used to try to avoid the exprType call by using
-       -- the type of the binder.  But this type doesn't necessarily
-       -- belong to the same substitution environment as this rhs;
-       -- and we are going to make extra term binders (y_bndrs) from the type
-       -- which will be processed with the rhs substitution environment.
-       -- This only went wrong in a mind bendingly complicated case.
-    (potential_extra_arg_tys, inner_ty) = splitFunTys (exprType body)
-       
-    y_tys :: [InType]
-    y_tys  = take no_extras_wanted potential_extra_arg_tys
-       
-    no_extras_wanted :: Int
-    no_extras_wanted = 0 `max`
-
-       -- We used to expand the arity to the previous arity fo the
-       -- function; but this is pretty dangerous.  Consdier
-       --      f = \xy -> e
-       -- so that f has arity 2.  Now float something into f's RHS:
-       --      f = let z = BIG in \xy -> e
-       -- The last thing we want to do now is to put some lambdas
-       -- outside, to get
-       --      f = \xy -> let z = BIG in e
-       --
-       -- (bndr_arity - no_of_xs)              `max`
-
-       -- See if the body could obviously do with more args
-       (fun_arity - valArgCount args)
-
--- This case is now deal with by exprEtaExpandArity
-       -- Finally, see if it's a state transformer, and xs is non-null
-       -- (so it's also a function not a thunk) in which
-       -- case we eta-expand on principle! This can waste work,
-       -- but usually doesn't.
-       -- I originally checked for a singleton type [ty] in this case
-       -- but then I found a situation in which I had
-       --      \ x -> let {..} in \ s -> f (...) s
-       -- AND f RETURNED A FUNCTION.  That is, 's' wasn't the only
-       -- potential extra arg.
---     case (x_bndrs, potential_extra_arg_tys) of
---         (_:_, ty:_)  -> case splitTyConApp_maybe ty of
---                               Just (tycon,_) | tycon == statePrimTyCon -> 1
---                               other                                    -> 0
---         other -> 0
-\end{code}
+    filtered_alts       = filter keep con_alts
+    keep (con,bndrs,rhs) = not (all isDeadBinder bndrs && rhs `cheapEqExpr` rhs1)
+    better_alts                 = (DEFAULT, [], rhs1) : filtered_alts
 
 
-%************************************************************************
-%*                                                                     *
-\subsection{Case absorption and identity-case elimination}
-%*                                                                     *
-%************************************************************************
+--------------------------------------------------
+--     2. Fill in missing constructor
+--------------------------------------------------
 
-\begin{code}
-mkCase :: OutExpr -> OutId -> [OutAlt] -> SimplM OutExpr
-\end{code}
+mkAlts scrut handled_cons case_bndr alts
+  | (alts_no_deflt, Just rhs) <- findDefault alts,
+                       -- There is a DEFAULT case
 
-@mkCase@ tries the following transformation (if possible):
-
-case e of b {             ==>   case e of b {
-  p1 -> rhs1                     p1 -> rhs1
-  ...                            ...
-  pm -> rhsm                      pm -> rhsm
-  _  -> case b of b' {            pn -> rhsn[b/b'] {or (alg)  let b=b' in rhsn}
-                                                  {or (prim) case b of b' { _ -> rhsn}}
-             pn -> rhsn          ...
-             ...                 po -> rhso[b/b']
-             po -> rhso          _  -> rhsd[b/b'] {or let b'=b in rhsd}
-             _  -> rhsd
-}
-
-which merges two cases in one case when -- the default alternative of
-the outer case scrutises the same variable as the outer case This
-transformation is called Case Merging.  It avoids that the same
-variable is scrutinised multiple times.
+    Just (tycon, inst_tys) <- splitTyConApp_maybe (idType case_bndr),
+    isAlgTyCon tycon,          -- It's a data type, tuple, or unboxed tuples.  
+    not (isNewTyCon tycon),    -- We can have a newtype, if we are just doing an eval:
+                               --      case x of { DEFAULT -> e }
+                               -- and we don't want to fill in a default for them!
 
-\begin{code}
-mkCase scrut outer_bndr outer_alts
-  |  opt_SimplCaseMerge
-  && maybeToBool maybe_case_in_default
-     
-  = tick (CaseMerge outer_bndr)                `thenSmpl_`
-    returnSmpl (Case scrut outer_bndr new_alts)
-       -- Warning: don't call mkCase recursively!
+    [missing_con] <- [con | con <- tyConDataConsIfAvailable tycon,
+                           not (con `elem` handled_data_cons)]
+                       -- There is just one missing constructor!
+
+  = tick (FillInCaseDefault case_bndr) `thenSmpl_`
+    getUniquesSmpl                     `thenSmpl` \ tv_uniqs ->
+    getUniquesSmpl                     `thenSmpl` \ id_uniqs ->
+    let
+       (_,_,ex_tyvars,_,_,_) = dataConSig missing_con
+       ex_tyvars'  = zipWith mk tv_uniqs ex_tyvars
+       mk uniq tv  = mkSysTyVar uniq (tyVarKind tv)
+       arg_ids     = zipWith (mkSysLocal SLIT("a")) id_uniqs arg_tys
+       arg_tys     = dataConArgTys missing_con (inst_tys ++ mkTyVarTys ex_tyvars')
+       better_alts = (DataAlt missing_con, ex_tyvars' ++ arg_ids, rhs) : alts_no_deflt
+    in
+    returnSmpl better_alts
+  where
+    handled_data_cons = [data_con | DataAlt data_con <- handled_cons]
+
+--------------------------------------------------
+--     3.  Merge nested cases
+--------------------------------------------------
+
+mkAlts scrut handled_cons outer_bndr outer_alts
+  | opt_SimplCaseMerge,
+    (outer_alts_without_deflt, maybe_outer_deflt)   <- findDefault outer_alts,
+    Just (Case (Var scrut_var) inner_bndr inner_alts) <- maybe_outer_deflt,
+    scruting_same_var scrut_var
+
+  = let            --  Eliminate any inner alts which are shadowed by the outer ones
+       outer_cons = [con | (con,_,_) <- outer_alts_without_deflt]
+    
+       munged_inner_alts = [ (con, args, munge_rhs rhs) 
+                           | (con, args, rhs) <- inner_alts, 
+                              not (con `elem` outer_cons)      -- Eliminate shadowed inner alts
+                           ]
+       munge_rhs rhs = bindCaseBndr inner_bndr (Var outer_bndr) rhs
+    
+       (inner_con_alts, maybe_inner_default) = findDefault munged_inner_alts
+
+       new_alts = add_default maybe_inner_default
+                              (outer_alts_without_deflt ++ inner_con_alts)
+    in
+    tick (CaseMerge outer_bndr)                                `thenSmpl_`
+    returnSmpl new_alts
+       -- Warning: don't call mkAlts recursively!
        -- Firstly, there's no point, because inner alts have already had
        -- mkCase applied to them, so they won't have a case in their default
-       -- Secondly, if you do, you get an infinite loop, because the bindNonRec
-       -- in munge_rhs puts a case into the DEFAULT branch!
+       -- Secondly, if you do, you get an infinite loop, because the bindCaseBndr
+       -- in munge_rhs may put a case into the DEFAULT branch!
   where
-    new_alts = outer_alts_without_deflt ++ munged_inner_alts
-    maybe_case_in_default = case findDefault outer_alts of
-                               (outer_alts_without_default,
-                                Just (Case (Var scrut_var) inner_bndr inner_alts))
-                                
-                                  | outer_bndr == scrut_var
-                                  -> Just (outer_alts_without_default, inner_bndr, inner_alts)
-                               other -> Nothing
-
-    Just (outer_alts_without_deflt, inner_bndr, inner_alts) = maybe_case_in_default
-
-               --  Eliminate any inner alts which are shadowed by the outer ones
-    outer_cons = [con | (con,_,_) <- outer_alts_without_deflt]
-
-    munged_inner_alts = [ (con, args, munge_rhs rhs) 
-                       | (con, args, rhs) <- inner_alts, 
-                          not (con `elem` outer_cons)  -- Eliminate shadowed inner alts
-                       ]
-    munge_rhs rhs = bindNonRec inner_bndr (Var outer_bndr) rhs
+       -- We are scrutinising the same variable if it's
+       -- the outer case-binder, or if the outer case scrutinises a variable
+       -- (and it's the same).  Testing both allows us not to replace the
+       -- outer scrut-var with the outer case-binder (Simplify.simplCaseBinder).
+    scruting_same_var = case scrut of
+                         Var outer_scrut -> \ v -> v == outer_bndr || v == outer_scrut
+                         other           -> \ v -> v == outer_bndr
+
+    add_default (Just rhs) alts = (DEFAULT,[],rhs) : alts
+    add_default Nothing    alts = alts
+
+
+--------------------------------------------------
+--     Catch-all
+--------------------------------------------------
+
+mkAlts scrut handled_cons case_bndr other_alts = returnSmpl other_alts
 \end{code}
 
-Now the identity-case transformation:
+
+
+=================================================================================
+
+mkCase1 tries these things
+
+1.  Eliminate the case altogether if possible
+
+2.  Case-identity:
 
        case e of               ===> e
-               True -> True;
+               True  -> True;
                False -> False
 
-and similar friends.
+    and similar friends.
+
+
+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!
+
+Actually, we 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:
+\begin{verbatim}
+       case x of
+         0#    -> ...
+         other -> ...(case x of
+                        0#    -> ...
+                        other -> ...) ...
+\end{code}
+Here the inner case can be eliminated.  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 
+       - x is used strictly, or
+       - e is already evaluated (it may so if e is a variable)
+
+Lastly, we generalise the transformation to handle this:
+
+       case e of       ===> r
+          True  -> r
+          False -> r
+
+We only do this for very cheaply compared r's (constructors, literals
+and variables).  If pedantic bottoms is on, we only do it when the
+scrutinee is a PrimOp which can't fail.
+
+We do it *here*, looking at un-simplified alternatives, because we
+have to check that r doesn't mention the variables bound by the
+pattern in each alternative, so the binder-info is rather useful.
+
+So the case-elimination algorithm is:
+
+       1. Eliminate alternatives which can't match
+
+       2. Check whether all the remaining alternatives
+               (a) do not mention in their rhs any of the variables bound in their pattern
+          and  (b) have equal rhss
+
+       3. Check we can safely ditch the case:
+                  * PedanticBottoms is off,
+               or * the scrutinee is an already-evaluated variable
+               or * the scrutinee is a primop which is ok for speculation
+                       -- ie we want to preserve divide-by-zero errors, and
+                       -- calls to error itself!
+
+               or * [Prim cases] the scrutinee is a primitive variable
+
+               or * [Alg cases] the scrutinee is a variable and
+                    either * the rhs is the same variable
+                       (eg case x of C a b -> x  ===>   x)
+                    or     * there is only one alternative, the default alternative,
+                               and the binder is used strictly in its scope.
+                               [NB this is helped by the "use default binder where
+                                possible" transformation; see below.]
+
+
+If so, then we can replace the case with one of the rhss.
+
 
 \begin{code}
-mkCase scrut case_bndr alts
+--------------------------------------------------
+--     1. Eliminate the case altogether if poss
+--------------------------------------------------
+
+mkCase1 scrut case_bndr [(con,bndrs,rhs)]
+  -- 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,
+
+       -- 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)
+       || exprIsValue 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
+  = tick (CaseElim case_bndr)                  `thenSmpl_` 
+    returnSmpl (bindCaseBndr case_bndr scrut 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)
+    var_demanded_later other   = False
+
+
+--------------------------------------------------
+--     2. Identity case
+--------------------------------------------------
+
+mkCase1 scrut case_bndr alts   -- Identity case
   | all identity_alt alts
   = tick (CaseIdentity case_bndr)              `thenSmpl_`
-    returnSmpl scrut
+    returnSmpl (re_note scrut)
   where
-    identity_alt (DEFAULT, [], Var v)     = v == case_bndr
-    identity_alt (DataAlt con, args, rhs) = cheapEqExpr rhs
-                                                       (mkConApp con (map Type arg_tys ++ map varToCoreExpr args))
-    identity_alt other                   = False
+    identity_alt (con, args, rhs) = de_note rhs `cheapEqExpr` identity_rhs con args
 
-    arg_tys = case splitTyConApp_maybe (idType case_bndr) of
-               Just (tycon, arg_tys) -> arg_tys
-\end{code}
+    identity_rhs (DataAlt con) args = mkConApp con (arg_tys ++ map varToCoreExpr args)
+    identity_rhs (LitAlt lit)  _    = Lit lit
+    identity_rhs DEFAULT       _    = Var case_bndr
 
-The catch-all case
+    arg_tys = map Type (tyConAppArgs (idType case_bndr))
 
-\begin{code}
-mkCase other_scrut case_bndr other_alts
-  = returnSmpl (Case other_scrut case_bndr other_alts)
+       -- We've seen this:
+       --      case coerce T e of x { _ -> coerce T' x }
+       -- And we definitely want to eliminate this case!
+       -- So we throw away notes from the RHS, and reconstruct
+       -- (at least an approximation) at the other end
+    de_note (Note _ e) = de_note e
+    de_note e         = e
+
+       -- re_note wraps a coerce if it might be necessary
+    re_note scrut = case head alts of
+                       (_,_,rhs1@(Note _ _)) -> mkCoerce (exprType rhs1) (idType case_bndr) scrut
+                       other                 -> scrut
+
+
+--------------------------------------------------
+--     Catch-all
+--------------------------------------------------
+mkCase1 scrut bndr alts = returnSmpl (Case scrut bndr alts)
 \end{code}
 
 
-\begin{code}
-findDefault :: [CoreAlt] -> ([CoreAlt], Maybe CoreExpr)
-findDefault []                         = ([], Nothing)
-findDefault ((DEFAULT,args,rhs) : alts) = ASSERT( null alts && null args ) 
-                                         ([], Just rhs)
-findDefault (alt : alts)               = case findDefault alts of 
-                                           (alts', deflt) -> (alt : alts', deflt)
-
-findAlt :: AltCon -> [CoreAlt] -> CoreAlt
-findAlt con alts
-  = go alts
-  where
-    go []          = pprPanic "Missing alternative" (ppr con $$ vcat (map ppr alts))
-    go (alt : alts) | matches alt = alt
-                   | otherwise   = go alts
+When adding auxiliary bindings for the case binder, it's worth checking if
+its dead, because it often is, and occasionally these mkCase transformations
+cascade rather nicely.
 
-    matches (DEFAULT, _, _) = True
-    matches (con1, _, _)    = con == con1
+\begin{code}
+bindCaseBndr bndr rhs body
+  | isDeadBinder bndr = body
+  | otherwise        = bindNonRec bndr rhs body
 \end{code}