Fix nasty bug in w/w for absence analysis
[ghc.git] / compiler / simplCore / Simplify.hs
index 3614bb3..d6b859a 100644 (file)
 
 {-# LANGUAGE CPP #-}
 
-module Simplify ( simplTopBinds, simplExpr ) where
+module Simplify ( simplTopBinds, simplExpr, simplRules ) where
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import DynFlags
 import SimplMonad
-import Type hiding      ( substTy, extendTvSubst, substTyVar )
+import Type hiding      ( substTy, substTyVar, extendTvSubst, extendCvSubst )
 import SimplEnv
 import SimplUtils
+import OccurAnal        ( occurAnalyseExpr )
 import FamInstEnv       ( FamInstEnv )
 import Literal          ( litIsLifted ) --, mkMachInt ) -- temporalily commented out. See #8326
 import Id
-import MkId             ( seqId, voidPrimId )
+import MkId             ( seqId )
 import MkCore           ( mkImpossibleExpr, castBottomExpr )
 import IdInfo
-import Name             ( mkSystemVarName, isExternalName )
-import Coercion hiding  ( substCo, substTy, substCoVar, extendTvSubst )
+import Name             ( Name, mkSystemVarName, isExternalName, getOccFS )
+import Coercion hiding  ( substCo, substCoVar )
 import OptCoercion      ( optCoercion )
 import FamInstEnv       ( topNormaliseType_maybe )
-import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness
-                        , isMarkedStrict ) --, dataConTyCon, dataConTag, fIRST_TAG )
---import TyCon            ( isEnumerationTyCon ) -- temporalily commented out. See #8326
-import CoreMonad        ( Tick(..), SimplifierMode(..) )
+import DataCon          ( DataCon, dataConWorkId, dataConRepStrictness, dataConRepArgTys )
+import CoreMonad        ( Tick(..), SimplMode(..) )
 import CoreSyn
 import Demand           ( StrictSig(..), dmdTypeDepth, isStrictDmd )
 import PprCore          ( pprCoreExpr )
 import CoreUnfold
 import CoreUtils
-import CoreArity
---import PrimOp           ( tagToEnumKey ) -- temporalily commented out. See #8326
-import Rules            ( lookupRule, getRules )
-import TysPrim          ( voidPrimTy ) --, intPrimTy ) -- temporalily commented out. See #8326
-import BasicTypes       ( TopLevelFlag(..), isTopLevel, RecFlag(..) )
-import MonadUtils       ( foldlM, mapAccumLM, liftIO )
-import Maybes           ( orElse )
---import Unique           ( hasKey ) -- temporalily commented out. See #8326
+import CoreOpt          ( pushCoTyArg, pushCoValArg
+                        , joinPointBinding_maybe, joinPointBindings_maybe )
+import Rules            ( mkRuleInfo, lookupRule, getRules )
+import Demand           ( mkClosedStrictSig, topDmd, exnRes )
+import BasicTypes       ( TopLevelFlag(..), isNotTopLevel, isTopLevel,
+                          RecFlag(..), Arity )
+import MonadUtils       ( mapAccumLM, liftIO )
+import Maybes           (  orElse )
 import Control.Monad
-import Data.List        ( mapAccumL )
 import Outputable
 import FastString
 import Pair
 import Util
 import ErrUtils
+import Module          ( moduleName, pprModuleName )
 
 {-
 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.
-
-
------------------------------------------
-        *** IMPORTANT NOTE ***
------------------------------------------
-Many parts of the simplifier return a bunch of "floats" as well as an
-expression. This is wrapped as a datatype SimplUtils.FloatsWith.
-
-All "floats" are let-binds, not case-binds, but some non-rec lets may
-be unlifted (with RHS ok-for-speculation).
-
-
-
------------------------------------------
-        ORGANISATION OF FUNCTIONS
------------------------------------------
-simplTopBinds
-  - simplify all top-level binders
-  - for NonRec, call simplRecOrTopPair
-  - for Rec,    call simplRecBind
-
-
-        ------------------------------
-simplExpr (applied lambda)      ==> simplNonRecBind
-simplExpr (Let (NonRec ...) ..) ==> simplNonRecBind
-simplExpr (Let (Rec ...)    ..) ==> simplify binders; simplRecBind
-
-        ------------------------------
-simplRecBind    [binders already simplfied]
-  - use simplRecOrTopPair on each pair in turn
-
-simplRecOrTopPair [binder already simplified]
-  Used for: recursive bindings (top level and nested)
-            top-level non-recursive bindings
-  Returns:
-  - check for PreInlineUnconditionally
-  - simplLazyBind
-
-simplNonRecBind
-  Used for: non-top-level non-recursive bindings
-            beta reductions (which amount to the same thing)
-  Because it can deal with strict arts, it takes a
-        "thing-inside" and returns an expression
-
-  - check for PreInlineUnconditionally
-  - simplify binder, including its IdInfo
-  - if strict binding
-        simplStrictArg
-        mkAtomicArgs
-        completeNonRecX
-    else
-        simplLazyBind
-        addFloats
-
-simplNonRecX:   [given a *simplified* RHS, but an *unsimplified* binder]
-  Used for: binding case-binder and constr args in a known-constructor case
-  - check for PreInLineUnconditionally
-  - simplify binder
-  - completeNonRecX
-
-        ------------------------------
-simplLazyBind:  [binder already simplified, RHS not]
-  Used for: recursive bindings (top level and nested)
-            top-level non-recursive bindings
-            non-top-level, but *lazy* non-recursive bindings
-        [must not be strict or unboxed]
-  Returns floats + an augmented environment, not an expression
-  - substituteIdInfo and add result to in-scope
-        [so that rules are available in rec rhs]
-  - simplify rhs
-  - mkAtomicArgs
-  - float if exposes constructor or PAP
-  - completeBind
-
-
-completeNonRecX:        [binder and rhs both simplified]
-  - if the the thing needs case binding (unlifted and not ok-for-spec)
-        build a Case
-   else
-        completeBind
-        addFloats
-
-completeBind:   [given a simplified RHS]
-        [used for both rec and non-rec bindings, top level and not]
-  - try PostInlineUnconditionally
-  - add unfolding [this is the only place we add an unfolding]
-  - add arity
-
-
+the simplifier is in SimplCore.hs.
 
-Right hand sides and arguments
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In many ways we want to treat
-        (a) the right hand side of a let(rec), and
-        (b) a function argument
-in the same way.  But not always!  In particular, we would
-like to leave these arguments exactly as they are, so they
-will match a RULE more easily.
-
-        f (g x, h x)
-        g (+ x)
+Note [The big picture]
+~~~~~~~~~~~~~~~~~~~~~~
+The general shape of the simplifier is this:
 
-It's harder to make the rule match if we ANF-ise the constructor,
-or eta-expand the PAP:
+  simplExpr :: SimplEnv -> InExpr -> SimplCont -> SimplM (SimplFloats, OutExpr)
+  simplBind :: SimplEnv -> InBind -> SimplM (SimplFloats, SimplEnv)
 
-        f (let { a = g x; b = h x } in (a,b))
-        g (\y. + x y)
+ * SimplEnv contains
+     - Simplifier mode (which includes DynFlags for convenience)
+     - Ambient substitution
+     - InScopeSet
 
-On the other hand if we see the let-defns
+ * SimplFloats contains
+     - Let-floats (which includes ok-for-spec case-floats)
+     - Join floats
+     - InScopeSet (including all the floats)
 
-        p = (g x, h x)
-        q = + x
+ * Expressions
+      simplExpr :: SimplEnv -> InExpr -> SimplCont
+                -> SimplM (SimplFloats, OutExpr)
+   The result of simplifying an /expression/ is (floats, expr)
+      - A bunch of floats (let bindings, join bindings)
+      - A simplified expression.
+   The overall result is effectively (let floats in expr)
 
-then we *do* want to ANF-ise and eta-expand, so that p and q
-can be safely inlined.
+ * Bindings
+      simplBind :: SimplEnv -> InBind -> SimplM (SimplFloats, SimplEnv)
+   The result of simplifying a binding is
+     - A bunch of floats, the last of which is the simplified binding
+       There may be auxiliary bindings too; see prepareRhs
+     - An environment suitable for simplifying the scope of the binding
 
-Even floating lets out is a bit dubious.  For let RHS's we float lets
-out if that exposes a value, so that the value can be inlined more vigorously.
-For example
+   The floats may also be empty, if the binding is inlined unconditionally;
+   in that case the returned SimplEnv will have an augmented substitution.
 
-        r = let x = e in (x,x)
+   The returned floats and env both have an in-scope set, and they are
+   guaranteed to be the same.
 
-Here, if we float the let out we'll expose a nice constructor. We did experiments
-that showed this to be a generally good thing.  But it was a bad thing to float
-lets out unconditionally, because that meant they got allocated more often.
 
-For function arguments, there's less reason to expose a constructor (it won't
-get inlined).  Just possibly it might make a rule match, but I'm pretty skeptical.
-So for the moment we don't float lets out of function arguments either.
+Note [Shadowing]
+~~~~~~~~~~~~~~~~
+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.
 
 
 Eta expansion
@@ -203,7 +112,6 @@ lambdas together.  And in general that's a good thing to do.  Perhaps
 we should eta expand wherever we find a (value) lambda?  Then the eta
 expansion at a let RHS can concentrate solely on the PAP case.
 
-
 ************************************************************************
 *                                                                      *
 \subsection{Bindings}
@@ -211,8 +119,8 @@ expansion at a let RHS can concentrate solely on the PAP case.
 ************************************************************************
 -}
 
-simplTopBinds :: SimplEnv -> [InBind] -> SimplM SimplEnv
-
+simplTopBinds :: SimplEnv -> [InBind] -> SimplM (SimplFloats, SimplEnv)
+-- See Note [The big picture]
 simplTopBinds env0 binds0
   = do  {       -- Put all the top-level binders into scope at the start
                 -- so that if a transformation rule has unexpectedly brought
@@ -220,28 +128,30 @@ simplTopBinds env0 binds0
                 -- It's rather as if the top-level binders were imported.
                 -- See note [Glomming] in OccurAnal.
         ; env1 <- simplRecBndrs env0 (bindersOfBinds binds0)
-        ; env2 <- simpl_binds env1 binds0
+        ; (floats, env2) <- simpl_binds env1 binds0
         ; freeTick SimplifierDone
-        ; return env2 }
+        ; return (floats, env2) }
   where
         -- We need to track the zapped top-level binders, because
         -- they should have their fragile IdInfo zapped (notably occurrence info)
         -- That's why we run down binds and bndrs' simultaneously.
         --
-    simpl_binds :: SimplEnv -> [InBind] -> SimplM SimplEnv
-    simpl_binds env []           = return env
-    simpl_binds env (bind:binds) = do { env' <- simpl_bind env bind
-                                      ; simpl_binds env' binds }
-
-    simpl_bind env (Rec pairs)  = simplRecBind      env  TopLevel pairs
-    simpl_bind env (NonRec b r) = simplRecOrTopPair env' TopLevel NonRecursive b b' r
-        where
-          (env', b') = addBndrRules env b (lookupRecBndr env b)
+    simpl_binds :: SimplEnv -> [InBind] -> SimplM (SimplFloats, SimplEnv)
+    simpl_binds env []           = return (emptyFloats env, env)
+    simpl_binds env (bind:binds) = do { (float,  env1) <- simpl_bind env bind
+                                      ; (floats, env2) <- simpl_binds env1 binds
+                                      ; return (float `addFloats` floats, env2) }
+
+    simpl_bind env (Rec pairs)  = simplRecBind env TopLevel Nothing pairs
+    simpl_bind env (NonRec b r) = do { (env', b') <- addBndrRules env b (lookupRecBndr env b)
+                                     ; simplRecOrTopPair env' TopLevel
+                                                         NonRecursive Nothing
+                                                         b b' r }
 
 {-
 ************************************************************************
 *                                                                      *
-\subsection{Lazy bindings}
+        Lazy bindings
 *                                                                      *
 ************************************************************************
 
@@ -249,27 +159,27 @@ simplRecBind is used for
         * recursive bindings only
 -}
 
-simplRecBind :: SimplEnv -> TopLevelFlag
+simplRecBind :: SimplEnv -> TopLevelFlag -> Maybe SimplCont
              -> [(InId, InExpr)]
-             -> SimplM SimplEnv
-simplRecBind env0 top_lvl pairs0
-  = do  { let (env_with_info, triples) = mapAccumL add_rules env0 pairs0
-        ; env1 <- go (zapFloats env_with_info) triples
-        ; return (env0 `addRecFloats` env1) }
-        -- addFloats adds the floats from env1,
-        -- _and_ updates env0 with the in-scope set from env1
+             -> SimplM (SimplFloats, SimplEnv)
+simplRecBind env0 top_lvl mb_cont pairs0
+  = do  { (env_with_info, triples) <- mapAccumLM add_rules env0 pairs0
+        ; (rec_floats, env1) <- go env_with_info triples
+        ; return (mkRecFloats rec_floats, env1) }
   where
-    add_rules :: SimplEnv -> (InBndr,InExpr) -> (SimplEnv, (InBndr, OutBndr, InExpr))
+    add_rules :: SimplEnv -> (InBndr,InExpr) -> SimplM (SimplEnv, (InBndr, OutBndr, InExpr))
         -- Add the (substituted) rules to the binder
-    add_rules env (bndr, rhs) = (env', (bndr, bndr', rhs))
-        where
-          (env', bndr') = addBndrRules env bndr (lookupRecBndr env bndr)
+    add_rules env (bndr, rhs)
+        = do { (env', bndr') <- addBndrRules env bndr (lookupRecBndr env bndr)
+             ; return (env', (bndr, bndr', rhs)) }
 
-    go env [] = return env
+    go env [] = return (emptyFloats env, env)
 
     go env ((old_bndr, new_bndr, rhs) : pairs)
-        = do { env' <- simplRecOrTopPair env top_lvl Recursive old_bndr new_bndr rhs
-             ; go env' pairs }
+        = do { (float, env1) <- simplRecOrTopPair env top_lvl Recursive mb_cont
+                                                  old_bndr new_bndr rhs
+             ; (floats, env2) <- go env1 pairs
+             ; return (float `addFloats` floats, env2) }
 
 {-
 simplOrTopPair is used for
@@ -280,60 +190,64 @@ It assumes the binder has already been simplified, but not its IdInfo.
 -}
 
 simplRecOrTopPair :: SimplEnv
-                  -> TopLevelFlag -> RecFlag
+                  -> TopLevelFlag -> RecFlag -> Maybe SimplCont
                   -> InId -> OutBndr -> InExpr  -- Binder and rhs
-                  -> SimplM SimplEnv    -- Returns an env that includes the binding
-
-simplRecOrTopPair env top_lvl is_rec old_bndr new_bndr rhs
-  = do { dflags <- getDynFlags
-       ; trace_bind dflags $
-           if preInlineUnconditionally dflags env top_lvl old_bndr rhs
-                    -- Check for unconditional inline
-           then do tick (PreInlineUnconditionally old_bndr)
-                   return (extendIdSubst env old_bndr (mkContEx env rhs))
-           else simplLazyBind env top_lvl is_rec old_bndr new_bndr rhs env }
-  where
-    trace_bind dflags thing_inside
-      | not (dopt Opt_D_verbose_core2core dflags)
-      = thing_inside
-      | otherwise
-      = pprTrace "SimplBind" (ppr old_bndr) thing_inside
-        -- trace_bind emits a trace for each top-level binding, which
-        -- helps to locate the tracing for inlining and rule firing
+                  -> SimplM (SimplFloats, SimplEnv)
 
-{-
-simplLazyBind is used for
-  * [simplRecOrTopPair] recursive bindings (whether top level or not)
-  * [simplRecOrTopPair] top-level non-recursive bindings
-  * [simplNonRecE]      non-top-level *lazy* non-recursive bindings
+simplRecOrTopPair env top_lvl is_rec mb_cont old_bndr new_bndr rhs
+  | preInlineUnconditionally env top_lvl old_bndr rhs
+  = trace_bind "pre-inline-uncond" $
+    do { tick (PreInlineUnconditionally old_bndr)
+       ; return ( emptyFloats env
+                , extendIdSubst env old_bndr (mkContEx env rhs)) }
+
+  | Just cont <- mb_cont
+  = ASSERT( isNotTopLevel top_lvl && isJoinId new_bndr )
+    trace_bind "join" $
+    simplJoinBind env cont old_bndr new_bndr rhs
 
-Nota bene:
-    1. It assumes that the binder is *already* simplified,
-       and is in scope, and its IdInfo too, except unfolding
+  | otherwise
+  = trace_bind "normal" $
+    simplLazyBind env top_lvl is_rec old_bndr new_bndr rhs env
 
-    2. It assumes that the binder type is lifted.
+  where
+    dflags = seDynFlags env
 
-    3. It does not check for pre-inline-unconditionally;
-       that should have been done already.
--}
+    -- trace_bind emits a trace for each top-level binding, which
+    -- helps to locate the tracing for inlining and rule firing
+    trace_bind what thing_inside
+      | not (dopt Opt_D_verbose_core2core dflags)
+      = thing_inside
+      | otherwise
+      = pprTrace ("SimplBind " ++ what) (ppr old_bndr) thing_inside
 
+--------------------------
 simplLazyBind :: SimplEnv
               -> TopLevelFlag -> RecFlag
               -> InId -> OutId          -- Binder, both pre-and post simpl
+                                        -- Not a JoinId
                                         -- The OutId has IdInfo, except arity, unfolding
+                                        -- Ids only, no TyVars
               -> InExpr -> SimplEnv     -- The RHS and its environment
-              -> SimplM SimplEnv
+              -> SimplM (SimplFloats, SimplEnv)
+-- Precondition: not a JoinId
 -- Precondition: rhs obeys the let/app invariant
+-- NOT used for JoinIds
 simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
-  = -- pprTrace "simplLazyBind" ((ppr bndr <+> ppr bndr1) $$ ppr rhs $$ ppr (seIdSubst rhs_se)) $
-    do  { let   rhs_env     = rhs_se `setInScope` env
-                (tvs, body) = case collectTyBinders rhs of
-                                (tvs, body) | not_lam body -> (tvs,body)
-                                            | otherwise    -> ([], rhs)
-                not_lam (Lam _ _)  = False
-                not_lam (Tick t e) | not (tickishFloatable t)
-                                   = not_lam e -- eta-reduction could float
-                not_lam _          = True
+  = ASSERT( isId bndr )
+    ASSERT2( not (isJoinId bndr), ppr bndr )
+    -- pprTrace "simplLazyBind" ((ppr bndr <+> ppr bndr1) $$ ppr rhs $$ ppr (seIdSubst rhs_se)) $
+    do  { let   rhs_env     = rhs_se `setInScopeFromE` env
+                (tvs, body) = case collectTyAndValBinders rhs of
+                                (tvs, [], body)
+                                  | surely_not_lam body -> (tvs, body)
+                                _                       -> ([], rhs)
+
+                surely_not_lam (Lam {})     = False
+                surely_not_lam (Tick t e)
+                  | not (tickishFloatable t) = surely_not_lam e
+                   -- eta-reduction could float
+                surely_not_lam _            = True
                         -- Do not do the "abstract tyyvar" thing if there's
                         -- a lambda inside, because it defeats eta-reduction
                         --    f = /\a. \x. g a x
@@ -344,98 +258,115 @@ simplLazyBind env top_lvl is_rec bndr bndr1 rhs rhs_se
                 -- See Note [Floating and type abstraction] in SimplUtils
 
         -- Simplify the RHS
-        ; let   rhs_cont = mkRhsStop (substTy body_env (exprType body))
-        ; (body_env1, body1) <- simplExprF body_env body rhs_cont
-        -- ANF-ise a constructor or PAP rhs
-        ; (body_env2, body2) <- prepareRhs top_lvl body_env1 bndr1 body1
+        ; let rhs_cont = mkRhsStop (substTy body_env (exprType body))
+        ; (body_floats0, body0) <- simplExprF body_env body rhs_cont
 
-        ; (env', rhs')
-            <-  if not (doFloatFromRhs top_lvl is_rec False body2 body_env2)
-                then                            -- No floating, revert to body1
-                     do { rhs' <- mkLam tvs' (wrapFloats body_env1 body1) rhs_cont
-                        ; return (env, rhs') }
+              -- Never float join-floats out of a non-join let-binding
+              -- So wrap the body in the join-floats right now
+              -- Henc: body_floats1 consists only of let-floats
+        ; let (body_floats1, body1) = wrapJoinFloatsX body_floats0 body0
 
-                else if null tvs then           -- Simple floating
+        -- ANF-ise a constructor or PAP rhs
+        -- We get at most one float per argument here
+        ; (let_floats, body2) <- prepareRhs (getMode env) top_lvl
+                                            (getOccFS bndr1) (idInfo bndr1) body1
+        ; let body_floats2 = body_floats1 `addLetFloats` let_floats
+
+        ; (rhs_floats, rhs')
+            <-  if not (doFloatFromRhs top_lvl is_rec False body_floats2 body2)
+                then                    -- No floating, revert to body1
+                     do { rhs' <- mkLam env tvs' (wrapFloats body_floats2 body1) rhs_cont
+                        ; return (emptyFloats env, rhs') }
+
+                else if null tvs then   -- Simple floating
                      do { tick LetFloatFromLet
-                        ; return (addFloats env body_env2, body2) }
+                        ; return (body_floats2, body2) }
 
-                else                            -- Do type-abstraction first
+                else                    -- Do type-abstraction first
                      do { tick LetFloatFromLet
-                        ; (poly_binds, body3) <- abstractFloats tvs' body_env2 body2
-                        ; rhs' <- mkLam tvs' body3 rhs_cont
-                        ; env' <- foldlM (addPolyBind top_lvl) env poly_binds
-                        ; return (env', rhs') }
-
-        ; completeBind env' top_lvl bndr bndr1 rhs' }
-
-{-
-A specialised variant of simplNonRec used when the RHS is already simplified,
-notably in knownCon.  It uses case-binding where necessary.
--}
-
+                        ; (poly_binds, body3) <- abstractFloats (seDynFlags env) top_lvl
+                                                                tvs' body_floats2 body2
+                        ; let floats = foldl extendFloats (emptyFloats env) poly_binds
+                        ; rhs' <- mkLam env tvs' body3 rhs_cont
+                        ; return (floats, rhs') }
+
+        ; (bind_float, env2) <- completeBind (env `setInScopeFromF` rhs_floats)
+                                             top_lvl Nothing bndr bndr1 rhs'
+        ; return (rhs_floats `addFloats` bind_float, env2) }
+
+--------------------------
+simplJoinBind :: SimplEnv
+              -> SimplCont
+              -> InId -> OutId          -- Binder, both pre-and post simpl
+                                        -- The OutId has IdInfo, except arity,
+                                        --   unfolding
+              -> InExpr
+              -> SimplM (SimplFloats, SimplEnv)
+simplJoinBind env cont old_bndr new_bndr rhs
+  = do  { rhs' <- simplJoinRhs env old_bndr rhs cont
+        ; completeBind env NotTopLevel (Just cont) old_bndr new_bndr rhs' }
+
+--------------------------
 simplNonRecX :: SimplEnv
-             -> InId            -- Old binder
+             -> InId            -- Old binder; not a JoinId
              -> OutExpr         -- Simplified RHS
-             -> SimplM SimplEnv
+             -> SimplM (SimplFloats, SimplEnv)
+-- A specialised variant of simplNonRec used when the RHS is already
+-- simplified, notably in knownCon.  It uses case-binding where necessary.
+--
 -- Precondition: rhs satisfies the let/app invariant
+
 simplNonRecX env bndr new_rhs
-  | isDeadBinder bndr   -- Not uncommon; e.g. case (a,b) of c { (p,q) -> p }
-  = return env    --  Here c is dead, and we avoid creating
-                  --   the binding c = (a,b)
+  | ASSERT2( not (isJoinId bndr), ppr bndr )
+    isDeadBinder bndr   -- Not uncommon; e.g. case (a,b) of c { (p,q) -> p }
+  = return (emptyFloats env, env)    --  Here c is dead, and we avoid
+                                         --  creating the binding c = (a,b)
 
   | Coercion co <- new_rhs
-  = return (extendCvSubst env bndr co)
+  = return (emptyFloats env, extendCvSubst env bndr co)
 
   | otherwise
   = do  { (env', bndr') <- simplBinder env bndr
         ; completeNonRecX NotTopLevel env' (isStrictId bndr) bndr bndr' new_rhs }
                 -- simplNonRecX is only used for NotTopLevel things
 
+--------------------------
 completeNonRecX :: TopLevelFlag -> SimplEnv
                 -> Bool
-                -> InId                 -- Old binder
+                -> InId                 -- Old binder; not a JoinId
                 -> OutId                -- New binder
                 -> OutExpr              -- Simplified RHS
-                -> SimplM SimplEnv
+                -> SimplM (SimplFloats, SimplEnv)    -- The new binding is in the floats
 -- Precondition: rhs satisfies the let/app invariant
 --               See Note [CoreSyn let/app invariant] in CoreSyn
 
 completeNonRecX top_lvl env is_strict old_bndr new_bndr new_rhs
-  = do  { (env1, rhs1) <- prepareRhs top_lvl (zapFloats env) new_bndr new_rhs
-        ; (env2, rhs2) <-
-                if doFloatFromRhs NotTopLevel NonRecursive is_strict rhs1 env1
-                then do { tick LetFloatFromLet
-                        ; return (addFloats env env1, rhs1) }   -- Add the floats to the main env
-                else return (env, wrapFloats env1 rhs1)         -- Wrap the floats around the RHS
-        ; completeBind env2 NotTopLevel old_bndr new_bndr rhs2 }
+  = ASSERT2( not (isJoinId new_bndr), ppr new_bndr )
+    do  { (prepd_floats, rhs1) <- prepareRhs (getMode env) top_lvl (getOccFS new_bndr)
+                                             (idInfo new_bndr) new_rhs
+        ; let floats = emptyFloats env `addLetFloats` prepd_floats
+        ; (rhs_floats, rhs2) <-
+                if doFloatFromRhs NotTopLevel NonRecursive is_strict floats rhs1
+                then    -- Add the floats to the main env
+                     do { tick LetFloatFromLet
+                        ; return (floats, rhs1) }
+                else    -- Do not float; wrap the floats around the RHS
+                     return (emptyFloats env, wrapFloats floats rhs1)
 
-{-
-{- No, no, no!  Do not try preInlineUnconditionally in completeNonRecX
-   Doing so risks exponential behaviour, because new_rhs has been simplified once already
-   In the cases described by the folowing commment, postInlineUnconditionally will
-   catch many of the relevant cases.
-        -- 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 ...
-        --
-        -- Similarly, single occurrences can be inlined vigourously
-        -- e.g.  case (f x, g y) of (a,b) -> ....
-        -- If a,b occur once we can avoid constructing the let binding for them.
-
-   Furthermore in the case-binding case preInlineUnconditionally risks extra thunks
-        -- Consider     case I# (quotInt# x y) of
-        --                I# v -> let w = J# v in ...
-        -- If we gaily inline (quotInt# x y) for v, we end up building an
-        -- extra thunk:
-        --                let w = J# (quotInt# x y) in ...
-        -- because quotInt# can fail.
-
-  | preInlineUnconditionally env NotTopLevel bndr new_rhs
-  = thing_inside (extendIdSubst env bndr (DoneEx new_rhs))
--}
+        ; (bind_float, env2) <- completeBind (env `setInScopeFromF` rhs_floats)
+                                             NotTopLevel Nothing
+                                             old_bndr new_bndr rhs2
+        ; return (rhs_floats `addFloats` bind_float, env2) }
 
-----------------------------------
+
+{- *********************************************************************
+*                                                                      *
+           prepareRhs, makeTrivial
+*                                                                      *
+************************************************************************
+
+Note [prepareRhs]
+~~~~~~~~~~~~~~~~~
 prepareRhs takes a putative RHS, checks whether it's a PAP or
 constructor application and, if so, converts it to ANF, so that the
 resulting thing can be inlined more easily.  Thus
@@ -452,59 +383,74 @@ Here we want to make e1,e2 trivial and get
 That's what the 'go' loop in prepareRhs does
 -}
 
-prepareRhs :: TopLevelFlag -> SimplEnv -> OutId -> OutExpr -> SimplM (SimplEnv, OutExpr)
--- Adds new floats to the env iff that allows us to return a good RHS
-prepareRhs top_lvl env id (Cast rhs co)    -- Note [Float coercions]
-  | Pair ty1 _ty2 <- coercionKind co       -- Do *not* do this if rhs has an unlifted type
-  , not (isUnLiftedType ty1)            -- see Note [Float coercions (unlifted)]
-  = do  { (env', rhs') <- makeTrivialWithInfo top_lvl env sanitised_info rhs
-        ; return (env', Cast rhs' co) }
+prepareRhs :: SimplMode -> TopLevelFlag
+           -> FastString   -- Base for any new variables
+           -> IdInfo       -- IdInfo for the LHS of this binding
+           -> OutExpr
+           -> SimplM (LetFloats, OutExpr)
+-- Transforms a RHS into a better RHS by adding floats
+-- e.g        x = Just e
+-- becomes    a = e
+--            x = Just a
+-- See Note [prepareRhs]
+prepareRhs mode top_lvl occ info (Cast rhs co)  -- Note [Float coercions]
+  | Pair ty1 _ty2 <- coercionKind co         -- Do *not* do this if rhs has an unlifted type
+  , not (isUnliftedType ty1)                 -- see Note [Float coercions (unlifted)]
+  = do  { (floats, rhs') <- makeTrivialWithInfo mode top_lvl occ sanitised_info rhs
+        ; return (floats, Cast rhs' co) }
   where
     sanitised_info = vanillaIdInfo `setStrictnessInfo` strictnessInfo info
-                                   `setDemandInfo` demandInfo info
-    info = idInfo id
+                                   `setDemandInfo`     demandInfo info
 
-prepareRhs top_lvl env0 _ rhs0
-  = do  { (_is_exp, env1, rhs1) <- go 0 env0 rhs0
-        ; return (env1, rhs1) }
+prepareRhs mode top_lvl occ _ rhs0
+  = do  { (_is_exp, floats, rhs1) <- go 0 rhs0
+        ; return (floats, rhs1) }
   where
-    go n_val_args env (Cast rhs co)
-        = do { (is_exp, env', rhs') <- go n_val_args env rhs
-             ; return (is_exp, env', Cast rhs' co) }
-    go n_val_args env (App fun (Type ty))
-        = do { (is_exp, env', rhs') <- go n_val_args env fun
-             ; return (is_exp, env', App rhs' (Type ty)) }
-    go n_val_args env (App fun arg)
-        = do { (is_exp, env', fun') <- go (n_val_args+1) env fun
+    go :: Int -> OutExpr -> SimplM (Bool, LetFloats, OutExpr)
+    go n_val_args (Cast rhs co)
+        = do { (is_exp, floats, rhs') <- go n_val_args rhs
+             ; return (is_exp, floats, Cast rhs' co) }
+    go n_val_args (App fun (Type ty))
+        = do { (is_exp, floats, rhs') <- go n_val_args fun
+             ; return (is_exp, floats, App rhs' (Type ty)) }
+    go n_val_args (App fun arg)
+        = do { (is_exp, floats1, fun') <- go (n_val_args+1) fun
              ; case is_exp of
-                True -> do { (env'', arg') <- makeTrivial top_lvl env' arg
-                           ; return (True, env'', App fun' arg') }
-                False -> return (False, env, App fun arg) }
-    go n_val_args env (Var fun)
-        = return (is_exp, env, Var fun)
+                False -> return (False, emptyLetFloats, App fun arg)
+                True  -> do { (floats2, arg') <- makeTrivial mode top_lvl occ arg
+                            ; return (True, floats1 `addLetFlts` floats2, App fun' arg') } }
+    go n_val_args (Var fun)
+        = return (is_exp, emptyLetFloats, Var fun)
         where
           is_exp = isExpandableApp fun n_val_args   -- The fun a constructor or PAP
                         -- See Note [CONLIKE pragma] in BasicTypes
                         -- The definition of is_exp should match that in
                         -- OccurAnal.occAnalApp
 
-    go n_val_args env (Tick t rhs)
+    go n_val_args (Tick t rhs)
         -- We want to be able to float bindings past this
         -- tick. Non-scoping ticks don't care.
         | tickishScoped t == NoScope
-        = do { (is_exp, env', rhs') <- go n_val_args env rhs
-             ; return (is_exp, env', Tick t rhs') }
+        = do { (is_exp, floats, rhs') <- go n_val_args rhs
+             ; return (is_exp, floats, Tick t rhs') }
+
         -- On the other hand, for scoping ticks we need to be able to
         -- copy them on the floats, which in turn is only allowed if
         -- we can obtain non-counting ticks.
-        | not (tickishCounts t) || tickishCanSplit t
-        = do { (is_exp, env', rhs') <- go n_val_args (zapFloats env) rhs
-             ; let tickIt (id, expr) = (id, mkTick (mkNoCount t) expr)
-                   floats' = seFloats $ env `addFloats` mapFloats env' tickIt
-             ; return (is_exp, env' { seFloats = floats' }, Tick t rhs') }
-
-    go _ env other
-        = return (False, env, other)
+        | (not (tickishCounts t) || tickishCanSplit t)
+        = do { (is_exp, floats, rhs') <- go n_val_args rhs
+             ; let tickIt (id, expr)
+                       -- we have to take care not to tick top-level literal
+                       -- strings. See Note [CoreSyn top-level string literals].
+                     | isTopLevel top_lvl && exprIsLiteralString expr
+                     = (id, expr)
+                     | otherwise
+                     = (id, mkTick (mkNoCount t) expr)
+                   floats' = mapLetFloats floats tickIt
+             ; return (is_exp, floats', Tick t rhs') }
+
+    go _ other
+        = return (False, emptyLetFloats, other)
 
 {-
 Note [Float coercions]
@@ -515,7 +461,7 @@ we'd like to transform it to
         x' = e
         x = x `cast` co         -- A trivial binding
 There's a chance that e will be a constructor application or function, or something
-like that, so moving the coerion to the usage site may well cancel the coersions
+like that, so moving the coercion to the usage site may well cancel the coercions
 and lead to further optimisation.  Example:
 
      data family T a :: *
@@ -557,55 +503,73 @@ These strange casts can happen as a result of case-of-case
                 (# p,q #) -> p+q
 -}
 
-makeTrivialArg :: SimplEnv -> ArgSpec -> SimplM (SimplEnv, ArgSpec)
-makeTrivialArg env (ValArg e) = do { (env', e') <- makeTrivial NotTopLevel env e
-                                   ; return (env', ValArg e') }
-makeTrivialArg env arg        = return (env, arg)  -- CastBy, TyArg
-
-makeTrivial :: TopLevelFlag -> SimplEnv -> OutExpr -> SimplM (SimplEnv, OutExpr)
+makeTrivialArg :: SimplMode -> ArgSpec -> SimplM (LetFloats, ArgSpec)
+makeTrivialArg mode (ValArg e)
+  = do { (floats, e') <- makeTrivial mode NotTopLevel (fsLit "arg") e
+       ; return (floats, ValArg e') }
+makeTrivialArg _ arg
+  = return (emptyLetFloats, arg)  -- CastBy, TyArg
+
+makeTrivial :: SimplMode -> TopLevelFlag
+            -> FastString  -- ^ A "friendly name" to build the new binder from
+            -> OutExpr     -- ^ This expression satisfies the let/app invariant
+            -> SimplM (LetFloats, OutExpr)
 -- Binds the expression to a variable, if it's not trivial, returning the variable
-makeTrivial top_lvl env expr = makeTrivialWithInfo top_lvl env vanillaIdInfo expr
-
-makeTrivialWithInfo :: TopLevelFlag -> SimplEnv -> IdInfo
-                    -> OutExpr -> SimplM (SimplEnv, OutExpr)
+makeTrivial mode top_lvl context expr
+ = makeTrivialWithInfo mode top_lvl context vanillaIdInfo expr
+
+makeTrivialWithInfo :: SimplMode -> TopLevelFlag
+                    -> FastString  -- ^ a "friendly name" to build the new binder from
+                    -> IdInfo
+                    -> OutExpr     -- ^ This expression satisfies the let/app invariant
+                    -> SimplM (LetFloats, OutExpr)
 -- Propagate strictness and demand info to the new binder
 -- Note [Preserve strictness when floating coercions]
 -- Returned SimplEnv has same substitution as incoming one
-makeTrivialWithInfo top_lvl env info expr
+makeTrivialWithInfo mode top_lvl occ_fs info expr
   | exprIsTrivial expr                          -- Already trivial
   || not (bindingOk top_lvl expr expr_ty)       -- Cannot trivialise
                                                 --   See Note [Cannot trivialise]
-  = return (env, expr)
-  | otherwise           -- See Note [Take care] below
-  = do  { uniq <- getUniqueM
-        ; let name = mkSystemVarName uniq (fsLit "a")
-              var = mkLocalIdWithInfo name expr_ty info
-        ; env'  <- completeNonRecX top_lvl env False var var expr
-        ; expr' <- simplVar env' var
-        ; return (env', expr') }
-        -- The simplVar is needed becase we're constructing a new binding
-        --     a = rhs
-        -- And if rhs is of form (rhs1 |> co), then we might get
-        --     a1 = rhs1
-        --     a = a1 |> co
-        -- and now a's RHS is trivial and can be substituted out, and that
-        -- is what completeNonRecX will do
-        -- To put it another way, it's as if we'd simplified
-        --    let var = e in var
-  where
-    expr_ty = exprType expr
+  = return (emptyLetFloats, expr)
+
+  | otherwise
+  = do  { (floats, expr1) <- prepareRhs mode top_lvl occ_fs info expr
+        ; if   exprIsTrivial expr1  -- See Note [Trivial after prepareRhs]
+          then return (floats, expr1)
+          else do
+        { uniq <- getUniqueM
+        ; let name = mkSystemVarName uniq occ_fs
+              var  = mkLocalIdOrCoVarWithInfo name expr_ty info
+
+        -- Now something very like completeBind,
+        -- but without the postInlineUnconditinoally part
+        ; (arity, is_bot, expr2) <- tryEtaExpandRhs mode var expr1
+        ; unf <- mkLetUnfolding (sm_dflags mode) top_lvl InlineRhs var expr2
+
+        ; let final_id = addLetBndrInfo var arity is_bot unf
+              bind     = NonRec final_id expr2
+
+        ; return ( floats `addLetFlts` unitLetFloat bind, Var final_id ) }}
+   where
+     expr_ty = exprType expr
 
 bindingOk :: TopLevelFlag -> CoreExpr -> Type -> Bool
 -- True iff we can have a binding of this expression at this level
 -- Precondition: the type is the type of the expression
-bindingOk top_lvl _ expr_ty
-  | isTopLevel top_lvl = not (isUnLiftedType expr_ty)
+bindingOk top_lvl expr expr_ty
+  | isTopLevel top_lvl = exprIsTopLevelBindable expr expr_ty
   | otherwise          = True
 
-{-
+{- Note [Trivial after prepareRhs]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we call makeTrival on (e |> co), the recursive use of prepareRhs
+may leave us with
+   { a1 = e }  and   (a1 |> co)
+Now the latter is trivial, so we don't want to let-bind it.
+
 Note [Cannot trivialise]
 ~~~~~~~~~~~~~~~~~~~~~~~~
-Consider tih
+Consider:
    f :: Int -> Addr#
 
    foo :: Bar
@@ -618,16 +582,20 @@ so we don't want to turn it into
 because we'll just end up inlining x back, and that makes the
 simplifier loop.  Better not to ANF-ise it at all.
 
-A case in point is literal strings (a MachStr is not regarded as
-trivial):
+Literal strings are an exception.
 
    foo = Ptr "blob"#
 
-We don't want to ANF-ise this.
+We want to turn this into:
+
+   foo1 = "blob"#
+   foo = Ptr foo1
+
+See Note [CoreSyn top-level string literals] in CoreSyn.
 
 ************************************************************************
 *                                                                      *
-\subsection{Completing a lazy binding}
+          Completing a lazy binding
 *                                                                      *
 ************************************************************************
 
@@ -653,19 +621,21 @@ Nor does it do the atomic-argument thing
 
 completeBind :: SimplEnv
              -> TopLevelFlag            -- Flag stuck into unfolding
+             -> Maybe SimplCont         -- Required only for join point
              -> InId                    -- Old binder
              -> OutId -> OutExpr        -- New binder and RHS
-             -> SimplM SimplEnv
+             -> SimplM (SimplFloats, SimplEnv)
 -- completeBind may choose to do its work
 --      * by extending the substitution (e.g. let x = y in ...)
 --      * or by adding to the floats in the envt
 --
+-- Binder /can/ be a JoinId
 -- Precondition: rhs obeys the let/app invariant
-completeBind env top_lvl old_bndr new_bndr new_rhs
+completeBind env top_lvl mb_cont old_bndr new_bndr new_rhs
  | isCoVar old_bndr
  = case new_rhs of
-     Coercion co -> return (extendCvSubst env old_bndr co)
-     _           -> return (addNonRec env new_bndr new_rhs)
+     Coercion co -> return (emptyFloats env, extendCvSubst env old_bndr co)
+     _           -> return (mkFloatBind env (NonRec new_bndr new_rhs))
 
  | otherwise
  = ASSERT( isId new_bndr )
@@ -673,136 +643,64 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
             old_unf  = unfoldingInfo old_info
             occ_info = occInfo old_info
 
-        -- Do eta-expansion on the RHS of the binding
-        -- See Note [Eta-expanding at let bindings] in SimplUtils
-      ; (new_arity, final_rhs) <- tryEtaExpandRhs env new_bndr new_rhs
+         -- Do eta-expansion on the RHS of the binding
+         -- See Note [Eta-expanding at let bindings] in SimplUtils
+      ; (new_arity, is_bot, final_rhs) <- tryEtaExpandRhs (getMode env)
+                                                          new_bndr new_rhs
 
         -- Simplify the unfolding
-      ; new_unfolding <- simplUnfolding env top_lvl old_bndr final_rhs old_unf
+      ; new_unfolding <- simplLetUnfolding env top_lvl mb_cont old_bndr
+                                           final_rhs old_unf
 
-      ; dflags <- getDynFlags
-      ; if postInlineUnconditionally dflags env top_lvl new_bndr occ_info
-                                     final_rhs new_unfolding
+      ; let final_bndr = addLetBndrInfo new_bndr new_arity is_bot new_unfolding
 
-                        -- Inline and discard the binding
-        then do  { tick (PostInlineUnconditionally old_bndr)
-                 ; return (extendIdSubst env old_bndr (DoneEx final_rhs)) }
+      ; if postInlineUnconditionally env top_lvl final_bndr occ_info final_rhs
+
+        then -- Inline and discard the binding
+             do  { tick (PostInlineUnconditionally old_bndr)
+                 ; return ( emptyFloats env
+                          , extendIdSubst env old_bndr $
+                            DoneEx final_rhs (isJoinId_maybe new_bndr)) }
                 -- Use the substitution to make quite, quite sure that the
                 -- substitution will happen, since we are going to discard the binding
-        else
-   do { let info1 = idInfo new_bndr `setArityInfo` new_arity
-
-              -- Unfolding info: Note [Setting the new unfolding]
-            info2 = info1 `setUnfoldingInfo` new_unfolding
-
-              -- Demand info: Note [Setting the demand info]
-              --
-              -- We also have to nuke demand info if for some reason
-              -- eta-expansion *reduces* the arity of the binding to less
-              -- than that of the strictness sig. This can happen: see Note [Arity decrease].
-            info3 | isEvaldUnfolding new_unfolding
-                    || (case strictnessInfo info2 of
-                          StrictSig dmd_ty -> new_arity < dmdTypeDepth dmd_ty)
-                  = zapDemandInfo info2 `orElse` info2
-                  | otherwise
-                  = info2
-
-            final_id = new_bndr `setIdInfo` info3
-
-      ; -- pprTrace "Binding" (ppr final_id <+> ppr new_unfolding) $
-        return (addNonRec env final_id final_rhs) } }
-                -- The addNonRec adds it to the in-scope set too
-
-------------------------------
-addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplM SimplEnv
--- Add a new binding to the environment, complete with its unfolding
--- but *do not* do postInlineUnconditionally, because we have already
--- processed some of the scope of the binding
--- We still want the unfolding though.  Consider
---      let
---            x = /\a. let y = ... in Just y
---      in body
--- Then we float the y-binding out (via abstractFloats and addPolyBind)
--- but 'x' may well then be inlined in 'body' in which case we'd like the
--- opportunity to inline 'y' too.
---
--- INVARIANT: the arity is correct on the incoming binders
-
-addPolyBind top_lvl env (NonRec poly_id rhs)
-  = do  { unfolding <- simplUnfolding env top_lvl poly_id rhs noUnfolding
-                        -- Assumes that poly_id did not have an INLINE prag
-                        -- which is perhaps wrong.  ToDo: think about this
-        ; let final_id = setIdInfo poly_id $
-                         idInfo poly_id `setUnfoldingInfo` unfolding
-
-        ; return (addNonRec env final_id rhs) }
-
-addPolyBind _ env bind@(Rec _)
-  = return (extendFloats env bind)
-        -- Hack: letrecs are more awkward, so we extend "by steam"
-        -- without adding unfoldings etc.  At worst this leads to
-        -- more simplifier iterations
-
-------------------------------
-simplUnfolding :: SimplEnv-> TopLevelFlag
-               -> InId
-               -> OutExpr
-               -> Unfolding -> SimplM Unfolding
--- Note [Setting the new unfolding]
-simplUnfolding env top_lvl id new_rhs unf
-  = case unf of
-      DFunUnfolding { df_bndrs = bndrs, df_con = con, df_args = args }
-        -> do { (env', bndrs') <- simplBinders rule_env bndrs
-              ; args' <- mapM (simplExpr env') args
-              ; return (mkDFunUnfolding bndrs' con args') }
 
-      CoreUnfolding { uf_tmpl = expr, uf_src = src, uf_guidance = guide }
-        | isStableSource src
-        -> do { expr' <- simplExpr rule_env expr
-              ; case guide of
-                  UnfWhen { ug_arity = arity, ug_unsat_ok = sat_ok }  -- Happens for INLINE things
-                     -> let guide' = UnfWhen { ug_arity = arity, ug_unsat_ok = sat_ok
-                                             , ug_boring_ok = inlineBoringOk expr' }
-                        -- Refresh the boring-ok flag, in case expr'
-                        -- has got small. This happens, notably in the inlinings
-                        -- for dfuns for single-method classes; see
-                        -- Note [Single-method classes] in TcInstDcls.
-                        -- A test case is Trac #4138
-                        in return (mkCoreUnfolding src is_top_lvl expr' guide')
-                            -- See Note [Top-level flag on inline rules] in CoreUnfold
-
-                  _other              -- Happens for INLINABLE things
-                     -> bottoming `seq` -- See Note [Force bottoming field]
-                        do { dflags <- getDynFlags
-                           ; return (mkUnfolding dflags src is_top_lvl bottoming expr') } }
-                -- If the guidance is UnfIfGoodArgs, this is an INLINABLE
-                -- unfolding, and we need to make sure the guidance is kept up
-                -- to date with respect to any changes in the unfolding.
+        else -- Keep the binding
+             -- pprTrace "Binding" (ppr final_bndr <+> ppr new_unfolding) $
+             return (mkFloatBind env (NonRec final_bndr final_rhs)) }
 
-      _other -> bottoming `seq`  -- See Note [Force bottoming field]
-                do { dflags <- getDynFlags
-                   ; return (mkUnfolding dflags InlineRhs is_top_lvl bottoming new_rhs) }
-                     -- We make an  unfolding *even for loop-breakers*.
-                     -- Reason: (a) It might be useful to know that they are WHNF
-                     --         (b) In TidyPgm we currently assume that, if we want to
-                     --             expose the unfolding then indeed we *have* an unfolding
-                     --             to expose.  (We could instead use the RHS, but currently
-                     --             we don't.)  The simple thing is always to have one.
+addLetBndrInfo :: OutId -> Arity -> Bool -> Unfolding -> OutId
+addLetBndrInfo new_bndr new_arity is_bot new_unf
+  = new_bndr `setIdInfo` info5
   where
-    bottoming = isBottomingId id
-    is_top_lvl = isTopLevel top_lvl
-    act      = idInlineActivation id
-    rule_env = updMode (updModeForStableUnfoldings act) env
-               -- See Note [Simplifying inside stable unfoldings] in SimplUtils
-
-{-
-Note [Force bottoming field]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We need to force bottoming, or the new unfolding holds
-on to the old unfolding (which is part of the id).
-
-Note [Arity decrease]
-~~~~~~~~~~~~~~~~~~~~~
+    info1 = idInfo new_bndr `setArityInfo` new_arity
+
+    -- Unfolding info: Note [Setting the new unfolding]
+    info2 = info1 `setUnfoldingInfo` new_unf
+
+    -- Demand info: Note [Setting the demand info]
+    -- We also have to nuke demand info if for some reason
+    -- eta-expansion *reduces* the arity of the binding to less
+    -- than that of the strictness sig. This can happen: see Note [Arity decrease].
+    info3 | isEvaldUnfolding new_unf
+            || (case strictnessInfo info2 of
+                  StrictSig dmd_ty -> new_arity < dmdTypeDepth dmd_ty)
+          = zapDemandInfo info2 `orElse` info2
+          | otherwise
+          = info2
+
+    -- Bottoming bindings: see Note [Bottoming bindings]
+    info4 | is_bot    = info3 `setStrictnessInfo`
+                        mkClosedStrictSig (replicate new_arity topDmd) exnRes
+          | otherwise = info3
+
+     -- Zap call arity info. We have used it by now (via
+     -- `tryEtaExpandRhs`), and the simplifier can invalidate this
+     -- information, leading to broken code later (e.g. #13479)
+    info5 = zapCallArityInfo info4
+
+
+{- Note [Arity decrease]
+~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking the arity of a binding should not decrease.  But it *can*
 legitimately happen because of RULES.  Eg
         f = g Int
@@ -824,21 +722,25 @@ Here opInt has arity 1; but when we apply the rule its arity drops to 0.
 That's why Specialise goes to a little trouble to pin the right arity
 on specialised functions too.
 
-Note [Setting the new unfolding]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-* If there's an INLINE pragma, we simplify the RHS gently.  Maybe we
-  should do nothing at all, but simplifying gently might get rid of
-  more crap.
+Note [Bottoming bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+   let x = error "urk"
+   in ...(case x of <alts>)...
+or
+   let f = \x. error (x ++ "urk")
+   in ...(case f "foo" of <alts>)...
 
-* If not, we make an unfolding from the new RHS.  But *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
+Then we'd like to drop the dead <alts> immediately.  So it's good to
+propagate the info that x's RHS is bottom to x's IdInfo as rapidly as
+possible.
 
-If there's an stable unfolding on a loop breaker (which happens for
-INLINEABLE), we hang on to the inlining.  It's pretty dodgy, but the
-user did say 'INLINE'.  May need to revisit this choice.
+We use tryEtaExpandRhs on every binding, and it turns ou that the
+arity computation it performs (via CoreArity.findRhsArity) already
+does a simple bottoming-expression analysis.  So all we need to do
+is propagate that info to the binder's IdInfo.
+
+This showed up in Trac #12150; see comment:16.
 
 Note [Setting the demand info]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -902,24 +804,36 @@ might do the same again.
 -}
 
 simplExpr :: SimplEnv -> CoreExpr -> SimplM CoreExpr
-simplExpr env expr = simplExprC env expr (mkBoringStop expr_out_ty)
+simplExpr env (Type ty)
+  = do { ty' <- simplType env ty  -- See Note [Avoiding space leaks in OutType]
+       ; return (Type ty') }
+
+simplExpr env expr
+  = simplExprC env expr (mkBoringStop expr_out_ty)
   where
     expr_out_ty :: OutType
     expr_out_ty = substTy env (exprType expr)
+    -- NB: Since 'expr' is term-valued, not (Type ty), this call
+    --     to exprType will succeed.  exprType fails on (Type ty).
 
-simplExprC :: SimplEnv -> CoreExpr -> SimplCont -> SimplM CoreExpr
+simplExprC :: SimplEnv
+           -> InExpr     -- A term-valued expression, never (Type ty)
+           -> SimplCont
+           -> SimplM OutExpr
         -- Simplify an expression, given a continuation
 simplExprC env expr cont
-  = -- pprTrace "simplExprC" (ppr expr $$ ppr cont {- $$ ppr (seIdSubst env) -} $$ ppr (seFloats env) ) $
-    do  { (env', expr') <- simplExprF (zapFloats env) expr cont
+  = -- pprTrace "simplExprC" (ppr expr $$ ppr cont {- $$ ppr (seIdSubst env) -} $$ ppr (seLetFloats env) ) $
+    do  { (floats, expr') <- simplExprF env expr cont
         ; -- pprTrace "simplExprC ret" (ppr expr $$ ppr expr') $
           -- pprTrace "simplExprC ret3" (ppr (seInScope env')) $
-          -- pprTrace "simplExprC ret4" (ppr (seFloats env')) $
-          return (wrapFloats env' expr') }
+          -- pprTrace "simplExprC ret4" (ppr (seLetFloats env')) $
+          return (wrapFloats floats expr') }
 
 --------------------------------------------------
-simplExprF :: SimplEnv -> InExpr -> SimplCont
-           -> SimplM (SimplEnv, OutExpr)
+simplExprF :: SimplEnv
+           -> InExpr     -- A term-valued expression, never (Type ty)
+           -> SimplCont
+           -> SimplM (SimplFloats, OutExpr)
 
 simplExprF env e cont
   = {- pprTrace "simplExprF" (vcat
@@ -929,27 +843,42 @@ simplExprF env e cont
       , text "tvsubst =" <+> ppr (seTvSubst env)
       , text "idsubst =" <+> ppr (seIdSubst env)
       , text "cvsubst =" <+> ppr (seCvSubst env)
-      {- , ppr (seFloats env) -}
       ]) $ -}
     simplExprF1 env e cont
 
 simplExprF1 :: SimplEnv -> InExpr -> SimplCont
-            -> SimplM (SimplEnv, OutExpr)
+            -> SimplM (SimplFloats, OutExpr)
+
+simplExprF1 _ (Type ty) _
+  = pprPanic "simplExprF: type" (ppr ty)
+    -- simplExprF does only with term-valued expressions
+    -- The (Type ty) case is handled separately by simplExpr
+    -- and by the other callers of simplExprF
+
 simplExprF1 env (Var v)        cont = simplIdF env v cont
 simplExprF1 env (Lit lit)      cont = rebuild env (Lit lit) cont
 simplExprF1 env (Tick t expr)  cont = simplTick env t expr cont
 simplExprF1 env (Cast body co) cont = simplCast env body co cont
 simplExprF1 env (Coercion co)  cont = simplCoercionF env co cont
-simplExprF1 env (Type ty)      cont = ASSERT( contIsRhsOrArg cont )
-                                      rebuild env (Type (substTy env ty)) cont
 
 simplExprF1 env (App fun arg) cont
-  = simplExprF env fun $
-    case arg of
-      Type ty -> ApplyToTy  { sc_arg_ty  = substTy env ty
-                            , sc_hole_ty = substTy env (exprType fun)
-                            , sc_cont    = cont }
-      _       -> ApplyToVal { sc_arg = arg, sc_env = env
+  = case arg of
+      Type ty -> do { -- The argument type will (almost) certainly be used
+                      -- in the output program, so just force it now.
+                      -- See Note [Avoiding space leaks in OutType]
+                      arg' <- simplType env ty
+
+                      -- But use substTy, not simplType, to avoid forcing
+                      -- the hole type; it will likely not be needed.
+                      -- See Note [The hole type in ApplyToTy]
+                    ; let hole' = substTy env (exprType fun)
+
+                    ; simplExprF env fun $
+                      ApplyToTy { sc_arg_ty  = arg'
+                                , sc_hole_ty = hole'
+                                , sc_cont    = cont } }
+      _       -> simplExprF env fun $
+                 ApplyToVal { sc_arg = arg, sc_env = env
                             , sc_dup = NoDup, sc_cont = cont }
 
 simplExprF1 env expr@(Lam {}) cont
@@ -975,22 +904,95 @@ simplExprF1 env expr@(Lam {}) cont
           | otherwise = zapLamIdInfo b
 
 simplExprF1 env (Case scrut bndr _ alts) cont
-  = simplExprF env scrut (Select NoDup bndr alts env cont)
+  = simplExprF env scrut (Select { sc_dup = NoDup, sc_bndr = bndr
+                                 , sc_alts = alts
+                                 , sc_env = env, sc_cont = cont })
 
 simplExprF1 env (Let (Rec pairs) body) cont
-  = do  { env' <- simplRecBndrs env (map fst pairs)
-                -- NB: bndrs' don't have unfoldings or rules
-                -- We add them as we go down
+  | Just pairs' <- joinPointBindings_maybe pairs
+  = simplRecJoinPoint env pairs' body cont
 
-        ; env'' <- simplRecBind env' NotTopLevel pairs
-        ; simplExprF env'' body cont }
+  | otherwise
+  = simplRecE env pairs body cont
 
 simplExprF1 env (Let (NonRec bndr rhs) body) cont
+  | Type ty <- rhs    -- First deal with type lets (let a = Type ty in e)
+  = ASSERT( isTyVar bndr )
+    do { ty' <- simplType env ty
+       ; simplExprF (extendTvSubst env bndr ty') body cont }
+
+  | Just (bndr', rhs') <- joinPointBinding_maybe bndr rhs
+  = simplNonRecJoinPoint env bndr' rhs' body cont
+
+  | otherwise
   = simplNonRecE env bndr (rhs, env) ([], body) cont
 
+{- Note [Avoiding space leaks in OutType]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Since the simplifier is run for multiple iterations, we need to ensure
+that any thunks in the output of one simplifier iteration are forced
+by the evaluation of the next simplifier iteration. Otherwise we may
+retain multiple copies of the Core program and leak a terrible amount
+of memory (as in #13426).
+
+The simplifier is naturally strict in the entire "Expr part" of the
+input Core program, because any expression may contain binders, which
+we must find in order to extend the SimplEnv accordingly. But types
+do not contain binders and so it is tempting to write things like
+
+    simplExpr env (Type ty) = return (Type (substTy env ty))   -- Bad!
+
+This is Bad because the result includes a thunk (substTy env ty) which
+retains a reference to the whole simplifier environment; and the next
+simplifier iteration will not force this thunk either, because the
+line above is not strict in ty.
+
+So instead our strategy is for the simplifier to fully evaluate
+OutTypes when it emits them into the output Core program, for example
+
+    simplExpr env (Type ty) = do { ty' <- simplType env ty     -- Good
+                                 ; return (Type ty') }
+
+where the only difference from above is that simplType calls seqType
+on the result of substTy.
+
+However, SimplCont can also contain OutTypes and it's not necessarily
+a good idea to force types on the way in to SimplCont, because they
+may end up not being used and forcing them could be a lot of wasted
+work. T5631 is a good example of this.
+
+- For ApplyToTy's sc_arg_ty, we force the type on the way in because
+  the type will almost certainly appear as a type argument in the
+  output program.
+
+- For the hole types in Stop and ApplyToTy, we force the type when we
+  emit it into the output program, after obtaining it from
+  contResultType. (The hole type in ApplyToTy is only directly used
+  to form the result type in a new Stop continuation.)
+-}
+
+---------------------------------
+-- Simplify a join point, adding the context.
+-- Context goes *inside* the lambdas. IOW, if the join point has arity n, we do:
+--   \x1 .. xn -> e => \x1 .. xn -> E[e]
+-- Note that we need the arity of the join point, since e may be a lambda
+-- (though this is unlikely). See Note [Case-of-case and join points].
+simplJoinRhs :: SimplEnv -> InId -> InExpr -> SimplCont
+             -> SimplM OutExpr
+simplJoinRhs env bndr expr cont
+  | Just arity <- isJoinId_maybe bndr
+  =  do { let (join_bndrs, join_body) = collectNBinders arity expr
+        ; (env', join_bndrs') <- simplLamBndrs env join_bndrs
+        ; join_body' <- simplExprC env' join_body cont
+        ; return $ mkLams join_bndrs' join_body' }
+
+  | otherwise
+  = pprPanic "simplJoinRhs" (ppr bndr)
+
 ---------------------------------
 simplType :: SimplEnv -> InType -> SimplM OutType
         -- Kept monadic just so we can do the seqType
+        -- See Note [Avoiding space leaks in OutType]
 simplType env ty
   = -- pprTrace "simplType" (ppr ty $$ ppr (seTvSubst env)) $
     seqType new_ty `seq` return new_ty
@@ -999,14 +1001,14 @@ simplType env ty
 
 ---------------------------------
 simplCoercionF :: SimplEnv -> InCoercion -> SimplCont
-               -> SimplM (SimplEnv, OutExpr)
+               -> SimplM (SimplFloats, OutExpr)
 simplCoercionF env co cont
   = do { co' <- simplCoercion env co
        ; rebuild env (Coercion co') cont }
 
 simplCoercion :: SimplEnv -> InCoercion -> SimplM OutCoercion
 simplCoercion env co
-  = let opt_co = optCoercion (getCvSubst env) co
+  = let opt_co = optCoercion (getTCvSubst env) co
     in seqCo opt_co `seq` return opt_co
 
 -----------------------------------
@@ -1015,7 +1017,7 @@ simplCoercion env co
 -- optimisations apply.
 
 simplTick :: SimplEnv -> Tickish Id -> InExpr -> SimplCont
-          -> SimplM (SimplEnv, OutExpr)
+          -> SimplM (SimplFloats, OutExpr)
 simplTick env tickish expr cont
   -- A scoped tick turns into a continuation, so that we can spot
   -- (scc t (\x . e)) in simplLam and eliminate the scc.  If we didn't do
@@ -1042,8 +1044,8 @@ simplTick env tickish expr cont
   -- application context, allowing the normal case and application
   -- optimisations to fire.
   | tickish `tickishScopesLike` SoftScope
-  = do { (env', expr') <- simplExprF env expr cont
-       ; return (env', mkTick tickish expr')
+  = do { (floats, expr') <- simplExprF env expr cont
+       ; return (floats, mkTick tickish expr')
        }
 
   -- Push tick inside if the context looks like this will allow us to
@@ -1081,12 +1083,10 @@ simplTick env tickish expr cont
 
   no_floating_past_tick =
     do { let (inc,outc) = splitCont cont
-       ; (env', expr') <- simplExprF (zapFloats env) expr inc
-       ; let tickish' = simplTickish env tickish
-       ; (env'', expr'') <- rebuild (zapFloats env')
-                                    (wrapFloats env' expr')
-                                    (TickIt tickish' outc)
-       ; return (addFloats env env'', expr'')
+       ; (floats, expr1) <- simplExprF env expr inc
+       ; let expr2    = wrapFloats floats expr1
+             tickish' = simplTickish env tickish
+       ; rebuild env (mkTick tickish' expr2) outc
        }
 
 -- Alternative version that wraps outgoing floats with the tick.  This
@@ -1122,8 +1122,8 @@ simplTick env tickish expr cont
     where (inc,outc) = splitCont c
   splitCont other = (mkBoringStop (contHoleType other), other)
 
-  getDoneId (DoneId id) = id
-  getDoneId (DoneEx e = getIdFromTrivialExpr e -- Note [substTickish] in CoreSubst
+  getDoneId (DoneId id)  = id
+  getDoneId (DoneEx e _) = getIdFromTrivialExpr e -- Note [substTickish] in CoreSubst
   getDoneId other = pprPanic "getDoneId" (ppr other)
 
 -- Note [case-of-scc-of-case]
@@ -1166,32 +1166,36 @@ simplTick env tickish expr cont
 ************************************************************************
 -}
 
-rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM (SimplEnv, OutExpr)
--- At this point the substitution in the SimplEnv should be irrelevant
--- only the in-scope set and floats should matter
+rebuild :: SimplEnv -> OutExpr -> SimplCont -> SimplM (SimplFloats, OutExpr)
+-- At this point the substitution in the SimplEnv should be irrelevant;
+-- only the in-scope set matters
 rebuild env expr cont
   = case cont of
-      Stop {}                       -> return (env, expr)
-      TickIt t cont                 -> rebuild env (mkTick t expr) cont
-      CastIt co cont                -> rebuild env (mkCast expr co) cont
-                                    -- NB: mkCast implements the (Coercion co |> g) optimisation
-
-      Select _ bndr alts se cont    -> rebuildCase (se `setFloats` env) expr bndr alts cont
-      StrictArg info _ cont         -> rebuildCall env (info `addValArgTo` expr) cont
-
-      StrictBind b bs body se cont  -> do { env' <- simplNonRecX (se `setFloats` env) b expr
-                                               -- expr satisfies let/app since it started life
-                                               -- in a call to simplNonRecE
-                                          ; simplLam env' bs body cont }
+      Stop {}          -> return (emptyFloats env, expr)
+      TickIt t cont    -> rebuild env (mkTick t expr) cont
+      CastIt co cont   -> rebuild env (mkCast expr co) cont
+                       -- NB: mkCast implements the (Coercion co |> g) optimisation
+
+      Select { sc_bndr = bndr, sc_alts = alts, sc_env = se, sc_cont = cont }
+        -> rebuildCase (se `setInScopeFromE` env) expr bndr alts cont
+
+      StrictArg { sc_fun = fun, sc_cont = cont }
+        -> rebuildCall env (fun `addValArgTo` expr) cont
+      StrictBind { sc_bndr = b, sc_bndrs = bs, sc_body = body
+                 , sc_env = se, sc_cont = cont }
+        -> do { (floats1, env') <- simplNonRecX (se `setInScopeFromE` env) b expr
+                                  -- expr satisfies let/app since it started life
+                                  -- in a call to simplNonRecE
+              ; (floats2, expr') <- simplLam env' bs body cont
+              ; return (floats1 `addFloats` floats2, expr') }
 
       ApplyToTy  { sc_arg_ty = ty, sc_cont = cont}
         -> rebuild env (App expr (Type ty)) cont
+
       ApplyToVal { sc_arg = arg, sc_env = se, sc_dup = dup_flag, sc_cont = cont}
         -- See Note [Avoid redundant simplification]
-        | isSimplified dup_flag     -> rebuild env (App expr arg) cont
-        | otherwise                 -> do { arg' <- simplExpr (se `setInScope` env) arg
-                                          ; rebuild env (App expr arg') cont }
-
+        -> do { (_, _, arg') <- simplArg env dup_flag se arg
+              ; rebuild env (App expr arg') cont }
 
 {-
 ************************************************************************
@@ -1202,71 +1206,62 @@ rebuild env expr cont
 -}
 
 simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
-          -> SimplM (SimplEnv, OutExpr)
+          -> SimplM (SimplFloats, OutExpr)
 simplCast env body co0 cont0
-  = do  { co1 <- simplCoercion env co0
-        ; -- pprTrace "simplCast" (ppr co1) $
-          simplExprF env body (addCoerce co1 cont0) }
+  = do  { co1   <- simplCoercion env co0
+        ; cont1 <- addCoerce co1 cont0
+        ; simplExprF env body cont1 }
   where
-       addCoerce co cont = add_coerce co (coercionKind co) cont
-
-       add_coerce _co (Pair s1 k1) cont     -- co :: ty~ty
-         | s1 `eqType` k1 = cont    -- is a no-op
-
-       add_coerce co1 (Pair s1 _k2) (CastIt co2 cont)
-         | (Pair _l1 t1) <- coercionKind co2
-                --      e |> (g1 :: S1~L) |> (g2 :: L~T1)
-                -- ==>
-                --      e,                       if S1=T1
-                --      e |> (g1 . g2 :: S1~T1)  otherwise
-                --
+       addCoerce :: OutCoercion -> SimplCont -> SimplM SimplCont
+       addCoerce co1 (CastIt co2 cont)
+         = addCoerce (mkTransCo co1 co2) cont
+
+       addCoerce co cont@(ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })
+         | Just (arg_ty', co') <- pushCoTyArg co arg_ty
+         = do { tail' <- addCoerce co' tail
+              ; return (cont { sc_arg_ty = arg_ty', sc_cont = tail' }) }
+
+       addCoerce co cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se
+                                , sc_dup = dup, sc_cont = tail })
+         | Just (co1, co2) <- pushCoValArg co
+         , Pair _ new_ty <- coercionKind co1
+         , not (isTypeLevPoly new_ty)  -- without this check, we get a lev-poly arg
+                                       -- See Note [Levity polymorphism invariants] in CoreSyn
+                                       -- test: typecheck/should_run/EtaExpandLevPoly
+         = do { tail' <- addCoerce co2 tail
+              ; if isReflCo co1
+                then return (cont { sc_cont = tail' })
+                     -- Avoid simplifying if possible;
+                     -- See Note [Avoiding exponential behaviour]
+                else do
+              { (dup', arg_se', arg') <- simplArg env dup arg_se arg
+                   -- When we build the ApplyTo we can't mix the OutCoercion
+                   -- 'co' with the InExpr 'arg', so we simplify
+                   -- to make it all consistent.  It's a bit messy.
+                   -- But it isn't a common case.
+                   -- Example of use: Trac #995
+              ; return (ApplyToVal { sc_arg  = mkCast arg' co1
+                                   , sc_env  = arg_se'
+                                   , sc_dup  = dup'
+                                   , sc_cont = tail' }) } }
+
+       addCoerce co cont
+         | isReflexiveCo co = return cont
+         | otherwise        = return (CastIt co cont)
+                -- It's worth checking isReflexiveCo.
                 -- 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
-         , s1 `eqType` t1  = cont            -- The coerces cancel out
-         | otherwise       = CastIt (mkTransCo co1 co2) cont
-
-       add_coerce co (Pair s1s2 _t1t2) cont@(ApplyToTy { sc_arg_ty = arg_ty, sc_cont = tail })
-                -- (f |> g) ty  --->   (f ty) |> (g @ ty)
-                -- This implements the PushT rule from the paper
-         | Just (tyvar,_) <- splitForAllTy_maybe s1s2
-         = ASSERT( isTyVar tyvar )
-           cont { sc_cont = addCoerce new_cast tail }
-         where
-           new_cast = mkInstCo co arg_ty
-
-       add_coerce co (Pair s1s2 t1t2) (ApplyToVal { sc_arg = arg, sc_env = arg_se
-                                                  , sc_dup = dup, sc_cont = cont })
-         | isFunTy s1s2   -- This implements the Push rule from the paper
-         , isFunTy t1t2   -- Check t1t2 to ensure 'arg' is a value arg
-                --      (e |> (g :: s1s2 ~ t1->t2)) f
-                -- ===>
-                --      (e (f |> (arg g :: t1~s1))
-                --      |> (res g :: s2->t2)
-                --
-                -- t1t2 must be a function type, t1->t2, because it's applied
-                -- to something but s1s2 might conceivably not be
-                --
-                -- When we build the ApplyTo we can't mix the out-types
-                -- with the InExpr in the argument, so we simply substitute
-                -- to make it all consistent.  It's a bit messy.
-                -- But it isn't a common case.
-                --
-                -- Example of use: Trac #995
-         = ApplyToVal { sc_arg  = mkCast arg' (mkSymCo co1)
-                      , sc_env  = zapSubstEnv arg_se
-                      , sc_dup  = dup
-                      , sc_cont = addCoerce co2 cont }
-         where
-           -- we split coercion t1->t2 ~ s1->s2 into t1 ~ s1 and
-           -- t2 ~ s2 with left and right on the curried form:
-           --    (->) t1 t2 ~ (->) s1 s2
-           [co1, co2] = decomposeCo 2 co
-           arg'       = substExpr (text "move-cast") arg_se' arg
-           arg_se'    = arg_se `setInScope` env
-
-       add_coerce co _ cont = CastIt co cont
+
+simplArg :: SimplEnv -> DupFlag -> StaticEnv -> CoreExpr
+         -> SimplM (DupFlag, StaticEnv, OutExpr)
+simplArg env dup_flag arg_env arg
+  | isSimplified dup_flag
+  = return (dup_flag, arg_env, arg)
+  | otherwise
+  = do { arg' <- simplExpr (arg_env `setInScopeFromE` env) arg
+       ; return (Simplified, zapSubstEnv arg_env, arg') }
 
 {-
 ************************************************************************
@@ -1274,43 +1269,36 @@ simplCast env body co0 cont0
 \subsection{Lambdas}
 *                                                                      *
 ************************************************************************
-
-Note [Zap unfolding when beta-reducing]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Lambda-bound variables can have stable unfoldings, such as
-   $j = \x. \b{Unf=Just x}. e
-See Note [Case binders and join points] below; the unfolding for lets
-us optimise e better.  However when we beta-reduce it we want to
-revert to using the actual value, otherwise we can end up in the
-stupid situation of
-          let x = blah in
-          let b{Unf=Just x} = y
-          in ...b...
-Here it'd be far better to drop the unfolding and use the actual RHS.
 -}
 
 simplLam :: SimplEnv -> [InId] -> InExpr -> SimplCont
-         -> SimplM (SimplEnv, OutExpr)
+         -> SimplM (SimplFloats, OutExpr)
 
-simplLam env [] body cont = simplExprF env body cont
-
-        -- Beta reduction
+simplLam env [] body cont
+  = simplExprF env body cont
 
 simplLam env (bndr:bndrs) body (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = cont })
   = do { tick (BetaReduction bndr)
        ; simplLam (extendTvSubst env bndr arg_ty) bndrs body cont }
 
 simplLam env (bndr:bndrs) body (ApplyToVal { sc_arg = arg, sc_env = arg_se
-                                           , sc_cont = cont })
+                                           , sc_cont = cont, sc_dup = dup })
+  | isSimplified dup  -- Don't re-simplify if we've simplified it once
+                      -- See Note [Avoiding exponential behaviour]
+  = do  { tick (BetaReduction bndr)
+        ; (floats1, env') <- simplNonRecX env zapped_bndr arg
+        ; (floats2, expr') <- simplLam env' bndrs body cont
+        ; return (floats1 `addFloats` floats2, expr') }
+
+  | otherwise
   = do  { tick (BetaReduction bndr)
-        ; simplNonRecE env (zap_unfolding bndr) (arg, arg_se) (bndrs, body) cont }
+        ; simplNonRecE env zapped_bndr (arg, arg_se) (bndrs, body) cont }
   where
-    zap_unfolding bndr  -- See Note [Zap unfolding when beta-reducing]
-      | isId bndr, isStableUnfolding (realIdUnfolding bndr)
-      = setIdUnfolding bndr NoUnfolding
+    zapped_bndr  -- See Note [Zap unfolding when beta-reducing]
+      | isId bndr = zapStableUnfolding bndr
       | otherwise = bndr
 
-      -- discard a non-counting tick on a lambda.  This may change the
+      -- Discard a non-counting tick on a lambda.  This may change the
       -- cost attribution slightly (moving the allocation of the
       -- lambda elsewhere), but we don't care: optimisation changes
       -- cost attribution all the time.
@@ -1322,22 +1310,50 @@ simplLam env bndrs body (TickIt tickish cont)
 simplLam env bndrs body cont
   = do  { (env', bndrs') <- simplLamBndrs env bndrs
         ; body' <- simplExpr env' body
-        ; new_lam <- mkLam bndrs' body' cont
+        ; new_lam <- mkLam env bndrs' body' cont
         ; rebuild env' new_lam cont }
 
+-------------
+simplLamBndr :: SimplEnv -> InBndr -> SimplM (SimplEnv, OutBndr)
+-- Used for lambda binders.  These sometimes have unfoldings added by
+-- the worker/wrapper pass that must be preserved, because they can't
+-- be reconstructed from context.  For example:
+--      f x = case x of (a,b) -> fw a b x
+--      fw a b x{=(a,b)} = ...
+-- The "{=(a,b)}" is an unfolding we can't reconstruct otherwise.
+simplLamBndr env bndr
+  | isId bndr && isFragileUnfolding old_unf   -- Special case
+  = do { (env1, bndr1) <- simplBinder env bndr
+       ; unf'          <- simplStableUnfolding env1 NotTopLevel Nothing bndr old_unf
+       ; let bndr2 = bndr1 `setIdUnfolding` unf'
+       ; return (modifyInScope env1 bndr2, bndr2) }
+
+  | otherwise
+  = simplBinder env bndr                -- Normal case
+  where
+    old_unf = idUnfolding bndr
+
+simplLamBndrs :: SimplEnv -> [InBndr] -> SimplM (SimplEnv, [OutBndr])
+simplLamBndrs env bndrs = mapAccumLM simplLamBndr env bndrs
+
 ------------------
 simplNonRecE :: SimplEnv
-             -> InBndr                  -- The binder
+             -> InId                    -- The binder, always an Id
+                                        -- Never a join point
              -> (InExpr, SimplEnv)      -- Rhs of binding (or arg of lambda)
              -> ([InBndr], InExpr)      -- Body of the let/lambda
                                         --      \xs.e
              -> SimplCont
-             -> SimplM (SimplEnv, OutExpr)
+             -> SimplM (SimplFloats, OutExpr)
 
 -- simplNonRecE is used for
---  * non-top-level non-recursive lets in expressions
+--  * non-top-level non-recursive non-join-point lets in expressions
 --  * beta reduction
 --
+-- simplNonRec env b (rhs, rhs_se) (bs, body) k
+--   = let env in
+--     cont< let b = rhs_se(rhs) in \bs.body >
+--
 -- It deals with strict bindings, via the StrictBind continuation,
 -- which may abort the whole process
 --
@@ -1349,33 +1365,250 @@ simplNonRecE :: SimplEnv
 -- Why?  Because of the binder-occ-info-zapping done before
 --       the call to simplLam in simplExprF (Lam ...)
 
-        -- First deal with type applications and type lets
-        --   (/\a. e) (Type ty)   and   (let a = Type ty in e)
-simplNonRecE env bndr (Type ty_arg, rhs_se) (bndrs, body) cont
-  = ASSERT( isTyVar bndr )
-    do  { ty_arg' <- simplType (rhs_se `setInScope` env) ty_arg
-        ; simplLam (extendTvSubst env bndr ty_arg') bndrs body cont }
-
 simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
-  = do dflags <- getDynFlags
-       case () of
-         _ | preInlineUnconditionally dflags env NotTopLevel bndr rhs
-           -> do { tick (PreInlineUnconditionally bndr)
-                 ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
-                  simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
-
-           | isStrictId bndr          -- Includes coercions
-           -> simplExprF (rhs_se `setFloats` env) rhs
-                         (StrictBind bndr bndrs body env cont)
-
-           | otherwise
-           -> ASSERT( not (isTyVar bndr) )
-              do { (env1, bndr1) <- simplNonRecBndr env bndr
-                 ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
-                 ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
-                 ; simplLam env3 bndrs body cont }
+  | ASSERT( isId bndr && not (isJoinId bndr) )
+    preInlineUnconditionally env NotTopLevel bndr rhs
+  = do { tick (PreInlineUnconditionally bndr)
+       ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
+         simplLam (extendIdSubst env bndr (mkContEx rhs_se rhs)) bndrs body cont }
+
+  -- Deal with strict bindings
+  | isStrictId bndr          -- Includes coercions
+  , sm_case_case (getMode env)
+  = simplExprF (rhs_se `setInScopeFromE` env) rhs
+               (StrictBind { sc_bndr = bndr, sc_bndrs = bndrs, sc_body = body
+                           , sc_env = env, sc_cont = cont, sc_dup = NoDup })
+
+  -- Deal with lazy bindings
+  | otherwise
+  = ASSERT( not (isTyVar bndr) )
+    do { (env1, bndr1) <- simplNonRecBndr env bndr
+       ; (env2, bndr2) <- addBndrRules env1 bndr bndr1
+       ; (floats1, env3) <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
+       ; (floats2, expr') <- simplLam env3 bndrs body cont
+       ; return (floats1 `addFloats` floats2, expr') }
+
+------------------
+simplRecE :: SimplEnv
+          -> [(InId, InExpr)]
+          -> InExpr
+          -> SimplCont
+          -> SimplM (SimplFloats, OutExpr)
+
+-- simplRecE is used for
+--  * non-top-level recursive lets in expressions
+simplRecE env pairs body cont
+  = do  { let bndrs = map fst pairs
+        ; MASSERT(all (not . isJoinId) bndrs)
+        ; env1 <- simplRecBndrs env bndrs
+                -- NB: bndrs' don't have unfoldings or rules
+                -- We add them as we go down
+        ; (floats1, env2) <- simplRecBind env1 NotTopLevel Nothing pairs
+        ; (floats2, expr') <- simplExprF env2 body cont
+        ; return (floats1 `addFloats` floats2, expr') }
+
+{- Note [Avoiding exponential behaviour]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+One way in which we can get exponential behaviour is if we simplify a
+big expression, and the re-simplify it -- and then this happens in a
+deeply-nested way.  So we must be jolly careful about re-simplifying
+an expression.  That is why completeNonRecX does not try
+preInlineUnconditionally.
+
+Example:
+  f BIG, where f has a RULE
+Then
+ * We simplify BIG before trying the rule; but the rule does not fire
+ * We inline f = \x. x True
+ * So if we did preInlineUnconditionally we'd re-simplify (BIG True)
+
+However, if BIG has /not/ already been simplified, we'd /like/ to
+simplify BIG True; maybe good things happen.  That is why
+
+* simplLam has
+    - a case for (isSimplified dup), which goes via simplNonRecX, and
+    - a case for the un-simplified case, which goes via simplNonRecE
+
+* We go to some efforts to avoid unnecessarily simplifying ApplyToVal,
+  in at least two places
+    - In simplCast/addCoerce, where we check for isReflCo
+    - In rebuildCall we avoid simplifying arguments before we have to
+      (see Note [Trying rewrite rules])
+
+
+Note [Zap unfolding when beta-reducing]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Lambda-bound variables can have stable unfoldings, such as
+   $j = \x. \b{Unf=Just x}. e
+See Note [Case binders and join points] below; the unfolding for lets
+us optimise e better.  However when we beta-reduce it we want to
+revert to using the actual value, otherwise we can end up in the
+stupid situation of
+          let x = blah in
+          let b{Unf=Just x} = y
+          in ...b...
+Here it'd be far better to drop the unfolding and use the actual RHS.
+
+************************************************************************
+*                                                                      *
+                     Join points
+*                                                                      *
+********************************************************************* -}
+
+simplNonRecJoinPoint :: SimplEnv -> InId -> InExpr
+                     -> InExpr -> SimplCont
+                     -> SimplM (SimplFloats, OutExpr)
+simplNonRecJoinPoint env bndr rhs body cont
+  | ASSERT( isJoinId bndr )
+    preInlineUnconditionally env NotTopLevel bndr rhs
+  = do { tick (PreInlineUnconditionally bndr)
+       ; simplExprF (extendIdSubst env bndr (mkContEx env rhs)) body cont }
+
+   | otherwise
+   = wrapJoinCont env cont $ \ cont ->
+     do { -- We push join_cont into the join RHS and the body;
+          -- and wrap wrap_cont around the whole thing
+        ; let res_ty = contResultType cont
+        ; (env1, bndr1)    <- simplNonRecJoinBndr env res_ty bndr
+        ; (env2, bndr2)    <- addBndrRules env1 bndr bndr1
+        ; (floats1, env3)  <- simplJoinBind env2 cont bndr bndr2 rhs
+        ; (floats2, body') <- simplExprF env3 body cont
+        ; return (floats1 `addFloats` floats2, body') }
+
+
+------------------
+simplRecJoinPoint :: SimplEnv -> [(InId, InExpr)]
+                  -> InExpr -> SimplCont
+                  -> SimplM (SimplFloats, OutExpr)
+simplRecJoinPoint env pairs body cont
+  = wrapJoinCont env cont $ \ cont ->
+    do { let bndrs = map fst pairs
+             res_ty = contResultType cont
+       ; env1 <- simplRecJoinBndrs env res_ty bndrs
+               -- NB: bndrs' don't have unfoldings or rules
+               -- We add them as we go down
+       ; (floats1, env2)  <- simplRecBind env1 NotTopLevel (Just cont) pairs
+       ; (floats2, body') <- simplExprF env2 body cont
+       ; return (floats1 `addFloats` floats2, body') }
+
+--------------------
+wrapJoinCont :: SimplEnv -> SimplCont
+             -> (SimplCont -> SimplM (SimplFloats, OutExpr))
+             -> SimplM (SimplFloats, OutExpr)
+-- Deal with making the continuation duplicable if necessary,
+-- and with the no-case-of-case situation.
+wrapJoinCont env cont thing_inside
+  | contIsStop cont        -- Common case; no need for fancy footwork
+  = thing_inside cont
+
+  | not (sm_case_case (getMode env))
+    -- See Note [Join points wih -fno-case-of-case]
+  = do { (floats1, expr1) <- thing_inside (mkBoringStop (contHoleType cont))
+       ; let (floats2, expr2) = wrapJoinFloatsX floats1 expr1
+       ; (floats3, expr3) <- rebuild (env `setInScopeFromF` floats2) expr2 cont
+       ; return (floats2 `addFloats` floats3, expr3) }
+
+  | otherwise
+    -- Normal case; see Note [Join points and case-of-case]
+  = do { (floats1, cont')  <- mkDupableCont env cont
+       ; (floats2, result) <- thing_inside cont'
+       ; return (floats1 `addFloats` floats2, result) }
+
+
+--------------------
+trimJoinCont :: Id -> Maybe JoinArity -> SimplCont -> SimplCont
+-- Drop outer context from join point invocation (jump)
+-- See Note [Join points and case-of-case]
+
+trimJoinCont _ Nothing cont
+  = cont -- Not a jump
+trimJoinCont var (Just arity) cont
+  = trim arity cont
+  where
+    trim 0 cont@(Stop {})
+      = cont
+    trim 0 cont
+      = mkBoringStop (contResultType cont)
+    trim n cont@(ApplyToVal { sc_cont = k })
+      = cont { sc_cont = trim (n-1) k }
+    trim n cont@(ApplyToTy { sc_cont = k })
+      = cont { sc_cont = trim (n-1) k } -- join arity counts types!
+    trim _ cont
+      = pprPanic "completeCall" $ ppr var $$ ppr cont
+
+
+{- Note [Join points and case-of-case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we perform the case-of-case transform (or otherwise push continuations
+inward), we want to treat join points specially. Since they're always
+tail-called and we want to maintain this invariant, we can do this (for any
+evaluation context E):
+
+  E[join j = e
+    in case ... of
+         A -> jump j 1
+         B -> jump j 2
+         C -> f 3]
+
+    -->
+
+  join j = E[e]
+  in case ... of
+       A -> jump j 1
+       B -> jump j 2
+       C -> E[f 3]
+
+As is evident from the example, there are two components to this behavior:
+
+  1. When entering the RHS of a join point, copy the context inside.
+  2. When a join point is invoked, discard the outer context.
+
+We need to be very careful here to remain consistent---neither part is
+optional!
+
+We need do make the continuation E duplicable (since we are duplicating it)
+with mkDuableCont.
+
+
+Note [Join points wih -fno-case-of-case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose case-of-case is switched off, and we are simplifying
+
+    case (join j x = <j-rhs> in
+          case y of
+             A -> j 1
+             B -> j 2
+             C -> e) of <outer-alts>
+
+Usually, we'd push the outer continuation (case . of <outer-alts>) into
+both the RHS and the body of the join point j.  But since we aren't doing
+case-of-case we may then end up with this totally bogus result
+
+    join x = case <j-rhs> of <outer-alts> in
+    case (case y of
+             A -> j 1
+             B -> j 2
+             C -> e) of <outer-alts>
+
+This would be OK in the language of the paper, but not in GHC: j is no longer
+a join point.  We can only do the "push contination into the RHS of the
+join point j" if we also push the contination right down to the /jumps/ to
+j, so that it can evaporate there.  If we are doing case-of-case, we'll get to
+
+    join x = case <j-rhs> of <outer-alts> in
+    case y of
+      A -> j 1
+      B -> j 2
+      C -> case e of <outer-alts>
+
+which is great.
+
+Bottom line: if case-of-case is off, we must stop pushing the continuation
+inwards altogether at any join point.  Instead simplify the (join ... in ...)
+with a Stop continuation, and wrap the original continuation around the
+outside.  Surprisingly tricky!
+
 
-{-
 ************************************************************************
 *                                                                      *
                      Variables
@@ -1390,53 +1623,57 @@ simplVar env var
   | isCoVar var = return (Coercion (substCoVar env var))
   | otherwise
   = case substId env var of
-        DoneId var1          -> return (Var var1)
-        DoneEx e             -> return e
         ContEx tvs cvs ids e -> simplExpr (setSubstEnv env tvs cvs ids) e
+        DoneId var1          -> return (Var var1)
+        DoneEx e _           -> return e
 
-simplIdF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplEnv, OutExpr)
+simplIdF :: SimplEnv -> InId -> SimplCont -> SimplM (SimplFloats, OutExpr)
 simplIdF env var cont
   = case substId env var of
-        DoneEx e             -> simplExprF (zapSubstEnv env) e cont
-        ContEx tvs cvs ids e -> simplExprF (setSubstEnv env tvs cvs ids) e cont
-        DoneId var1          -> completeCall env var1 cont
-                -- Note [zapSubstEnv]
-                -- The template is already simplified, so don't re-substitute.
-                -- This is VITAL.  Consider
-                --      let x = e in
-                --      let y = \z -> ...x... in
-                --      \ x -> ...y...
-                -- We'll clone the inner \x, adding x->x' in the id_subst
-                -- Then when we inline y, we must *not* replace x by x' in
-                -- the inlined copy!!
+      ContEx tvs cvs ids e -> simplExprF (setSubstEnv env tvs cvs ids) e cont
+                                -- Don't trim; haven't already simplified e,
+                                -- so the cont is not embodied in e
+
+      DoneId var1 -> completeCall env var1 (trimJoinCont var (isJoinId_maybe var1) cont)
+
+      DoneEx e mb_join -> simplExprF (zapSubstEnv env) e (trimJoinCont var mb_join cont)
+              -- Note [zapSubstEnv]
+              -- The template is already simplified, so don't re-substitute.
+              -- This is VITAL.  Consider
+              --      let x = e in
+              --      let y = \z -> ...x... in
+              --      \ x -> ...y...
+              -- We'll clone the inner \x, adding x->x' in the id_subst
+              -- Then when we inline y, we must *not* replace x by x' in
+              -- the inlined copy!!
 
 ---------------------------------------------------------
 --      Dealing with a call site
 
-completeCall :: SimplEnv -> OutId -> SimplCont -> SimplM (SimplEnv, OutExpr)
+completeCall :: SimplEnv -> OutId -> SimplCont -> SimplM (SimplFloats, OutExpr)
 completeCall env var cont
-  = do  {   ------------- Try inlining ----------------
-          dflags <- getDynFlags
-        ; let  (lone_variable, arg_infos, call_cont) = contArgs cont
-               n_val_args = length arg_infos
-               interesting_cont = interestingCallContext call_cont
-               unfolding    = activeUnfolding env var
-               maybe_inline = callSiteInline dflags var unfolding
-                                             lone_variable arg_infos interesting_cont
-        ; case maybe_inline of {
-            Just expr      -- There is an inlining!
-              ->  do { checkedTick (UnfoldingDone var)
-                     ; dump_inline dflags expr cont
-                     ; simplExprF (zapSubstEnv env) expr cont }
-
-            ; Nothing -> do               -- No inlining!
-
-        { rule_base <- getSimplRules
-        ; let info = mkArgInfo var (getRules rule_base var) n_val_args call_cont
-        ; rebuildCall env info cont
-    }}}
+  | Just expr <- callSiteInline dflags var unfolding
+                                lone_variable arg_infos interesting_cont
+  -- Inline the variable's RHS
+  = do { checkedTick (UnfoldingDone var)
+       ; dump_inline expr cont
+       ; simplExprF (zapSubstEnv env) expr cont }
+
+  | otherwise
+  -- Don't inline; instead rebuild the call
+  = do { rule_base <- getSimplRules
+       ; let info = mkArgInfo var (getRules rule_base var)
+                              n_val_args call_cont
+       ; rebuildCall env info cont }
+
   where
-    dump_inline dflags unfolding cont
+    dflags = seDynFlags env
+    (lone_variable, arg_infos, call_cont) = contArgs cont
+    n_val_args       = length arg_infos
+    interesting_cont = interestingCallContext env call_cont
+    unfolding        = activeUnfolding env var
+
+    dump_inline unfolding cont
       | not (dopt Opt_D_dump_inlinings dflags) = return ()
       | not (dopt Opt_D_verbose_core2core dflags)
       = when (isExternalName (idName var)) $
@@ -1451,7 +1688,13 @@ completeCall env var cont
 rebuildCall :: SimplEnv
             -> ArgInfo
             -> SimplCont
-            -> SimplM (SimplEnv, OutExpr)
+            -> SimplM (SimplFloats, OutExpr)
+-- We decided not to inline, so
+--    - simplify the arguments
+--    - try rewrite rules
+--    - and rebuild
+
+---------- Bottoming applications --------------
 rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_strs = [] }) cont
   -- When we run out of strictness args, it means
   -- that the call is definitely bottom; see SimplUtils.mkArgInfo
@@ -1464,16 +1707,40 @@ rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_strs = [] }) con
   -- the continuation, leaving just the bottoming expression.  But the
   -- type might not be right, so we may have to add a coerce.
   | not (contIsTrivial cont)     -- Only do this if there is a non-trivial
-  = return (env, castBottomExpr res cont_ty)  -- contination to discard, else we do it
-  where                                       -- again and again!
+                                 -- continuation to discard, else we do it
+                                 -- again and again!
+  = seqType cont_ty `seq`        -- See Note [Avoiding space leaks in OutType]
+    return (emptyFloats env, castBottomExpr res cont_ty)
+  where
     res     = argInfoExpr fun rev_args
     cont_ty = contResultType cont
 
+---------- Try rewrite RULES --------------
+-- See Note [Trying rewrite rules]
+rebuildCall env info@(ArgInfo { ai_fun = fun, ai_args = rev_args
+                              , ai_rules = Just (nr_wanted, rules) }) cont
+  | nr_wanted == 0 || no_more_args
+  , let info' = info { ai_rules = Nothing }
+  = -- We've accumulated a simplified call in <fun,rev_args>
+    -- so try rewrite rules; see Note [RULEs apply to simplified arguments]
+    -- See also Note [Rules for recursive functions]
+    do { mb_match <- tryRules env rules fun (reverse rev_args) cont
+       ; case mb_match of
+             Just (env', rhs, cont') -> simplExprF env' rhs cont'
+             Nothing                 -> rebuildCall env info' cont }
+  where
+    no_more_args = case cont of
+                      ApplyToTy  {} -> False
+                      ApplyToVal {} -> False
+                      _             -> True
+
+
+---------- Simplify applications and casts --------------
 rebuildCall env info (CastIt co cont)
   = rebuildCall env (addCastTo info co) cont
 
 rebuildCall env info (ApplyToTy { sc_arg_ty = arg_ty, sc_cont = cont })
-  = rebuildCall env (info `addTyArgTo` arg_ty) cont
+  = rebuildCall env (addTyArgTo info arg_ty) cont
 
 rebuildCall env info@(ArgInfo { ai_encl = encl_rules, ai_type = fun_ty
                               , ai_strs = str:strs, ai_discs = disc:discs })
@@ -1482,10 +1749,12 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules, ai_type = fun_ty
   | isSimplified dup_flag     -- See Note [Avoid redundant simplification]
   = rebuildCall env (addValArgTo info' arg) cont
 
-  | str                 -- Strict argument
+  | str         -- Strict argument
+  , sm_case_case (getMode env)
   = -- pprTrace "Strict Arg" (ppr arg $$ ppr (seIdSubst env) $$ ppr (seInScope env)) $
-    simplExprF (arg_se `setFloats` env) arg
-               (StrictArg info' cci cont)
+    simplExprF (arg_se `setInScopeFromE` env) arg
+               (StrictArg { sc_fun = info', sc_cci = cci_strict
+                          , sc_dup = Simplified, sc_cont = cont })
                 -- Note [Shadowing]
 
   | otherwise                           -- Lazy argument
@@ -1493,34 +1762,55 @@ rebuildCall env info@(ArgInfo { ai_encl = encl_rules, ai_type = fun_ty
         -- There is no benefit (unlike in a let-binding), and we'd
         -- have to be very careful about bogus strictness through
         -- floating a demanded let.
-  = do  { arg' <- simplExprC (arg_se `setInScope` env) arg
-                             (mkLazyArgStop (funArgTy fun_ty) cci)
+  = do  { arg' <- simplExprC (arg_se `setInScopeFromE` env) arg
+                             (mkLazyArgStop arg_ty cci_lazy)
         ; rebuildCall env (addValArgTo info' arg') cont }
   where
-    info' = info { ai_strs = strs, ai_discs = discs }
-    cci | encl_rules = RuleArgCtxt
-        | disc > 0   = DiscArgCtxt  -- Be keener here
-        | otherwise  = BoringCtxt   -- Nothing interesting
+    info'  = info { ai_strs = strs, ai_discs = discs }
+    arg_ty = funArgTy fun_ty
+
+    -- Use this for lazy arguments
+    cci_lazy | encl_rules = RuleArgCtxt
+             | disc > 0   = DiscArgCtxt  -- Be keener here
+             | otherwise  = BoringCtxt   -- Nothing interesting
+
+    -- ..and this for strict arguments
+    cci_strict | encl_rules = RuleArgCtxt
+               | disc > 0   = DiscArgCtxt
+               | otherwise  = RhsCtxt
+      -- Why RhsCtxt?  if we see f (g x) (h x), and f is strict, we
+      -- want to be a bit more eager to inline g, because it may
+      -- expose an eval (on x perhaps) that can be eliminated or
+      -- shared. I saw this in nofib 'boyer2', RewriteFuns.onewayunify1
+      -- It's worth an 18% improvement in allocation for this
+      -- particular benchmark; 5% on 'mate' and 1.3% on 'multiplier'
+
+---------- No further useful info, revert to generic rebuild ------------
+rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args }) cont
+  = rebuild env (argInfoExpr fun rev_args) cont
+
+{- Note [Trying rewrite rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider an application (f e1 e2 e3) where the e1,e2,e3 are not yet
+simplified.  We want to simplify enough arguments to allow the rules
+to apply, but it's more efficient to avoid simplifying e2,e3 if e1 alone
+is sufficient.  Example: class ops
+   (+) dNumInt e2 e3
+If we rewrite ((+) dNumInt) to plusInt, we can take advantage of the
+latter's strictness when simplifying e2, e3.  Moreover, suppose we have
+  RULE  f Int = \x. x True
+
+Then given (f Int e1) we rewrite to
+   (\x. x True) e1
+without simplifying e1.  Now we can inline x into its unique call site,
+and absorb the True into it all in the same pass.  If we simplified
+e1 first, we couldn't do that; see Note [Avoiding exponential behaviour].
+
+So we try to apply rules if either
+  (a) no_more_args: we've run out of argument that the rules can "see"
+  (b) nr_wanted: none of the rules wants any more arguments
 
-rebuildCall env (ArgInfo { ai_fun = fun, ai_args = rev_args, ai_rules = rules }) cont
-  | null rules
-  = rebuild env (argInfoExpr fun rev_args) cont      -- No rules, common case
 
-  | otherwise
-  = do {  -- We've accumulated a simplified call in <fun,rev_args>
-          -- so try rewrite rules; see Note [RULEs apply to simplified arguments]
-          -- See also Note [Rules for recursive functions]
-        ; let env' = zapSubstEnv env  -- See Note [zapSubstEnv];
-                                      -- and NB that 'rev_args' are all fully simplified
-        ; mb_rule <- tryRules env' rules fun (reverse rev_args) cont
-        ; case mb_rule of {
-             Just (rule_rhs, cont') -> simplExprF env' rule_rhs cont'
-
-                 -- Rules don't match
-           ; Nothing -> rebuild env (argInfoExpr fun rev_args) cont      -- No rules
-    } }
-
-{-
 Note [RULES apply to simplified arguments]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's very desirable to try RULES once the arguments have been simplified, because
@@ -1532,7 +1822,7 @@ Then we want to rewrite (g (h x)) to (k x) and only then try f's rules. If
 we match f's rules against the un-simplified RHS, it won't match.  This
 makes a particularly big difference when superclass selectors are involved:
         op ($p1 ($p2 (df d)))
-We want all this to unravel in one sweeep.
+We want all this to unravel in one sweep.
 
 Note [Avoid redundant simplification]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1576,20 +1866,20 @@ all this at once is TOO HARD!
 -}
 
 tryRules :: SimplEnv -> [CoreRule]
-         -> Id -> [ArgSpec] -> SimplCont
-         -> SimplM (Maybe (CoreExpr, SimplCont))
--- The SimplEnv already has zapSubstEnv applied to it
+         -> Id -> [ArgSpec]
+         -> SimplCont
+         -> SimplM (Maybe (SimplEnv, CoreExpr, SimplCont))
 
 tryRules env rules fn args call_cont
   | null rules
   = return Nothing
+
 {- Disabled until we fix #8326
   | fn `hasKey` tagToEnumKey   -- See Note [Optimising tagToEnum#]
   , [_type_arg, val_arg] <- args
   , Select dup bndr ((_,[],rhs1) : rest_alts) se cont <- call_cont
   , isDeadBinder bndr
-  = do { dflags <- getDynFlags
-       ; let enum_to_tag :: CoreAlt -> CoreAlt
+  = do { let enum_to_tag :: CoreAlt -> CoreAlt
                 -- Takes   K -> e  into   tagK# -> e
                 -- where tagK# is the tag of constructor K
              enum_to_tag (DataAlt con, [], rhs)
@@ -1604,31 +1894,61 @@ tryRules env rules fn args call_cont
                  -- The binder is dead, but should have the right type
       ; return (Just (val_arg, Select dup new_bndr new_alts se cont)) }
 -}
-  | otherwise
-  = do { dflags <- getDynFlags
-       ; case lookupRule dflags (getUnfoldingInRuleMatch env) (activeRule env)
-                         fn (argInfoAppArgs args) rules of {
-           Nothing               -> return Nothing ;   -- No rule matches
-           Just (rule, rule_rhs) ->
-             do { checkedTick (RuleFired (ru_name rule))
-                ; let cont' = pushSimplifiedArgs env
-                                                 (drop (ruleArity rule) args)
-                                                 call_cont
-                      -- (ruleArity rule) says how many args the rule consumed
-                ; dump dflags rule rule_rhs
-                ; return (Just (rule_rhs, cont')) }}}
+
+  | Just (rule, rule_rhs) <- lookupRule dflags (getUnfoldingInRuleMatch env)
+                                        (activeRule env) fn
+                                        (argInfoAppArgs args) rules
+  -- Fire a rule for the function
+  = do { checkedTick (RuleFired (ruleName rule))
+       ; let cont' = pushSimplifiedArgs zapped_env
+                                        (drop (ruleArity rule) args)
+                                        call_cont
+                     -- (ruleArity rule) says how
+                     -- many args the rule consumed
+
+             occ_anald_rhs = occurAnalyseExpr rule_rhs
+                 -- See Note [Occurrence-analyse after rule firing]
+       ; dump rule rule_rhs
+       ; return (Just (zapped_env, occ_anald_rhs, cont')) }
+            -- The occ_anald_rhs and cont' are all Out things
+            -- hence zapping the environment
+
+  | otherwise  -- No rule fires
+  = do { nodump  -- This ensures that an empty file is written
+       ; return Nothing }
+
   where
-    dump dflags rule rule_rhs
+    dflags     = seDynFlags env
+    zapped_env = zapSubstEnv env  -- See Note [zapSubstEnv]
+
+    printRuleModule rule
+      = parens (maybe (text "BUILTIN")
+                      (pprModuleName . moduleName)
+                      (ruleModule rule))
+
+    dump rule rule_rhs
       | dopt Opt_D_dump_rule_rewrites dflags
       = log_rule dflags Opt_D_dump_rule_rewrites "Rule fired" $ vcat
-          [ text "Rule:" <+> ftext (ru_name rule)
+          [ text "Rule:" <+> ftext (ruleName rule)
+          , text "Module:" <+>  printRuleModule rule
           , text "Before:" <+> hang (ppr fn) 2 (sep (map ppr args))
           , text "After: " <+> pprCoreExpr rule_rhs
           , text "Cont:  " <+> ppr call_cont ]
 
       | dopt Opt_D_dump_rule_firings dflags
       = log_rule dflags Opt_D_dump_rule_firings "Rule fired:" $
-          ftext (ru_name rule)
+          ftext (ruleName rule)
+            <+> printRuleModule rule
+
+      | otherwise
+      = return ()
+
+    nodump
+      | dopt Opt_D_dump_rule_rewrites dflags
+      = liftIO $ dumpSDoc dflags alwaysQualify Opt_D_dump_rule_rewrites "" empty
+
+      | dopt Opt_D_dump_rule_firings dflags
+      = liftIO $ dumpSDoc dflags alwaysQualify Opt_D_dump_rule_firings "" empty
 
       | otherwise
       = return ()
@@ -1637,7 +1957,105 @@ tryRules env rules fn args call_cont
       = liftIO . dumpSDoc dflags alwaysQualify flag "" $
                    sep [text hdr, nest 4 details]
 
-{-
+trySeqRules :: SimplEnv
+            -> OutExpr -> InExpr   -- Scrutinee and RHS
+            -> SimplCont
+            -> SimplM (Maybe (SimplEnv, CoreExpr, SimplCont))
+-- See Note [User-defined RULES for seq]
+trySeqRules in_env scrut rhs cont
+  = do { rule_base <- getSimplRules
+       ; tryRules in_env (getRules rule_base seqId) seqId out_args rule_cont }
+  where
+    no_cast_scrut = drop_casts scrut
+    scrut_ty  = exprType no_cast_scrut
+    seq_id_ty = idType seqId
+    rhs_ty    = substTy in_env (exprType rhs)
+    out_args  = [ TyArg { as_arg_ty  = scrut_ty
+                        , as_hole_ty = seq_id_ty }
+                , TyArg { as_arg_ty  = rhs_ty
+                       , as_hole_ty  = piResultTy seq_id_ty scrut_ty }
+                , ValArg no_cast_scrut]
+    rule_cont = ApplyToVal { sc_dup = NoDup, sc_arg = rhs
+                           , sc_env = in_env, sc_cont = cont }
+    -- Lazily evaluated, so we don't do most of this
+
+    drop_casts (Cast e _) = drop_casts e
+    drop_casts e          = e
+
+{- Note [User-defined RULES for seq]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given
+   case (scrut |> co) of _ -> rhs
+look for rules that match the expression
+   seq @t1 @t2 scrut
+where scrut :: t1
+      rhs   :: t2
+
+If you find a match, rewrite it, and apply to 'rhs'.
+
+Notice that we can simply drop casts on the fly here, which
+makes it more likely that a rule will match.
+
+See Note [User-defined RULES for seq] in MkId.
+
+Note [Occurrence-analyse after rule firing]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+After firing a rule, we occurrence-analyse the instantiated RHS before
+simplifying it.  Usually this doesn't make much difference, but it can
+be huge.  Here's an example (simplCore/should_compile/T7785)
+
+  map f (map f (map f xs)
+
+= -- Use build/fold form of map, twice
+  map f (build (\cn. foldr (mapFB c f) n
+                           (build (\cn. foldr (mapFB c f) n xs))))
+
+= -- Apply fold/build rule
+  map f (build (\cn. (\cn. foldr (mapFB c f) n xs) (mapFB c f) n))
+
+= -- Beta-reduce
+  -- Alas we have no occurrence-analysed, so we don't know
+  -- that c is used exactly once
+  map f (build (\cn. let c1 = mapFB c f in
+                     foldr (mapFB c1 f) n xs))
+
+= -- Use mapFB rule:   mapFB (mapFB c f) g = mapFB c (f.g)
+  -- We can do this because (mapFB c n) is a PAP and hence expandable
+  map f (build (\cn. let c1 = mapFB c n in
+                     foldr (mapFB c (f.f)) n x))
+
+This is not too bad.  But now do the same with the outer map, and
+we get another use of mapFB, and t can interact with /both/ remaining
+mapFB calls in the above expression.  This is stupid because actually
+that 'c1' binding is dead.  The outer map introduces another c2. If
+there is a deep stack of maps we get lots of dead bindings, and lots
+of redundant work as we repeatedly simplify the result of firing rules.
+
+The easy thing to do is simply to occurrence analyse the result of
+the rule firing.  Note that this occ-anals not only the RHS of the
+rule, but also the function arguments, which by now are OutExprs.
+E.g.
+      RULE f (g x) = x+1
+
+Call   f (g BIG)  -->   (\x. x+1) BIG
+
+The rule binders are lambda-bound and applied to the OutExpr arguments
+(here BIG) which lack all internal occurrence info.
+
+Is this inefficient?  Not really: we are about to walk over the result
+of the rule firing to simplify it, so occurrence analysis is at most
+a constant factor.
+
+Possible improvement: occ-anal the rules when putting them in the
+database; and in the simplifier just occ-anal the OutExpr arguments.
+But that's more complicated and the rule RHS is usually tiny; so I'm
+just doing the simple thing.
+
+Historical note: previously we did occ-anal the rules in Rule.hs,
+but failed to occ-anal the OutExpr arguments, which led to the
+nasty performance problem described above.
+
+
 Note [Optimising tagToEnum#]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we have an enumeration data type:
@@ -1718,41 +2136,49 @@ to just
 This particular example shows up in default methods for
 comparison operations (e.g. in (>=) for Int.Int32)
 
-Note [Case elimination: lifted case]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If a case over a lifted type has a single alternative, and is being used
-as a strict 'let' (all isDeadBinder bndrs), we may want to do this
-transformation:
+Note [Case to let transformation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If a case over a lifted type has a single alternative, and is being
+used as a strict 'let' (all isDeadBinder bndrs), we may want to do
+this transformation:
 
     case e of r       ===>   let r = e in ...r...
       _ -> ...r...
 
-        (a) 'e' is already evaluated (it may so if e is a variable)
-            Specifically we check (exprIsHNF e).  In this case
-            we can just allocate the WHNF directly with a let.
-or
-        (b) 'x' is not used at all and e is ok-for-speculation
-             The ok-for-spec bit checks that we don't lose any
-             exceptions or divergence.
-
-             NB: it'd be *sound* to switch from case to let if the
-             scrutinee was not yet WHNF but was guaranteed to
-             converge; but sticking with case means we won't build a
-             thunk
+We treat the unlifted and lifted cases separately:
+
+* Unlifted case: 'e' satisfies exprOkForSpeculation
+  (ok-for-spec is needed to satisfy the let/app invariant).
+  This turns     case a +# b of r -> ...r...
+  into           let r = a +# b in ...r...
+  and thence     .....(a +# b)....
+
+  However, if we have
+      case indexArray# a i of r -> ...r...
+  we might like to do the same, and inline the (indexArray# a i).
+  But indexArray# is not okForSpeculation, so we don't build a let
+  in rebuildCase (lest it get floated *out*), so the inlining doesn't
+  happen either.  Annoying.
+
+* Lifted case: we need to be sure that the expression is already
+  evaluated (exprIsHNF).  If it's not already evaluated
+      - we risk losing exceptions, divergence or
+        user-specified thunk-forcing
+      - even if 'e' is guaranteed to converge, we don't want to
+        create a thunk (call by need) instead of evaluating it
+        right away (call by value)
+
+  However, we can turn the case into a /strict/ let if the 'r' is
+  used strictly in the body.  Then we won't lose divergence; and
+  we won't build a thunk because the let is strict.
+  See also Note [Eliminating redundant seqs]
+
+  NB: absentError satisfies exprIsHNF: see Note [aBSENT_ERROR_ID] in MkCore.
+  We want to turn
+     case (absentError "foo") of r -> ...MkT r...
+  into
+     let r = absentError "foo" in ...MkT r...
 
-or
-        (c) 'x' is used strictly in the body, and 'e' is a variable
-            Then we can just substitute 'e' for 'x' in the body.
-            See Note [Eliminating redundant seqs]
-
-For (b), the "not used at all" test is important.  Consider
-   case (case a ># b of { True -> (p,q); False -> (q,p) }) of
-     r -> blah
-The scrutinee is ok-for-speculation (it looks inside cases), but we do
-not want to transform to
-   let r = case a ># b of { True -> (p,q); False -> (q,p) }
-   in blah
-because that builds an unnecessary thunk.
 
 Note [Eliminating redundant seqs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1791,23 +2217,6 @@ Just for reference, the original code (added Jan 13) looked like this:
 an eval'd function] in CoreUtils.)
 
 
-Note [Case elimination: unlifted case]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   case a +# b of r -> ...r...
-Then we do case-elimination (to make a let) followed by inlining,
-to get
-        .....(a +# b)....
-If we have
-   case indexArray# a i of r -> ...r...
-we might like to do the same, and inline the (indexArray# a i).
-But indexArray# is not okForSpeculation, so we don't build a let
-in rebuildCase (lest it get floated *out*), so the inlining doesn't
-happen either.
-
-This really isn't a big deal I think. The let can be
-
-
 Further notes about case elimination
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider:       test :: Integer -> IO ()
@@ -1857,7 +2266,7 @@ rebuildCase, reallyRebuildCase
    -> InId             -- Case binder
    -> [InAlt]          -- Alternatives (inceasing order)
    -> SimplCont
-   -> SimplM (SimplEnv, OutExpr)
+   -> SimplM (SimplFloats, OutExpr)
 
 --------------------------------------------------
 --      1. Eliminate the case if there's a known constructor
@@ -1884,10 +2293,11 @@ rebuildCase env scrut case_bndr alts cont
         }
   where
     simple_rhs bs rhs = ASSERT( null bs )
-                        do { env' <- simplNonRecX env case_bndr scrut
+                        do { (floats1, env') <- simplNonRecX env case_bndr scrut
                                -- scrut is a constructor application,
                                -- hence satisfies let/app invariant
-                           ; simplExprF env' rhs cont }
+                           ; (floats2, expr') <- simplExprF env' rhs cont
+                           ; return (floats1 `addFloats` floats2, expr') }
 
 
 --------------------------------------------------
@@ -1915,40 +2325,28 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
   --      a) it binds only the case-binder
   --      b) unlifted case: the scrutinee is ok-for-speculation
   --           lifted case: the scrutinee is in HNF (or will later be demanded)
+  -- See Note [Case to let transformation]
   | all_dead_bndrs
-  , if is_unlifted
-    then exprOkForSpeculation scrut  -- See Note [Case elimination: unlifted case]
-    else exprIsHNF scrut             -- See Note [Case elimination: lifted case]
-      || scrut_is_demanded_var scrut
+  , if isUnliftedType (idType case_bndr)
+    then exprOkForSpeculation scrut
+    else exprIsHNF scrut || scrut_is_demanded_var scrut
   = do { tick (CaseElim case_bndr)
-       ; env' <- simplNonRecX env case_bndr scrut
-       ; simplExprF env' rhs cont }
+       ; (floats1, env') <- simplNonRecX env case_bndr scrut
+       ; (floats2, expr') <- simplExprF env' rhs cont
+       ; return (floats1 `addFloats` floats2, expr') }
 
   -- 2c. Try the seq rules if
   --     a) it binds only the case binder
   --     b) a rule for seq applies
   -- See Note [User-defined RULES for seq] in MkId
   | is_plain_seq
-  = do { let rhs' = substExpr (text "rebuild-case") env rhs
-             env' = zapSubstEnv env
-             scrut_ty = substTy env (idType case_bndr)
-             out_args = [ TyArg { as_arg_ty  = scrut_ty
-                                , as_hole_ty = seq_id_ty }
-                        , TyArg { as_arg_ty  = exprType rhs'
-                                , as_hole_ty = applyTy seq_id_ty scrut_ty }
-                        , ValArg scrut, ValArg rhs']
-                      -- Lazily evaluated, so we don't do most of this
-
-       ; rule_base <- getSimplRules
-       ; mb_rule <- tryRules env' (getRules rule_base seqId) seqId out_args cont
+  = do { mb_rule <- trySeqRules env scrut rhs cont
        ; case mb_rule of
-           Just (rule_rhs, cont') -> simplExprF env' rule_rhs cont'
-           Nothing                -> reallyRebuildCase env scrut case_bndr alts cont }
+           Just (env', rule_rhs, cont') -> simplExprF env' rule_rhs cont'
+           Nothing                      -> reallyRebuildCase env scrut case_bndr alts cont }
   where
-    is_unlifted        = isUnLiftedType (idType case_bndr)
-    all_dead_bndrs     = all isDeadBinder bndrs       -- bndrs are [InId]
-    is_plain_seq       = all_dead_bndrs && isDeadBinder case_bndr -- Evaluation *only* for effect
-    seq_id_ty          = idType seqId
+    all_dead_bndrs = all isDeadBinder bndrs       -- bndrs are [InId]
+    is_plain_seq   = all_dead_bndrs && isDeadBinder case_bndr -- Evaluation *only* for effect
 
     scrut_is_demanded_var :: CoreExpr -> Bool
             -- See Note [Eliminating redundant seqs]
@@ -1965,21 +2363,16 @@ rebuildCase env scrut case_bndr alts cont
 --------------------------------------------------
 
 reallyRebuildCase env scrut case_bndr alts cont
-  = do  {       -- Prepare the continuation;
-                -- The new subst_env is in place
-          (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont
-
-        -- Simplify the alternatives
-        ; (scrut', case_bndr', alts') <- simplAlts env' scrut case_bndr alts dup_cont
-
-        ; dflags <- getDynFlags
-        ; let alts_ty' = contResultType dup_cont
-        ; case_expr <- mkCase dflags scrut' case_bndr' alts_ty' alts'
+  | not (sm_case_case (getMode env))
+  = do { case_expr <- simplAlts env scrut case_bndr alts
+                                (mkBoringStop (contHoleType cont))
+       ; rebuild env case_expr cont }
 
-        -- Notice that rebuild gets the in-scope set from env', not alt_env
-        -- (which in any case is only build in simplAlts)
-        -- The case binder *not* scope over the whole returned case-expression
-        ; rebuild env' case_expr nodup_cont }
+  | otherwise
+  = do { (floats, cont') <- mkDupableCaseCont env alts cont
+       ; case_expr <- simplAlts (env `setInScopeFromF` floats)
+                                scrut case_bndr alts cont'
+       ; return (floats, case_expr) }
 
 {-
 simplCaseBinder checks whether the scrutinee is a variable, v.  If so,
@@ -1989,7 +2382,7 @@ inlined.
 
 Historical note: we use to do the "case binder swap" in the Simplifier
 so there were additional complications if the scrutinee was a variable.
-Now the binder-swap stuff is done in the occurrence analyer; see
+Now the binder-swap stuff is done in the occurrence analyser; see
 OccurAnal Note [Binder swap].
 
 Note [knownCon occ info]
@@ -2018,37 +2411,33 @@ Consider
         type family F :: * -> *
         type instance F Int = Int
 
-        ... case e of x { DEFAULT -> rhs } ...
-
-where x::F Int.  Then we'd like to rewrite (F Int) to Int, getting
-
-        case e `cast` co of x'::Int
+We'd like to transform
+        case e of (x :: F Int) { DEFAULT -> rhs }
+===>
+        case e `cast` co of (x'::Int)
            I# x# -> let x = x' `cast` sym co
                     in rhs
 
-so that 'rhs' can take advantage of the form of x'.
-
-Notice that Note [Case of cast] (in OccurAnal) may then apply to the result.
-
-Nota Bene: We only do the [Improving seq] transformation if the
-case binder 'x' is actually used in the rhs; that is, if the case
-is *not* a *pure* seq.
-  a) There is no point in adding the cast to a pure seq.
-  b) There is a good reason not to: doing so would interfere
-     with seq rules (Note [Built-in RULES for seq] in MkId).
-     In particular, this [Improving seq] thing *adds* a cast
-     while [Built-in RULES for seq] *removes* one, so they
-     just flip-flop.
-
-You might worry about
-   case v of x { __DEFAULT ->
-      ... case (v `cast` co) of y { I# -> ... }}
-This is a pure seq (since x is unused), so [Improving seq] won't happen.
-But it's ok: the simplifier will replace 'v' by 'x' in the rhs to get
-   case v of x { __DEFAULT ->
-      ... case (x `cast` co) of y { I# -> ... }}
-Now the outer case is not a pure seq, so [Improving seq] will happen,
-and then the inner case will disappear.
+so that 'rhs' can take advantage of the form of x'.  Notice that Note
+[Case of cast] (in OccurAnal) may then apply to the result.
+
+We'd also like to eliminate empty types (Trac #13468). So if
+
+    data Void
+    type instance F Bool = Void
+
+then we'd like to transform
+        case (x :: F Bool) of { _ -> error "urk" }
+===>
+        case (x |> co) of (x' :: Void) of {}
+
+Nota Bene: we used to have a built-in rule for 'seq' that dropped
+casts, so that
+    case (x |> co) of { _ -> blah }
+dropped the cast; in order to improve the chances of trySeqRules
+firing.  But that works in the /opposite/ direction to Note [Improving
+seq] so there's a danger of flip/flopping.  Better to make trySeqRules
+insensitive to the cast, which is now is.
 
 The need for [Improving seq] showed up in Roman's experiments.  Example:
   foo :: F Int -> Int -> Int
@@ -2065,23 +2454,21 @@ robust here.  (Otherwise, there's a danger that we'll simply drop the
 -}
 
 simplAlts :: SimplEnv
-          -> OutExpr
-          -> InId                       -- Case binder
-          -> [InAlt]                    -- Non-empty
+          -> OutExpr         -- Scrutinee
+          -> InId            -- Case binder
+          -> [InAlt]         -- Non-empty
           -> SimplCont
-          -> SimplM (OutExpr, OutId, [OutAlt])  -- Includes the continuation
--- Like simplExpr, this just returns the simplified alternatives;
--- it does not return an environment
--- The returned alternatives can be empty, none are possible
-
-simplAlts env scrut case_bndr alts cont'
-  = do  { let env0 = zapFloats env
+          -> SimplM OutExpr  -- Returns the complete simplified case expression
 
-        ; (env1, case_bndr1) <- simplBinder env0 case_bndr
+simplAlts env0 scrut case_bndr alts cont'
+  = do  { (env1, case_bndr1) <- simplBinder env0 case_bndr
+        ; let case_bndr2 = case_bndr1 `setIdUnfolding` evaldUnfolding
+              env2       = modifyInScope env1 case_bndr2
+              -- See Note [Case binder evaluated-ness]
 
         ; fam_envs <- getFamEnvs
-        ; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env1 scrut
-                                                       case_bndr case_bndr1 alts
+        ; (alt_env', scrut', case_bndr') <- improveSeq fam_envs env2 scrut
+                                                       case_bndr case_bndr2 alts
 
         ; (imposs_deflt_cons, in_alts) <- prepareAlts scrut' case_bndr' alts
           -- NB: it's possible that the returned in_alts is empty: this is handled
@@ -2089,7 +2476,11 @@ simplAlts env scrut case_bndr alts cont'
 
         ; alts' <- mapM (simplAlt alt_env' (Just scrut') imposs_deflt_cons case_bndr' cont') in_alts
         ; -- pprTrace "simplAlts" (ppr case_bndr $$ ppr alts_ty $$ ppr alts_ty' $$ ppr alts $$ ppr cont') $
-          return (scrut', case_bndr', alts') }
+
+        ; let alts_ty' = contResultType cont'
+        -- See Note [Avoiding space leaks in OutType]
+        ; seqType alts_ty' `seq`
+          mkCase (seDynFlags env0) scrut' case_bndr' alts_ty' alts' }
 
 
 ------------------------------------
@@ -2098,10 +2489,9 @@ improveSeq :: (FamInstEnv, FamInstEnv) -> SimplEnv
            -> SimplM (SimplEnv, OutExpr, OutId)
 -- Note [Improving seq]
 improveSeq fam_envs env scrut case_bndr case_bndr1 [(DEFAULT,_,_)]
-  | not (isDeadBinder case_bndr) -- Not a pure seq!  See Note [Improving seq]
-  , Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
+  | Just (co, ty2) <- topNormaliseType_maybe fam_envs (idType case_bndr1)
   = do { case_bndr2 <- newId (fsLit "nt") ty2
-        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co)
+        ; let rhs  = DoneEx (Var case_bndr2 `Cast` mkSymCo co) Nothing
               env2 = extendIdSubst env case_bndr rhs
         ; return (env2, scrut `Cast` co, case_bndr2) }
 
@@ -2158,36 +2548,45 @@ simplAlt env scrut' _ case_bndr' cont' (DataAlt con, vs, rhs)
         --
         -- We really must record that b is already evaluated so that we don't
         -- go and re-evaluate it when constructing the result.
-        -- See Note [Data-con worker strictness] in MkId.lhs
+        -- See Note [Data-con worker strictness] in MkId.hs
     add_evals the_strs
         = go vs the_strs
         where
           go [] [] = []
           go (v:vs') strs | isTyVar v = v : go vs' strs
-          go (v:vs') (str:strs)
-            | isMarkedStrict str = evald_v  : go vs' strs
-            | otherwise          = zapped_v : go vs' strs
+          go (v:vs') (str:strs) = zap str v : go vs' strs
+          go _ _ = pprPanic "cat_evals"
+                    (ppr con $$
+                     ppr vs  $$
+                     ppr_with_length the_strs $$
+                     ppr_with_length (dataConRepArgTys con) $$
+                     ppr_with_length (dataConRepStrictness con))
             where
-              zapped_v = zapIdOccInfo v   -- See Note [Case alternative occ info]
-              evald_v  = zapped_v `setIdUnfolding` evaldUnfolding
-          go _ _ = pprPanic "cat_evals" (ppr con $$ ppr vs $$ ppr the_strs)
+              ppr_with_length list
+                = ppr list <+> parens (text "length =" <+> ppr (length list))
+                                    -- NB: If this panic triggers, note that
+                                    -- NoStrictnessMark doesn't print!
 
+          zap str v = setCaseBndrEvald str $ -- Add eval'dness info
+                      zapIdOccInfo v         -- And kill occ info;
+                                             -- see Note [Case alternative occ info]
 
 addAltUnfoldings :: SimplEnv -> Maybe OutExpr -> OutId -> OutExpr -> SimplM SimplEnv
 addAltUnfoldings env scrut case_bndr con_app
-  = do { dflags <- getDynFlags
-       ; let con_app_unf = mkSimpleUnfolding dflags con_app
+  = do { let con_app_unf = mk_simple_unf con_app
              env1 = addBinderUnfolding env case_bndr con_app_unf
 
              -- See Note [Add unfolding for scrutinee]
              env2 = case scrut of
                       Just (Var v)           -> addBinderUnfolding env1 v con_app_unf
                       Just (Cast (Var v) co) -> addBinderUnfolding env1 v $
-                                                mkSimpleUnfolding dflags (Cast con_app (mkSymCo co))
+                                                mk_simple_unf (Cast con_app (mkSymCo co))
                       _                      -> env1
 
        ; traceSmpl "addAltUnf" (vcat [ppr case_bndr <+> ppr scrut, ppr con_app])
        ; return env2 }
+  where
+    mk_simple_unf = mkSimpleUnfolding (seDynFlags env)
 
 addBinderUnfolding :: SimplEnv -> Id -> Unfolding -> SimplEnv
 addBinderUnfolding env bndr unf
@@ -2207,12 +2606,27 @@ zapBndrOccInfo keep_occ_info pat_id
   | keep_occ_info = pat_id
   | otherwise     = zapIdOccInfo pat_id
 
-{-
+{- Note [Case binder evaluated-ness]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We pin on a (OtherCon []) unfolding to the case-binder of a Case,
+even though it'll be over-ridden in every case alternative with a more
+informative unfolding.  Why?  Because suppose a later, less clever, pass
+simply replaces all occurrences of the case binder with the binder itself;
+then Lint may complain about the let/app invariant.  Example
+    case e of b { DEFAULT -> let v = reallyUnsafePtrEq# b y in ....
+                ; K       -> blah }
+
+The let/app invariant requires that y is evaluated in the call to
+reallyUnsafePtrEq#, which it is.  But we still want that to be true if we
+propagate binders to occurrences.
+
+This showed up in Trac #13027.
+
 Note [Add unfolding for scrutinee]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In general it's unlikely that a variable scrutinee will appear
 in the case alternatives   case x of { ...x unlikely to appear... }
-because the binder-swap in OccAnal has got rid of all such occcurrences
+because the binder-swap in OccAnal has got rid of all such occurrences
 See Note [Binder swap] in OccAnal.
 
 BUT it is still VERY IMPORTANT to add a suitable unfolding for a
@@ -2268,22 +2682,27 @@ knownCon :: SimplEnv
          -> DataCon -> [OutType] -> [OutExpr]   -- The scrutinee (in pieces)
          -> InId -> [InBndr] -> InExpr          -- The alternative
          -> SimplCont
-         -> SimplM (SimplEnv, OutExpr)
+         -> SimplM (SimplFloats, OutExpr)
 
 knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
-  = do  { env'  <- bind_args env bs dc_args
-        ; env'' <- bind_case_bndr env'
-        ; simplExprF env'' rhs cont }
+  = do  { (floats1, env1)  <- bind_args env bs dc_args
+        ; (floats2, env2) <- bind_case_bndr env1
+        ; (floats3, expr') <- simplExprF env2 rhs cont
+        ; return (floats1 `addFloats` floats2 `addFloats` floats3, expr') }
   where
     zap_occ = zapBndrOccInfo (isDeadBinder bndr)    -- bndr is an InId
 
                   -- Ugh!
-    bind_args env' [] _  = return env'
+    bind_args env' [] _  = return (emptyFloats env', env')
 
     bind_args env' (b:bs') (Type ty : args)
       = ASSERT( isTyVar b )
         bind_args (extendTvSubst env' b ty) bs' args
 
+    bind_args env' (b:bs') (Coercion co : args)
+      = ASSERT( isCoVar b )
+        bind_args (extendCvSubst env' b co) bs' args
+
     bind_args env' (b:bs') (arg : args)
       = ASSERT( isId b )
         do { let b' = zap_occ b
@@ -2292,8 +2711,9 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
              -- it via postInlineUnconditionally.
              -- Nevertheless we must keep it if the case-binder is alive,
              -- because it may be used in the con_app.  See Note [knownCon occ info]
-           ; env'' <- simplNonRecX env' b' arg  -- arg satisfies let/app invariant
-           ; bind_args env'' bs' args }
+           ; (floats1, env2) <- simplNonRecX env' b' arg  -- arg satisfies let/app invariant
+           ; (floats2, env3)  <- bind_args env2 bs' args
+           ; return (floats1 `addFloats` floats2, env3) }
 
     bind_args _ _ _ =
       pprPanic "bind_args" $ ppr dc $$ ppr bs $$ ppr dc_args $$
@@ -2307,8 +2727,9 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
        -- about duplicating the arg redexes; in that case, make
        -- a new con-app from the args
     bind_case_bndr env
-      | isDeadBinder bndr   = return env
-      | exprIsTrivial scrut = return (extendIdSubst env bndr (DoneEx scrut))
+      | isDeadBinder bndr   = return (emptyFloats env, env)
+      | exprIsTrivial scrut = return (emptyFloats env
+                                     , extendIdSubst env bndr (DoneEx scrut Nothing))
       | otherwise           = do { dc_args <- mapM (simplVar env) bs
                                          -- dc_ty_args are aready OutTypes,
                                          -- but bs are InBndrs
@@ -2318,15 +2739,19 @@ knownCon env scrut dc dc_ty_args dc_args bndr bs rhs cont
                                  ; simplNonRecX env bndr con_app }
 
 -------------------
-missingAlt :: SimplEnv -> Id -> [InAlt] -> SimplCont -> SimplM (SimplEnv, OutExpr)
+missingAlt :: SimplEnv -> Id -> [InAlt] -> SimplCont
+           -> SimplM (SimplFloats, OutExpr)
                 -- This isn't strictly an error, although it is unusual.
-                -- It's possible that the simplifer might "see" that
+                -- It's possible that the simplifier might "see" that
                 -- an inner case has no accessible alternatives before
                 -- it "sees" that the entire branch of an outer case is
                 -- inaccessible.  So we simply put an error case here instead.
 missingAlt env case_bndr _ cont
-  = WARN( True, ptext (sLit "missingAlt") <+> ppr case_bndr )
-    return (env, mkImpossibleExpr (contResultType cont))
+  = WARN( True, text "missingAlt" <+> ppr case_bndr )
+    -- See Note [Avoiding space leaks in OutType]
+    let cont_ty = contResultType cont
+    in seqType cont_ty `seq`
+       return (emptyFloats env, mkImpossibleExpr cont_ty)
 
 {-
 ************************************************************************
@@ -2334,42 +2759,29 @@ missingAlt env case_bndr _ cont
 \subsection{Duplicating continuations}
 *                                                                      *
 ************************************************************************
--}
-
-prepareCaseCont :: SimplEnv
-                -> [InAlt] -> SimplCont
-                -> SimplM (SimplEnv,
-                           SimplCont,   -- Dupable part
-                           SimplCont)   -- Non-dupable part
--- We are considering
---     K[case _ of { p1 -> r1; ...; pn -> rn }]
--- where K is some enclosing continuation for the case
--- Goal: split K into two pieces Kdup,Knodup so that
---       a) Kdup can be duplicated
---       b) Knodup[Kdup[e]] = K[e]
--- The idea is that we'll transform thus:
---          Knodup[ (case _ of { p1 -> Kdup[r1]; ...; pn -> Kdup[rn] }
---
--- We may also return some extra bindings in SimplEnv (that scope over
--- the entire continuation)
---
--- When case-of-case is off, just make the entire continuation non-dupable
-
-prepareCaseCont env alts cont
-  | not (sm_case_case (getMode env)) = return (env, mkBoringStop (contHoleType cont), cont)
-  | not (many_alts alts)             = return (env, cont, mkBoringStop (contResultType cont))
-  | otherwise                        = mkDupableCont env cont
-  where
-    many_alts :: [InAlt] -> Bool  -- True iff strictly > 1 non-bottom alternative
-    many_alts []  = False         -- See Note [Bottom alternatives]
-    many_alts [_] = False
-    many_alts (alt:alts)
-      | is_bot_alt alt = many_alts alts
-      | otherwise      = not (all is_bot_alt alts)
 
-    is_bot_alt (_,_,rhs) = exprIsBottom rhs
+Consider
+  let x* = case e of { True -> e1; False -> e2 }
+  in b
+where x* is a strict binding.  Then mkDupableCont will be given
+the continuation
+   case [] of { True -> e1; False -> e2 } ; let x* = [] in b ; stop
+and will split it into
+   dupable:      case [] of { True -> $j1; False -> $j2 } ; stop
+   join floats:  $j1 = e1, $j2 = e2
+   non_dupable:  let x* = [] in b; stop
+
+Putting this back together would give
+   let x* = let { $j1 = e1; $j2 = e2 } in
+            case e of { True -> $j1; False -> $j2 }
+   in b
+(Of course we only do this if 'e' wants to duplicate that continuation.)
+Note how important it is that the new join points wrap around the
+inner expression, and not around the whole thing.
+
+In contrast, any let-bindings introduced by mkDupableCont can wrap
+around the entire thing.
 
-{-
 Note [Bottom alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we have
@@ -2377,81 +2789,123 @@ When we have
        of alts
 then we can just duplicate those alts because the A and C cases
 will disappear immediately.  This is more direct than creating
-join points and inlining them away; and in some cases we would
-not even create the join points (see Note [Single-alternative case])
-and we would keep the case-of-case which is silly.  See Trac #4930.
+join points and inlining them away.  See Trac #4930.
 -}
 
+--------------------
+mkDupableCaseCont :: SimplEnv -> [InAlt] -> SimplCont
+                  -> SimplM (SimplFloats, SimplCont)
+mkDupableCaseCont env alts cont
+  | altsWouldDup alts = mkDupableCont env cont
+  | otherwise         = return (emptyFloats env, cont)
+
+altsWouldDup :: [InAlt] -> Bool -- True iff strictly > 1 non-bottom alternative
+altsWouldDup []  = False        -- See Note [Bottom alternatives]
+altsWouldDup [_] = False
+altsWouldDup (alt:alts)
+  | is_bot_alt alt = altsWouldDup alts
+  | otherwise      = not (all is_bot_alt alts)
+  where
+    is_bot_alt (_,_,rhs) = exprIsBottom rhs
+
+-------------------------
 mkDupableCont :: SimplEnv -> SimplCont
-              -> SimplM (SimplEnv, SimplCont, SimplCont)
+              -> SimplM ( SimplFloats  -- Incoming SimplEnv augmented with
+                                       --   extra let/join-floats and in-scope variables
+                        , SimplCont)   -- dup_cont: duplicable continuation
 
 mkDupableCont env cont
   | contIsDupable cont
-  = return (env, cont, mkBoringStop (contResultType cont))
+  = return (emptyFloats env, cont)
 
-mkDupableCont _   (Stop {}) = panic "mkDupableCont"     -- Handled by previous eqn
+mkDupableCont _ (Stop {}) = panic "mkDupableCont"     -- Handled by previous eqn
 
 mkDupableCont env (CastIt ty cont)
-  = do  { (env', dup, nodup) <- mkDupableCont env cont
-        ; return (env', CastIt ty dup, nodup) }
+  = do  { (floats, cont') <- mkDupableCont env cont
+        ; return (floats, CastIt ty cont') }
 
 -- Duplicating ticks for now, not sure if this is good or not
-mkDupableCont env cont@(TickIt{})
-  = return (env, mkBoringStop (contHoleType cont), cont)
-
-mkDupableCont env cont@(StrictBind {})
-  =  return (env, mkBoringStop (contHoleType cont), cont)
-        -- See Note [Duplicating StrictBind]
-
-mkDupableCont env (StrictArg info cci cont)
+mkDupableCont env (TickIt t cont)
+  = do  { (floats, cont') <- mkDupableCont env cont
+        ; return (floats, TickIt t cont') }
+
+mkDupableCont env (StrictBind { sc_bndr = bndr, sc_bndrs = bndrs
+                              , sc_body = body, sc_env = se, sc_cont = cont})
+  -- See Note [Duplicating StrictBind]
+  = do { let sb_env = se `setInScopeFromE` env
+       ; (sb_env1, bndr') <- simplBinder sb_env bndr
+       ; (floats1, join_inner) <- simplLam sb_env1 bndrs body cont
+          -- No need to use mkDupableCont before simplLam; we
+          -- use cont once here, and then share the result if necessary
+
+       ; let join_body = wrapFloats floats1 join_inner
+             res_ty    = contResultType cont
+
+       ; (floats2, body2)
+            <- if exprIsDupable (seDynFlags env) join_body
+               then return (emptyFloats env, join_body)
+               else do { join_bndr <- newJoinId [bndr'] res_ty
+                       ; let join_call = App (Var join_bndr) (Var bndr')
+                             join_rhs  = Lam (setOneShotLambda bndr') join_body
+                             join_bind = NonRec join_bndr join_rhs
+                             floats    = emptyFloats env `extendFloats` join_bind
+                       ; return (floats, join_call) }
+       ; return ( floats2
+                , StrictBind { sc_bndr = bndr', sc_bndrs = []
+                             , sc_body = body2
+                             , sc_env  = zapSubstEnv se
+                             , sc_dup  = OkToDup
+                             , sc_cont = mkBoringStop res_ty } ) }
+
+mkDupableCont env (StrictArg { sc_fun = info, sc_cci = cci, sc_cont = cont })
         -- See Note [Duplicating StrictArg]
-  = do { (env', dup, nodup) <- mkDupableCont env cont
-       ; (env'', args')     <- mapAccumLM makeTrivialArg env' (ai_args info)
-       ; return (env'', StrictArg (info { ai_args = args' }) cci dup, nodup) }
-
-mkDupableCont env cont@(ApplyToTy { sc_cont = tail })
-  = do  { (env', dup_cont, nodup_cont) <- mkDupableCont env tail
-        ; return (env', cont { sc_cont = dup_cont }, nodup_cont ) }
-
-mkDupableCont env (ApplyToVal { sc_arg = arg, sc_env = se, sc_cont = cont })
+        -- NB: sc_dup /= OkToDup; that is caught earlier by contIsDupable
+  = do { (floats1, cont') <- mkDupableCont env cont
+       ; (floats_s, args') <- mapAndUnzipM (makeTrivialArg (getMode env))
+                                           (ai_args info)
+       ; return ( foldl addLetFloats floats1 floats_s
+                , StrictArg { sc_fun = info { ai_args = args' }
+                            , sc_cci = cci
+                            , sc_cont = cont'
+                            , sc_dup = OkToDup} ) }
+
+mkDupableCont env (ApplyToTy { sc_cont = cont
+                             , sc_arg_ty = arg_ty, sc_hole_ty = hole_ty })
+  = do  { (floats, cont') <- mkDupableCont env cont
+        ; return (floats, ApplyToTy { sc_cont = cont'
+                                    , sc_arg_ty = arg_ty, sc_hole_ty = hole_ty }) }
+
+mkDupableCont env (ApplyToVal { sc_arg = arg, sc_dup = dup
+                              , sc_env = se, sc_cont = cont })
   =     -- e.g.         [...hole...] (...arg...)
         --      ==>
         --              let a = ...arg...
         --              in [...hole...] a
-    do  { (env', dup_cont, nodup_cont) <- mkDupableCont env cont
-        ; arg' <- simplExpr (se `setInScope` env') arg
-        ; (env'', arg'') <- makeTrivial NotTopLevel env' arg'
-        ; let app_cont = ApplyToVal { sc_arg = arg'', sc_env = zapSubstEnv env''
-                                    , sc_dup = OkToDup, sc_cont = dup_cont }
-        ; return (env'', app_cont, nodup_cont) }
-
-mkDupableCont env cont@(Select _ case_bndr [(_, bs, _rhs)] _ _)
---  See Note [Single-alternative case]
---  | not (exprIsDupable rhs && contIsDupable case_cont)
---  | not (isDeadBinder case_bndr)
-  | all isDeadBinder bs  -- InIds
-    && not (isUnLiftedType (idType case_bndr))
-    -- Note [Single-alternative-unlifted]
-  = return (env, mkBoringStop (contHoleType cont), cont)
-
-mkDupableCont env (Select _ case_bndr alts se cont)
+        -- NB: sc_dup /= OkToDup; that is caught earlier by contIsDupable
+    do  { (floats1, cont') <- mkDupableCont env cont
+        ; let env' = env `setInScopeFromF` floats1
+        ; (_, se', arg') <- simplArg env' dup se arg
+        ; (let_floats2, arg'') <- makeTrivial (getMode env) NotTopLevel (fsLit "karg") arg'
+        ; return ( floats1 `addLetFloats` let_floats2
+                 , ApplyToVal { sc_arg = arg'', sc_env = se'
+                              , sc_dup = OkToDup, sc_cont = cont' }) }
+
+mkDupableCont env (Select { sc_bndr = case_bndr, sc_alts = alts
+                            , sc_env = se, sc_cont = cont })
   =     -- e.g.         (case [...hole...] of { pi -> ei })
         --      ===>
         --              let ji = \xij -> ei
         --              in case [...hole...] of { pi -> ji xij }
+        -- NB: sc_dup /= OkToDup; that is caught earlier by contIsDupable
     do  { tick (CaseOfCase case_bndr)
-        ; (env', dup_cont, nodup_cont) <- prepareCaseCont env alts cont
-                -- NB: We call prepareCaseCont here.  If there is only one
-                -- alternative, then dup_cont may be big, but that's ok
-                -- because we push it into the single alternative, and then
-                -- use mkDupableAlt to turn that simplified alternative into
-                -- a join point if it's too big to duplicate.
+        ; (floats, alt_cont) <- mkDupableCaseCont env alts cont
+                -- NB: We call mkDupableCaseCont here to make cont duplicable
+                --     (if necessary, depending on the number of alts)
                 -- And this is important: see Note [Fusing case continuations]
 
-        ; let alt_env = se `setInScope` env'
-
+        ; let alt_env = se `setInScopeFromF` floats
         ; (alt_env', case_bndr') <- simplBinder alt_env case_bndr
-        ; alts' <- mapM (simplAlt alt_env' Nothing [] case_bndr' dup_cont) alts
+        ; alts' <- mapM (simplAlt alt_env' Nothing [] case_bndr' alt_cont) alts
         -- Safe to say that there are no handled-cons for the DEFAULT case
                 -- NB: simplBinder does not zap deadness occ-info, so
                 -- a dead case_bndr' will still advertise its deadness
@@ -2464,34 +2918,25 @@ mkDupableCont env (Select _ case_bndr alts se cont)
         -- NB: we don't use alt_env further; it has the substEnv for
         --     the alternatives, and we don't want that
 
-        ; (env'', alts'') <- mkDupableAlts env' case_bndr' alts'
-        ; return (env'',  -- Note [Duplicated env]
-                  Select OkToDup case_bndr' alts'' (zapSubstEnv env'')
-                         (mkBoringStop (contHoleType nodup_cont)),
-                  nodup_cont) }
+        ; (join_floats, alts'') <- mapAccumLM (mkDupableAlt (seDynFlags env) case_bndr')
+                                              emptyJoinFloats alts'
 
+        ; return (floats `addJoinFloats` join_floats,  -- Note [Duplicated env]
+                  Select { sc_dup  = OkToDup
+                         , sc_bndr = case_bndr'
+                         , sc_alts = alts''
+                         , sc_env  = zapSubstEnv env
+                         , sc_cont = mkBoringStop (contResultType cont) } ) }
 
-mkDupableAlts :: SimplEnv -> OutId -> [InAlt]
-              -> SimplM (SimplEnv, [InAlt])
--- Absorbs the continuation into the new alternatives
+mkDupableAlt :: DynFlags -> OutId
+             -> JoinFloats -> OutAlt
+             -> SimplM (JoinFloats, OutAlt)
+mkDupableAlt dflags case_bndr jfloats (con, bndrs', rhs')
+  | exprIsDupable dflags rhs'  -- Note [Small alternative rhs]
+  = return (jfloats, (con, bndrs', rhs'))
 
-mkDupableAlts env case_bndr' the_alts
-  = go env the_alts
-  where
-    go env0 [] = return (env0, [])
-    go env0 (alt:alts)
-        = do { (env1, alt') <- mkDupableAlt env0 case_bndr' alt
-             ; (env2, alts') <- go env1 alts
-             ; return (env2, alt' : alts' ) }
-
-mkDupableAlt :: SimplEnv -> OutId -> (AltCon, [CoreBndr], CoreExpr)
-              -> SimplM (SimplEnv, (AltCon, [CoreBndr], CoreExpr))
-mkDupableAlt env case_bndr (con, bndrs', rhs') = do
-  dflags <- getDynFlags
-  if exprIsDupable dflags rhs'  -- Note [Small alternative rhs]
-   then return (env, (con, bndrs', rhs'))
-   else
-    do  { let rhs_ty'  = exprType rhs'
+  | otherwise
+  = do  { let rhs_ty'  = exprType rhs'
               scrut_ty = idType case_bndr
               case_bndr_w_unf
                 = case con of
@@ -2499,45 +2944,42 @@ mkDupableAlt env case_bndr (con, bndrs', rhs') = do
                       DataAlt dc -> setIdUnfolding case_bndr unf
                           where
                                  -- See Note [Case binders and join points]
-                             unf = mkInlineUnfolding Nothing rhs
+                             unf = mkInlineUnfolding rhs
                              rhs = mkConApp2 dc (tyConAppArgs scrut_ty) bndrs'
 
-                      LitAlt {} -> WARN( True, ptext (sLit "mkDupableAlt")
+                      LitAlt {} -> WARN( True, text "mkDupableAlt"
                                                 <+> ppr case_bndr <+> ppr con )
                                    case_bndr
                            -- The case binder is alive but trivial, so why has
                            -- it not been substituted away?
 
-              used_bndrs' | isDeadBinder case_bndr = filter abstract_over bndrs'
-                          | otherwise              = bndrs' ++ [case_bndr_w_unf]
+              final_bndrs'
+                | isDeadBinder case_bndr = filter abstract_over bndrs'
+                | otherwise              = bndrs' ++ [case_bndr_w_unf]
 
               abstract_over bndr
                   | isTyVar bndr = True -- Abstract over all type variables just in case
                   | otherwise    = not (isDeadBinder bndr)
                         -- The deadness info on the new Ids is preserved by simplBinders
+              final_args = varsToCoreExprs final_bndrs'
+                           -- Note [Join point abstraction]
 
-        ; (final_bndrs', final_args)    -- Note [Join point abstraction]
-                <- if (any isId used_bndrs')
-                   then return (used_bndrs', varsToCoreExprs used_bndrs')
-                    else do { rw_id <- newId (fsLit "w") voidPrimTy
-                            ; return ([setOneShotLambda rw_id], [Var voidPrimId]) }
-
-        ; join_bndr <- newId (fsLit "$j") (mkPiTypes final_bndrs' rhs_ty')
-                -- Note [Funky mkPiTypes]
-
-        ; let   -- We make the lambdas into one-shot-lambdas.  The
+                -- 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
-                really_final_bndrs     = map one_shot final_bndrs'
-                one_shot v | isId v    = setOneShotLambda v
-                           | otherwise = v
-                join_rhs   = mkLams really_final_bndrs rhs'
-                join_arity = exprArity join_rhs
-                join_call  = mkApps (Var join_bndr) final_args
-
-        ; env' <- addPolyBind NotTopLevel env (NonRec (join_bndr `setIdArity` join_arity) join_rhs)
-        ; return (env', (con, bndrs', join_call)) }
+              really_final_bndrs     = map one_shot final_bndrs'
+              one_shot v | isId v    = setOneShotLambda v
+                         | otherwise = v
+              join_rhs   = mkLams really_final_bndrs rhs'
+
+        ; join_bndr <- newJoinId final_bndrs' rhs_ty'
+
+        ; let join_call = mkApps (Var join_bndr) final_args
+              alt'      = (con, bndrs', join_call)
+
+        ; return ( jfloats `addJoinFlts` unitJoinFloat (NonRec join_bndr join_rhs)
+                 , alt') }
                 -- See Note [Duplicated env]
 
 {-
@@ -2562,7 +3004,7 @@ The simplifier will find
 So we'll call mkDupableCont on
    Select [I# a -> I# a] (StrictBind body Stop)
 There is just one alternative in the first Select, so we want to
-simplify the rhs (I# a) with continuation (StricgtBind body Stop)
+simplify the rhs (I# a) with continuation (StrictBind body Stop)
 Supposing that body is big, we end up with
           let $j a = <let x = I# a in body>
           in case v of { pn -> case rn of
@@ -2581,7 +3023,7 @@ Consider this
 If we make a join point with c but not c# we get
   $j = \c -> ....c....
 
-But if later inlining scrutines the c, thus
+But if later inlining scrutinises the c, thus
 
   $j = \c -> ... case c of { I# y -> ... } ...
 
@@ -2603,7 +3045,7 @@ So instead we do both: we pass 'c' and 'c#' , and record in c's inlining
 Absence analysis may later discard 'c'.
 
 NB: take great care when doing strictness analysis;
-    see Note [Lamba-bound unfoldings] in DmdAnal.
+    see Note [Lambda-bound unfoldings] in DmdAnal.
 
 Also note that we can still end up passing stuff that isn't used.  Before
 strictness analysis we have
@@ -2616,7 +3058,7 @@ and c is unused.
 Note [Duplicated env]
 ~~~~~~~~~~~~~~~~~~~~~
 Some of the alternatives are simplified, but have not been turned into a join point
-So they *must* have an zapped subst-env.  So we can't use completeNonRecX to
+So they *must* have a zapped subst-env.  So we can't use completeNonRecX to
 bind the join point, because it might to do PostInlineUnconditionally, and
 we'd lose that when zapping the subst-env.  We could have a per-alt subst-env,
 but zapping it (as we do in mkDupableCont, the Select case) is safe, and
@@ -2627,7 +3069,7 @@ Note [Small alternative rhs]
 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
+The Ord instance of Maybe in PrelMaybe.hs, 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.
@@ -2640,9 +3082,9 @@ but we only have one env shared between all the alts.
 (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.
 
-Note [Funky mkPiTypes]
+Note [Funky mkLamTypes]
 ~~~~~~~~~~~~~~~~~~~~~~
-Notice the funky mkPiTypes.  If the contructor has existentials
+Notice the funky mkLamTypes.  If the constructor has existentials
 it's possible that the join point will be abstracted over
 type variables as well as term variables.
  Example:  Suppose we have
@@ -2657,8 +3099,80 @@ type variables as well as term variables.
         case (case e of ...) of
             C t xs::[t] -> j t xs
 
-Note [Join point abstraction]
+Note [Duplicating StrictArg]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We make a StrictArg duplicable simply by making all its
+stored-up arguments (in sc_fun) trivial, by let-binding
+them.  Thus:
+        f E [..hole..]
+        ==>     let a = E
+                in f a [..hole..]
+Now if the thing in the hole is a case expression (which is when
+we'll call mkDupableCont), we'll push the function call into the
+branches, which is what we want.  Now RULES for f may fire, and
+call-pattern specialisation.  Here's an example from Trac #3116
+     go (n+1) (case l of
+                 1  -> bs'
+                 _  -> Chunk p fpc (o+1) (l-1) bs')
+If we can push the call for 'go' inside the case, we get
+call-pattern specialisation for 'go', which is *crucial* for
+this program.
+
+Here is the (&&) example:
+        && E (case x of { T -> F; F -> T })
+  ==>   let a = E in
+        case x of { T -> && a F; F -> && a T }
+Much better!
+
+Notice that
+  * Arguments to f *after* the strict one are handled by
+    the ApplyToVal case of mkDupableCont.  Eg
+        f [..hole..] E
+
+  * We can only do the let-binding of E because the function
+    part of a StrictArg continuation is an explicit syntax
+    tree.  In earlier versions we represented it as a function
+    (CoreExpr -> CoreEpxr) which we couldn't take apart.
+
+Historical aide: previously we did this (where E is a
+big argument:
+        f E [..hole..]
+        ==>     let $j = \a -> f E a
+                in $j [..hole..]
+
+But this is terrible! Here's an example:
+        && E (case x of { T -> F; F -> T })
+Now, && is strict so we end up simplifying the case with
+an ArgOf continuation.  If we let-bind it, we get
+        let $j = \v -> && E v
+        in simplExpr (case x of { T -> F; F -> T })
+                     (ArgOf (\r -> $j r)
+And after simplifying more we get
+        let $j = \v -> && E v
+        in case x of { T -> $j F; F -> $j T }
+Which is a Very Bad Thing
+
+
+Note [Duplicating StrictBind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We make a StrictBind duplicable in a very similar way to
+that for case expressions.  After all,
+   let x* = e in b   is similar to    case e of x -> b
+
+So we potentially make a join-point for the body, thus:
+   let x = [] in b   ==>   join j x = b
+                           in let x = [] in j x
+
+
+Note [Join point abstraction]  Historical note
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+NB: This note is now historical, describing how (in the past) we used
+to add a void argument to nullary join points.  But now that "join
+point" is not a fuzzy concept but a formal syntactic construct (as
+distinguished by the JoinId constructor of IdDetails), each of these
+concerns is handled separately, with no need for a vestigial extra
+argument.
+
 Join points always have at least one value argument,
 for several reasons
 
@@ -2669,7 +3183,7 @@ for several reasons
   where v::Void#.  The value passed to this function is void,
   which generates (almost) no code.
 
-* CPR.  We used to say "&& isUnLiftedType rhs_ty'" here, but now
+* CPR.  We used to say "&& isUnliftedType rhs_ty'" here, but now
   we make the join point into a function whenever used_bndrs'
   is empty.  This makes the join-point more CPR friendly.
   Consider:       let j = if .. then I# 3 else I# 4
@@ -2704,173 +3218,156 @@ case_bndr to all the join points if it's used in *any* RHS,
 because we don't know its usage in each RHS separately
 
 
-Note [Duplicating StrictArg]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The original plan had (where E is a big argument)
-e.g.    f E [..hole..]
-        ==>     let $j = \a -> f E a
-                in $j [..hole..]
 
-But this is terrible! Here's an example:
-        && E (case x of { T -> F; F -> T })
-Now, && is strict so we end up simplifying the case with
+************************************************************************
+*                                                                      *
+                    Unfoldings
+*                                                                      *
+************************************************************************
+-}
 
-an ArgOf continuation.  If we let-bind it, we get
-        let $j = \v -> && E v
-        in simplExpr (case x of { T -> F; F -> T })
-                     (ArgOf (\r -> $j r)
-And after simplifying more we get
-        let $j = \v -> && E v
-        in case x of { T -> $j F; F -> $j T }
-Which is a Very Bad Thing
+simplLetUnfolding :: SimplEnv-> TopLevelFlag
+                  -> Maybe SimplCont
+                  -> InId
+                  -> OutExpr
+                  -> Unfolding -> SimplM Unfolding
+simplLetUnfolding env top_lvl cont_mb id new_rhs unf
+  | isStableUnfolding unf
+  = simplStableUnfolding env top_lvl cont_mb id unf
+  | otherwise
+  = mkLetUnfolding (seDynFlags env) top_lvl InlineRhs id new_rhs
 
-What we do now is this
-        f E [..hole..]
-        ==>     let a = E
-                in f a [..hole..]
-Now if the thing in the hole is a case expression (which is when
-we'll call mkDupableCont), we'll push the function call into the
-branches, which is what we want.  Now RULES for f may fire, and
-call-pattern specialisation.  Here's an example from Trac #3116
-     go (n+1) (case l of
-                 1  -> bs'
-                 _  -> Chunk p fpc (o+1) (l-1) bs')
-If we can push the call for 'go' inside the case, we get
-call-pattern specialisation for 'go', which is *crucial* for
-this program.
+-------------------
+mkLetUnfolding :: DynFlags -> TopLevelFlag -> UnfoldingSource
+               -> InId -> OutExpr -> SimplM Unfolding
+mkLetUnfolding dflags top_lvl src id new_rhs
+  = is_bottoming `seq`  -- See Note [Force bottoming field]
+    return (mkUnfolding dflags src is_top_lvl is_bottoming new_rhs)
+            -- We make an  unfolding *even for loop-breakers*.
+            -- Reason: (a) It might be useful to know that they are WHNF
+            --         (b) In TidyPgm we currently assume that, if we want to
+            --             expose the unfolding then indeed we *have* an unfolding
+            --             to expose.  (We could instead use the RHS, but currently
+            --             we don't.)  The simple thing is always to have one.
+  where
+    is_top_lvl   = isTopLevel top_lvl
+    is_bottoming = isBottomingId id
 
-Here is the (&&) example:
-        && E (case x of { T -> F; F -> T })
-  ==>   let a = E in
-        case x of { T -> && a F; F -> && a T }
-Much better!
+-------------------
+simplStableUnfolding :: SimplEnv -> TopLevelFlag
+                     -> Maybe SimplCont  -- Just k => a join point with continuation k
+                     -> InId
+                     -> Unfolding -> SimplM Unfolding
+-- Note [Setting the new unfolding]
+simplStableUnfolding env top_lvl mb_cont id unf
+  = case unf of
+      NoUnfolding   -> return unf
+      BootUnfolding -> return unf
+      OtherCon {}   -> return unf
 
-Notice that
-  * Arguments to f *after* the strict one are handled by
-    the ApplyToVal case of mkDupableCont.  Eg
-        f [..hole..] E
+      DFunUnfolding { df_bndrs = bndrs, df_con = con, df_args = args }
+        -> do { (env', bndrs') <- simplBinders rule_env bndrs
+              ; args' <- mapM (simplExpr env') args
+              ; return (mkDFunUnfolding bndrs' con args') }
 
-  * We can only do the let-binding of E because the function
-    part of a StrictArg continuation is an explicit syntax
-    tree.  In earlier versions we represented it as a function
-    (CoreExpr -> CoreEpxr) which we couldn't take apart.
+      CoreUnfolding { uf_tmpl = expr, uf_src = src, uf_guidance = guide }
+        | isStableSource src
+        -> do { expr' <- case mb_cont of
+                           Just cont -> simplJoinRhs rule_env id expr cont
+                           Nothing   -> simplExpr rule_env expr
+              ; case guide of
+                  UnfWhen { ug_arity = arity, ug_unsat_ok = sat_ok }  -- Happens for INLINE things
+                     -> let guide' = UnfWhen { ug_arity = arity, ug_unsat_ok = sat_ok
+                                             , ug_boring_ok = inlineBoringOk expr' }
+                        -- Refresh the boring-ok flag, in case expr'
+                        -- has got small. This happens, notably in the inlinings
+                        -- for dfuns for single-method classes; see
+                        -- Note [Single-method classes] in TcInstDcls.
+                        -- A test case is Trac #4138
+                        in return (mkCoreUnfolding src is_top_lvl expr' guide')
+                            -- See Note [Top-level flag on inline rules] in CoreUnfold
 
-Do *not* duplicate StrictBind and StritArg continuations.  We gain
-nothing by propagating them into the expressions, and we do lose a
-lot.
+                  _other              -- Happens for INLINABLE things
+                     -> mkLetUnfolding dflags top_lvl src id expr' }
+                -- If the guidance is UnfIfGoodArgs, this is an INLINABLE
+                -- unfolding, and we need to make sure the guidance is kept up
+                -- to date with respect to any changes in the unfolding.
 
-The desire not to duplicate is the entire reason that
-mkDupableCont returns a pair of continuations.
+        | otherwise -> return noUnfolding   -- Discard unstable unfoldings
+  where
+    dflags     = seDynFlags env
+    is_top_lvl = isTopLevel top_lvl
+    act        = idInlineActivation id
+    rule_env   = updMode (updModeForStableUnfoldings act) env
+         -- See Note [Simplifying inside stable unfoldings] in SimplUtils
 
-Note [Duplicating StrictBind]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Unlike StrictArg, there doesn't seem anything to gain from
-duplicating a StrictBind continuation, so we don't.
+{-
+Note [Force bottoming field]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We need to force bottoming, or the new unfolding holds
+on to the old unfolding (which is part of the id).
 
+Note [Setting the new unfolding]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* If there's an INLINE pragma, we simplify the RHS gently.  Maybe we
+  should do nothing at all, but simplifying gently might get rid of
+  more crap.
 
-Note [Single-alternative cases]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This case is just like the ArgOf case.  Here's an example:
-        data T a = MkT !a
-        ...(MkT (abs x))...
-Then we get
-        case (case x of I# x' ->
-              case x' <# 0# of
-                True  -> I# (negate# x')
-                False -> I# x') of y {
-          DEFAULT -> MkT y
-Because the (case x) has only one alternative, we'll transform to
-        case x of I# x' ->
-        case (case x' <# 0# of
-                True  -> I# (negate# x')
-                False -> I# x') of y {
-          DEFAULT -> MkT y
-But now we do *NOT* want to make a join point etc, giving
-        case x of I# x' ->
-        let $j = \y -> MkT y
-        in case x' <# 0# of
-                True  -> $j (I# (negate# x'))
-                False -> $j (I# x')
-In this case the $j will inline again, but suppose there was a big
-strict computation enclosing the orginal call to MkT.  Then, it won't
-"see" the MkT any more, because it's big and won't get duplicated.
-And, what is worse, nothing was gained by the case-of-case transform.
-
-So, in circumstances like these, we don't want to build join points
-and push the outer case into the branches of the inner one. Instead,
-don't duplicate the continuation.
-
-When should we use this strategy?  We should not use it on *every*
-single-alternative case:
-  e.g.  case (case ....) of (a,b) -> (# a,b #)
-Here we must push the outer case into the inner one!
-Other choices:
-
-   * Match [(DEFAULT,_,_)], but in the common case of Int,
-     the alternative-filling-in code turned the outer case into
-                case (...) of y { I# _ -> MkT y }
-
-   * Match on single alternative plus (not (isDeadBinder case_bndr))
-     Rationale: pushing the case inwards won't eliminate the construction.
-     But there's a risk of
-                case (...) of y { (a,b) -> let z=(a,b) in ... }
-     Now y looks dead, but it'll come alive again.  Still, this
-     seems like the best option at the moment.
-
-   * Match on single alternative plus (all (isDeadBinder bndrs))
-     Rationale: this is essentially  seq.
-
-   * Match when the rhs is *not* duplicable, and hence would lead to a
-     join point.  This catches the disaster-case above.  We can test
-     the *un-simplified* rhs, which is fine.  It might get bigger or
-     smaller after simplification; if it gets smaller, this case might
-     fire next time round.  NB also that we must test contIsDupable
-     case_cont *too, because case_cont might be big!
-
-     HOWEVER: I found that this version doesn't work well, because
-     we can get         let x = case (...) of { small } in ...case x...
-     When x is inlined into its full context, we find that it was a bad
-     idea to have pushed the outer case inside the (...) case.
-
-Note [Single-alternative-unlifted]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here's another single-alternative where we really want to do case-of-case:
-
-data Mk1 = Mk1 Int# | Mk2 Int#
-
-M1.f =
-    \r [x_s74 y_s6X]
-        case
-            case y_s6X of tpl_s7m {
-              M1.Mk1 ipv_s70 -> ipv_s70;
-              M1.Mk2 ipv_s72 -> ipv_s72;
-            }
-        of
-        wild_s7c
-        { __DEFAULT ->
-              case
-                  case x_s74 of tpl_s7n {
-                    M1.Mk1 ipv_s77 -> ipv_s77;
-                    M1.Mk2 ipv_s79 -> ipv_s79;
-                  }
-              of
-              wild1_s7b
-              { __DEFAULT -> ==# [wild1_s7b wild_s7c];
-              };
-        };
-
-So the outer case is doing *nothing at all*, other than serving as a
-join-point.  In this case we really want to do case-of-case and decide
-whether to use a real join point or just duplicate the continuation:
-
-    let $j s7c = case x of
-                   Mk1 ipv77 -> (==) s7c ipv77
-                   Mk1 ipv79 -> (==) s7c ipv79
-    in
-    case y of
-      Mk1 ipv70 -> $j ipv70
-      Mk2 ipv72 -> $j ipv72
+* If not, we make an unfolding from the new RHS.  But *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
+
+If there's a stable unfolding on a loop breaker (which happens for
+INLINABLE), we hang on to the inlining.  It's pretty dodgy, but the
+user did say 'INLINE'.  May need to revisit this choice.
+
+************************************************************************
+*                                                                      *
+                    Rules
+*                                                                      *
+************************************************************************
 
-Hence: check whether the case binder's type is unlifted, because then
-the outer case is *not* a seq.
+Note [Rules in a letrec]
+~~~~~~~~~~~~~~~~~~~~~~~~
+After creating fresh binders for the binders of a letrec, we
+substitute the RULES and add them back onto the binders; this is done
+*before* processing any of the RHSs.  This is important.  Manuel found
+cases where he really, really wanted a RULE for a recursive function
+to apply in that function's own right-hand side.
+
+See Note [Forming Rec groups] in OccurAnal
 -}
+
+addBndrRules :: SimplEnv -> InBndr -> OutBndr -> SimplM (SimplEnv, OutBndr)
+-- Rules are added back into the bin
+addBndrRules env in_id out_id
+  | null old_rules
+  = return (env, out_id)
+  | otherwise
+  = do { new_rules <- simplRules env (Just (idName out_id)) old_rules
+       ; let final_id  = out_id `setIdSpecialisation` mkRuleInfo new_rules
+       ; return (modifyInScope env final_id, final_id) }
+  where
+    old_rules = ruleInfoRules (idSpecialisation in_id)
+
+simplRules :: SimplEnv -> Maybe Name -> [CoreRule] -> SimplM [CoreRule]
+simplRules env mb_new_nm rules
+  = mapM simpl_rule rules
+  where
+    simpl_rule rule@(BuiltinRule {})
+      = return rule
+
+    simpl_rule rule@(Rule { ru_bndrs = bndrs, ru_args = args
+                          , ru_fn = fn_name, ru_rhs = rhs })
+      = do { (env', bndrs') <- simplBinders env bndrs
+           ; let rhs_ty = substTy env' (exprType rhs)
+                 rule_cont = mkBoringStop rhs_ty
+                 rule_env  = updMode updModeForRules env'
+           ; args' <- mapM (simplExpr rule_env) args
+           ; rhs'  <- simplExprC rule_env rhs rule_cont
+           ; return (rule { ru_bndrs = bndrs'
+                          , ru_fn    = mb_new_nm `orElse` fn_name
+                          , ru_args  = args'
+                          , ru_rhs   = rhs' }) }