[project @ 2001-09-26 16:19:28 by simonpj]
[ghc-hetmet.git] / ghc / compiler / simplCore / SimplUtils.lhs
index 90a759d..6ce4ada 100644 (file)
@@ -5,45 +5,52 @@
 
 \begin{code}
 module SimplUtils (
-       simplBinder, simplBinders, simplIds,
-       transformRhs,
-       mkCase, findAlt, findDefault,
+       simplBinder, simplBinders, simplRecIds, simplLetId, simplLamBinders,
+       tryEtaExpansion,
+       newId, mkLam, mkCase,
 
        -- The continuation type
-       SimplCont(..), DupFlag(..), contIsDupable, contResultType,
-       countValArgs, countArgs,
+       SimplCont(..), DupFlag(..), LetRhsFlag(..), 
+       contIsDupable, contResultType,
+       countValArgs, countArgs, 
+       mkBoringStop, mkStop, contIsRhs, contIsRhsOrArg,
        getContArgs, interestingCallContext, interestingArg, isStrictType, discardInline
 
     ) where
 
 #include "HsVersions.h"
 
-import CmdLineOpts     ( switchIsOn, SimplifierSwitch(..),
-                         opt_SimplDoLambdaEtaExpansion, opt_SimplCaseMerge, opt_DictsStrict
+import CmdLineOpts     ( SimplifierSwitch(..),
+                         opt_SimplDoLambdaEtaExpansion, opt_SimplDoEtaReduction,
+                         opt_SimplCaseMerge, opt_UF_UpdateInPlace
                        )
 import CoreSyn
-import CoreUnfold      ( isValueUnfolding )
-import CoreUtils       ( exprIsTrivial, cheapEqExpr, exprType, exprIsCheap, exprEtaExpandArity, bindNonRec )
-import Subst           ( InScopeSet, mkSubst, substBndrs, substBndr, substIds, lookupIdSubst )
-import Id              ( Id, idType, isId, idName, 
-                         idOccInfo, idUnfolding, idStrictness,
-                         mkId, idInfo
+import CoreFVs         ( exprSomeFreeVars, exprsSomeFreeVars )
+import CoreUtils       ( exprIsTrivial, cheapEqExpr, exprType, exprIsCheap, 
+                         etaExpand, exprEtaExpandArity, bindNonRec, mkCoerce,
+                         findDefault, exprOkForSpeculation, exprIsValue
                        )
-import IdInfo          ( StrictnessInfo(..), arityLowerBound, setOccInfo, vanillaIdInfo )
-import Maybes          ( maybeToBool, catMaybes )
-import Name            ( isLocalName, setNameUnique )
-import Demand          ( Demand, isStrict, wwLazy, wwLazy )
+import Subst           ( InScopeSet, mkSubst, substExpr )
+import qualified Subst ( simplBndrs, simplBndr, simplLetId, simplLamBndr )
+import Id              ( Id, idType, idName, 
+                         mkSysLocal, hasNoBinding, isDeadBinder, idNewDemandInfo,
+                         idUnfolding, idNewStrictness,
+                         mkLocalId, idInfo
+                       )
+import Name            ( setNameUnique )
+import NewDemand       ( isStrictDmd, isBotRes, splitStrictSig )
 import SimplMonad
-import Type            ( Type, tyVarsOfType, tyVarsOfTypes, mkForAllTys, seqType, repType,
-                         splitTyConApp_maybe, mkTyVarTys, applyTys, splitFunTys, mkFunTys,
-                         isDictTy, isDataType, applyTy, splitFunTy, isUnLiftedType,
-                         splitRepFunTys
+import Type            ( Type, mkForAllTys, seqType, 
+                         splitTyConApp_maybe, tyConAppArgs, mkTyVarTys,
+                         isUnLiftedType, splitRepFunTys, isStrictType
                        )
-import TyCon           ( tyConDataConsIfAvailable )
-import DataCon         ( dataConRepArity )
-import VarSet
-import VarEnv          ( SubstEnv, SubstResult(..) )
-import Util            ( lengthExceeds )
+import OccName         ( UserFS )
+import TyCon           ( tyConDataConsIfAvailable, isDataTyCon )
+import DataCon         ( dataConRepArity, dataConSig, dataConArgTys )
+import Var             ( mkSysTyVar, tyVarKind )
+import VarEnv          ( SubstEnv )
+import VarSet          ( mkVarSet, varSetElems, intersectVarSet )
+import Util            ( lengthExceeds, mapAccumL )
 import Outputable
 \end{code}
 
@@ -56,7 +63,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
@@ -65,27 +76,35 @@ 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 
                                --      of a strict function, or a primitive-arg fn
                                --      or a PrimOp
+            LetRhsFlag
             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   dup _ _ _)           = ptext SLIT("ArgOf...") <+> ppr dup
   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
@@ -97,11 +116,28 @@ 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 (ArgOf    OkToDup _ _ _)   = True
 contIsDupable (Select   OkToDup _ _ _ _) = True
 contIsDupable (CoerceIt _ cont)          = contIsDupable cont
 contIsDupable (InlinePlease cont)       = contIsDupable cont
@@ -115,22 +151,23 @@ discardInline cont                   = cont
 
 -------------------
 discardableCont :: SimplCont -> Bool
-discardableCont (Stop _)           = False
+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
@@ -149,17 +186,17 @@ countArgs other                     = 0
 
 
 \begin{code}
-getContArgs :: OutId -> SimplCont 
-           -> SimplM ([(InExpr, SubstEnv, Bool)],      -- Arguments; the Bool is true for strict args
-                       SimplCont,                      -- Remaining continuation
-                       Bool)                           -- Whether we came across an InlineCall
+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 fun orig_cont
-  = getSwitchChecker   `thenSmpl` \ chkr ->
-    let
+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
@@ -191,9 +228,8 @@ getContArgs fun orig_cont
        --      * f (error "Hello") where f is strict
        --      etc
     go acc ss inl cont 
-       | null ss && discardableCont cont = tick BottomFound    `thenSmpl_`
-                                           returnSmpl (reverse acc, discardCont cont, inl)
-       | otherwise                       = returnSmpl (reverse acc, cont,             inl)
+       | null ss && discardableCont cont = (reverse acc, discardCont cont, inl)
+       | otherwise                       = (reverse acc, cont,             inl)
 
     ----------------------------
     vanilla_stricts, computed_stricts :: [Bool]
@@ -215,8 +251,8 @@ getContArgs fun orig_cont
        -- after that number of value args have been consumed
        -- Otherwise it's infinite, extended with False
     fun_stricts
-      = case idStrictness fun of
-         StrictnessInfo demands result_bot 
+      = 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
@@ -225,26 +261,13 @@ getContArgs fun orig_cont
                        -- 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 result_bot then
-                       map isStrict demands            -- Finite => result is bottom
+                  if isBotRes result_info then
+                       map isStrictDmd demands         -- Finite => result is bottom
                   else
-                       map isStrict demands ++ vanilla_stricts
+                       map isStrictDmd demands ++ vanilla_stricts
 
          other -> vanilla_stricts      -- Not enough args, or no strictness
 
-
--------------------
-isStrictType :: Type -> Bool
-       -- isStrictType computes whether an argument (or let RHS) should
-       -- be computed strictly or lazily, based only on its type
-isStrictType ty
-  | isUnLiftedType ty                              = True
-  | opt_DictsStrict && isDictTy ty && isDataType ty = True
-  | otherwise                                      = False 
-       -- Return true only for dictionary types where the dictionary
-       -- has more than one component (else we risk poking on the component
-       -- of a newtype dictionary)
-
 -------------------
 interestingArg :: InScopeSet -> InExpr -> SubstEnv -> Bool
        -- An argument is interesting if it has *some* structure
@@ -253,23 +276,24 @@ interestingArg :: InScopeSet -> InExpr -> SubstEnv -> Bool
        -- (i.e. they are probably lambda bound): f x y z
        -- There is little point in inlining f here.
 interestingArg in_scope arg subst
-  = analyse arg
+  = analyse (substExpr (mkSubst in_scope subst) arg)
+       -- 'analyse' only looks at the top part of the result
+       -- and substExpr is lazy, so this isn't nearly as brutal
+       -- as it looks.
   where
-    analyse (Var v)
-       = case lookupIdSubst (mkSubst in_scope subst) v of
-           DoneId v' _ -> hasSomeUnfolding (idUnfolding v')
-                                       -- was: isValueUnfolding (idUnfolding v')
-                                       -- But that seems over-pessimistic
-
-           other       -> True         -- was: False
-                                       -- But that is *definitely* too pessimistic.
-                                       -- E.g.         let x = 3 in f 
-                                       -- Here, x will be unconditionally substituted, via
-                                       -- the substitution!
+    analyse (Var v)          = hasSomeUnfolding (idUnfolding v)
+                               -- Was: isValueUnfolding (idUnfolding v')
+                               -- But that seems over-pessimistic
     analyse (Type _)         = False
     analyse (App fn (Type _)) = analyse fn
     analyse (Note _ a)       = analyse a
     analyse 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
@@ -316,11 +340,15 @@ interestingCallContext :: Bool            -- False <=> no args at all
        --      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
@@ -329,16 +357,17 @@ interestingCallContext :: Bool            -- False <=> no args at all
        --      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.
        --
-       -- For now, I'm treating treating a variable applied to types as
-       -- "lone". The motivating example was
+       -- 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
@@ -347,12 +376,15 @@ interestingCallContext :: Bool            -- False <=> no args at all
 interestingCallContext some_args some_val_args cont
   = interesting cont
   where
-    interesting (InlinePlease _)   = True
-    interesting (ApplyTo _ _ _ _)  = some_args -- Can happen if we have (coerce t (f x)) y
-    interesting (Select _ _ _ _ _) = some_args
-    interesting (ArgOf _ _ _)     = some_val_args
-    interesting (Stop ty)         = some_val_args && canUpdateInPlace ty
-    interesting (CoerceIt _ cont)  = interesting cont
+    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.
@@ -379,18 +411,16 @@ canUpdateInPlace :: Type -> Bool
 -- small arity.  But arity zero isn't good -- we share the single copy
 -- for that case, so no point in sharing.
 
--- Note the repType: we want to look through newtypes for this purpose
-
-canUpdateInPlace ty = case splitTyConApp_maybe (repType ty) of {
-                       Nothing         -> False ;
-                       Just (tycon, _) -> 
-
-                     case tyConDataConsIfAvailable tycon of
-                       [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}
 
 
@@ -401,37 +431,49 @@ canUpdateInPlace ty = case splitTyConApp_maybe (repType 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
+simplLamBinders :: SimplEnv -> [InBinder] -> SimplM (SimplEnv, [OutBinder])
+simplLamBinders env bndrs
+  = let
+       (subst', bndrs') = mapAccumL Subst.simplLamBndr (getSubst env) bndrs
     in
     seqBndrs bndrs'    `seq`
-    setSubst subst' (thing_inside bndrs')
+    returnSmpl (setSubst env subst', bndrs')
+
+simplRecIds :: SimplEnv -> [InBinder] -> SimplM (SimplEnv, [OutBinder])
+simplRecIds env ids
+  = let
+       (subst', ids') = mapAccumL Subst.simplLetId (getSubst env) ids
+    in
+    seqBndrs ids'      `seq`
+    returnSmpl (setSubst env subst', ids')
+
+simplLetId :: SimplEnv -> InBinder -> SimplM (SimplEnv, OutBinder)
+simplLetId env id
+  = let
+       (subst', id') = Subst.simplLetId (getSubst env) id
+    in
+    seqBndr id'                `seq`
+    returnSmpl (setSubst env subst', id')
 
 seqBndrs [] = ()
 seqBndrs (b:bs) = seqBndr b `seq` seqBndrs bs
@@ -443,32 +485,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}
+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
+    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) && not (hasNoBinding fun)
+    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}
-transformRhs :: InExpr -> SimplM InExpr
-transformRhs rhs 
-  = tryEtaExpansion body               `thenSmpl` \ body' ->
-    mkRhsTyLam tyvars body'
+tryEtaExpansion :: OutExpr -> SimplM OutExpr
+-- There is at least one runtime binder in the binders
+tryEtaExpansion body
+  | arity_is_manifest          -- Some lambdas but not enough
+  = returnSmpl body
+
+  | otherwise
+  = getUniquesSmpl                     `thenSmpl` \ us ->
+    returnSmpl (etaExpand fun_arity us body (exprType body))
   where
-    (tyvars, body) = collectTyBinders rhs
+    (fun_arity, arity_is_manifest) = 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
@@ -491,7 +631,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
        
@@ -533,31 +673,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 env fn (Let bind@(NonRec var rhs) body)
+      | exprIsTrivial rhs
+      = go env (fn . Let bind) body
 
-    go fn (Let bind@(NonRec var rhs) body) | exprIsTrivial rhs
-      = go (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
-               --      main_tyvar_set = mkVarSet tyvars
-               --      var_ty = idType var
-               -- 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:
@@ -573,32 +724,32 @@ 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
 
-    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)
-               --       var_tys     = map idType vars
+        tyvars_here = varSetElems (main_tyvar_set `intersectVarSet` exprsSomeFreeVars isTyVar (map snd prs))
                -- See notes with tyvars_here above
 
-
-    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
@@ -607,238 +758,391 @@ mkRhsTyLam tyvars body                  -- Only does something if there's a let
                -- where x* has an INLINE prag on it.  Now, once x* is inlined,
                -- 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
-               -- We need to be careful about inlining.
+    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:        * the binding for g gets floated out
-               --              * but then it MIGHT get inlined into the rhs of g*
-               --              * then the binding for g* is floated out of the /\b
-               --              * so we're back to square one
-               -- We rely on the simplifier not to inline g into the RHS of g*,
-               -- because it's a "lone" occurrence, and there is no benefit in
-               -- inlining.  But it's a slightly delicate property, and there's
-               -- a danger of making the simplifier loop here.
+               -- Then we'll float to get
+               --
+               --      x = let poly_g = /\ a -> G
+               --          in /\ a -> let g = poly_g a in E
+               --
+               -- 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
-
-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
+mkCase puts a case expression back together, trying various transformations first.
 
-where (in both cases) N is a NORMAL FORM (i.e. no redexes anywhere)
-wanting a suitable number of extra args.
+\begin{code}
+mkCase :: OutExpr -> OutId -> [OutAlt] -> SimplM OutExpr
 
-NB: the Ei may have unlifted type, but the simplifier (which is applied
-to the result) deals OK with this.
+mkCase scrut case_bndr alts
+  = mkAlts scrut case_bndr alts        `thenSmpl` \ better_alts ->
+    mkCase1 scrut case_bndr better_alts
+\end{code}
 
-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 SLIT("y") 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))))
-  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 SLIT("z") (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, _) = splitFunTys (exprType body)
+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
        
-    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}
+       p `is` n = p /= (-1) && p == n
 
+This gave rise to a horrible sequence of cases
 
-%************************************************************************
-%*                                                                     *
-\subsection{Case absorption and identity-case elimination}
-%*                                                                     *
-%************************************************************************
+       case p of
+         (-1) -> $j p
+         1    -> e1
+         DEFAULT -> $j p
+
+and similarly in cascade for all the join points!
 
-\begin{code}
-mkCase :: OutExpr -> OutId -> [OutAlt] -> SimplM OutExpr
-\end{code}
 
-@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.
 
 \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!
+--------------------------------------------------
+--     1. Merge identical branches
+--------------------------------------------------
+mkAlts scrut 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
+    filtered_alts       = filter keep con_alts
+    keep (con,bndrs,rhs) = not (all isDeadBinder bndrs && rhs `cheapEqExpr` rhs1)
+    better_alts                 = (DEFAULT, [], rhs1) : filtered_alts
+
+
+--------------------------------------------------
+--     2. Fill in missing constructor
+--------------------------------------------------
+
+mkAlts scrut case_bndr alts
+  | Just (tycon, inst_tys) <- splitTyConApp_maybe (idType case_bndr),
+    isDataTyCon tycon,                 -- It's a data type
+    (alts_no_deflt, Just rhs) <- findDefault alts,
+               -- There is a DEFAULT case
+    [missing_con] <- filter is_missing (tyConDataConsIfAvailable tycon)
+               -- 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
+    impossible_cons   = otherCons (idUnfolding case_bndr)
+    handled_data_cons = [data_con | DataAlt data_con         <- impossible_cons] ++
+                       [data_con | (DataAlt data_con, _, _) <- alts]
+    is_missing con    = not (con `elem` handled_data_cons)
+
+--------------------------------------------------
+--     3.  Merge nested cases
+--------------------------------------------------
+
+mkAlts scrut 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 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}