Fix a huge space leak in the mighty Simplifier

This long-standing, terrible, adn somewhat subtle bug was exposed
by Trac #10370, thanks to Reid Barton's brilliant test case (comment:3).

The effect is large on the Trac #10370 test.
Here is what the profile report says:

Before:
 total time  =       24.35 secs   (24353 ticks @ 1000 us, 1 processor)
 total alloc = 11,864,360,816 bytes  (excludes profiling overheads)

After:
 total time  =       21.16 secs   (21160 ticks @ 1000 us, 1 processor)
 total alloc = 7,947,141,136 bytes  (excludes profiling overheads)

The /combined/ effect of the tidyOccName fix, plus this one, is dramtic
for Trac #10370.  Here is what +RTS -s says:

Before:
  15,490,210,952 bytes allocated in the heap
   1,783,919,456 bytes maximum residency (20 sample(s))

  MUT     time   30.117s  ( 31.383s elapsed)
  GC      time   90.103s  ( 90.107s elapsed)
  Total   time  120.843s  (122.065s elapsed)

After:
   7,928,671,936 bytes allocated in the heap
      52,914,832 bytes maximum residency (25 sample(s))

  MUT     time   13.912s  ( 15.110s elapsed)
  GC      time    6.809s  (  6.808s elapsed)
  Total   time   20.789s  ( 21.954s elapsed)

- Heap allocation halved
- Residency cut by a factor of more than 30.
- ELapsed time cut by a factor of 6

Not bad!

The details
~~~~~~~~~~~
The culprit was SimplEnv.mkCoreSubst, which used mapVarEnv to do some
impedence-matching from the substitituion used by the simplifier to
the one used by CoreSubst.  But the impedence-mactching was recursive!

  mk_subst tv_env cv_env id_env
    = CoreSubst.mkSubst in_scope tv_env cv_env (mapVarEnv fiddle id_env)

  fiddle (DoneEx e)          = e
  fiddle (DoneId v)          = Var v
  fiddle (ContEx tv cv id e) = CoreSubst.substExpr (mk_subst tv cv id) e

Inside fiddle, in the ContEx case, we may do another whole level of
fiddle.  And so on.  Moreover, UniqFM (which is built on Data.IntMap) is
strict, so the fiddling is done eagerly.  I didn't wok through all the
details but the result is a gargatuan blow-up of entirely unnecessary work.

Laziness would make this go away, I think, but I don't want to mess
with IntMap.  And in any case, the impedence matching is a royal pain.

In the end I simply ceased trying to use CoreSubst.substExpr in the
simplifier, and instead just use simplExpr.  That does mean bit of
duplication; e.g.  new code for simplRules.  But it's not a big deal
and it's far more direct and easy to reason about.

A bit of knock-on refactoring:

 * Data type ArgSummary moves to CoreUnfold.

 * interestingArg moves from CoreUnfold to SimplUtils, and gets a
   SimplEnv argument which can be used when we encounter a variable.

 * simplLamBndrs, addBndrRules move from SimplEnv to Simplify
   (because they now calls simplUnfolding, simplRules resp)

 * SimplUtils.substExpr, substUnfolding, mkCoreSubst die completely

 * In Simplify some several functions that were previously pure
   substitution-based functions are now monadic:
     - addBndrRules, simplRule
     - addCoerce, add_coerce in simplCast

 * In case 2c of Simplify.rebuildCase, there was a pretty disgusting
   expression-substitution taking place for 'rhs'; and we really don't
   want to make that monadic becuase 'rhs' can be big.
   Solution: reduce the arity of the rules for seq.
   See Note [User-defined RULES for seq] in MkId.

9 files changed, 398 insertions, 362 deletions

diff --git a/compiler/coreSyn/CoreUnfold.hs b/compiler/coreSyn/CoreUnfold.hs
index 92160c7dbc..3a54b2773e 100644
--- a/compiler/coreSyn/CoreUnfold.hs
+++ b/compiler/coreSyn/CoreUnfold.hs
@@ -27,7 +27,7 @@ module CoreUnfold (
         mkCompulsoryUnfolding, mkDFunUnfolding,
         specUnfolding,
 
-        interestingArg, ArgSummary(..),
+        ArgSummary(..),
 
         couldBeSmallEnoughToInline, inlineBoringOk,
         certainlyWillInline, smallEnoughToInline,
@@ -986,11 +986,20 @@ callSiteInline :: DynFlags
                -> CallCtxt              -- True <=> continuation is interesting
                -> Maybe CoreExpr        -- Unfolding, if any
 
+data ArgSummary = TrivArg       -- Nothing interesting
+                | NonTrivArg    -- Arg has structure
+                | ValueArg      -- Arg is a con-app or PAP
+                                -- ..or con-like. Note [Conlike is interesting]
+
 instance Outputable ArgSummary where
   ppr TrivArg    = ptext (sLit "TrivArg")
   ppr NonTrivArg = ptext (sLit "NonTrivArg")
   ppr ValueArg   = ptext (sLit "ValueArg")
 
+nonTriv ::  ArgSummary -> Bool
+nonTriv TrivArg = False
+nonTriv _       = True
+
 data CallCtxt
   = BoringCtxt
   | RhsCtxt             -- Rhs of a let-binding; see Note [RHS of lets]
@@ -1358,80 +1367,3 @@ computeDiscount dflags arg_discounts res_discount arg_infos cont_info
                 -- But we want to aovid inlining large functions that return
                 -- constructors into contexts that are simply "interesting"
 
-{-
-************************************************************************
-*                                                                      *
-        Interesting arguments
-*                                                                      *
-************************************************************************
-
-Note [Interesting arguments]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An argument is interesting if it deserves a discount for unfoldings
-with a discount in that argument position.  The idea is to avoid
-unfolding a function that is applied only to variables that have no
-unfolding (i.e. they are probably lambda bound): f x y z There is
-little point in inlining f here.
-
-Generally, *values* (like (C a b) and (\x.e)) deserve discounts.  But
-we must look through lets, eg (let x = e in C a b), because the let will
-float, exposing the value, if we inline.  That makes it different to
-exprIsHNF.
-
-Before 2009 we said it was interesting if the argument had *any* structure
-at all; i.e. (hasSomeUnfolding v).  But does too much inlining; see Trac #3016.
-
-But we don't regard (f x y) as interesting, unless f is unsaturated.
-If it's saturated and f hasn't inlined, then it's probably not going
-to now!
-
-Note [Conlike is interesting]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-        f d = ...((*) d x y)...
-        ... f (df d')...
-where df is con-like. Then we'd really like to inline 'f' so that the
-rule for (*) (df d) can fire.  To do this
-  a) we give a discount for being an argument of a class-op (eg (*) d)
-  b) we say that a con-like argument (eg (df d)) is interesting
--}
-
-data ArgSummary = TrivArg       -- Nothing interesting
-                | NonTrivArg    -- Arg has structure
-                | ValueArg      -- Arg is a con-app or PAP
-                                -- ..or con-like. Note [Conlike is interesting]
-
-interestingArg :: CoreExpr -> ArgSummary
--- See Note [Interesting arguments]
-interestingArg e = go e 0
-  where
-    -- n is # value args to which the expression is applied
-    go (Lit {}) _          = ValueArg
-    go (Var v)  n
-       | isConLikeId v     = ValueArg   -- Experimenting with 'conlike' rather that
-                                        --    data constructors here
-       | idArity v > n     = ValueArg   -- Catches (eg) primops with arity but no unfolding
-       | n > 0             = NonTrivArg -- Saturated or unknown call
-       | conlike_unfolding = ValueArg   -- n==0; look for an interesting unfolding
-                                        -- See Note [Conlike is interesting]
-       | otherwise         = TrivArg    -- n==0, no useful unfolding
-       where
-         conlike_unfolding = isConLikeUnfolding (idUnfolding v)
-
-    go (Type _)          _ = TrivArg
-    go (Coercion _)      _ = TrivArg
-    go (App fn (Type _)) n = go fn n
-    go (App fn (Coercion _)) n = go fn n
-    go (App fn _)        n = go fn (n+1)
-    go (Tick _ a)      n = go a n
-    go (Cast e _)        n = go e n
-    go (Lam v e)         n
-       | isTyVar v         = go e n
-       | n>0               = go e (n-1)
-       | otherwise         = ValueArg
-    go (Let _ e)         n = case go e n of { ValueArg -> ValueArg; _ -> NonTrivArg }
-    go (Case {})         _ = NonTrivArg
-
-nonTriv ::  ArgSummary -> Bool
-nonTriv TrivArg = False
-nonTriv _       = True
diff --git a/compiler/simplCore/SimplCore.hs b/compiler/simplCore/SimplCore.hs
index 0fd929a2a6..da27c3557f 100644
--- a/compiler/simplCore/SimplCore.hs
+++ b/compiler/simplCore/SimplCore.hs
@@ -12,7 +12,6 @@ module SimplCore ( core2core, simplifyExpr ) where
 
 import DynFlags
 import CoreSyn
-import CoreSubst
 import HscTypes
 import CSE              ( cseProgram )
 import Rules            ( emptyRuleBase, mkRuleBase, unionRuleBase,
@@ -24,7 +23,7 @@ import CoreUtils        ( coreBindsSize, coreBindsStats, exprSize,
                           mkTicks, stripTicksTop )
 import CoreLint         ( showPass, endPass, lintPassResult, dumpPassResult,
                           lintAnnots )
-import Simplify         ( simplTopBinds, simplExpr )
+import Simplify         ( simplTopBinds, simplExpr, simplRule )
 import SimplUtils       ( simplEnvForGHCi, activeRule )
 import SimplEnv
 import SimplMonad
@@ -640,20 +639,20 @@ simplifyPgmIO pass@(CoreDoSimplify max_iterations mode)
            eps <- hscEPS hsc_env ;
            let  { rule_base1 = unionRuleBase hpt_rule_base (eps_rule_base eps)
                 ; rule_base2 = extendRuleBaseList rule_base1 rules
-                ; simpl_binds = {-# SCC "SimplTopBinds" #-}
-                                simplTopBinds simpl_env tagged_binds
                 ; fam_envs = (eps_fam_inst_env eps, fam_inst_env) } ;
 
                 -- Simplify the program
-           (env1, counts1) <- initSmpl dflags rule_base2 fam_envs us1 sz simpl_binds ;
-
-                -- Apply the substitution to rules defined in this module
-                -- for imported Ids.  Eg  RULE map my_f = blah
-                -- If we have a substitution my_f :-> other_f, we'd better
-                -- apply it to the rule to, or it'll never match
-           let  { binds1 = getFloatBinds env1
-                ; rules1 = substRulesForImportedIds (mkCoreSubst (text "imp-rules") env1) rules
-                } ;
+           ((binds1, rules1), counts1) <- initSmpl dflags rule_base2 fam_envs us1 sz $
+               do { env1 <- {-# SCC "SimplTopBinds" #-}
+                            simplTopBinds simpl_env tagged_binds
+
+                      -- Apply the substitution to rules defined in this module
+                      -- for imported Ids.  Eg  RULE map my_f = blah
+                      -- If we have a substitution my_f :-> other_f, we'd better
+                      -- apply it to the rule to, or it'll never match
+                  ; rules1 <- mapM (simplRule env1 Nothing) rules
+
+                  ; return (getFloatBinds env1, rules1) } ;
 
                 -- Stop if nothing happened; don't dump output
            if isZeroSimplCount counts1 then
diff --git a/compiler/simplCore/SimplEnv.hs b/compiler/simplCore/SimplEnv.hs
index 96c2fc046d..17367ef74f 100644
--- a/compiler/simplCore/SimplEnv.hs
+++ b/compiler/simplCore/SimplEnv.hs
@@ -21,13 +21,12 @@ module SimplEnv (
         getInScope, setInScope, setInScopeSet, modifyInScope, addNewInScopeIds,
         getSimplRules,
 
-        SimplSR(..), mkContEx, substId, lookupRecBndr,
+        SimplSR(..), mkContEx, substId, lookupRecBndr, refineFromInScope,
 
-        simplNonRecBndr, simplRecBndrs, simplLamBndr, simplLamBndrs,
-        simplBinder, simplBinders, addBndrRules,
-        substExpr, substTy, substTyVar, getTvSubst,
+        simplNonRecBndr, simplRecBndrs,
+        simplBinder, simplBinders,
+        substTy, substTyVar, getTvSubst,
         getCvSubst, substCo, substCoVar,
-        mkCoreSubst,
 
         -- Floats
         Floats, emptyFloats, isEmptyFloats, addNonRec, addFloats, extendFloats,
@@ -39,7 +38,6 @@ module SimplEnv (
 
 import SimplMonad
 import CoreMonad        ( SimplifierMode(..) )
-import IdInfo
 import CoreSyn
 import CoreUtils
 import Var
@@ -49,7 +47,6 @@ import OrdList
 import Id
 import MkCore                   ( mkWildValBinder )
 import TysWiredIn
-import qualified CoreSubst
 import qualified Type
 import Type hiding              ( substTy, substTyVarBndr, substTyVar )
 import qualified Coercion
@@ -516,16 +513,16 @@ substId :: SimplEnv -> InId -> SimplSR
 -- Returns DoneEx only on a non-Var expression
 substId (SimplEnv { seInScope = in_scope, seIdSubst = ids }) v
   = case lookupVarEnv ids v of  -- Note [Global Ids in the substitution]
-        Nothing               -> DoneId (refine in_scope v)
-        Just (DoneId v)       -> DoneId (refine in_scope v)
-        Just (DoneEx (Var v)) -> DoneId (refine in_scope v)
+        Nothing               -> DoneId (refineFromInScope in_scope v)
+        Just (DoneId v)       -> DoneId (refineFromInScope in_scope v)
+        Just (DoneEx (Var v)) -> DoneId (refineFromInScope in_scope v)
         Just res              -> res    -- DoneEx non-var, or ContEx
 
         -- Get the most up-to-date thing from the in-scope set
         -- Even though it isn't in the substitution, it may be in
         -- the in-scope set with better IdInfo
-refine :: InScopeSet -> Var -> Var
-refine in_scope v
+refineFromInScope :: InScopeSet -> Var -> Var
+refineFromInScope in_scope v
   | isLocalId v = case lookupInScope in_scope v of
                   Just v' -> v'
                   Nothing -> WARN( True, ppr v ) v  -- This is an error!
@@ -538,7 +535,7 @@ lookupRecBndr (SimplEnv { seInScope = in_scope, seIdSubst = ids }) v
   = case lookupVarEnv ids v of
         Just (DoneId v) -> v
         Just _ -> pprPanic "lookupRecBndr" (ppr v)
-        Nothing -> refine in_scope v
+        Nothing -> refineFromInScope in_scope v
 
 {-
 ************************************************************************
@@ -551,10 +548,8 @@ lookupRecBndr (SimplEnv { seInScope = in_scope, seIdSubst = ids }) v
 These functions are in the monad only so that they can be made strict via seq.
 -}
 
-simplBinders, simplLamBndrs
-        :: SimplEnv -> [InBndr] -> SimplM (SimplEnv, [OutBndr])
+simplBinders :: SimplEnv -> [InBndr] -> SimplM (SimplEnv, [OutBndr])
 simplBinders  env bndrs = mapAccumLM simplBinder  env bndrs
-simplLamBndrs env bndrs = mapAccumLM simplLamBndr env bndrs
 
 -------------
 simplBinder :: SimplEnv -> InBndr -> SimplM (SimplEnv, OutBndr)
@@ -569,23 +564,6 @@ simplBinder env bndr
   | otherwise     = do  { let (env', id) = substIdBndr env bndr
                         ; seqId id `seq` return (env', id) }
 
--------------
-simplLamBndr :: SimplEnv -> Var -> SimplM (SimplEnv, Var)
--- 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 && hasSomeUnfolding old_unf = seqId id2 `seq` return (env2, id2)  -- Special case
-  | otherwise                             = simplBinder env bndr                -- Normal case
-  where
-    old_unf = idUnfolding bndr
-    (env1, id1) = substIdBndr env bndr
-    id2  = id1 `setIdUnfolding` substUnfolding env old_unf
-    env2 = modifyInScope env1 id2
-
 ---------------
 simplNonRecBndr :: SimplEnv -> InBndr -> SimplM (SimplEnv, OutBndr)
 -- A non-recursive let binder
@@ -696,29 +674,8 @@ Note [Robust OccInfo]
 It's important that we *do* retain the loop-breaker OccInfo, because
 that's what stops the Id getting inlined infinitely, in the body of
 the letrec.
-
-
-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 [Loop breaking and RULES] in OccAnal.
 -}
 
-addBndrRules :: SimplEnv -> InBndr -> OutBndr -> (SimplEnv, OutBndr)
--- Rules are added back into the bin
-addBndrRules env in_id out_id
-  | isEmptySpecInfo old_rules = (env, out_id)
-  | otherwise = (modifyInScope env final_id, final_id)
-  where
-    subst     = mkCoreSubst (text "local rules") env
-    old_rules = idSpecialisation in_id
-    new_rules = CoreSubst.substSpec subst out_id old_rules
-    final_id  = out_id `setIdSpecialisation` new_rules
 
 {-
 ************************************************************************
@@ -760,22 +717,6 @@ substCoVarBndr env cv
 substCo :: SimplEnv -> Coercion -> Coercion
 substCo env co = Coercion.substCo (getCvSubst env) co
 
--- When substituting in rules etc we can get CoreSubst to do the work
--- But CoreSubst uses a simpler form of IdSubstEnv, so we must impedence-match
--- here.  I think the this will not usually result in a lot of work;
--- the substitutions are typically small, and laziness will avoid work in many cases.
-
-mkCoreSubst  :: SDoc -> SimplEnv -> CoreSubst.Subst
-mkCoreSubst doc (SimplEnv { seInScope = in_scope, seTvSubst = tv_env, seCvSubst = cv_env, seIdSubst = id_env })
-  = mk_subst tv_env cv_env id_env
-  where
-    mk_subst tv_env cv_env id_env = CoreSubst.mkSubst in_scope tv_env cv_env (mapVarEnv fiddle id_env)
-
-    fiddle (DoneEx e)          = e
-    fiddle (DoneId v)          = Var v
-    fiddle (ContEx tv cv id e) = CoreSubst.substExpr (text "mkCoreSubst" <+> doc) (mk_subst tv cv id) e
-                                                -- Don't shortcut here
-
 ------------------
 substIdType :: SimplEnv -> Id -> Id
 substIdType (SimplEnv { seInScope = in_scope,  seTvSubst = tv_env }) id
@@ -786,16 +727,3 @@ substIdType (SimplEnv { seInScope = in_scope,  seTvSubst = tv_env }) id
                 -- in a Note in the id's type itself
   where
     old_ty = idType id
-
-------------------
-substExpr :: SDoc -> SimplEnv -> CoreExpr -> CoreExpr
-substExpr doc env
-  = CoreSubst.substExpr (text "SimplEnv.substExpr1" <+> doc)
-                        (mkCoreSubst (text "SimplEnv.substExpr2" <+> doc) env)
-  -- Do *not* short-cut in the case of an empty substitution
-  -- See Note [SimplEnv invariants]
-
-substUnfolding :: SimplEnv -> Unfolding -> Unfolding
-substUnfolding env unf = CoreSubst.substUnfolding (mkCoreSubst (text "subst-unfolding") env) unf
-  -- Do *not* short-cut in the case of an empty substitution
-  -- See Note [SimplEnv invariants]
diff --git a/compiler/simplCore/SimplUtils.hs b/compiler/simplCore/SimplUtils.hs
index 4c469d111f..7dbe3fc4b6 100644
--- a/compiler/simplCore/SimplUtils.hs
+++ b/compiler/simplCore/SimplUtils.hs
@@ -20,10 +20,10 @@ module SimplUtils (
         SimplCont(..), DupFlag(..),
         isSimplified,
         contIsDupable, contResultType, contHoleType,
-        contIsTrivial, contArgs, 
+        contIsTrivial, contArgs,
         countValArgs, countArgs,
         mkBoringStop, mkRhsStop, mkLazyArgStop, contIsRhsOrArg,
-        interestingCallContext, interestingArg,
+        interestingCallContext,
 
         -- ArgInfo
         ArgInfo(..), ArgSpec(..), mkArgInfo,
@@ -54,6 +54,7 @@ import SimplMonad
 import Type     hiding( substTy )
 import Coercion hiding( substCo, substTy )
 import DataCon          ( dataConWorkId )
+import VarEnv
 import VarSet
 import BasicTypes
 import Util
@@ -390,77 +391,10 @@ contArgs cont
     go args (CastIt _ k)                = go args k
     go args k                           = (False, reverse args, k)
 
-    is_interesting arg se = interestingArg (substExpr (text "contArgs") se arg)
+    is_interesting arg se = interestingArg se arg
                    -- Do *not* use short-cutting substitution here
                    -- because we want to get as much IdInfo as possible
 
-{-
-Note [Interesting call context]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We want to avoid inlining an expression where there can't possibly be
-any gain, such as in an argument position.  Hence, if the continuation
-is interesting (eg. a case scrutinee, application etc.) then we
-inline, otherwise we don't.
-
-Previously some_benefit used to return True only if the variable was
-applied to some value arguments.  This didn't work:
-
-        let x = _coerce_ (T Int) Int (I# 3) in
-        case _coerce_ Int (T Int) x of
-                I# y -> ....
-
-we want to inline x, but can't see that it's a constructor in a case
-scrutinee position, and some_benefit is False.
-
-Another example:
-
-dMonadST = _/\_ t -> :Monad (g1 _@_ t, g2 _@_ t, g3 _@_ t)
-
-....  case dMonadST _@_ x0 of (a,b,c) -> ....
-
-we'd really like to inline dMonadST here, but we *don't* want to
-inline if the case expression is just
-
-        case x of y { DEFAULT -> ... }
-
-since we can just eliminate this case instead (x is in WHNF).  Similar
-applies when x is bound to a lambda expression.  Hence
-contIsInteresting looks for case expressions with just a single
-default case.
--}
-
-interestingCallContext :: SimplCont -> CallCtxt
--- See Note [Interesting call context]
-interestingCallContext cont
-  = interesting cont
-  where
-    interesting (Select _ _bndr _ _ _) = CaseCtxt
-    interesting (ApplyToVal {})        = ValAppCtxt
-        -- Can happen if we have (f Int |> co) y
-        -- If f has an INLINE prag we need to give it some
-        -- motivation to inline. See Note [Cast then apply]
-        -- in CoreUnfold
-    interesting (StrictArg _ cci _)         = cci
-    interesting (StrictBind {})             = BoringCtxt
-    interesting (Stop _ cci)                = cci
-    interesting (TickIt _ k)                = interesting k
-    interesting (ApplyToTy { sc_cont = k }) = interesting k
-    interesting (CastIt _ k)                = interesting k
-        -- If this call is the arg of a strict function, the context
-        -- is a bit interesting.  If we inline here, we may get useful
-        -- evaluation information to avoid repeated evals: e.g.
-        --      x + (y * z)
-        -- Here the contIsInteresting makes the '*' keener to inline,
-        -- which in turn exposes a constructor which makes the '+' inline.
-        -- Assuming that +,* aren't small enough to inline regardless.
-        --
-        -- It's also very important to inline in a strict context for things
-        -- like
-        --              foldr k z (f x)
-        -- Here, the context of (f x) is strict, and if f's unfolding is
-        -- a build it's *great* to inline it here.  So we must ensure that
-        -- the context for (f x) is not totally uninteresting.
-
 
 -------------------
 mkArgInfo :: Id
@@ -541,6 +475,80 @@ it'll just be floated out again.  Even if f has lots of discounts
 on its first argument -- it must be saturated for these to kick in
 -}
 
+
+{-
+************************************************************************
+*                                                                      *
+        Interesting arguments
+*                                                                      *
+************************************************************************
+
+Note [Interesting call context]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We want to avoid inlining an expression where there can't possibly be
+any gain, such as in an argument position.  Hence, if the continuation
+is interesting (eg. a case scrutinee, application etc.) then we
+inline, otherwise we don't.
+
+Previously some_benefit used to return True only if the variable was
+applied to some value arguments.  This didn't work:
+
+        let x = _coerce_ (T Int) Int (I# 3) in
+        case _coerce_ Int (T Int) x of
+                I# y -> ....
+
+we want to inline x, but can't see that it's a constructor in a case
+scrutinee position, and some_benefit is False.
+
+Another example:
+
+dMonadST = _/\_ t -> :Monad (g1 _@_ t, g2 _@_ t, g3 _@_ t)
+
+....  case dMonadST _@_ x0 of (a,b,c) -> ....
+
+we'd really like to inline dMonadST here, but we *don't* want to
+inline if the case expression is just
+
+        case x of y { DEFAULT -> ... }
+
+since we can just eliminate this case instead (x is in WHNF).  Similar
+applies when x is bound to a lambda expression.  Hence
+contIsInteresting looks for case expressions with just a single
+default case.
+-}
+
+interestingCallContext :: SimplCont -> CallCtxt
+-- See Note [Interesting call context]
+interestingCallContext cont
+  = interesting cont
+  where
+    interesting (Select _ _bndr _ _ _) = CaseCtxt
+    interesting (ApplyToVal {})        = ValAppCtxt
+        -- Can happen if we have (f Int |> co) y
+        -- If f has an INLINE prag we need to give it some
+        -- motivation to inline. See Note [Cast then apply]
+        -- in CoreUnfold
+    interesting (StrictArg _ cci _)         = cci
+    interesting (StrictBind {})             = BoringCtxt
+    interesting (Stop _ cci)                = cci
+    interesting (TickIt _ k)                = interesting k
+    interesting (ApplyToTy { sc_cont = k }) = interesting k
+    interesting (CastIt _ k)                = interesting k
+        -- If this call is the arg of a strict function, the context
+        -- is a bit interesting.  If we inline here, we may get useful
+        -- evaluation information to avoid repeated evals: e.g.
+        --      x + (y * z)
+        -- Here the contIsInteresting makes the '*' keener to inline,
+        -- which in turn exposes a constructor which makes the '+' inline.
+        -- Assuming that +,* aren't small enough to inline regardless.
+        --
+        -- It's also very important to inline in a strict context for things
+        -- like
+        --              foldr k z (f x)
+        -- Here, the context of (f x) is strict, and if f's unfolding is
+        -- a build it's *great* to inline it here.  So we must ensure that
+        -- the context for (f x) is not totally uninteresting.
+
 interestingArgContext :: [CoreRule] -> SimplCont -> Bool
 -- If the argument has form (f x y), where x,y are boring,
 -- and f is marked INLINE, then we don't want to inline f.
@@ -579,6 +587,77 @@ interestingArgContext rules call_cont
     interesting RuleArgCtxt = True
     interesting _           = False
 
+
+{- Note [Interesting arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+An argument is interesting if it deserves a discount for unfoldings
+with a discount in that argument position.  The idea is to avoid
+unfolding a function that is applied only to variables that have no
+unfolding (i.e. they are probably lambda bound): f x y z There is
+little point in inlining f here.
+
+Generally, *values* (like (C a b) and (\x.e)) deserve discounts.  But
+we must look through lets, eg (let x = e in C a b), because the let will
+float, exposing the value, if we inline.  That makes it different to
+exprIsHNF.
+
+Before 2009 we said it was interesting if the argument had *any* structure
+at all; i.e. (hasSomeUnfolding v).  But does too much inlining; see Trac #3016.
+
+But we don't regard (f x y) as interesting, unless f is unsaturated.
+If it's saturated and f hasn't inlined, then it's probably not going
+to now!
+
+Note [Conlike is interesting]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+        f d = ...((*) d x y)...
+        ... f (df d')...
+where df is con-like. Then we'd really like to inline 'f' so that the
+rule for (*) (df d) can fire.  To do this
+  a) we give a discount for being an argument of a class-op (eg (*) d)
+  b) we say that a con-like argument (eg (df d)) is interesting
+-}
+
+interestingArg :: SimplEnv -> CoreExpr -> ArgSummary
+-- See Note [Interesting arguments]
+interestingArg env e = go env 0 e
+  where
+    -- n is # value args to which the expression is applied
+    go env n (Var v)
+       | SimplEnv { seIdSubst = ids, seInScope = in_scope } <- env
+       = case lookupVarEnv ids v of
+           Nothing                     -> go_var n (refineFromInScope in_scope v)
+           Just (DoneId v')            -> go_var n (refineFromInScope in_scope v')
+           Just (DoneEx e)             -> go (zapSubstEnv env)             n e
+           Just (ContEx tvs cvs ids e) -> go (setSubstEnv env tvs cvs ids) n e
+
+    go _   _ (Lit {})              = ValueArg
+    go _   _ (Type _)              = TrivArg
+    go _   _ (Coercion _)          = TrivArg
+    go env n (App fn (Type _))     = go env n fn
+    go env n (App fn (Coercion _)) = go env n fn
+    go env n (App fn _)            = go env (n+1) fn
+    go env n (Tick _ a)            = go env n a
+    go env n (Cast e _)            = go env n e
+    go env n (Lam v e)
+       | isTyVar v                 = go env n     e
+       | n>0                       = go env (n-1) e
+       | otherwise                 = ValueArg
+    go env n (Let _ e)             = case go env n e of { ValueArg -> ValueArg; _ -> NonTrivArg }
+    go _ _ (Case {})               = NonTrivArg
+
+    go_var n v
+       | isConLikeId v     = ValueArg   -- Experimenting with 'conlike' rather that
+                                        --    data constructors here
+       | idArity v > n     = ValueArg   -- Catches (eg) primops with arity but no unfolding
+       | n > 0             = NonTrivArg -- Saturated or unknown call
+       | conlike_unfolding = ValueArg   -- n==0; look for an interesting unfolding
+                                        -- See Note [Conlike is interesting]
+       | otherwise         = TrivArg    -- n==0, no useful unfolding
+       where
+         conlike_unfolding = isConLikeUnfolding (idUnfolding v)
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/simplCore/Simplify.hs b/compiler/simplCore/Simplify.hs
index aee62000fe..d708f4bf85 100644
--- a/compiler/simplCore/Simplify.hs
+++ b/compiler/simplCore/Simplify.hs
@@ -6,7 +6,7 @@
 
 {-# LANGUAGE CPP #-}
 
-module Simplify ( simplTopBinds, simplExpr ) where
+module Simplify ( simplTopBinds, simplExpr, simplRule ) where
 
 #include "HsVersions.h"
 
@@ -21,7 +21,7 @@ import Id
 import MkId             ( seqId, voidPrimId )
 import MkCore           ( mkImpossibleExpr, castBottomExpr )
 import IdInfo
-import Name             ( mkSystemVarName, isExternalName )
+import Name             ( Name, mkSystemVarName, isExternalName )
 import Coercion hiding  ( substCo, substTy, substCoVar, extendTvSubst )
 import OptCoercion      ( optCoercion )
 import FamInstEnv       ( topNormaliseType_maybe )
@@ -36,14 +36,13 @@ import CoreUnfold
 import CoreUtils
 import CoreArity
 --import PrimOp           ( tagToEnumKey ) -- temporalily commented out. See #8326
-import Rules            ( lookupRule, getRules )
+import Rules            ( mkSpecInfo, 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 Control.Monad
-import Data.List        ( mapAccumL )
 import Outputable
 import FastString
 import Pair
@@ -234,9 +233,8 @@ simplTopBinds env0 binds0
                                       ; 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_bind env (NonRec b r) = do { (env', b') <- addBndrRules env b (lookupRecBndr env b)
+                                     ; simplRecOrTopPair env' TopLevel NonRecursive b b' r }
 
 {-
 ************************************************************************
@@ -253,17 +251,17 @@ simplRecBind :: SimplEnv -> TopLevelFlag
              -> [(InId, InExpr)]
              -> SimplM SimplEnv
 simplRecBind env0 top_lvl pairs0
-  = do  { let (env_with_info, triples) = mapAccumL add_rules env0 pairs0
+  = do  { (env_with_info, triples) <- mapAccumLM 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
   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
 
@@ -678,7 +676,7 @@ completeBind env top_lvl old_bndr new_bndr new_rhs
       ; (new_arity, final_rhs) <- tryEtaExpandRhs 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 old_bndr final_rhs old_unf
 
       ; dflags <- getDynFlags
       ; if postInlineUnconditionally dflags env top_lvl new_bndr occ_info
@@ -729,7 +727,7 @@ addPolyBind :: TopLevelFlag -> SimplEnv -> OutBind -> SimplM SimplEnv
 -- 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
+  = do  { unfolding <- simplLetUnfolding 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 $
@@ -743,66 +741,8 @@ addPolyBind _ env bind@(Rec _)
         -- 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.
-
-      _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.
-  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]
-~~~~~~~~~~~~~~~~~~~~~
+{- 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,22 +764,6 @@ 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.
-
-* 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 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.
-
 Note [Setting the demand info]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If the unfolding is a value, the demand info may
@@ -1204,14 +1128,14 @@ rebuild env expr cont
 simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont
           -> SimplM (SimplEnv, 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
+         | s1 `eqType` k1 = return cont    -- is a no-op
 
        add_coerce co1 (Pair s1 _k2) (CastIt co2 cont)
          | (Pair _l1 t1) <- coercionKind co2
@@ -1224,15 +1148,16 @@ simplCast env body co0 cont0
                 -- 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
+         , s1 `eqType` t1  = return cont     -- The coerces cancel out
+         | otherwise       = return (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 }
+           do { cont' <- addCoerce new_cast tail
+              ; return (cont { sc_cont = cont' }) }
          where
            new_cast = mkInstCo co arg_ty
 
@@ -1254,19 +1179,28 @@ simplCast env body co0 cont0
                 -- 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 }
+         = do { (dup', arg_se', arg') <- simplArg env dup arg_se arg
+              ; cont'                <- addCoerce co2 cont
+              ; return (ApplyToVal { sc_arg  = mkCast arg' (mkSymCo co1)
+                                   , sc_env  = arg_se'
+                                   , sc_dup  = dup'
+                                   , sc_cont = 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
+       add_coerce co _ cont = return (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 `setInScope` env) arg
+       ; return (Simplified, zapSubstEnv arg_env, arg') }
 
 {-
 ************************************************************************
@@ -1325,6 +1259,29 @@ simplLam env bndrs body cont
         ; new_lam <- mkLam bndrs' body' cont
         ; rebuild env' new_lam cont }
 
+simplLamBndrs :: SimplEnv -> [InBndr] -> SimplM (SimplEnv, [OutBndr])
+simplLamBndrs env bndrs = mapAccumLM simplLamBndr env bndrs
+
+-------------
+simplLamBndr :: SimplEnv -> Var -> SimplM (SimplEnv, Var)
+-- 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 && hasSomeUnfolding old_unf   -- Special case
+  = do { (env1, bndr1) <- simplBinder env bndr
+       ; unf'          <- simplUnfolding env1 NotTopLevel bndr old_unf
+       ; let bndr2 = bndr1 `setIdUnfolding` unf'
+       ; return (modifyInScope env1 bndr2, bndr2) }
+
+  | otherwise
+  = simplBinder env bndr                -- Normal case
+  where
+    old_unf = idUnfolding bndr
+
 ------------------
 simplNonRecE :: SimplEnv
              -> InBndr                  -- The binder
@@ -1371,7 +1328,7 @@ simplNonRecE env bndr (rhs, rhs_se) (bndrs, body) cont
            | otherwise
            -> ASSERT( not (isTyVar bndr) )
               do { (env1, bndr1) <- simplNonRecBndr env bndr
-                 ; let (env2, bndr2) = addBndrRules env1 bndr bndr1
+                 ; (env2, bndr2) <- addBndrRules env1 bndr bndr1
                  ; env3 <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
                  ; simplLam env3 bndrs body cont }
 
@@ -1929,18 +1886,20 @@ rebuildCase env scrut case_bndr alts@[(_, bndrs, rhs)] cont
   --     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)
+  = do { let scrut_ty = exprType scrut
+             rhs_ty   = substTy env (exprType rhs)
              out_args = [ TyArg { as_arg_ty  = scrut_ty
                                 , as_hole_ty = seq_id_ty }
-                        , TyArg { as_arg_ty  = exprType rhs'
+                        , TyArg { as_arg_ty  = rhs_ty
                                 , as_hole_ty = applyTy seq_id_ty scrut_ty }
-                        , ValArg scrut, ValArg rhs']
-                      -- Lazily evaluated, so we don't do most of this
+                        , ValArg scrut]
+             rule_cont = ApplyToVal { sc_dup = NoDup, sc_arg = rhs
+                                    , sc_env = env, sc_cont = cont }
+             env' = zapSubstEnv env
+             -- 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
+       ; mb_rule <- tryRules env' (getRules rule_base seqId) seqId out_args rule_cont
        ; case mb_rule of
            Just (rule_rhs, cont') -> simplExprF env' rule_rhs cont'
            Nothing                -> reallyRebuildCase env scrut case_bndr alts cont }
@@ -2413,15 +2372,15 @@ 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 })
+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
+        ; (_, se', arg') <- simplArg env' dup se arg
         ; (env'', arg'') <- makeTrivial NotTopLevel env' arg'
-        ; let app_cont = ApplyToVal { sc_arg = arg'', sc_env = zapSubstEnv env''
+        ; let app_cont = ApplyToVal { sc_arg = arg'', sc_env = se'
                                     , sc_dup = OkToDup, sc_cont = dup_cont }
         ; return (env'', app_cont, nodup_cont) }
 
@@ -2873,4 +2832,138 @@ whether to use a real join point or just duplicate the continuation:
 
 Hence: check whether the case binder's type is unlifted, because then
 the outer case is *not* a seq.
+
+************************************************************************
+*                                                                      *
+                    Unfoldings
+*                                                                      *
+************************************************************************
 -}
+
+simplLetUnfolding :: SimplEnv-> TopLevelFlag
+                  -> InId
+                  -> OutExpr
+                  -> Unfolding -> SimplM Unfolding
+simplLetUnfolding env top_lvl id new_rhs unf
+  | isStableUnfolding unf
+  = simplUnfolding env top_lvl id unf
+  | otherwise
+  = bottoming `seq`  -- See Note [Force bottoming field]
+    do { dflags <- getDynFlags
+       ; return (mkUnfolding dflags InlineRhs (isTopLevel 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.
+  where
+    bottoming = isBottomingId id
+
+simplUnfolding :: SimplEnv-> TopLevelFlag -> InId -> Unfolding -> SimplM Unfolding
+-- Note [Setting the new unfolding]
+simplUnfolding env top_lvl id unf
+  = case unf of
+      NoUnfolding -> return unf
+      OtherCon {} -> return unf
+
+      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.
+
+        | otherwise -> return noUnfolding   -- Discard unstable unfoldings
+  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 [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.
+
+* 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 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.
+
+************************************************************************
+*                                                                      *
+                    Rules
+*                                                                      *
+************************************************************************
+
+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 [Loop breaking and RULES] in OccAnal.
+-}
+
+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 <- mapM (simplRule env (Just (idName out_id))) old_rules
+       ; let final_id  = out_id `setIdSpecialisation` mkSpecInfo new_rules
+       ; return (modifyInScope env final_id, final_id) }
+  where
+    old_rules = specInfoRules (idSpecialisation in_id)
+
+simplRule :: SimplEnv -> Maybe Name -> CoreRule -> SimplM CoreRule
+simplRule _   _         rule@(BuiltinRule {}) = return rule
+simplRule env mb_new_nm rule@(Rule { ru_bndrs = bndrs, ru_args = args
+                                   , ru_fn = fn_name, ru_rhs = rhs
+                                   , ru_act = act })
+  = do { (env, bndrs') <- simplBinders env bndrs
+       ; let rule_env = updMode (updModeForStableUnfoldings act) env
+       ; args' <- mapM (simplExpr rule_env) args
+       ; rhs'  <- simplExpr rule_env rhs
+       ; return (rule { ru_bndrs = bndrs'
+                      , ru_fn    = mb_new_nm `orElse` fn_name
+                      , ru_args  = args'
+                      , ru_rhs   = rhs' }) }
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index bb6ceaa32f..43f0b23640 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -636,8 +636,10 @@ test('T9872d',
 test('T9961',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 772510192, 5),
+          [(wordsize(64), 663978160, 5),
           # 2015-01-12    807117816   Initally created
+          # 2015-spring   772510192   Got better
+          # 2015-05-22    663978160   Fix for #10370 improves it more
            (wordsize(32), 375647160, 5)
           ]),
       ],
diff --git a/testsuite/tests/simplCore/should_compile/T7785.stderr b/testsuite/tests/simplCore/should_compile/T7785.stderr
index db80b9965b..f0b9117543 100644
--- a/testsuite/tests/simplCore/should_compile/T7785.stderr
+++ b/testsuite/tests/simplCore/should_compile/T7785.stderr
@@ -4,5 +4,7 @@
     forall ($dMyFunctor :: MyFunctor []) (irred :: Domain [] Int).
       shared @ [] $dMyFunctor irred
       = bar_$sshared
+"SPEC/Foo myfmap @ []" [ALWAYS]
+    forall (tpl :: MyFunctor []). myfmap @ [] tpl = $cmyfmap
 
 
diff --git a/testsuite/tests/simplCore/should_compile/rule2.stderr b/testsuite/tests/simplCore/should_compile/rule2.stderr
index a9f3a3b0f7..082f9aa134 100644
--- a/testsuite/tests/simplCore/should_compile/rule2.stderr
+++ b/testsuite/tests/simplCore/should_compile/rule2.stderr
@@ -10,13 +10,14 @@
 
 
 ==================== Grand total simplifier statistics ====================
-Total ticks:     11
+Total ticks:     12
 
 2 PreInlineUnconditionally
   1 f
   1 lvl
 1 UnfoldingDone 1 Roman.bar
 1 RuleFired 1 foo/bar
+1 EtaReduction 1 ds
 7 BetaReduction
   1 f
   1 m
diff --git a/testsuite/tests/simplCore/should_run/SeqRule.hs b/testsuite/tests/simplCore/should_run/SeqRule.hs
index b1569efd7b..29a1951209 100644
--- a/testsuite/tests/simplCore/should_run/SeqRule.hs
+++ b/testsuite/tests/simplCore/should_run/SeqRule.hs
@@ -10,7 +10,7 @@ module Main where
 f x = not x
 
 {-# RULES 
-     "f/seq" forall n e.  seq (f n) e = True
+     "f/seq" forall n.  seq (f n) = const True
  #-}
 
 main = print (seq (f True) False)