[project @ 2001-02-26 15:42:24 by simonpj]
[ghc-hetmet.git] / ghc / compiler / simplCore / Simplify.lhs
index 03ad9eb..131b56c 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,62 @@ module Simplify ( simplTopBinds, simplExpr ) where
 
 #include "HsVersions.h"
 
-import CmdLineOpts     ( intSwitchSet,
-                         opt_SccProfilingOn, opt_PprStyle_Debug, opt_SimplDoEtaReduction,
-                         opt_SimplNoPreInlining, opt_DictsStrict, opt_SimplPedanticBottoms,
-                         opt_SimplDoCaseElim,
+import CmdLineOpts     ( switchIsOn, opt_SimplDoEtaReduction,
+                         opt_SimplNoPreInlining, 
+                         dopt, DynFlag(Opt_D_dump_inlinings),
                          SimplifierSwitch(..)
                        )
 import SimplMonad
-import SimplUtils      ( mkCase, transformRhs, findAlt,
-                         simplBinder, simplBinders, simplIds, findDefault, mkCoerce
+import SimplUtils      ( mkCase, tryRhsTyLam, tryEtaExpansion,
+                         simplBinder, simplBinders, simplIds, 
+                         SimplCont(..), DupFlag(..), mkStop, mkRhsStop,
+                         contResultType, discardInline, countArgs, contIsDupable,
+                         getContArgs, interestingCallContext, interestingArg, isStrictType
                        )
-import Var             ( TyVar, mkSysTyVar, tyVarKind, maybeModifyIdInfo )
+import Var             ( mkSysTyVar, tyVarKind )
 import VarEnv
-import VarSet
-import Id              ( Id, idType, idInfo, idUnique,
-                         getIdUnfolding, setIdUnfolding, isExportedId, 
-                         getIdSpecialisation, setIdSpecialisation,
-                         getIdDemandInfo, setIdDemandInfo,
-                         getIdArity, setIdArity, 
-                         getIdStrictness, 
-                         setInlinePragma, getInlinePragma, idMustBeINLINEd,
-                         setOneShotLambda
+import Id              ( Id, idType, idInfo, isDataConId, hasNoBinding,
+                         idUnfolding, setIdUnfolding, isExportedId, isDeadBinder,
+                         idDemandInfo, setIdInfo,
+                         idOccInfo, setIdOccInfo, 
+                         zapLamIdInfo, setOneShotLambda, 
                        )
-import IdInfo          ( InlinePragInfo(..), OccInfo(..), StrictnessInfo(..), 
-                         ArityInfo(..), atLeastArity, arityLowerBound, unknownArity,
-                         specInfo, inlinePragInfo, zapLamIdInfo
+import IdInfo          ( OccInfo(..), isDeadOcc, isLoopBreaker,
+                         setArityInfo, 
+                         setUnfoldingInfo, atLeastArity,
+                         occInfo
+                       )
+import Demand          ( isStrict )
+import DataCon         ( dataConNumInstArgs, dataConRepStrictness,
+                         dataConSig, dataConArgTys
                        )
-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 Name            ( isLocallyDefined )
 import CoreSyn
-import CoreFVs         ( exprFreeVars )
-import CoreUnfold      ( Unfolding, mkOtherCon, mkUnfolding, otherCons,
-                         callSiteInline, blackListed
+import PprCore         ( pprParendExpr, pprCoreExpr )
+import CoreFVs         ( mustHaveLocalBinding )
+import CoreUnfold      ( mkOtherCon, mkUnfolding, otherCons,
+                         callSiteInline
                        )
-import CoreUtils       ( cheapEqExpr, exprIsDupable, exprIsCheap, exprIsTrivial,
-                         coreExprType, coreAltsType, exprArity, exprIsValue,
-                         exprOkForSpeculation
+import CoreUtils       ( cheapEqExpr, exprIsDupable, exprIsTrivial, 
+                         exprIsConApp_maybe, mkPiType, findAlt, findDefault,
+                         exprType, coreAltsType, exprIsValue, 
+                         exprOkForSpeculation, exprArity, exprIsCheap,
+                         mkCoerce, mkSCC, mkInlineMe, mkAltExpr
                        )
 import Rules           ( lookupRule )
-import CostCentre      ( isSubsumedCCS, currentCCS, isEmptyCC )
-import Type            ( Type, mkTyVarTy, mkTyVarTys, isUnLiftedType, 
-                         mkFunTy, splitFunTys, splitTyConApp_maybe, splitFunTy_maybe,
-                         funResultTy, isDictTy, isDataType, applyTy, applyTys, mkFunTys
+import CostCentre      ( currentCCS )
+import Type            ( mkTyVarTys, isUnLiftedType, seqType,
+                         mkFunTy, splitTyConApp_maybe, tyConAppArgs,
+                         funResultTy
                        )
-import Subst           ( Subst, mkSubst, emptySubst, substExpr, substTy, 
-                         substEnv, lookupInScope, lookupSubst, substRules
+import Subst           ( mkSubst, substTy, 
+                         isInScope, lookupIdSubst, substIdInfo
                        )
-import TyCon           ( isDataTyCon, tyConDataCons, tyConClass_maybe, tyConArity, isDataTyCon )
+import TyCon           ( isDataTyCon, tyConDataConsIfAvailable )
 import TysPrim         ( realWorldStatePrimTy )
 import PrelInfo                ( realWorldPrimId )
-import BasicTypes      ( TopLevelFlag(..), isTopLevel )
+import OrdList
 import Maybes          ( maybeToBool )
-import Util            ( zipWithEqual, stretchZipEqual, lengthExceeds )
-import PprCore
+import Util            ( zipWithEqual )
 import Outputable
 \end{code}
 
@@ -74,6 +72,16 @@ The guts of the simplifier is in this module, but the driver
 loop for the simplifier is in SimplCore.lhs.
 
 
+-----------------------------------------
+       *** IMPORTANT NOTE ***
+-----------------------------------------
+The simplifier used to guarantee that the output had no shadowing, but
+it does not do so any more.   (Actually, it never did!)  The reason is
+documented with simplifyArgs.
+
+
+
+
 %************************************************************************
 %*                                                                     *
 \subsection{Bindings}
@@ -88,26 +96,28 @@ 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_`
-    returnSmpl binds'
+    simplIds (bindersOfBinds binds)    $ \ bndrs' -> 
+    simpl_binds binds bndrs'           `thenSmpl` \ (binds', _) ->
+    freeTick SimplifierDone            `thenSmpl_`
+    returnSmpl (fromOL 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 (nilOL, 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 (unitOL (Rec (flattenBinds (fromOL binds'))) `appOL` binds'', res)
   where
     go [] _ = thing_inside     `thenSmpl` \ stuff ->
-             returnSmpl ([], stuff)
+             returnOutStuff stuff
        
     go ((bndr, rhs) : pairs) (bndr' : bndrs')
        = simplLazyBind top_lvl bndr bndr' rhs (go pairs bndrs')
@@ -122,15 +132,6 @@ simplRecBind top_lvl pairs bndrs' thing_inside
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-addBind :: CoreBind -> OutStuff a -> OutStuff a
-addBind bind    (binds,  res) = (bind:binds,     res)
-
-addBinds :: [CoreBind] -> OutStuff a -> OutStuff a
-addBinds []     stuff        = stuff
-addBinds binds1 (binds2, res) = (binds1++binds2, res)
-\end{code}
-
 The reason for this OutExprStuff stuff is that we want to float *after*
 simplifying a RHS, not before.  If we do so naively we get quadratic
 behaviour as things float out.
@@ -172,16 +173,17 @@ 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 (mkStop (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
 
 simplExprC expr cont = simplExprF expr cont    `thenSmpl` \ (floats, (_, body)) ->
-                      returnSmpl (mkLets floats body)
+                      returnSmpl (wrapFloats floats body)
 
 simplExprF :: InExpr -> SimplCont -> SimplM OutExprStuff
        -- Simplify an expression, returning floated binds
@@ -189,47 +191,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 
+                                (mkStop (contResultType cont)))        `thenSmpl` \ case_expr' ->
+       rebuild case_expr' cont
 
 
 simplExprF (Let (Rec pairs) body) cont
@@ -237,32 +221,47 @@ 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 } )
+  = 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)
 
--- Comments about the InlineMe case 
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--      Comments about the InlineMe case 
+--      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -- Don't inline in the RHS of something that has an
 -- inline pragma.  But be careful that the InScopeEnv that
 -- we return does still have inlinings on!
@@ -278,17 +277,31 @@ simplExprF (Note InlineCall e) cont
 -- the specialised version of g when f is inlined at some call site
 -- (perhaps in some other module).
 
-simplExprF (Note InlineMe e) cont
-  = case cont of
-       Stop _ ->       -- Totally boring continuation
-                       -- Don't inline inside an INLINE expression
-                 switchOffInlining (simplExpr e)       `thenSmpl` \ e' ->
-                 rebuild (mkNote InlineMe e') cont
+-- It's also important not to inline a worker back into a wrapper.
+-- A wrapper looks like
+--     wraper = inline_me (\x -> ...worker... )
+-- Normally, the inline_me prevents the worker getting inlined into
+-- the wrapper (initially, the worker's only call site!).  But,
+-- if the wrapper is sure to be called, the strictness analyser will
+-- mark it 'demanded', so when the RHS is simplified, it'll get an ArgOf
+-- continuation.  That's why the keep_inline predicate returns True for
+-- ArgOf continuations.  It shouldn't do any harm not to dissolve the
+-- inline-me note under these circumstances
 
-       other  ->       -- Dissolve the InlineMe note if there's
-                       -- an interesting context of any kind to combine with
-                       -- (even a type application -- anything except Stop)
-                 simplExprF e cont     
+simplExprF (Note InlineMe e) cont
+  | keep_inline cont           -- Totally boring continuation
+  =                            -- Don't inline inside an INLINE expression
+    setBlackList noInlineBlackList (simplExpr e)       `thenSmpl` \ e' ->
+    rebuild (mkInlineMe e') cont
+
+  | otherwise          -- Dissolve the InlineMe note if there's
+               -- an interesting context of any kind to combine with
+               -- (even a type application -- anything except Stop)
+  = simplExprF e cont
+  where
+    keep_inline (Stop _ _)    = True           -- See notes above
+    keep_inline (ArgOf _ _ _) = True           -- about this predicate
+    keep_inline other        = False
 
 -- A non-recursive let is dealt with by simplBeta
 simplExprF (Let (NonRec bndr rhs) body) cont
@@ -304,18 +317,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
@@ -332,78 +342,58 @@ 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, so there are real lambdas left to put in the result
+
+-- 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
 
-completeLam acc (Lam bndr body) cont
+completeLam rev_bndrs (Lam bndr body) cont
   = simplBinder bndr                   $ \ bndr' ->
-    completeLam (bndr':acc) body cont
+    completeLam (bndr':rev_bndrs) body cont
 
-completeLam acc body cont
+completeLam rev_bndrs body cont
   = simplExpr body                     `thenSmpl` \ body' ->
+    case try_eta body' of
+       Just etad_lam -> tick (EtaReduction (head rev_bndrs))   `thenSmpl_`
+                        rebuild etad_lam cont
 
-    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
+       Nothing       -> rebuild (foldl (flip Lam) body' rev_bndrs) cont
   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
+       -- 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]
+       --  (c) we don't want to eta-reduce a data con worker or primop
+       --      because we only have to eta-expand them later when we saturate
+    try_eta body | not opt_SimplDoEtaReduction = Nothing
+                | otherwise                   = go rev_bndrs body
+
+    go (b : bs) (App fun arg) | ok_arg b arg = go bs fun       -- Loop round
+    go []       body          | ok_body body = Just body       -- Success!
+    go _        _                           = Nothing          -- Failure!
+
+    ok_body (Var v) = not (v `elem` rev_bndrs) && not (hasNoBinding v)
+    ok_body other   = False
+    ok_arg b arg    = varToCoreExpr b `cheapEqExpr` arg
 
 mkLamBndrZapper :: CoreExpr    -- Function
-               -> Int          -- Number of args
+               -> SimplCont    -- The context
                -> Id -> Id     -- Use this to zap the binders
-mkLamBndrZapper fun n_args
+mkLamBndrZapper fun cont
   | n_args >= n_params fun = \b -> b           -- Enough args
-  | otherwise             = \b -> maybeModifyIdInfo zapLamIdInfo b
+  | otherwise             = \b -> zapLamIdInfo b
   where
-    n_params (Lam b e) | isId b    = 1 + n_params e
-                      | otherwise = n_params e
-    n_params other                = 0::Int
-\end{code}
-
+       -- NB: we count all the args incl type args
+       -- so we must count all the binders (incl type lambdas)
+    n_args = countArgs cont
 
----------------------------------
-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 []
-
-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}
 
 
@@ -412,7 +402,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}
 
 
@@ -440,54 +434,59 @@ 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' ->
+    let
+       bndr_ty'  = idType bndr'
+       is_strict = isStrict (idDemandInfo bndr) || isStrictType bndr_ty'
+    in
+    simplValArg bndr_ty' is_strict 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 bndr_ty' 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
-  | 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!!
+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         -- rhs_ty: Type of arg; used only occasionally
+           -> Bool             -- True <=> evaluate eagerly
+           -> InExpr -> SubstEnv
+           -> OutType          -- cont_ty: Type of thing computed by the context
+           -> (OutExpr -> SimplM OutExprStuff) 
+                               -- Takes an expression of type rhs_ty, 
+                               -- returns an expression of type cont_ty
+           -> SimplM OutExprStuff      -- An expression of type cont_ty
+
+simplValArg arg_ty is_strict arg arg_se cont_ty thing_inside
+  | is_strict
+  = getEnv                             `thenSmpl` \ env ->
+    setSubstEnv arg_se                                 $
+    simplExprF arg (ArgOf NoDup cont_ty        $ \ rhs' ->
+    setAllExceptInScope env                    $
+    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
 \end{code}
 
 
@@ -506,57 +505,120 @@ 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
+completeBinding old_bndr new_bndr top_lvl black_listed new_rhs thing_inside
+  |  isDeadOcc occ_info        -- 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
                                -- create the (dead) let-binding  let x = (a,b) in ...
   =  thing_inside
 
-  |  postInlineUnconditionally 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.
+  | trivial_rhs && not must_keep_binding
+       -- We're looking at a binding with a trivial RHS, so
+       -- perhaps we can discard it altogether!
        --
-       -- NB: a loop breaker never has postInlineUnconditionally True
+       -- NB: a loop breaker has must_keep_binding = True
        -- and non-loop-breakers only have *forward* references
        -- Hence, it's safe to discard the binding
-  =  tick (PostInlineUnconditionally old_bndr) `thenSmpl_`
-     extendSubst old_bndr (DoneEx new_rhs)     
-     thing_inside
+       --      
+       -- NOTE: This isn't our last opportunity to inline.
+       -- We're at the binding site right now, and
+       -- we'll get another opportunity when we get to the ocurrence(s)
+
+       -- Note that we do this unconditional inlining only for trival RHSs.
+       -- 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.
+  =            -- Drop the binding
+    extendSubst old_bndr (DoneEx new_rhs)      $
+               -- Use the substitution to make quite, quite sure that the substitution
+               -- will happen, since we are going to discard the binding
+    tick (PostInlineUnconditionally old_bndr)  `thenSmpl_`
+    thing_inside
+
+  | Note coercion@(Coerce _ inner_ty) inner_rhs <- new_rhs,
+    not trivial_rhs && not (isUnLiftedType inner_ty)
+       -- x = coerce t e  ==>  c = e; x = inline_me (coerce t c)
+       -- Now x can get inlined, which moves the coercion
+       -- to the usage site.  This is a bit like worker/wrapper stuff,
+       -- but it's useful to do it very promptly, so that
+       --      x = coerce T (I# 3)
+       -- get's w/wd to
+       --      c = I# 3
+       --      x = coerce T c
+       -- This in turn means that
+       --      case (coerce Int x) of ...
+       -- will inline x.  
+       -- Also the full-blown w/w thing isn't set up for non-functions
+       --
+       -- The (not (isUnLiftedType inner_ty)) avoids the nasty case of
+       --      x::Int = coerce Int Int# (foo y)
+       -- ==>
+       --      v::Int# = foo y
+       --      x::Int  = coerce Int Int# v
+       -- which would be bogus because then v will be evaluated strictly.
+       -- How can this arise?  Via 
+       --      x::Int = case (foo y) of { ... }
+       -- followed by case elimination.
+       --
+       -- The inline_me note is so that the simplifier doesn't 
+       -- just substitute c back inside x's rhs!  (Typically, x will
+       -- get substituted away, but not if it's exported.)
+  = newId SLIT("c") inner_ty                                   $ \ c_id ->
+    completeBinding c_id c_id top_lvl False inner_rhs          $
+    completeBinding old_bndr new_bndr top_lvl black_listed
+                   (Note InlineMe (Note coercion (Var c_id)))  $
+    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
-     in
-     modifyInScope occ_site_id thing_inside    `thenSmpl` \ stuff ->
-     returnSmpl (addBind (NonRec binding_site_id new_rhs) stuff)
+  = getSubst                   `thenSmpl` \ subst ->
+    let
+               -- 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
+       new_bndr_info = substIdInfo subst old_info (idInfo new_bndr)
+                       `setArityInfo` arity_info
+
+               -- Add the unfolding *only* for non-loop-breakers
+               -- Making loop breakers not have an unfolding at all 
+               -- means that we can avoid tests in exprIsConApp, for example.
+               -- This is important: if exprIsConApp says 'yes' for a recursive
+               -- thing, then we can get into an infinite loop
+        info_w_unf | loop_breaker = new_bndr_info
+                  | otherwise    = new_bndr_info `setUnfoldingInfo` mkUnfolding top_lvl new_rhs
+
+       final_id = new_bndr `setIdInfo` info_w_unf
+    in
+               -- These seqs forces the Id, and hence its IdInfo,
+               -- and hence any inner substitutions
+    final_id                           `seq`
+    addLetBind (NonRec final_id new_rhs)       $
+    modifyInScope new_bndr final_id thing_inside
+
+  where
+    old_info          = idInfo old_bndr
+    occ_info          = occInfo old_info
+    loop_breaker      = isLoopBreaker occ_info
+    trivial_rhs              = exprIsTrivial new_rhs
+    must_keep_binding = black_listed || loop_breaker || isExportedId old_bndr
+    arity_info       = atLeastArity (exprArity new_rhs)
 \end{code}    
 
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{simplLazyBind}
@@ -572,7 +634,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
@@ -582,84 +644,98 @@ 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
 
-    simplRhs top_lvl False {- Not ok to float unboxed -}
+       -- Simplify the RHS
+    getSubstEnv                                        `thenSmpl` \ rhs_se ->
+    simplRhs top_lvl False {- Not ok to float unboxed (conservative) -}
             (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
+                               --          False for (a) recursive and (b) top-level bindings
+        -> OutType             -- Type of RHS; used only occasionally
+        -> InExpr -> SubstEnv
         -> (OutExpr -> SimplM (OutStuff a))
         -> SimplM (OutStuff a)
 simplRhs top_lvl float_ubx rhs_ty rhs rhs_se thing_inside
-  =            -- Swizzle the inner lets past the big lambda (if any)
-       -- and try eta expansion
-    transformRhs rhs                                   `thenSmpl` \ t_rhs ->
-
-       -- Simplify it
-    setSubstEnv rhs_se (simplExprF t_rhs (Stop rhs_ty))        `thenSmpl` \ (floats, (in_scope', rhs')) ->
-
-       -- Float lets out of RHS
+  =    -- Simplify it
+    setSubstEnv rhs_se (simplExprF rhs (mkRhsStop rhs_ty))     `thenSmpl` \ (floats1, (rhs_in_scope, rhs1)) ->
     let
-       (floats_out, rhs'') | float_ubx = (floats, rhs')
-                           | otherwise = splitFloats floats rhs' 
+       (floats2, rhs2) = splitFloats float_ubx floats1 rhs1
     in
-    if (isTopLevel top_lvl || exprIsCheap rhs') &&     -- Float lets if (a) we're at the top level
-        not (null floats_out)                          -- or            (b) it exposes a cheap (i.e. duplicatable) expression
-    then
-       tickLetFloat floats_out                         `thenSmpl_`
-               -- Do the float
-               -- 
                -- There's a subtlety here.  There may be a binding (x* = e) in the
                -- floats, where the '*' means 'will be demanded'.  So is it safe
                -- to float it out?  Answer no, but it won't matter because
                -- we only float if arg' is a WHNF,
                -- 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 ->
-               -- in_scope' may be excessive, but that's OK;
-               -- it's a superset of what's in scope
-       returnSmpl (addBinds floats_out stuff)
+    WARN( any demanded_float (fromOL floats2), ppr (fromOL floats2) )
+
+       --                      Transform the RHS
+       -- It's important that we do eta expansion on function *arguments* (which are
+       -- simplified with simplRhs), as well as let-bound right-hand sides.  
+       -- Otherwise we find that things like
+       --      f (\x -> case x of I# x' -> coerce T (\ y -> ...))
+       -- get right through to the code generator as two separate lambdas, 
+       -- which is a Bad Thing
+    tryRhsTyLam rhs2           `thenSmpl` \ (floats3, rhs3) ->
+    tryEtaExpansion rhs3 rhs_ty        `thenSmpl` \ (floats4, rhs4) ->
+
+       -- Float lets if (a) we're at the top level
+       -- or            (b) the resulting RHS is one we'd like to expose
+    if (top_lvl || exprIsCheap rhs4) then
+       (if (isNilOL floats2 && null floats3 && null floats4) then
+               returnSmpl ()
+        else
+               tick LetFloatFromLet)                   `thenSmpl_`
+
+       addFloats floats2 rhs_in_scope  $
+       addAuxiliaryBinds floats3       $
+       addAuxiliaryBinds floats4       $
+       thing_inside rhs4
     else       
                -- Don't do the float
-       thing_inside (mkLets floats rhs')
+       thing_inside (wrapFloats floats1 rhs1)
 
--- 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
 
--- Don't float any unlifted bindings out, because the context
+-- If float_ubx is true we float all the bindings, otherwise
+-- we just float until we come across an unlifted one.
+-- Remember that the unlifted bindings in the floats are all for
+-- guaranteed-terminating non-exception-raising unlifted things,
+-- which we are happy to do speculatively.  However, we may still
+-- not be able to float them out, because the context
 -- is either a Rec group, or the top level, neither of which
 -- can tolerate them.
-splitFloats floats rhs
-  = go floats
+splitFloats float_ubx floats rhs
+  | float_ubx = (floats, rhs)          -- Float them all
+  | otherwise = go (fromOL floats)
   where
-    go []                  = ([], rhs)
-    go (f:fs) | must_stay f = ([], mkLets (f:fs) rhs)
+    go []                  = (nilOL, rhs)
+    go (f:fs) | must_stay f = (nilOL, mkLets (f:fs) rhs)
              | otherwise   = case go fs of
-                                  (out, rhs') -> (f:out, rhs')
+                                  (out, rhs') -> (f `consOL` out, rhs')
 
     must_stay (Rec prs)    = False     -- No unlifted bindings in here
     must_stay (NonRec b r) = isUnLiftedType (idType b)
@@ -675,119 +751,13 @@ 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 dictionary constructors 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 ->
-
-                  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)
-
-
----------------------------------------------------------
---     Preparing arguments for a call
-
-prepareArgs :: SDoc    -- Error message info
-           -> OutType -> ([Demand],Bool) -> SimplCont
-           -> ([OutExpr] -> SimplCont -> SimplM OutExprStuff)
-           -> SimplM OutExprStuff
-
-prepareArgs pp_fun orig_fun_ty (fun_demands, result_bot) 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
-
-       -- 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
-
-       -- Type argument
-    go acc ds fun_ty (ApplyTo _ arg@(Type ty_arg) se cont)
-       = getInScope            `thenSmpl` \ in_scope ->
-         let
-               ty_arg' = substTy (mkSubst in_scope se) ty_arg
-               res_ty  = applyTy fun_ty ty_arg'
-         in
-         go (Type ty_arg' : 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)
-
-       -- We're run out of arguments
-    go acc ds fun_ty cont = thing_inside (reverse acc) cont
-
--- Boring: we must only record a tick if there was an interesting
---        continuation to discard.  If not, we tick forever.
-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))
+  = 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) && mustHaveLocalBinding var1,
+                                text "simplVar:" <+> ppr var )
+                          zapSubstEnv (completeCall var1 occ cont)
                -- The template is already simplified, so don't re-substitute.
                -- This is VITAL.  Consider
                --      let x = e in
@@ -796,93 +766,180 @@ completeCall black_list_fn in_scope var args cont
                -- 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 zapped_bndr && not opt_SimplNoPreInlining
-         = tick (BetaReduction bndr)                   `thenSmpl_`
-           tick (PreInlineUnconditionally bndr)        `thenSmpl_`
-           extendSubst zapped_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:
+---------------------------------------------------------
+--     Dealing with a call
+
+completeCall var occ_info cont
+  = getBlackList               `thenSmpl` \ black_list_fn ->
+    getInScope                 `thenSmpl` \ in_scope ->
+    getContArgs var cont       `thenSmpl` \ (args, call_cont, inline_call) ->
+    getDOptsSmpl               `thenSmpl` \ dflags ->
+    let
+       black_listed       = black_list_fn var
+       arg_infos          = [ interestingArg in_scope arg subst 
+                            | (arg, subst, _) <- args, isValArg arg]
+
+       interesting_cont = interestingCallContext (not (null args)) 
+                                                 (not (null arg_infos))
+                                                 call_cont
+
+       inline_cont | inline_call = discardInline cont
+                   | otherwise   = cont
+
+       maybe_inline = callSiteInline dflags black_listed inline_call occ_info
+                                     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 inline_cont
+
+       ;
+       Nothing ->              -- No inlining!
+
+
+    simplifyArgs (isDataConId var) args (contResultType call_cont)  $ \ args' ->
+
+       -- 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.
+       --
+       -- You might think that we shouldn't apply rules for a loop breaker: 
+       -- doing so might give rise to an infinite loop, because a RULE is
+       -- rather like an extra equation for the function:
+       --      RULE:           f (g x) y = x+y
+       --      Eqn:            f a     y = a-y
+       --
+       -- But it's too drastic to disable rules for loop breakers.  
+       -- Even the foldr/build rule would be disabled, because foldr 
+       -- is recursive, and hence a loop breaker:
+       --      foldr k z (build g) = g k z
+       -- So it's up to the programmer: rules can cause divergence
+
+    getSwitchChecker   `thenSmpl` \ chkr ->
+    let
+       maybe_rule | switchIsOn chkr DontApplyRules = Nothing
+                  | otherwise                      = lookupRule in_scope var args' 
+    in
+    case maybe_rule of {
+       Just (rule_name, rule_rhs) -> 
+               tick (RuleFired rule_name)                      `thenSmpl_`
+#ifdef DEBUG
+               (if dopt Opt_D_dump_inlinings dflags then
+                  pprTrace "Rule fired" (vcat [
+                       text "Rule:" <+> ptext rule_name,
+                       text "Before:" <+> ppr var <+> sep (map pprParendExpr args'),
+                       text "After: " <+> pprCoreExpr rule_rhs])
+                else
+                       id)             $
+#endif
+               simplExprF rule_rhs call_cont ;
+       
+       Nothing ->              -- No rules
+
+       -- Done
+    rebuild (mkApps (Var var) args') call_cont
+    }}
+
+
+---------------------------------------------------------
+--     Simplifying the arguments of a call
+
+simplifyArgs :: Bool                           -- It's a data constructor
+            -> [(InExpr, SubstEnv, Bool)]      -- Details of the arguments
+            -> OutType                         -- Type of the continuation
+            -> ([OutExpr] -> SimplM OutExprStuff)
+            -> SimplM OutExprStuff
+
+-- Simplify the arguments to a call.
+-- This part of the simplifier may break the no-shadowing invariant
+-- Consider
+--     f (...(\a -> e)...) (case y of (a,b) -> e')
+-- where f is strict in its second arg
+-- If we simplify the innermost one first we get (...(\a -> e)...)
+-- Simplifying the second arg makes us float the case out, so we end up with
+--     case y of (a,b) -> f (...(\a -> e)...) e'
+-- So the output does not have the no-shadowing invariant.  However, there is
+-- no danger of getting name-capture, because when the first arg was simplified
+-- we used an in-scope set that at least mentioned all the variables free in its
+-- static environment, and that is enough.
 --
---     f x = let y = E in
---           scc "foo" (...y...)
+-- We can't just do innermost first, or we'd end up with a dual problem:
+--     case x of (a,b) -> f e (...(\a -> e')...)
 --
--- 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
+-- I spent hours trying to recover the no-shadowing invariant, but I just could
+-- not think of an elegant way to do it.  The simplifier is already knee-deep in
+-- continuations.  We have to keep the right in-scope set around; AND we have
+-- to get the effect that finding (error "foo") in a strict arg position will
+-- discard the entire application and replace it with (error "foo").  Getting
+-- all this at once is TOO HARD!
+
+simplifyArgs is_data_con args cont_ty thing_inside
+  | not is_data_con
+  = go args thing_inside
+
+  | otherwise  -- It's a data constructor, so we want 
+               -- to switch off inlining in the arguments
+               -- 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!
+  = getBlackList                               `thenSmpl` \ old_bl ->
+    setBlackList noInlineBlackList             $
+    go args                                    $ \ args' ->
+    setBlackList old_bl                                $
+    thing_inside args'
+
+  where
+    go []        thing_inside = thing_inside []
+    go (arg:args) thing_inside = simplifyArg is_data_con arg cont_ty   $ \ arg' ->
+                                go args                                $ \ args' ->
+                                thing_inside (arg':args')
+
+simplifyArg is_data_con (Type ty_arg, se, _) cont_ty thing_inside
+  = simplTyArg ty_arg se       `thenSmpl` \ new_ty_arg ->
+    thing_inside (Type new_ty_arg)
+
+simplifyArg is_data_con (val_arg, se, is_strict) cont_ty thing_inside
+  = getInScope         `thenSmpl` \ in_scope ->
+    let
+       arg_ty = substTy (mkSubst in_scope se) (exprType val_arg)
+    in
+    if not is_data_con then
+       -- An ordinary function
+       simplValArg arg_ty is_strict val_arg se cont_ty thing_inside
+    else
+       -- A data constructor
+       -- simplifyArgs has already switched off inlining, so 
+       -- all we have to do here is to let-bind any non-trivial argument
+
+       -- It's not always the case that 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.
+       simplValArg arg_ty is_strict val_arg se cont_ty         $ \ arg' ->
+       
+       if exprIsTrivial arg' then
+            thing_inside arg'
+       else
+       newId SLIT("a") (exprType arg')         $ \ arg_id ->
+       addNonRecBind arg_id arg'               $
+       thing_inside (Var arg_id)
 \end{code}                
 
 
@@ -892,8 +949,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 l
+       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
@@ -914,48 +988,13 @@ 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 NotInsideLam True -> True   -- Not inside a lambda,
-                                                       -- one occurrence ==> safe!
-       other -> False
-
-
-postInlineUnconditionally :: 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.
-
-       -- NOTE: This isn't our last opportunity to inline.
-       -- 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.
+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
 \end{code}
 
 
@@ -969,15 +1008,13 @@ postInlineUnconditionally bndr rhs
 \begin{code}
 -------------------------------------------------------------------
 -- Finish rebuilding
-rebuild_done expr
-  = getInScope                 `thenSmpl` \ in_scope ->
-    returnSmpl ([], (in_scope, expr))
+rebuild_done expr = returnOutStuff expr
 
 ---------------------------------------------------------
 rebuild :: OutExpr -> SimplCont -> SimplM OutExprStuff
 
 --     Stop continuation
-rebuild expr (Stop _) = rebuild_done expr
+rebuild expr (Stop _ _) = rebuild_done expr
 
 --     ArgOf continuation
 rebuild expr (ArgOf _ _ cont_fn) = cont_fn expr
@@ -989,61 +1026,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
-
-
----------------------------------------------------------
---     The other Select cases
-
 rebuild scrut (Select _ bndr alts se cont)
-  |    -- 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
-    && (   (isUnLiftedType (idType bndr) &&    -- It's unlifted and floatable
-           exprOkForSpeculation scrut)         -- NB: scrut = an unboxed variable satisfies 
-       || 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
-       )
-
-    && 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                     $                       
-    simplBinder bndr                   $ \ bndr' ->
-    completeBinding bndr bndr' 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
-
-    var_demanded_later (Var v) = isStrict (getIdDemandInfo bndr)       -- It's going to be evaluated later
-    var_demanded_later other   = False
 \end{code}
 
 Case elimination [see the code above]
@@ -1129,12 +1119,73 @@ 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                             $
@@ -1145,17 +1196,16 @@ rebuild_case scrut case_bndr alts se cont
        
 
        -- Deal with variable scrutinee
-    (  simplBinder case_bndr                   $ \ case_bndr' ->
-       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'
+       mkCase scrut case_bndr' alts'
     )                                          `thenSmpl` \ case_expr ->
 
        -- Notice that the simplBinder, prepareCaseCont, etc, do *not* scope
@@ -1163,37 +1213,37 @@ rebuild_case scrut case_bndr alts se cont
        -- 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 -> otherCons (getIdUnfolding v)
-                  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_`
+  =    -- Arguments should be atomic;
+       -- yell if not
+    WARN( not (all exprIsTrivial args), 
+         text "knownCon" <+> ppr expr )
+    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
@@ -1210,12 +1260,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.
-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.
+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
@@ -1230,20 +1297,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:
@@ -1273,11 +1343,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
@@ -1286,10 +1356,10 @@ prepareCaseAlts bndr (Just (tycon, inst_tys)) scrut_cons alts
                        []    -> alts
                        other -> [alt | alt@(con,_,_) <- alts, not (con `elem` scrut_cons)]
 
-    missing_cons = [data_con | data_con <- tyConDataCons tycon, 
+    missing_cons = [data_con | data_con <- tyConDataConsIfAvailable 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
@@ -1297,11 +1367,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
-                       Just (tycon, inst_tys) -> inst_tys
+    inst_tys' = tyConAppArgs (idType case_bndr')
 
        -- handled_cons is all the constructors that are dealt
        -- with, either by being impossible, or by there being an alternative
@@ -1311,21 +1380,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` mkOtherCon 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')
 
@@ -1339,7 +1411,7 @@ 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 [] [] = []
@@ -1359,7 +1431,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)
@@ -1377,23 +1449,27 @@ 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 ->
-       cont_fn (Var arg_id)                            `thenSmpl` \ (binds, (_, rhs)) ->
-       returnSmpl (Lam arg_id (mkLets binds rhs))
+    newId SLIT("a") join_arg_ty                                ( \ arg_id ->
+       cont_fn (Var arg_id)                            `thenSmpl` \ (floats, (_, rhs)) ->
+       returnSmpl (Lam (setOneShotLambda arg_id) (wrapFloats floats 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
+       -- [NOTE: the type used to be exprType join_rhs, but this seems more elegant.]
+    newId SLIT("$j") (mkFunTy join_arg_ty cont_ty)     $ \ 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 (NonRec join_id join_rhs)       $
+    thing_inside new_cont
 
 mkDupableCont ty (ApplyTo _ arg se cont) thing_inside
   = mkDupableCont (funResultTy ty) cont                $ \ cont' ->
@@ -1401,20 +1477,32 @@ 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 (NonRec 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_`
     setSubstEnv se (
        simplBinder case_bndr                                           $ \ case_bndr' ->
        prepareCaseCont alts cont                                       $ \ cont' ->
-       mapAndUnzipSmpl (mkDupableAlt case_bndr case_bndr' cont') alts  `thenSmpl` \ (alt_binds_s, alts') ->
-       returnSmpl (concat alt_binds_s, alts')
-    )                                  `thenSmpl` \ (alt_binds, alts') ->
+       mkDupableAlts case_bndr case_bndr' cont' alts                   $ \ alts' ->
+       returnOutStuff alts'
+    )                                  `thenSmpl` \ (alt_binds, (in_scope, alts')) ->
 
-    extendInScopes [b | NonRec b _ <- alt_binds]               $
+    addFloats alt_binds in_scope               $
 
        -- NB that the new alternatives, alts', are still InAlts, using the original
        -- binders.  That means we can keep the case_bndr intact. This is important
@@ -1423,19 +1511,45 @@ 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)
+    thing_inside (Select OkToDup case_bndr alts' se (mkStop (contResultType cont)))
 
+mkDupableAlts :: InId -> OutId -> SimplCont -> [InAlt] 
+            -> ([InAlt] -> SimplM (OutStuff a))
+            -> SimplM (OutStuff a)
+mkDupableAlts case_bndr case_bndr' cont [] thing_inside
+  = thing_inside []
+mkDupableAlts case_bndr case_bndr' cont (alt:alts) thing_inside
+  = mkDupableAlt  case_bndr case_bndr' cont alt                $ \ alt' -> 
+    mkDupableAlts case_bndr case_bndr' cont alts       $ \ alts' ->
+    thing_inside (alt' : alts')
 
-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' ->
+mkDupableAlt case_bndr case_bndr' cont alt@(con, bndrs, rhs) thing_inside
+  = 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.
+       thing_inside 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'),
@@ -1469,19 +1583,39 @@ mkDupableAlt case_bndr case_bndr' cont alt@(con, bndrs, rhs)
        --                  then 78
        --                  else 5
 
-       then newId realWorldStatePrimTy  $ \ rw_id ->
+       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 ->
-
-       -- Notice that we make the lambdas into one-shot-lambdas.  The
+       -- See comment about "$j" name above
+    newId SLIT("$j") (foldr mkPiType rhs_ty' final_bndrs')     $ \ join_bndr ->
+       -- Notice the funky mkPiType.  If the contructor has existentials
+       -- it's possible that the join point will be abstracted over
+       -- type varaibles as well as term variables.
+       --  Example:  Suppose we have
+       --      data T = forall t.  C [t]
+       --  Then faced with
+       --      case (case e of ...) of
+       --          C t xs::[t] -> rhs
+       --  We get the join point
+       --      let j :: forall t. [t] -> ...
+       --          j = /\t \xs::[t] -> rhs
+       --      in
+       --      case (case e of ...) of
+       --          C t xs::[t] -> j t xs
+
+    let 
+       -- 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))
+       really_final_bndrs = map one_shot final_bndrs'
+       one_shot v | isId v    = setOneShotLambda v
+                  | otherwise = v
+    in
+    addLetBind (NonRec join_bndr (mkLams really_final_bndrs rhs'))     $
+    thing_inside (con, bndrs, mkApps (Var join_bndr) final_args)
 \end{code}