[project @ 2000-05-24 12:43:20 by simonpj]
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 5940184..f6ccf6a 100644 (file)
@@ -1,4 +1,4 @@
-
+%
 % (c) The AQUA Project, Glasgow University, 1993-1998
 %
 \section[Simplify]{The main module of the simplifier}
@@ -8,64 +8,70 @@ module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
-import CmdLineOpts     ( intSwitchSet,
+import CmdLineOpts     ( intSwitchSet, switchIsOn,
                          opt_SccProfilingOn, opt_PprStyle_Debug, opt_SimplDoEtaReduction,
                          opt_SimplNoPreInlining, opt_DictsStrict, opt_SimplPedanticBottoms,
-                         opt_SimplDoCaseElim,
                          SimplifierSwitch(..)
                        )
 import SimplMonad
 import SimplUtils      ( mkCase, transformRhs, findAlt,
-                         simplBinder, simplBinders, simplIds, findDefault, mkCoerce
+                         simplBinder, simplBinders, simplIds, findDefault,
+                         SimplCont(..), DupFlag(..), contResultType, analyseCont, 
+                         discardInline, countArgs, countValArgs, discardCont, contIsDupable
                        )
 import Var             ( TyVar, mkSysTyVar, tyVarKind, maybeModifyIdInfo )
 import VarEnv
 import VarSet
-import Id              ( Id, idType, idInfo, idUnique,
-                         getIdUnfolding, setIdUnfolding, isExportedId, 
-                         getIdSpecialisation, setIdSpecialisation,
-                         getIdDemandInfo, setIdDemandInfo,
-                         getIdArity, setIdArity, 
-                         getIdStrictness, 
-                         setInlinePragma, getInlinePragma, idMustBeINLINEd
+import Id              ( Id, idType, idInfo, idUnique, isDataConId, isDataConId_maybe,
+                         idUnfolding, setIdUnfolding, isExportedId, isDeadBinder,
+                         idSpecialisation, setIdSpecialisation,
+                         idDemandInfo, 
+                         setIdInfo,
+                         idOccInfo, setIdOccInfo,
+                         zapLamIdInfo, zapFragileIdInfo,
+                         idStrictness, isBottomingId,
+                         setInlinePragma, mayHaveNoBinding,
+                         setOneShotLambda, maybeModifyIdInfo
                        )
 import IdInfo          ( InlinePragInfo(..), OccInfo(..), StrictnessInfo(..), 
                          ArityInfo(..), atLeastArity, arityLowerBound, unknownArity,
-                         specInfo, inlinePragInfo, zapLamIdInfo
+                         specInfo, inlinePragInfo, setArityInfo, setInlinePragInfo, setUnfoldingInfo,
+                         CprInfo(..), cprInfo, occInfo
                        )
 import Demand          ( Demand, isStrict, wwLazy )
-import Const           ( isWHNFCon, conOkForAlt )
-import ConFold         ( tryPrimOp )
-import PrimOp          ( PrimOp, primOpStrictness, primOpType )
-import DataCon         ( DataCon, dataConNumInstArgs, dataConRepStrictness, dataConSig, dataConArgTys )
-import Const           ( Con(..) )
+import DataCon         ( DataCon, dataConNumInstArgs, dataConRepStrictness, dataConRepArity,
+                         dataConSig, dataConArgTys
+                       )
 import Name            ( isLocallyDefined )
 import CoreSyn
 import CoreFVs         ( exprFreeVars )
-import CoreUnfold      ( Unfolding(..), mkUnfolding, callSiteInline, 
-                         isEvaldUnfolding, blackListed )
-import CoreUtils       ( cheapEqExpr, exprIsDupable, exprIsWHNF, exprIsTrivial,
-                         coreExprType, coreAltsType, exprIsCheap, exprArity,
-                         exprOkForSpeculation,
-                         FormSummary(..), mkFormSummary, whnfOrBottom
+import CoreUnfold      ( Unfolding, mkOtherCon, mkUnfolding, otherCons, maybeUnfoldingTemplate,
+                         callSiteInline, hasSomeUnfolding, noUnfolding
+                       )
+import CoreUtils       ( cheapEqExpr, exprIsDupable, exprIsCheap, exprIsTrivial, exprIsConApp_maybe,
+                         exprType, coreAltsType, exprArity, exprIsValue, idAppIsCheap,
+                         exprOkForSpeculation, etaReduceExpr,
+                         mkCoerce, mkSCC, mkInlineMe, mkAltExpr
                        )
 import Rules           ( lookupRule )
 import CostCentre      ( isSubsumedCCS, currentCCS, isEmptyCC )
-import Type            ( Type, mkTyVarTy, mkTyVarTys, isUnLiftedType, 
-                         mkFunTy, splitFunTys, splitTyConApp_maybe, splitFunTy_maybe,
+import Type            ( Type, mkTyVarTy, mkTyVarTys, isUnLiftedType, seqType,
+                         mkFunTy, splitFunTy, splitFunTys, splitFunTy_maybe,
+                         splitTyConApp_maybe, 
                          funResultTy, isDictTy, isDataType, applyTy, applyTys, mkFunTys
                        )
-import Subst           ( Subst, mkSubst, emptySubst, substExpr, substTy, 
-                         substEnv, lookupInScope, lookupSubst, substRules
+import Subst           ( Subst, mkSubst, emptySubst, substTy, substExpr,
+                         substEnv, isInScope, lookupIdSubst, substIdInfo
                        )
 import TyCon           ( isDataTyCon, tyConDataCons, tyConClass_maybe, tyConArity, isDataTyCon )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
-import BasicTypes      ( TopLevelFlag(..), isTopLevel )
+import BasicTypes      ( TopLevelFlag(..), isTopLevel, isLoopBreaker )
 import Maybes          ( maybeToBool )
-import Util            ( zipWithEqual, stretchZipEqual, lengthExceeds )
+import Util            ( zipWithEqual, lengthExceeds )
 import PprCore
 import Outputable
+import Unique          ( foldrIdKey )  -- Temp
 \end{code}
 
 
@@ -87,23 +93,25 @@ simplTopBinds binds
        -- so that if a transformation rule has unexpectedly brought
        -- anything into scope, then we don't get a complaint about that.
        -- It's rather as if the top-level binders were imported.
-    extendInScopes top_binders $
-    simpl_binds binds          `thenSmpl` \ (binds', _) ->
-    freeTick SimplifierDone    `thenSmpl_`
+    simplIds (bindersOfBinds binds)    $ \ bndrs' -> 
+    simpl_binds binds bndrs'           `thenSmpl` \ (binds', _) ->
+    freeTick SimplifierDone            `thenSmpl_`
     returnSmpl binds'
   where
-    top_binders        = bindersOfBinds binds
 
-    simpl_binds []                       = returnSmpl ([], panic "simplTopBinds corner")
-    simpl_binds (NonRec bndr rhs : binds) = simplLazyBind TopLevel bndr  bndr rhs       (simpl_binds binds)
-    simpl_binds (Rec pairs       : binds) = simplRecBind  TopLevel pairs (map fst pairs) (simpl_binds binds)
+       -- We need to track the zapped top-level binders, because
+       -- they should have their fragile IdInfo zapped (notably occurrence info)
+    simpl_binds []                       bs     = ASSERT( null bs ) returnSmpl ([], panic "simplTopBinds corner")
+    simpl_binds (NonRec bndr rhs : binds) (b:bs) = simplLazyBind True bndr  b rhs      (simpl_binds binds bs)
+    simpl_binds (Rec pairs       : binds) bs     = simplRecBind  True pairs (take n bs) (simpl_binds binds (drop n bs))
+                                                where 
+                                                  n = length pairs
 
-
-simplRecBind :: TopLevelFlag -> [(InId, InExpr)] -> [OutId]
+simplRecBind :: Bool -> [(InId, InExpr)] -> [OutId]
             -> SimplM (OutStuff a) -> SimplM (OutStuff a)
 simplRecBind top_lvl pairs bndrs' thing_inside
-  = go pairs bndrs'            `thenSmpl` \ (binds', stuff) ->
-    returnSmpl (addBind (Rec (flattenBinds binds')) stuff)
+  = go pairs bndrs'            `thenSmpl` \ (binds', (binds'', res)) ->
+    returnSmpl (Rec (flattenBinds binds') : binds'', res)
   where
     go [] _ = thing_inside     `thenSmpl` \ stuff ->
              returnSmpl ([], stuff)
@@ -122,12 +130,30 @@ simplRecBind top_lvl pairs bndrs' thing_inside
 %************************************************************************
 
 \begin{code}
-addBind :: CoreBind -> OutStuff a -> OutStuff a
-addBind bind    (binds,  res) = (bind:binds,     res)
+addLetBind :: OutId -> OutExpr -> SimplM (OutStuff a) -> SimplM (OutStuff a)
+addLetBind bndr rhs thing_inside
+  = thing_inside       `thenSmpl` \ (binds, res) ->
+    returnSmpl (NonRec bndr rhs : binds, res)
+
+addLetBinds :: [CoreBind] -> SimplM (OutStuff a) -> SimplM (OutStuff a)
+addLetBinds binds1 thing_inside
+  = thing_inside       `thenSmpl` \ (binds2, res) ->
+    returnSmpl (binds1 ++ binds2, res)
+
+needsCaseBinding ty rhs = isUnLiftedType ty && not (exprOkForSpeculation rhs)
+       -- Make a case expression instead of a let
+       -- These can arise either from the desugarer,
+       -- or from beta reductions: (\x.e) (x +# y)
+
+addCaseBind bndr rhs thing_inside
+  = getInScope                         `thenSmpl` \ in_scope ->
+    thing_inside               `thenSmpl` \ (floats, (_, body)) ->
+    returnSmpl ([], (in_scope, Case rhs bndr [(DEFAULT, [], mkLets floats body)]))
 
-addBinds :: [CoreBind] -> OutStuff a -> OutStuff a
-addBinds []     stuff        = stuff
-addBinds binds1 (binds2, res) = (binds1++binds2, res)
+addNonRecBind bndr rhs thing_inside
+       -- Checks for needing a case binding
+  | needsCaseBinding (idType bndr) rhs = addCaseBind bndr rhs thing_inside
+  | otherwise                         = addLetBind  bndr rhs thing_inside
 \end{code}
 
 The reason for this OutExprStuff stuff is that we want to float *after*
@@ -171,10 +197,11 @@ might do the same again.
 \begin{code}
 simplExpr :: CoreExpr -> SimplM CoreExpr
 simplExpr expr = getSubst      `thenSmpl` \ subst ->
-                simplExprC expr (Stop (substTy subst (coreExprType expr)))
+                simplExprC expr (Stop (substTy subst (exprType expr)))
        -- The type in the Stop continuation is usually not used
        -- It's only needed when discarding continuations after finding
-       -- a function that returns bottom
+       -- a function that returns bottom.
+       -- Hence the lazy substitution
 
 simplExprC :: CoreExpr -> SimplCont -> SimplM CoreExpr
        -- Simplify an expression, given a continuation
@@ -188,47 +215,29 @@ simplExprF :: InExpr -> SimplCont -> SimplM OutExprStuff
 simplExprF (Var v) cont
   = simplVar v cont
 
-simplExprF expr@(Con (PrimOp op) args) cont
-  = getSubstEnv                                `thenSmpl` \ se ->
-    prepareArgs (ppr op)
-               (primOpType op)
-               (primOpStrictness op)
-               (pushArgs se args cont) $ \ args1 cont1 ->
+simplExprF (Lit lit) (Select _ bndr alts se cont)
+  = knownCon (Lit lit) (LitAlt lit) [] bndr alts se cont
 
-    let
-       -- Boring... we may have too many arguments now, so we push them back
-       n_args = length args
-       args2 = ASSERT( length args1 >= n_args )
-                take n_args args1
-       cont2 = pushArgs emptySubstEnv (drop n_args args1) cont1
-    in                         
-       --      Try the prim op simplification
-       -- It's really worth trying simplExpr again if it succeeds,
-       -- because you can find
-       --      case (eqChar# x 'a') of ...
-       -- ==>  
-       --      case (case x of 'a' -> True; other -> False) of ...
-     case tryPrimOp op args2 of
-         Just e' -> zapSubstEnv (simplExprF e' cont2)
-         Nothing -> rebuild (Con (PrimOp op) args2) cont2
-
-simplExprF (Con con@(DataCon _) args) cont
-  = freeTick LeafVisit                 `thenSmpl_`
-    simplConArgs args          ( \ args' ->
-    rebuild (Con con args') cont)
-
-simplExprF expr@(Con con@(Literal _) args) cont
-  = ASSERT( null args )
-    freeTick LeafVisit                 `thenSmpl_`
-    rebuild expr cont
+simplExprF (Lit lit) cont
+  = rebuild (Lit lit) cont
 
 simplExprF (App fun arg) cont
   = getSubstEnv                `thenSmpl` \ se ->
     simplExprF fun (ApplyTo NoDup arg se cont)
 
 simplExprF (Case scrut bndr alts) cont
-  = getSubstEnv                `thenSmpl` \ se ->
-    simplExprF scrut (Select NoDup bndr alts se cont)
+  = getSubstEnv                        `thenSmpl` \ subst_env ->
+    getSwitchChecker           `thenSmpl` \ chkr ->
+    if not (switchIsOn chkr NoCaseOfCase) then
+       -- Simplify the scrutinee with a Select continuation
+       simplExprF scrut (Select NoDup bndr alts subst_env cont)
+
+    else
+       -- If case-of-case is off, simply simplify the case expression
+       -- in a vanilla Stop context, and rebuild the result around it
+       simplExprC scrut (Select NoDup bndr alts subst_env 
+                                (Stop (contResultType cont)))  `thenSmpl` \ case_expr' ->
+       rebuild case_expr' cont
 
 
 simplExprF (Let (Rec pairs) body) cont
@@ -236,25 +245,41 @@ simplExprF (Let (Rec pairs) body) cont
        -- NB: bndrs' don't have unfoldings or spec-envs
        -- We add them as we go down, using simplPrags
 
-    simplRecBind NotTopLevel pairs bndrs' (simplExprF body cont)
+    simplRecBind False pairs bndrs' (simplExprF body cont)
 
 simplExprF expr@(Lam _ _) cont = simplLam expr cont
+
 simplExprF (Type ty) cont
   = ASSERT( case cont of { Stop _ -> True; ArgOf _ _ _ -> True; other -> False } )
     simplType ty       `thenSmpl` \ ty' ->
     rebuild (Type ty') cont
 
+-- Comments about the Coerce case
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- It's worth checking for a coerce in the continuation,
+-- in case we can cancel them.  For example, in the initial form of a worker
+-- we may find         (coerce T (coerce S (\x.e))) y
+-- and we'd like it to simplify to e[y/x] in one round of simplification
+
+simplExprF (Note (Coerce to from) e) (CoerceIt outer_to cont)
+  = simplType from             `thenSmpl` \ from' ->
+    if outer_to == from' then
+       -- The coerces cancel out
+       simplExprF e cont
+    else
+       -- They don't cancel, but the inner one is redundant
+       simplExprF e (CoerceIt outer_to cont)
+
 simplExprF (Note (Coerce to from) e) cont
-  | to == from = simplExprF e cont
-  | otherwise  = getSubst              `thenSmpl` \ subst ->
-                simplExprF e (CoerceIt (substTy subst to) cont)
+  = simplType to               `thenSmpl` \ to' ->
+    simplExprF e (CoerceIt to' cont)
 
 -- hack: we only distinguish subsumed cost centre stacks for the purposes of
 -- inlining.  All other CCCSs are mapped to currentCCS.
 simplExprF (Note (SCC cc) e) cont
   = setEnclosingCC currentCCS $
     simplExpr e        `thenSmpl` \ e ->
-    rebuild (mkNote (SCC cc) e) cont
+    rebuild (mkSCC cc e) cont
 
 simplExprF (Note InlineCall e) cont
   = simplExprF e (InlinePlease cont)
@@ -281,7 +306,7 @@ simplExprF (Note InlineMe e) cont
        Stop _ ->       -- Totally boring continuation
                        -- Don't inline inside an INLINE expression
                  switchOffInlining (simplExpr e)       `thenSmpl` \ e' ->
-                 rebuild (mkNote InlineMe e') cont
+                 rebuild (mkInlineMe e') cont
 
        other  ->       -- Dissolve the InlineMe note if there's
                        -- an interesting context of any kind to combine with
@@ -302,18 +327,15 @@ simplExprF (Let (NonRec bndr rhs) body) cont
 simplLam fun cont
   = go fun cont
   where
-    zap_it = mkLamBndrZapper fun (countArgs cont)
+    zap_it  = mkLamBndrZapper fun cont
     cont_ty = contResultType cont
 
        -- Type-beta reduction
     go (Lam bndr body) (ApplyTo _ (Type ty_arg) arg_se body_cont)
       =        ASSERT( isTyVar bndr )
-       tick (BetaReduction bndr)               `thenSmpl_`
-       getInScope                              `thenSmpl` \ in_scope ->
-       let
-               ty' = substTy (mkSubst in_scope arg_se) ty_arg
-       in
-       extendSubst bndr (DoneTy ty')
+       tick (BetaReduction bndr)       `thenSmpl_`
+       simplTyArg ty_arg arg_se        `thenSmpl` \ ty_arg' ->
+       extendSubst bndr (DoneTy ty_arg')
        (go body body_cont)
 
        -- Ordinary beta reduction
@@ -330,11 +352,14 @@ simplLam fun cont
        -- Exactly enough args
     go expr cont = simplExprF expr cont
 
-
 -- completeLam deals with the case where a lambda doesn't have an ApplyTo
--- continuation.  Try for eta reduction, but *only* if we get all
--- the way to an exprIsTrivial expression.  
--- 'acc' holds the simplified binders, in reverse order
+-- continuation.  
+-- We used to try for eta reduction here, but I found that this was
+-- eta reducing things like 
+--     f = \x -> (coerce (\x -> e))
+-- This made f's arity reduce, which is a bad thing, so I removed the
+-- eta reduction at this point, and now do it only when binding 
+-- (at the call to postInlineUnconditionally)
 
 completeLam acc (Lam bndr body) cont
   = simplBinder bndr                   $ \ bndr' ->
@@ -342,66 +367,23 @@ completeLam acc (Lam bndr body) cont
 
 completeLam acc body cont
   = simplExpr body                     `thenSmpl` \ body' ->
-
-    case (opt_SimplDoEtaReduction, check_eta acc body') of
-       (True, Just body'')     -- Eta reduce!
-               -> tick (EtaReduction (head acc))       `thenSmpl_`
-                  rebuild body'' cont
-
-       other   ->      -- No eta reduction
-                  rebuild (foldl (flip Lam) body' acc) cont
-                       -- Remember, acc is the reversed binders
-  where
-       -- NB: the binders are reversed
-    check_eta (b : bs) (App fun arg)
-       |  (varToCoreExpr b `cheapEqExpr` arg)
-       = check_eta bs fun
-
-    check_eta [] body
-       | exprIsTrivial body &&                 -- ONLY if the body is trivial
-         not (any (`elemVarSet` body_fvs) acc)
-       = Just body             -- Success!
-       where
-         body_fvs = exprFreeVars body
-
-    check_eta _ _ = Nothing    -- Bale out
+    rebuild (foldl (flip Lam) body' acc) cont
+               -- Remember, acc is the *reversed* binders
 
 mkLamBndrZapper :: CoreExpr    -- Function
-               -> Int          -- Number of args
+               -> SimplCont    -- The context
                -> Id -> Id     -- Use this to zap the binders
-mkLamBndrZapper fun n_args
-  | saturated fun n_args = \b -> b
-  | otherwise           = \b -> maybeModifyIdInfo zapLamIdInfo b
+mkLamBndrZapper fun cont
+  | n_args >= n_params fun = \b -> b           -- Enough args
+  | otherwise             = \b -> zapLamIdInfo b
   where
-    saturated (Lam b e) 0 = False
-    saturated (Lam b e) n = saturated e (n-1)
-    saturated e                n = True
-\end{code}
-
-
----------------------------------
-simplConArgs makes sure that the arguments all end up being atomic.
-That means it may generate some Lets, hence the strange type
-
-\begin{code}
-simplConArgs :: [InArg] -> ([OutArg] -> SimplM OutExprStuff) -> SimplM OutExprStuff
-simplConArgs [] thing_inside
-  = thing_inside []
+       -- NB: we count all the args incl type args
+       -- so we must count all the binders (incl type lambdas)
+    n_args = countArgs cont
 
-simplConArgs (arg:args) thing_inside
-  = switchOffInlining (simplExpr arg)  `thenSmpl` \ arg' ->
-       -- Simplify the RHS with inlining switched off, so that
-       -- only absolutely essential things will happen.
-
-    simplConArgs args                          $ \ args' ->
-
-       -- If the argument ain't trivial, then let-bind it
-    if exprIsTrivial arg' then
-       thing_inside (arg' : args')
-    else
-       newId (coreExprType arg')               $ \ arg_id ->
-       thing_inside (Var arg_id : args')       `thenSmpl` \ res ->
-       returnSmpl (addBind (NonRec arg_id arg') res)
+    n_params (Note _ e) = n_params e
+    n_params (Lam b e)  = 1 + n_params e
+    n_params other     = 0::Int
 \end{code}
 
 
@@ -410,7 +392,11 @@ simplConArgs (arg:args) thing_inside
 simplType :: InType -> SimplM OutType
 simplType ty
   = getSubst   `thenSmpl` \ subst ->
-    returnSmpl (substTy subst ty)
+    let
+       new_ty = substTy subst ty
+    in
+    seqType new_ty `seq`  
+    returnSmpl new_ty
 \end{code}
 
 
@@ -438,54 +424,73 @@ simplBeta bndr rhs rhs_se cont_ty thing_inside
 #endif
 
 simplBeta bndr rhs rhs_se cont_ty thing_inside
-  | preInlineUnconditionally bndr && not opt_SimplNoPreInlining
+  | preInlineUnconditionally False {- not black listed -} bndr
   = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
     extendSubst bndr (ContEx rhs_se rhs) thing_inside
 
   | otherwise
-  =    -- Simplify the RHS
+  =    -- Simplify the RHS
     simplBinder bndr                                   $ \ bndr' ->
-    simplArg (idType bndr') (getIdDemandInfo bndr)
-            rhs rhs_se cont_ty                         $ \ rhs' ->
+    simplValArg (idType bndr') (idDemandInfo bndr)
+               rhs rhs_se cont_ty                      $ \ rhs' ->
 
        -- Now complete the binding and simplify the body
-    completeBeta bndr bndr' rhs' thing_inside
-
-completeBeta bndr bndr' rhs' thing_inside
-  | isUnLiftedType (idType bndr') && not (exprOkForSpeculation rhs')
-       -- Make a case expression instead of a let
-       -- These can arise either from the desugarer,
-       -- or from beta reductions: (\x.e) (x +# y)
-  = getInScope                         `thenSmpl` \ in_scope ->
-    thing_inside               `thenSmpl` \ (floats, (_, body)) ->
-    returnSmpl ([], (in_scope, Case rhs' bndr' [(DEFAULT, [], mkLets floats body)]))
-
-  | otherwise
-  = completeBinding bndr bndr' rhs' thing_inside
+    if needsCaseBinding (idType bndr') rhs' then
+       addCaseBind bndr' rhs' thing_inside
+    else
+       completeBinding bndr bndr' False False rhs' thing_inside
 \end{code}
 
 
 \begin{code}
-simplArg :: OutType -> Demand
-        -> InExpr -> SubstEnv
-        -> OutType             -- Type of thing computed by the context
-        -> (OutExpr -> SimplM OutExprStuff)
-        -> SimplM OutExprStuff
-simplArg arg_ty demand arg arg_se cont_ty thing_inside
+simplTyArg :: InType -> SubstEnv -> SimplM OutType
+simplTyArg ty_arg se
+  = getInScope         `thenSmpl` \ in_scope ->
+    let
+       ty_arg' = substTy (mkSubst in_scope se) ty_arg
+    in
+    seqType ty_arg'    `seq`
+    returnSmpl ty_arg'
+
+simplValArg :: OutType         -- Type of arg
+           -> Demand           -- Demand on the argument
+           -> InExpr -> SubstEnv
+           -> OutType          -- Type of thing computed by the context
+           -> (OutExpr -> SimplM OutExprStuff)
+           -> SimplM OutExprStuff
+
+simplValArg arg_ty demand arg arg_se cont_ty thing_inside
   | isStrict demand || 
     isUnLiftedType arg_ty || 
     (opt_DictsStrict && isDictTy arg_ty && isDataType arg_ty)
        -- 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)
-  = getSubstEnv                                        `thenSmpl` \ body_se ->
-    transformRhs arg                           `thenSmpl` \ t_arg ->
-    setSubstEnv arg_se (simplExprF t_arg (ArgOf NoDup cont_ty $ \ arg' ->
-    setSubstEnv body_se (thing_inside arg')
-    )) -- NB: we must restore body_se before carrying on with thing_inside!!
+  = transformRhs arg                   `thenSmpl` \ t_arg ->
+    getEnv                             `thenSmpl` \ env ->
+    setSubstEnv arg_se                                 $
+    simplExprF t_arg (ArgOf NoDup cont_ty      $ \ rhs' ->
+    setAllExceptInScope env                    $
+    etaFirst thing_inside rhs')
 
   | otherwise
-  = simplRhs NotTopLevel True arg_ty arg arg_se thing_inside
+  = simplRhs False {- Not top level -} 
+            True {- OK to float unboxed -}
+            arg_ty arg arg_se 
+            thing_inside
+   
+-- Do eta-reduction on the simplified RHS, if eta reduction is on
+-- NB: etaFirst only eta-reduces if that results in something trivial
+etaFirst | opt_SimplDoEtaReduction = \ thing_inside rhs -> thing_inside (etaCoreExprToTrivial rhs)
+        | otherwise               = \ thing_inside rhs -> thing_inside rhs
+
+-- Try for eta reduction, 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
+etaCoreExprToTrivial rhs | exprIsTrivial rhs' = rhs'
+                        | otherwise          = rhs
+                        where
+                          rhs' = etaReduceExpr rhs
 \end{code}
 
 
@@ -504,18 +509,20 @@ It does *not* attempt to do let-to-case.  Why?  Because they are used for
 \begin{code}
 completeBinding :: InId                -- Binder
                -> OutId                -- New binder
+               -> Bool                 -- True <=> top level
+               -> Bool                 -- True <=> black-listed; don't inline
                -> OutExpr              -- Simplified RHS
                -> SimplM (OutStuff a)  -- Thing inside
                -> SimplM (OutStuff a)
 
-completeBinding old_bndr new_bndr new_rhs thing_inside
-  |  isDeadBinder old_bndr     -- This happens; for example, the case_bndr during case of
-                               -- known constructor:  case (a,b) of x { (p,q) -> ... }
-                               -- Here x isn't mentioned in the RHS, so we don't want to
+completeBinding old_bndr new_bndr top_lvl black_listed new_rhs thing_inside
+  |  (case occ_info of         -- This happens; for example, the case_bndr during case of
+       IAmDead -> True         -- known constructor:  case (a,b) of x { (p,q) -> ... }
+       other   -> False)       -- Here x isn't mentioned in the RHS, so we don't want to
                                -- create the (dead) let-binding  let x = (a,b) in ...
   =  thing_inside
 
-  |  postInlineUnconditionally old_bndr new_rhs
+  |  postInlineUnconditionally black_listed occ_info old_bndr new_rhs
        -- Maybe we don't need a let-binding!  Maybe we can just
        -- inline it right away.  Unlike the preInlineUnconditionally case
        -- we are allowed to look at the RHS.
@@ -523,6 +530,14 @@ completeBinding old_bndr new_bndr new_rhs thing_inside
        -- NB: a loop breaker never has postInlineUnconditionally True
        -- and non-loop-breakers only have *forward* references
        -- Hence, it's safe to discard the binding
+       --      
+       -- NB: You might think that postInlineUnconditionally is an optimisation,
+       -- but if we have
+       --      let x = f Bool in (x, y)
+       -- then because of the constructor, x will not be *inlined* in the pair,
+       -- so the trivial binding will stay.  But in this postInlineUnconditionally 
+       -- gag we use the *substitution* to substitute (f Bool) for x, and that *will*
+       -- happen.
   =  tick (PostInlineUnconditionally old_bndr) `thenSmpl_`
      extendSubst old_bndr (DoneEx new_rhs)     
      thing_inside
@@ -530,28 +545,31 @@ completeBinding old_bndr new_bndr new_rhs thing_inside
   |  otherwise
   =  getSubst                  `thenSmpl` \ subst ->
      let
-       bndr_info = idInfo old_bndr
-       old_rules = specInfo bndr_info
-       new_rules = substRules subst old_rules
-
-       -- The new binding site Id needs its specialisations re-attached
-       bndr_w_arity = new_bndr `setIdArity` ArityAtLeast (exprArity new_rhs)
-
-       binding_site_id
-         | isEmptyCoreRules old_rules = bndr_w_arity 
-         | otherwise                  = bndr_w_arity `setIdSpecialisation` new_rules
-
-       -- At the occurrence sites we want to know the unfolding,
-       -- and the occurrence info of the original
-       -- (simplBinder cleaned up the inline prag of the original
-       --  to eliminate un-stable info, in case this expression is
-       --  simplified a second time; hence the need to reattach it)
-       occ_site_id = binding_site_id
-                     `setIdUnfolding` mkUnfolding new_rhs
-                     `setInlinePragma` inlinePragInfo bndr_info
+       -- We make new IdInfo for the new binder by starting from the old binder, 
+       -- doing appropriate substitutions.
+       -- Then we add arity and unfolding info to get the new binder
+       old_info      = idInfo old_bndr
+       new_bndr_info = substIdInfo subst old_info (idInfo new_bndr)
+                       `setArityInfo` ArityAtLeast (exprArity new_rhs)
+
+       -- Add the unfolding *only* for non-loop-breakers
+       -- Making loop breakers not have an unfolding at all 
+       -- means that we can avoid tests in exprIsConApp, for example.
+       -- This is important: if exprIsConApp says 'yes' for a recursive
+       -- thing we can get into an infinite loop
+       info_w_unf | isLoopBreaker (occInfo old_info) = new_bndr_info
+                  | otherwise = new_bndr_info `setUnfoldingInfo` mkUnfolding top_lvl new_rhs
+
+       final_id = new_bndr `setIdInfo` info_w_unf
      in
-     modifyInScope occ_site_id thing_inside    `thenSmpl` \ stuff ->
-     returnSmpl (addBind (NonRec binding_site_id new_rhs) stuff)
+       -- These seqs forces the Id, and hence its IdInfo,
+       -- and hence any inner substitutions
+     final_id                          `seq`
+     addLetBind final_id new_rhs       $
+     modifyInScope new_bndr final_id thing_inside
+
+  where
+    occ_info = idOccInfo old_bndr
 \end{code}    
 
 
@@ -570,7 +588,7 @@ It does two important optimisations though:
        * It does eta expansion
 
 \begin{code}
-simplLazyBind :: TopLevelFlag
+simplLazyBind :: Bool                  -- True <=> top level
              -> InId -> OutId
              -> InExpr                 -- The RHS
              -> SimplM (OutStuff a)    -- The body of the binding
@@ -580,27 +598,32 @@ simplLazyBind :: TopLevelFlag
 -- Also the binder has already been simplified, and hence is in scope
 
 simplLazyBind top_lvl bndr bndr' rhs thing_inside
-  | preInlineUnconditionally bndr && not opt_SimplNoPreInlining
-  = tick (PreInlineUnconditionally bndr)               `thenSmpl_`
-    getSubstEnv                                        `thenSmpl` \ rhs_se ->
-    (extendSubst bndr (ContEx rhs_se rhs) thing_inside)
+  = getBlackList               `thenSmpl` \ black_list_fn ->
+    let
+       black_listed = black_list_fn bndr
+    in
 
-  | otherwise
-  =    -- Simplify the RHS
-    getSubstEnv                                        `thenSmpl` \ rhs_se ->
+    if preInlineUnconditionally black_listed bndr then
+       -- Inline unconditionally
+       tick (PreInlineUnconditionally bndr)    `thenSmpl_`
+       getSubstEnv                             `thenSmpl` \ rhs_se ->
+       (extendSubst bndr (ContEx rhs_se rhs) thing_inside)
+    else
 
+       -- Simplify the RHS
+    getSubstEnv                                        `thenSmpl` \ rhs_se ->
     simplRhs top_lvl False {- Not ok to float unboxed -}
             (idType bndr')
             rhs rhs_se                                 $ \ rhs' ->
 
        -- Now compete the binding and simplify the body
-    completeBinding bndr bndr' rhs' thing_inside
+    completeBinding bndr bndr' top_lvl black_listed rhs' thing_inside
 \end{code}
 
 
 
 \begin{code}
-simplRhs :: TopLevelFlag
+simplRhs :: Bool               -- True <=> Top level
         -> Bool                -- True <=> OK to float unboxed (speculative) bindings
         -> OutType -> InExpr -> SubstEnv
         -> (OutExpr -> SimplM (OutStuff a))
@@ -618,8 +641,8 @@ simplRhs top_lvl float_ubx rhs_ty rhs rhs_se thing_inside
        (floats_out, rhs'') | float_ubx = (floats, rhs')
                            | otherwise = splitFloats floats rhs' 
     in
-    if (isTopLevel top_lvl || exprIsWHNF rhs') &&      -- Float lets if (a) we're at the top level
-        not (null floats_out)                          -- or            (b) it exposes a HNF
+    if (top_lvl || wantToExpose 0 rhs') &&     -- Float lets if (a) we're at the top level
+        not (null floats_out)                  -- or            (b) the resulting RHS is one we'd like to expose
     then
        tickLetFloat floats_out                         `thenSmpl_`
                -- Do the float
@@ -631,20 +654,21 @@ simplRhs top_lvl float_ubx rhs_ty rhs rhs_se thing_inside
                -- and so there can't be any 'will be demanded' bindings in the floats.
                -- Hence the assert
        WARN( any demanded_float floats_out, ppr floats_out )
-       setInScope in_scope' (thing_inside rhs'')       `thenSmpl` \ stuff ->
+       addLetBinds floats_out  $
+       setInScope in_scope'    $
+       etaFirst thing_inside rhs''
                -- in_scope' may be excessive, but that's OK;
                -- it's a superset of what's in scope
-       returnSmpl (addBinds floats_out stuff)
     else       
                -- Don't do the float
-       thing_inside (mkLets floats rhs')
+       etaFirst thing_inside (mkLets floats rhs')
 
 -- In a let-from-let float, we just tick once, arbitrarily
 -- choosing the first floated binder to identify it
 tickLetFloat (NonRec b r      : fs) = tick (LetFloatFromLet b)
 tickLetFloat (Rec ((b,r):prs) : fs) = tick (LetFloatFromLet b)
        
-demanded_float (NonRec b r) = isStrict (getIdDemandInfo b) && not (isUnLiftedType (idType b))
+demanded_float (NonRec b r) = isStrict (idDemandInfo b) && not (isUnLiftedType (idType b))
                -- Unlifted-type (cheap-eagerness) lets may well have a demanded flag on them
 demanded_float (Rec _)     = False
 
@@ -661,6 +685,37 @@ splitFloats floats rhs
 
     must_stay (Rec prs)    = False     -- No unlifted bindings in here
     must_stay (NonRec b r) = isUnLiftedType (idType b)
+
+wantToExpose :: Int -> CoreExpr -> Bool
+-- True for expressions that we'd like to expose at the
+-- top level of an RHS.  This includes partial applications
+-- even if the args aren't cheap; the next pass will let-bind the
+-- args and eta expand the partial application.  So exprIsCheap won't do.
+-- Here's the motivating example:
+--     z = letrec g = \x y -> ...g... in g E
+-- Even though E is a redex we'd like to float the letrec to give
+--     g = \x y -> ...g...
+--     z = g E
+-- Now the next use of SimplUtils.tryEtaExpansion will give
+--     g = \x y -> ...g...
+--     z = let v = E in \w -> g v w
+-- And now we'll float the v to give
+--     g = \x y -> ...g...
+--     v = E
+--     z = \w -> g v w
+-- Which is what we want; chances are z will be inlined now.
+--
+-- This defn isn't quite like 
+--     exprIsCheap (it ignores non-cheap args)
+--     exprIsValue (may not say True for a lone variable)
+-- which is slightly weird
+wantToExpose n (Var v)         = idAppIsCheap v n
+wantToExpose n (Lit l)         = True
+wantToExpose n (Lam _ e)       = True
+wantToExpose n (Note _ e)      = wantToExpose n e
+wantToExpose n (App f (Type _))        = wantToExpose n f
+wantToExpose n (App f a)       = wantToExpose (n+1) f
+wantToExpose n other           = False                 -- There won't be any lets
 \end{code}
 
 
@@ -673,92 +728,187 @@ splitFloats floats rhs
 
 \begin{code}
 simplVar var cont
-  = freeTick LeafVisit `thenSmpl_`
-    getSubst           `thenSmpl` \ subst ->
-    case lookupSubst subst var of
-       Just (DoneEx (Var v)) -> zapSubstEnv (simplVar v cont)
-       Just (DoneEx e)       -> zapSubstEnv (simplExprF e cont)
-       Just (ContEx env' e)  -> setSubstEnv env' (simplExprF e cont)
-
-       Nothing -> let
-                       var' = case lookupInScope subst var of
-                                Just v' -> v'
-                                Nothing -> 
-#ifdef DEBUG
-                                           if isLocallyDefined var && not (idMustBeINLINEd var)
-                                               -- The idMustBeINLINEd test accouunts for the fact
-                                               -- that class method selectors don't have top level
-                                               -- bindings and hence aren't in scope.
-                                           then
-                                               -- Not in scope
-                                               pprTrace "simplVar:" (ppr var) var
-                                           else
-#endif
-                                           var
-                  in
-                  getBlackList         `thenSmpl` \ black_list ->
-                  getInScope           `thenSmpl` \ in_scope ->
+  = getSubst           `thenSmpl` \ subst ->
+    case lookupIdSubst subst var of
+       DoneEx e        -> zapSubstEnv (simplExprF e cont)
+       ContEx env1 e   -> setSubstEnv env1 (simplExprF e cont)
+       DoneId var1 occ -> WARN( not (isInScope var1 subst) && isLocallyDefined var1 && not (mayHaveNoBinding var1),
+                                text "simplVar:" <+> ppr var )
+                                       -- The mayHaveNoBinding test accouunts for the fact
+                                       -- that class dictionary constructors dont have top level
+                                       -- bindings and hence aren't in scope.
+                          zapSubstEnv (completeCall var1 occ cont)
+               -- The template is already simplified, so don't re-substitute.
+               -- This is VITAL.  Consider
+               --      let x = e in
+               --      let y = \z -> ...x... in
+               --      \ x -> ...y...
+               -- We'll clone the inner \x, adding x->x' in the id_subst
+               -- Then when we inline y, we must *not* replace x by x' in
+               -- the inlined copy!!
 
-                  prepareArgs (ppr var') (idType var') (get_str var') cont     $ \ args' cont' ->
-                  completeCall black_list in_scope var' args' cont'
-  where
-    get_str var = case getIdStrictness var of
-                       NoStrictnessInfo                  -> (repeat wwLazy, False)
-                       StrictnessInfo demands result_bot -> (demands, result_bot)
+---------------------------------------------------------
+--     Dealing with a call
 
+completeCall var occ cont
+  = getBlackList       `thenSmpl` \ black_list_fn ->
+    getInScope         `thenSmpl` \ in_scope ->
+    getSwitchChecker   `thenSmpl` \ chkr ->
+    let
+       dont_use_rules     = switchIsOn chkr DontApplyRules
+       no_case_of_case    = switchIsOn chkr NoCaseOfCase
+       black_listed       = black_list_fn var
+
+       (arg_infos, interesting_cont, inline_call) = analyseCont in_scope cont
+       discard_inline_cont | inline_call = discardInline cont
+                           | otherwise   = cont
+
+       maybe_inline = callSiteInline black_listed inline_call occ
+                                     var arg_infos interesting_cont
+    in
+       -- First, look for an inlining
+
+    case maybe_inline of {
+       Just unfolding          -- There is an inlining!
+         ->  tick (UnfoldingDone var)          `thenSmpl_`
+             simplExprF unfolding discard_inline_cont
+
+       ;
+       Nothing ->              -- No inlining!
+
+       -- Next, look for rules or specialisations that match
+       --
+       -- It's important to simplify the args first, because the rule-matcher
+       -- doesn't do substitution as it goes.  We don't want to use subst_args
+       -- (defined in the 'where') because that throws away useful occurrence info,
+       -- and perhaps-very-important specialisations.
+       --
+       -- Some functions have specialisations *and* are strict; in this case,
+       -- we don't want to inline the wrapper of the non-specialised thing; better
+       -- to call the specialised thing instead.
+       -- But the black-listing mechanism means that inlining of the wrapper
+       -- won't occur for things that have specialisations till a later phase, so
+       -- it's ok to try for inlining first.
 
+    prepareArgs no_case_of_case var cont       $ \ args' cont' ->
+    let
+       maybe_rule | dont_use_rules = Nothing
+                  | otherwise      = lookupRule in_scope var args' 
+    in
+    case maybe_rule of {
+       Just (rule_name, rule_rhs) -> 
+               tick (RuleFired rule_name)                      `thenSmpl_`
+               simplExprF rule_rhs cont' ;
+       
+       Nothing ->              -- No rules
+
+       -- Done
+    rebuild (mkApps (Var var) args') cont'
+    }}
+\end{code}                
+
+
+\begin{code}
 ---------------------------------------------------------
 --     Preparing arguments for a call
 
-prepareArgs :: SDoc    -- Error message info
-           -> OutType -> ([Demand],Bool) -> SimplCont
+prepareArgs :: Bool    -- True if the no-case-of-case switch is on
+           -> OutId -> SimplCont
            -> ([OutExpr] -> SimplCont -> SimplM OutExprStuff)
            -> SimplM OutExprStuff
-
-prepareArgs pp_fun orig_fun_ty (fun_demands, result_bot) orig_cont thing_inside
+prepareArgs no_case_of_case fun orig_cont thing_inside
   = go [] demands orig_fun_ty orig_cont
   where
-    not_enough_args = fun_demands `lengthExceeds` countValArgs orig_cont
-       -- "No strictness info" is signalled by an infinite list of wwLazy
-    demands | not_enough_args = repeat wwLazy                  -- Not enough args, or no strictness
-           | result_bot      = fun_demands                     -- Enough args, and function returns bottom
-           | otherwise       = fun_demands ++ repeat wwLazy    -- Enough args and function does not return bottom
-       -- NB: demands is finite iff enough args and result_bot is True
+    orig_fun_ty = idType fun
+    is_data_con = isDataConId fun
+
+    (demands, result_bot)
+      | no_case_of_case = ([], False)  -- Ignore strictness info if the no-case-of-case
+                                       -- flag is on.  Strictness changes evaluation order
+                                       -- and that can change full laziness
+      | otherwise
+      = case idStrictness fun of
+         StrictnessInfo demands result_bot 
+               | 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)
+                  (demands, result_bot)
+
+         other -> ([], False)  -- Not enough args, or no strictness
 
        -- Main game plan: loop through the arguments, simplifying
        -- each of them in turn.  We carry with us a list of demands,
        -- and the type of the function-applied-to-earlier-args
 
+       -- We've run out of demands, and the result is now bottom
+       -- This deals with
+       --      * case (error "hello") of { ... }
+       --      * (error "Hello") arg
+       --      * f (error "Hello") where f is strict
+       --      etc
+    go acc [] fun_ty cont 
+       | result_bot
+       = tick_case_of_error cont               `thenSmpl_`
+         thing_inside (reverse acc) (discardCont cont)
+
        -- Type argument
     go acc ds fun_ty (ApplyTo _ arg@(Type ty_arg) se cont)
+       = simplTyArg ty_arg se  `thenSmpl` \ new_ty_arg ->
+         go (Type new_ty_arg : acc) ds (applyTy fun_ty new_ty_arg) cont
+
+       -- Value argument
+    go acc ds fun_ty (ApplyTo _ val_arg se cont)
+       | not is_data_con       -- Function isn't a data constructor
+       = simplValArg arg_ty dem val_arg se (contResultType cont)       $ \ new_arg ->
+         go (new_arg : acc) ds' res_ty cont
+
+       | exprIsTrivial val_arg -- Function is a data contstructor, arg is trivial
        = getInScope            `thenSmpl` \ in_scope ->
          let
-               ty_arg' = substTy (mkSubst in_scope se) ty_arg
-               res_ty  = applyTy fun_ty ty_arg'
+               new_arg = substExpr (mkSubst in_scope se) val_arg
+               -- Simplify the RHS with inlining switched off, so that
+               -- only absolutely essential things will happen.
+               -- If we don't do this, consider:
+               --      let x = +# p q in C {x}
+               -- Even though x get's an occurrence of 'many', its RHS looks cheap,
+               -- and there's a good chance it'll get inlined back into C's RHS. Urgh!
+               --
+               -- It's important that the substitution *does* deal with case-binder synonyms:
+               --      case x of y { True -> (x,1) }
+               -- Here we must be sure to substitute y for x when simplifying the args of the pair,
+               -- to increase the chances of being able to inline x.  The substituter will do
+               -- that because the x->y mapping is held in the in-scope set.
          in
-         go (Type ty_arg' : acc) ds res_ty cont
+               -- It's not always the case that the new arg will be trivial
+               -- Consider             f x
+               -- where, in one pass, f gets substituted by a constructor,
+               -- but x gets substituted by an expression (assume this is the
+               -- unique occurrence of x).  It doesn't really matter -- it'll get
+               -- fixed up next pass.  And it happens for dictionary construction,
+               -- which mentions the wrapper constructor to start with.
+
+         go (new_arg : acc) ds' res_ty cont
+
+       | otherwise
+       = simplValArg arg_ty dem val_arg se (contResultType cont)       $ \ new_arg ->
+                   -- A data constructor whose argument is now non-trivial;
+                   -- so let/case bind it.
+         newId SLIT("a") arg_ty                                $ \ arg_id ->
+         addNonRecBind arg_id new_arg                          $
+         go (Var arg_id : acc) ds' res_ty cont
 
-       -- Value argument
-    go acc (d:ds) fun_ty (ApplyTo _ val_arg se cont)
-       = case splitFunTy_maybe fun_ty of {
-               Nothing -> pprTrace "prepareArgs" (pp_fun $$ ppr orig_fun_ty $$ ppr orig_cont) 
-                          (thing_inside (reverse acc) cont) ;
-               Just (arg_ty, res_ty) ->
-         simplArg arg_ty d val_arg se (contResultType cont)    $ \ arg' ->
-         go (arg':acc) ds res_ty cont }
-
-       -- We've run out of demands, which only happens for functions
-       -- we *know* now return bottom
-       -- This deals with
-       --      * case (error "hello") of { ... }
-       --      * (error "Hello") arg
-       --      * f (error "Hello") where f is strict
-       --      etc
-    go acc [] fun_ty cont = tick_case_of_error cont            `thenSmpl_`
-                           thing_inside (reverse acc) (discardCont cont)
+       where
+         (arg_ty, res_ty) = splitFunTy fun_ty
+         (dem, ds') = case ds of 
+                       []     -> (wwLazy, [])
+                       (d:ds) -> (d,ds)
 
-       -- We're run out of arguments
+       -- We're run out of arguments and the result ain't bottom
     go acc ds fun_ty cont = thing_inside (reverse acc) cont
 
 -- Boring: we must only record a tick if there was an interesting
@@ -766,122 +916,7 @@ prepareArgs pp_fun orig_fun_ty (fun_demands, result_bot) orig_cont thing_inside
 tick_case_of_error (Stop _)             = returnSmpl ()
 tick_case_of_error (CoerceIt _ (Stop _)) = returnSmpl ()
 tick_case_of_error other                = tick BottomFound
-
----------------------------------------------------------
---     Dealing with a call
-
-completeCall black_list_fn in_scope var args cont
-       -- Look for rules or specialisations that match
-       -- Do this *before* trying inlining because some functions
-       -- have specialisations *and* are strict; we don't want to
-       -- inline the wrapper of the non-specialised thing... better
-       -- to call the specialised thing instead.
-  | maybeToBool maybe_rule_match
-  = tick (RuleFired rule_name)                 `thenSmpl_`
-    zapSubstEnv (completeApp rule_rhs rule_args cont)
-       -- See note below about zapping the substitution here
-
-       -- Look for an unfolding. There's a binding for the
-       -- thing, but perhaps we want to inline it anyway
-  | maybeToBool maybe_inline
-  = tick (UnfoldingDone var)           `thenSmpl_`
-    zapSubstEnv (completeInlining var unf_template args (discardInlineCont cont))
-               -- The template is already simplified, so don't re-substitute.
-               -- This is VITAL.  Consider
-               --      let x = e in
-               --      let y = \z -> ...x... in
-               --      \ x -> ...y...
-               -- We'll clone the inner \x, adding x->x' in the id_subst
-               -- Then when we inline y, we must *not* replace x by x' in
-               -- the inlined copy!!
-    
-  | otherwise          -- Neither rule nor inlining
-  = rebuild (mkApps (Var var) args) cont
-  
-  where
-       ---------- Unfolding stuff
-    maybe_inline  = callSiteInline black_listed inline_call 
-                                  var args interesting_cont
-    Just unf_template = maybe_inline
-    interesting_cont  = contIsInteresting cont
-    inline_call              = contIsInline cont
-    black_listed      = black_list_fn var
-
-       ---------- Specialisation stuff
-    maybe_rule_match           = lookupRule in_scope var args
-    Just (rule_name, rule_rhs, rule_args) = maybe_rule_match
-
-
--- First a special case
--- Don't actually inline the scrutinee when we see
---     case x of y { .... }
--- and x has unfolding (C a b).  Why not?  Because
--- we get a silly binding y = C a b.  If we don't
--- inline knownCon can directly substitute x for y instead.
-completeInlining var (Con con con_args) args (Select _ bndr alts se cont)
-  | conOkForAlt con 
-  = ASSERT( null args )
-    knownCon (Var var) con con_args bndr alts se cont
-
--- Now the normal case
-completeInlining var unfolding args cont
-  = completeApp unfolding args cont
-
--- completeApp applies a new InExpr (from an unfolding or rule)
--- to an *already simplified* set of arguments
-completeApp :: InExpr                  -- (\xs. body)
-           -> [OutExpr]                -- Args; already simplified
-           -> SimplCont                -- What to do with result of applicatoin
-           -> SimplM OutExprStuff
-completeApp fun args cont
-  = go fun args
-  where
-    zap_it = mkLamBndrZapper fun (length args)
-    cont_ty = contResultType cont
-
-    -- These equations are very similar to simplLam and simplBeta combined,
-    -- except that they deal with already-simplified arguments
-
-       -- Type argument
-    go (Lam bndr fun) (Type ty:args) = tick (BetaReduction bndr)       `thenSmpl_`
-                                      extendSubst bndr (DoneTy ty)
-                                      (go fun args)
-
-       -- Value argument
-    go (Lam bndr fun) (arg:args)
-         | preInlineUnconditionally bndr && not opt_SimplNoPreInlining
-         = tick (BetaReduction bndr)                   `thenSmpl_`
-           tick (PreInlineUnconditionally bndr)        `thenSmpl_`
-           extendSubst bndr (DoneEx arg)
-           (go fun args)
-         | otherwise
-         = tick (BetaReduction bndr)                   `thenSmpl_`
-           simplBinder zapped_bndr                     ( \ bndr' ->
-           completeBeta zapped_bndr bndr' arg          $
-           go fun args
-           )
-         where
-          zapped_bndr = zap_it bndr
-
-       -- Consumed all the lambda binders or args
-    go fun args = simplExprF fun (pushArgs emptySubstEnv args cont)
-
-
------------ costCentreOk
--- costCentreOk checks that it's ok to inline this thing
--- The time it *isn't* is this:
---
---     f x = let y = E in
---           scc "foo" (...y...)
---
--- Here y has a "current cost centre", and we can't inline it inside "foo",
--- regardless of whether E is a WHNF or not.
-    
-costCentreOk ccs_encl cc_rhs
-  =  not opt_SccProfilingOn
-  || isSubsumedCCS ccs_encl      -- can unfold anything into a subsumed scope
-  || not (isEmptyCC cc_rhs)      -- otherwise need a cc on the unfolding
-\end{code}                
+\end{code}
 
 
 %************************************************************************
@@ -890,8 +925,25 @@ costCentreOk ccs_encl cc_rhs
 %*                                                                     *
 %************************************************************************
 
+NB: At one time I tried not pre/post-inlining top-level things,
+even if they occur exactly once.  Reason: 
+       (a) some might appear as a function argument, so we simply
+               replace static allocation with dynamic allocation:
+                  l = <...>
+                  x = f x
+       becomes
+                  x = f <...>
+
+       (b) some top level things might be black listed
+
+HOWEVER, I found that some useful foldr/build fusion was lost (most
+notably in spectral/hartel/parstof) because the foldr didn't see the build.
+
+Doing the dynamic allocation isn't a big deal, in fact, but losing the
+fusion can be.
+
 \begin{code}
-preInlineUnconditionally :: InId -> Bool
+preInlineUnconditionally :: Bool {- Black listed -} -> InId -> Bool
        -- Examines a bndr to see if it is used just once in a 
        -- completely safe way, so that it is safe to discard the binding
        -- inline its RHS at the (unique) usage site, REGARDLESS of how
@@ -912,18 +964,18 @@ preInlineUnconditionally :: InId -> Bool
        -- 
        -- Evne RHSs labelled InlineMe aren't caught here, because
        -- there might be no benefit from inlining at the call site.
-       -- But things labelled 'IMustBeINLINEd' *are* caught.  We use this
-       -- for the trivial bindings introduced by SimplUtils.mkRhsTyLam
-preInlineUnconditionally bndr
-  = case getInlinePragma bndr of
-       IMustBeINLINEd                      -> True
-       ICanSafelyBeINLINEd InsideLam  _    -> False
-       ICanSafelyBeINLINEd not_in_lam True -> True     -- Not inside a lambda,
-                                                       -- one occurrence ==> safe!
-       other -> False
-
-
-postInlineUnconditionally :: InId -> OutExpr -> Bool
+
+preInlineUnconditionally black_listed bndr
+  | black_listed || opt_SimplNoPreInlining = False
+  | otherwise = case idOccInfo bndr of
+                 OneOcc in_lam once -> not in_lam && once
+                       -- Not inside a lambda, one occurrence ==> safe!
+                 other              -> False
+
+
+postInlineUnconditionally :: Bool      -- Black listed
+                         -> OccInfo
+                         -> InId -> OutExpr -> Bool
        -- Examines a (bndr = rhs) binding, AFTER the rhs has been simplified
        -- It returns True if it's ok to discard the binding and inline the
        -- RHS at every use site.
@@ -932,46 +984,22 @@ postInlineUnconditionally :: InId -> OutExpr -> Bool
        -- We're at the binding site right now, and
        -- we'll get another opportunity when we get to the ocurrence(s)
 
-postInlineUnconditionally bndr rhs
-  | isExportedId bndr 
-  = False
-  | otherwise
-  = case getInlinePragma bndr of
-       IAmALoopBreaker                           -> False   
-
-       ICanSafelyBeINLINEd InsideLam one_branch  -> exprIsTrivial rhs
-               -- Don't inline even WHNFs inside lambdas; doing so may
-               -- simply increase allocation when the function is called
-               -- This isn't the last chance; see NOTE above.
-
-       ICanSafelyBeINLINEd not_in_lam one_branch -> one_branch || exprIsTrivial rhs
-               -- Was 'exprIsDupable' instead of 'exprIsTrivial' but the
-               -- decision about duplicating code is best left to callSiteInline
-
-       other                                     -> exprIsTrivial rhs  -- Duplicating is *free*
-               -- NB: Even InlineMe and IMustBeINLINEd are ignored here
-               -- Why?  Because we don't even want to inline them into the
-               -- RHS of constructor arguments. See NOTE above
-               -- NB: Even IMustBeINLINEd is ignored here: if the rhs is trivial
-               -- it's best to inline it anyway.  We often get a=E; b=a
-               -- from desugaring, with both a and b marked NOINLINE.
-\end{code}
-
-\begin{code}
-inlineCase bndr scrut
-    =  exprIsTrivial scrut                     -- Duplication is free
-   && (  isUnLiftedType (idType bndr) 
-      || scrut_is_evald_var                    -- So dropping the case won't change termination
-      || isStrict (getIdDemandInfo bndr)       -- It's going to get evaluated later, so again
-                                               -- termination doesn't change
-      || not opt_SimplPedanticBottoms)         -- Or we don't care!
-  where
-       -- Check whether or not scrut is known to be evaluted
-       -- It's not going to be a visible value (else the previous
-       -- blob would apply) so we just check the variable case
-    scrut_is_evald_var = case scrut of
-                               Var v -> isEvaldUnfolding (getIdUnfolding v)
-                               other -> False
+postInlineUnconditionally black_listed occ_info bndr rhs
+  | isExportedId bndr  || 
+    black_listed       || 
+    isLoopBreaker occ_info = False             -- Don't inline these
+  | otherwise             = exprIsTrivial rhs  -- Duplicating is free
+       -- Don't inline even WHNFs inside lambdas; doing so may
+       -- simply increase allocation when the function is called
+       -- This isn't the last chance; see NOTE above.
+       --
+       -- NB: Even inline pragmas (e.g. IMustBeINLINEd) are ignored here
+       -- Why?  Because we don't even want to inline them into the
+       -- RHS of constructor arguments. See NOTE above
+       --
+       -- NB: Even NOINLINEis ignored here: if the rhs is trivial
+       -- it's best to inline it anyway.  We often get a=E; b=a
+       -- from desugaring, with both a and b marked NOINLINE.
 \end{code}
 
 
@@ -1005,50 +1033,14 @@ rebuild expr cont@(ApplyTo _ arg se cont')
 
 --     Coerce continuation
 rebuild expr (CoerceIt to_ty cont)
-  = rebuild (mkCoerce to_ty expr) cont
+  = rebuild (mkCoerce to_ty (exprType expr) expr) cont
 
 --     Inline continuation
 rebuild expr (InlinePlease cont)
   = rebuild (Note InlineCall expr) cont
 
---     Case of known constructor or literal
-rebuild expr@(Con con args) (Select _ bndr alts se cont)
-  | conOkForAlt con    -- Knocks out PrimOps and NoRepLits
-  = knownCon expr con args bndr alts se cont
-
---     Case of other value (e.g. a partial application or lambda)
---     Turn it back into a let
-rebuild scrut (Select _ bndr ((DEFAULT, bs, rhs):alts) se cont)
-  |  isUnLiftedType (idType bndr) && exprOkForSpeculation scrut
-  || exprIsWHNF scrut
-  = ASSERT( null bs && null alts )
-    setSubstEnv se                     $                       
-    simplBinder bndr                   $ \ bndr' ->
-    completeBinding bndr bndr' scrut   $
-    simplExprF rhs cont
-
-
----------------------------------------------------------
---     The other Select cases
-
 rebuild scrut (Select _ bndr alts se cont)
-  | all (cheapEqExpr rhs1) other_rhss
-    && inlineCase bndr scrut
-    && all binders_unused alts
-    && opt_SimplDoCaseElim
-  =    -- Get rid of the case altogether
-       -- See the extensive notes on case-elimination below
-       -- Remember to bind the binder though!
-           tick (CaseElim bndr)                `thenSmpl_`
-           setSubstEnv se                      (
-           extendSubst bndr (DoneEx scrut)     $
-           simplExprF rhs1 cont
-           )
-  | otherwise
   = rebuild_case scrut bndr alts se cont
-  where
-    (rhs1:other_rhss)           = [rhs | (_,_,rhs) <- alts]
-    binders_unused (_, bndrs, _) = all isDeadBinder bndrs
 \end{code}
 
 Case elimination [see the code above]
@@ -1134,68 +1126,127 @@ Blob of helper functions for the "case-of-something-else" situation.
 
 \begin{code}
 ---------------------------------------------------------
+--     Eliminate the case if possible
+
+rebuild_case scrut bndr alts se cont
+  | maybeToBool maybe_con_app
+  = knownCon scrut (DataAlt con) args bndr alts se cont
+
+  | canEliminateCase scrut bndr alts
+  = tick (CaseElim bndr)                       `thenSmpl_` (
+    setSubstEnv se                             $                       
+    simplBinder bndr                           $ \ bndr' ->
+       -- Remember to bind the case binder!
+    completeBinding bndr bndr' False False scrut       $
+    simplExprF (head (rhssOfAlts alts)) cont)
+
+  | otherwise
+  = complete_case scrut bndr alts se cont
+
+  where
+    maybe_con_app    = exprIsConApp_maybe scrut
+    Just (con, args) = maybe_con_app
+
+       -- See if we can get rid of the case altogether
+       -- See the extensive notes on case-elimination above
+canEliminateCase scrut bndr alts
+  =    -- Check that the RHSs are all the same, and
+       -- don't use the binders in the alternatives
+       -- This test succeeds rapidly in the common case of
+       -- a single DEFAULT alternative
+    all (cheapEqExpr rhs1) other_rhss && all binders_unused alts
+
+       -- 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
+       )
+
+  where
+    (rhs1:other_rhss)           = rhssOfAlts alts
+    binders_unused (_, bndrs, _) = all isDeadBinder bndrs
+
+    var_demanded_later (Var v) = isStrict (idDemandInfo bndr)  -- It's going to be evaluated later
+    var_demanded_later other   = False
+
+
+---------------------------------------------------------
 --     Case of something else
 
-rebuild_case scrut case_bndr alts se cont
+complete_case scrut case_bndr alts se cont
   =    -- Prepare case alternatives
     prepareCaseAlts case_bndr (splitTyConApp_maybe (idType case_bndr))
-                   scrut_cons alts             `thenSmpl` \ better_alts ->
+                   impossible_cons alts                `thenSmpl` \ better_alts ->
     
        -- Set the new subst-env in place (before dealing with the case binder)
     setSubstEnv se                             $
 
        -- Deal with the case binder, and prepare the continuation;
        -- The new subst_env is in place
-    simplBinder case_bndr                      $ \ case_bndr' ->
     prepareCaseCont better_alts cont           $ \ cont' ->
        
 
        -- Deal with variable scrutinee
-    substForVarScrut scrut case_bndr'          $ \ zap_occ_info ->
-    let
-       case_bndr'' = zap_occ_info case_bndr'
-    in
+    (  
+        getSwitchChecker                               `thenSmpl` \ chkr ->
+       simplCaseBinder (switchIsOn chkr NoCaseOfCase)
+                       scrut case_bndr                 $ \ case_bndr' zap_occ_info ->
 
-       -- Deal with the case alternaatives
-    simplAlts zap_occ_info scrut_cons 
-             case_bndr'' better_alts cont'     `thenSmpl` \ alts' ->
+       -- Deal with the case alternatives
+       simplAlts zap_occ_info impossible_cons
+                 case_bndr' better_alts cont'  `thenSmpl` \ alts' ->
 
-    mkCase scrut case_bndr'' alts'             `thenSmpl` \ case_expr ->
+       mkCase scrut case_bndr' alts'
+    )                                          `thenSmpl` \ case_expr ->
+
+       -- Notice that the simplBinder, prepareCaseCont, etc, do *not* scope
+       -- over the rebuild_done; rebuild_done returns the in-scope set, and
+       -- that should not include these chaps!
     rebuild_done case_expr     
   where
-       -- scrut_cons tells what constructors the scrutinee can't possibly match
-    scrut_cons = case scrut of
-                  Var v -> case getIdUnfolding v of
-                               OtherCon cons -> cons
-                               other         -> []
-                  other -> []
+    impossible_cons = case scrut of
+                           Var v -> otherCons (idUnfolding v)
+                           other -> []
 
 
+knownCon :: OutExpr -> AltCon -> [OutExpr]
+        -> InId -> [InAlt] -> SubstEnv -> SimplCont
+        -> SimplM OutExprStuff
+
 knownCon expr con args bndr alts se cont
   = tick (KnownBranch bndr)    `thenSmpl_`
     setSubstEnv se             (
     simplBinder bndr           $ \ bndr' ->
+    completeBinding bndr bndr' False False expr $
+       -- Don't use completeBeta here.  The expr might be
+       -- an unboxed literal, like 3, or a variable
+       -- whose unfolding is an unboxed literal... and
+       -- completeBeta will just construct another case
+                                       -- expression!
     case findAlt con alts of
        (DEFAULT, bs, rhs)     -> ASSERT( null bs )
-                                 completeBinding bndr bndr' expr $
-                                       -- Don't use completeBeta here.  The expr might be
-                                       -- an unboxed literal, like 3, or a variable
-                                       -- whose unfolding is an unboxed literal... and
-                                       -- completeBeta will just construct another case
-                                       -- expression!
                                  simplExprF rhs cont
 
-       (Literal lit, bs, rhs) -> ASSERT( null bs )
-                                 extendSubst bndr (DoneEx expr)        $
-                                       -- Unconditionally substitute, because expr must
-                                       -- be a variable or a literal.  It can't be a
-                                       -- NoRep literal because they don't occur in
-                                       -- case patterns.
+       (LitAlt lit, bs, rhs) ->  ASSERT( null bs )
                                  simplExprF rhs cont
 
-       (DataCon dc, bs, rhs)  -> ASSERT( length bs == length real_args )
-                                 completeBinding bndr bndr' expr       $
-                                       -- See note above
+       (DataAlt dc, bs, rhs)  -> ASSERT( length bs == length real_args )
                                  extendSubstList bs (map mk real_args) $
                                  simplExprF rhs cont
                               where
@@ -1212,13 +1263,29 @@ prepareCaseCont :: [InAlt] -> SimplCont
        -- Polymorphic recursion here!
 
 prepareCaseCont [alt] cont thing_inside = thing_inside cont
-prepareCaseCont alts  cont thing_inside = mkDupableCont (coreAltsType alts) cont thing_inside
+prepareCaseCont alts  cont thing_inside = simplType (coreAltsType alts)                `thenSmpl` \ alts_ty ->
+                                         mkDupableCont alts_ty cont thing_inside
+       -- At one time I passed in the un-simplified type, and simplified
+       -- it only if we needed to construct a join binder, but that    
+       -- didn't work because we have to decompse function types
+       -- (using funResultTy) in mkDupableCont.
 \end{code}
 
-substForVarScrut checks whether the scrutinee is a variable, v.
+simplCaseBinder checks whether the scrutinee is a variable, v.
 If so, try to eliminate uses of v in the RHSs in favour of case_bndr; 
 that way, there's a chance that v will now only be used once, and hence inlined.
 
+There is a time we *don't* want to do that, namely when -fno-case-of-case
+is on.  This happens in the first simplifier pass, and enhances full laziness.
+Here's the bad case:
+       f = \ y -> ...(case x of I# v -> ...(case x of ...) ... )
+If we eliminate the inner case, we trap it inside the I# v -> arm,
+which might prevent some full laziness happening.  I've seen this
+in action in spectral/cichelli/Prog.hs:
+        [(m,n) | m <- [1..max], n <- [1..max]]
+Hence the no_case_of_case argument
+
+
 If we do this, then we have to nuke any occurrence info (eg IAmDead)
 in the case binder, because the case-binder now effectively occurs
 whenever v does.  AND we have to do the same for the pattern-bound
@@ -1232,20 +1299,23 @@ case RHS, and eliminate the second case, we get
        case x or { (a,b) -> a b }
 
 Urk! b is alive!  Reason: the scrutinee was a variable, and case elimination
-happened.  Hence the zap_occ_info function returned by substForVarScrut
+happened.  Hence the zap_occ_info function returned by simplCaseBinder
 
 \begin{code}
-substForVarScrut (Var v) case_bndr' thing_inside
-  | isLocallyDefined v         -- No point for imported things
-  = modifyInScope (v `setIdUnfolding` mkUnfolding (Var case_bndr')
-                    `setInlinePragma` IMustBeINLINEd)                  $
+simplCaseBinder no_case_of_case (Var v) case_bndr thing_inside
+  | not no_case_of_case
+  = simplBinder (zap case_bndr)                                        $ \ case_bndr' ->
+    modifyInScope v case_bndr'                                 $
        -- We could extend the substitution instead, but it would be
        -- a hack because then the substitution wouldn't be idempotent
-       -- any more.
-    thing_inside (\ bndr ->  bndr `setInlinePragma` NoInlinePragInfo)
+       -- any more (v is an OutId).  And this just just as well.
+    thing_inside case_bndr' zap
+  where
+    zap b = b `setIdOccInfo` NoOccInfo
            
-substForVarScrut other_scrut case_bndr' thing_inside
-  = thing_inside (\ bndr -> bndr)      -- NoOp on bndr
+simplCaseBinder add_eval_info other_scrut case_bndr thing_inside
+  = simplBinder case_bndr              $ \ case_bndr' ->
+    thing_inside case_bndr' (\ bndr -> bndr)   -- NoOp on bndr
 \end{code}
 
 prepareCaseAlts does two things:
@@ -1275,11 +1345,11 @@ prepareCaseAlts bndr (Just (tycon, inst_tys)) scrut_cons alts
                   let
                        ex_tyvars' = zipWithEqual "simpl_alt" mk tv_uniqs ex_tyvars
                        mk uniq tv = mkSysTyVar uniq (tyVarKind tv)
+                       arg_tys    = dataConArgTys data_con
+                                                  (inst_tys ++ mkTyVarTys ex_tyvars')
                   in
-                  newIds (dataConArgTys
-                               data_con
-                               (inst_tys ++ mkTyVarTys ex_tyvars'))            $ \ bndrs ->
-                  returnSmpl ((DataCon data_con, ex_tyvars' ++ bndrs, rhs) : alts_no_deflt)
+                  newIds SLIT("a") arg_tys             $ \ bndrs ->
+                  returnSmpl ((DataAlt data_con, ex_tyvars' ++ bndrs, rhs) : alts_no_deflt)
 
        other -> returnSmpl filtered_alts
   where
@@ -1290,8 +1360,8 @@ prepareCaseAlts bndr (Just (tycon, inst_tys)) scrut_cons alts
 
     missing_cons = [data_con | data_con <- tyConDataCons tycon, 
                               not (data_con `elem` handled_data_cons)]
-    handled_data_cons = [data_con | DataCon data_con         <- scrut_cons] ++
-                       [data_con | (DataCon data_con, _, _) <- filtered_alts]
+    handled_data_cons = [data_con | DataAlt data_con         <- scrut_cons] ++
+                       [data_con | (DataAlt data_con, _, _) <- filtered_alts]
 
 -- The default case
 prepareCaseAlts _ _ scrut_cons alts
@@ -1299,10 +1369,10 @@ prepareCaseAlts _ _ scrut_cons alts
 
 
 ----------------------
-simplAlts zap_occ_info scrut_cons case_bndr'' alts cont'
+simplAlts zap_occ_info scrut_cons case_bndr' alts cont'
   = mapSmpl simpl_alt alts
   where
-    inst_tys' = case splitTyConApp_maybe (idType case_bndr'') of
+    inst_tys' = case splitTyConApp_maybe (idType case_bndr') of
                        Just (tycon, inst_tys) -> inst_tys
 
        -- handled_cons is all the constructors that are dealt
@@ -1313,21 +1383,24 @@ simplAlts zap_occ_info scrut_cons case_bndr'' alts cont'
        =       -- In the default case we record the constructors that the
                -- case-binder *can't* be.
                -- We take advantage of any OtherCon info in the case scrutinee
-         modifyInScope (case_bndr'' `setIdUnfolding` OtherCon handled_cons)    $ 
+         modifyInScope case_bndr' (case_bndr' `setIdUnfolding` mkOtherCon handled_cons)        $ 
          simplExprC rhs cont'                                                  `thenSmpl` \ rhs' ->
          returnSmpl (DEFAULT, [], rhs')
 
     simpl_alt (con, vs, rhs)
        =       -- Deal with the pattern-bound variables
                -- Mark the ones that are in ! positions in the data constructor
-               -- as certainly-evaluated
-         simplBinders (add_evals con vs)       $ \ vs' ->
+               -- as certainly-evaluated.
+               -- NB: it happens that simplBinders does *not* erase the OtherCon
+               --     form of unfolding, so it's ok to add this info before 
+               --     doing simplBinders
+         simplBinders (add_evals con vs)                                       $ \ vs' ->
 
-               -- Bind the case-binder to (Con args)
+               -- Bind the case-binder to (con args)
          let
-               con_app = Con con (map Type inst_tys' ++ map varToCoreExpr vs')
+               unfolding = mkUnfolding False (mkAltExpr con vs' inst_tys')
          in
-         modifyInScope (case_bndr'' `setIdUnfolding` mkUnfolding con_app)      $
+         modifyInScope case_bndr' (case_bndr' `setIdUnfolding` unfolding)      $
          simplExprC rhs cont'          `thenSmpl` \ rhs' ->
          returnSmpl (con, vs', rhs')
 
@@ -1341,14 +1414,14 @@ simplAlts zap_occ_info scrut_cons case_bndr'' alts cont'
        -- We really must record that b is already evaluated so that we don't
        -- go and re-evaluate it when constructing the result.
 
-    add_evals (DataCon dc) vs = cat_evals vs (dataConRepStrictness dc)
+    add_evals (DataAlt dc) vs = cat_evals vs (dataConRepStrictness dc)
     add_evals other_con    vs = vs
 
     cat_evals [] [] = []
     cat_evals (v:vs) (str:strs)
-       | isTyVar v    = v                                 : cat_evals vs (str:strs)
-       | isStrict str = (v' `setIdUnfolding` OtherCon []) : cat_evals vs strs
-       | otherwise    = v'                                : cat_evals vs strs
+       | isTyVar v    = v                                   : cat_evals vs (str:strs)
+       | isStrict str = (v' `setIdUnfolding` mkOtherCon []) : cat_evals vs strs
+       | otherwise    = v'                                  : cat_evals vs strs
        where
          v' = zap_occ_info v
 \end{code}
@@ -1361,7 +1434,7 @@ simplAlts zap_occ_info scrut_cons case_bndr'' alts cont'
 %************************************************************************
 
 \begin{code}
-mkDupableCont :: InType                -- Type of the thing to be given to the continuation
+mkDupableCont :: OutType               -- Type of the thing to be given to the continuation
              -> SimplCont 
              -> (SimplCont -> SimplM (OutStuff a))
              -> SimplM (OutStuff a)
@@ -1379,23 +1452,25 @@ mkDupableCont ty (InlinePlease cont) thing_inside
 
 mkDupableCont join_arg_ty (ArgOf _ cont_ty cont_fn) thing_inside
   =    -- Build the RHS of the join point
-    simplType join_arg_ty                              `thenSmpl` \ join_arg_ty' ->
-    newId join_arg_ty'                                 ( \ arg_id ->
-       getSwitchChecker                                `thenSmpl` \ chkr ->
+    newId SLIT("a") join_arg_ty                                ( \ arg_id ->
        cont_fn (Var arg_id)                            `thenSmpl` \ (binds, (_, rhs)) ->
-       returnSmpl (Lam arg_id (mkLets binds rhs))
+       returnSmpl (Lam (setOneShotLambda arg_id) (mkLets binds rhs))
     )                                                  `thenSmpl` \ join_rhs ->
    
        -- Build the join Id and continuation
-    newId (coreExprType join_rhs)              $ \ join_id ->
+       -- We give it a "$j" name just so that for later amusement
+       -- we can identify any join points that don't end up as let-no-escapes
+    newId SLIT("$j") (exprType join_rhs)               $ \ join_id ->
     let
        new_cont = ArgOf OkToDup cont_ty
                         (\arg' -> rebuild_done (App (Var join_id) arg'))
     in
-       
-       -- Do the thing inside
-    thing_inside new_cont              `thenSmpl` \ res ->
-    returnSmpl (addBind (NonRec join_id join_rhs) res)
+
+    tick (CaseOfCase join_id)                                          `thenSmpl_`
+       -- Want to tick here so that we go round again,
+       -- and maybe copy or inline the code;
+       -- not strictly CaseOf Case
+    addLetBind join_id join_rhs        (thing_inside new_cont)
 
 mkDupableCont ty (ApplyTo _ arg se cont) thing_inside
   = mkDupableCont (funResultTy ty) cont                $ \ cont' ->
@@ -1403,9 +1478,21 @@ mkDupableCont ty (ApplyTo _ arg se cont) thing_inside
     if exprIsDupable arg' then
        thing_inside (ApplyTo OkToDup arg' emptySubstEnv cont')
     else
-    newId (coreExprType arg')                                          $ \ bndr ->
-    thing_inside (ApplyTo OkToDup (Var bndr) emptySubstEnv cont')      `thenSmpl` \ res ->
-    returnSmpl (addBind (NonRec bndr arg') res)
+    newId SLIT("a") (exprType arg')                    $ \ bndr ->
+
+    tick (CaseOfCase bndr)                             `thenSmpl_`
+       -- Want to tick here so that we go round again,
+       -- and maybe copy or inline the code;
+       -- not strictly CaseOf Case
+
+     addLetBind bndr arg'                                              $
+       -- But what if the arg should be case-bound?  We can't use
+       -- addNonRecBind here because its type is too specific.
+       -- This has been this way for a long time, so I'll leave it,
+       -- but I can't convince myself that it's right.
+
+     thing_inside (ApplyTo OkToDup (Var bndr) emptySubstEnv cont')
+
 
 mkDupableCont ty (Select _ case_bndr alts se cont) thing_inside
   = tick (CaseOfCase case_bndr)                                                `thenSmpl_`
@@ -1425,19 +1512,37 @@ mkDupableCont ty (Select _ case_bndr alts se cont) thing_inside
        -- This is VITAL when the type of case_bndr is an unboxed pair (often the
        -- case in I/O rich code.  We aren't allowed a lambda bound
        -- arg of unboxed tuple type, and indeed such a case_bndr is always dead
-    thing_inside (Select OkToDup case_bndr alts' se (Stop (contResultType cont)))      `thenSmpl` \ res ->
-
-    returnSmpl (addBinds alt_binds res)
-
+    addLetBinds alt_binds                                      $
+    thing_inside (Select OkToDup case_bndr alts' se (Stop (contResultType cont)))
 
 mkDupableAlt :: InId -> OutId -> SimplCont -> InAlt -> SimplM (OutStuff InAlt)
 mkDupableAlt case_bndr case_bndr' cont alt@(con, bndrs, rhs)
-  =    -- Not worth checking whether the rhs is small; the
-       -- inliner will inline it if so.
-    simplBinders bndrs                                 $ \ bndrs' ->
+  = simplBinders bndrs                                 $ \ bndrs' ->
     simplExprC rhs cont                                        `thenSmpl` \ rhs' ->
+
+    if (case cont of { Stop _ -> exprIsDupable rhs'; other -> False}) then
+       -- It is worth checking for a small RHS because otherwise we
+       -- get extra let bindings that may cause an extra iteration of the simplifier to
+       -- inline back in place.  Quite often the rhs is just a variable or constructor.
+       -- The Ord instance of Maybe in PrelMaybe.lhs, for example, took several extra
+       -- iterations because the version with the let bindings looked big, and so wasn't
+       -- inlined, but after the join points had been inlined it looked smaller, and so
+       -- was inlined.
+       --
+       -- But since the continuation is absorbed into the rhs, we only do this
+       -- for a Stop continuation.
+       --
+       -- NB: we have to check the size of rhs', not rhs. 
+       -- Duplicating a small InAlt might invalidate occurrence information
+       -- However, if it *is* dupable, we return the *un* simplified alternative,
+       -- because otherwise we'd need to pair it up with an empty subst-env.
+       -- (Remember we must zap the subst-env before re-simplifying something).
+       -- Rather than do this we simply agree to re-simplify the original (small) thing later.
+       returnSmpl ([], alt)
+
+    else
     let
-       rhs_ty' = coreExprType rhs'
+       rhs_ty' = exprType rhs'
         (used_bndrs, used_bndrs')
           = unzip [pr | pr@(bndr,bndr') <- zip (case_bndr  : bndrs)
                                                (case_bndr' : bndrs'),
@@ -1465,15 +1570,26 @@ mkDupableAlt case_bndr case_bndr' cont alt@(con, bndrs, rhs)
        --
        -- Now CPR should not w/w j because it's a thunk, so
        -- that means that the enclosing function can't w/w either,
-       -- which is a BIG LOSE.  This actually happens in practice
-       then newId realWorldStatePrimTy  $ \ rw_id ->
+       -- which is a lose.  Here's the example that happened in practice:
+       --      kgmod :: Int -> Int -> Int
+       --      kgmod x y = if x > 0 && y < 0 || x < 0 && y > 0
+       --                  then 78
+       --                  else 5
+
+       then newId SLIT("w") realWorldStatePrimTy  $ \ rw_id ->
             returnSmpl ([rw_id], [Var realWorldPrimId])
        else 
             returnSmpl (used_bndrs', map varToCoreExpr used_bndrs)
     )
        `thenSmpl` \ (final_bndrs', final_args) ->
 
-    newId (foldr (mkFunTy . idType) rhs_ty' final_bndrs')      $ \ join_bndr ->
-    returnSmpl ([NonRec join_bndr (mkLams final_bndrs' rhs')],
+       -- See comment about "$j" name above
+    newId SLIT("$j") (foldr (mkFunTy . idType) rhs_ty' final_bndrs')   $ \ join_bndr ->
+
+       -- Notice that we make the lambdas into one-shot-lambdas.  The
+       -- join point is sure to be applied at most once, and doing so
+       -- prevents the body of the join point being floated out by
+       -- the full laziness pass
+    returnSmpl ([NonRec join_bndr (mkLams (map setOneShotLambda final_bndrs') rhs')],
                (con, bndrs, mkApps (Var join_bndr) final_args))
 \end{code}