Super-monster patch implementing the new typechecker -- at last
[ghc-hetmet.git] / compiler / simplCore / OccurAnal.lhs
index b92239e..a37b5f1 100644 (file)
@@ -19,23 +19,26 @@ module OccurAnal (
 
 import CoreSyn
 import CoreFVs
 
 import CoreSyn
 import CoreFVs
-import CoreUtils        ( exprIsTrivial, isDefaultAlt )
-import Coercion                ( mkSymCoercion )
+import Type            ( tyVarsOfType )
+import CoreUtils        ( exprIsTrivial, isDefaultAlt, mkCoerceI, isExpandableApp )
+import Coercion                ( CoercionI(..), mkSymCoI )
 import Id
 import Id
-import IdInfo
+import Name            ( localiseName )
 import BasicTypes
 
 import VarSet
 import VarEnv
 import BasicTypes
 
 import VarSet
 import VarEnv
+import Var             ( Var, varUnique )
 
 import Maybes           ( orElse )
 import Digraph          ( SCC(..), stronglyConnCompFromEdgedVerticesR )
 import PrelNames        ( buildIdKey, foldrIdKey, runSTRepIdKey, augmentIdKey )
 import Unique           ( Unique )
 import UniqFM           ( keysUFM, intersectUFM_C, foldUFM_Directly )
 
 import Maybes           ( orElse )
 import Digraph          ( SCC(..), stronglyConnCompFromEdgedVerticesR )
 import PrelNames        ( buildIdKey, foldrIdKey, runSTRepIdKey, augmentIdKey )
 import Unique           ( Unique )
 import UniqFM           ( keysUFM, intersectUFM_C, foldUFM_Directly )
-import Util             ( mapAndUnzip )
+import Util             ( mapAndUnzip, filterOut )
+import Bag
 import Outputable
 import Outputable
-
+import FastString
 import Data.List
 \end{code}
 
 import Data.List
 \end{code}
 
@@ -49,18 +52,21 @@ import Data.List
 Here's the externally-callable interface:
 
 \begin{code}
 Here's the externally-callable interface:
 
 \begin{code}
-occurAnalysePgm :: [CoreBind] -> [CoreBind]
-occurAnalysePgm binds
+occurAnalysePgm :: [CoreBind] -> [CoreRule] -> [CoreBind]
+occurAnalysePgm binds rules
   = snd (go initOccEnv binds)
   where
   = snd (go initOccEnv binds)
   where
+    initial_details = addIdOccs emptyDetails (rulesFreeVars rules)
+    -- The RULES keep things alive!
+
     go :: OccEnv -> [CoreBind] -> (UsageDetails, [CoreBind])
     go _ []
     go :: OccEnv -> [CoreBind] -> (UsageDetails, [CoreBind])
     go _ []
-        = (emptyDetails, [])
+        = (initial_details, [])
     go env (bind:binds)
         = (final_usage, bind' ++ binds')
         where
            (bs_usage, binds')   = go env binds
     go env (bind:binds)
         = (final_usage, bind' ++ binds')
         where
            (bs_usage, binds')   = go env binds
-           (final_usage, bind') = occAnalBind env bind bs_usage
+           (final_usage, bind') = occAnalBind env env bind bs_usage
 
 occurAnalyseExpr :: CoreExpr -> CoreExpr
         -- Do occurrence analysis, and discard occurence info returned
 
 occurAnalyseExpr :: CoreExpr -> CoreExpr
         -- Do occurrence analysis, and discard occurence info returned
@@ -78,14 +84,15 @@ Bindings
 ~~~~~~~~
 
 \begin{code}
 ~~~~~~~~
 
 \begin{code}
-occAnalBind :: OccEnv
+occAnalBind :: OccEnv          -- The incoming OccEnv
+           -> OccEnv           -- Same, but trimmed by (binderOf bind)
             -> CoreBind
             -> UsageDetails             -- Usage details of scope
             -> (UsageDetails,           -- Of the whole let(rec)
                 [CoreBind])
 
             -> CoreBind
             -> UsageDetails             -- Usage details of scope
             -> (UsageDetails,           -- Of the whole let(rec)
                 [CoreBind])
 
-occAnalBind env (NonRec binder rhs) body_usage
-  | isTyVar binder                     -- A type let; we don't gather usage info
+occAnalBind env _ (NonRec binder rhs) body_usage
+  | isTyCoVar binder                   -- A type let; we don't gather usage info
   = (body_usage, [NonRec binder rhs])
 
   | not (binder `usedIn` body_usage)    -- It's not mentioned
   = (body_usage, [NonRec binder rhs])
 
   | not (binder `usedIn` body_usage)    -- It's not mentioned
@@ -171,10 +178,10 @@ However things are made quite a bit more complicated by RULES.  Remember
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     We avoid infinite inlinings by choosing loop breakers, and
     ensuring that a loop breaker cuts each loop.  But what is a
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
     We avoid infinite inlinings by choosing loop breakers, and
     ensuring that a loop breaker cuts each loop.  But what is a
-    "loop"?  In particular, a RULES is like an equation for 'f' that
-    is *always* inlined if it are applicable.  We do *not* disable
+    "loop"?  In particular, a RULE is like an equation for 'f' that
+    is *always* inlined if it is applicable.  We do *not* disable
     rules for loop-breakers.  It's up to whoever makes the rules to
     rules for loop-breakers.  It's up to whoever makes the rules to
-    make sure that the rules themselves alwasys terminate.  See Note
+    make sure that the rules themselves always terminate.  See Note
     [Rules for recursive functions] in Simplify.lhs
 
     Hence, if
     [Rules for recursive functions] in Simplify.lhs
 
     Hence, if
@@ -220,13 +227,15 @@ However things are made quite a bit more complicated by RULES.  Remember
 
     So we must *not* postInlineUnconditionally 'g', even though
     its RHS turns out to be trivial.  (I'm assuming that 'g' is
 
     So we must *not* postInlineUnconditionally 'g', even though
     its RHS turns out to be trivial.  (I'm assuming that 'g' is
-    not choosen as a loop breaker.)
+    not choosen as a loop breaker.)  Why not?  Because then we
+    drop the binding for 'g', which leaves it out of scope in the
+    RULE!
 
     We "solve" this by making g a "weak" or "rules-only" loop breaker,
     with OccInfo = IAmLoopBreaker True.  A normal "strong" loop breaker
     has IAmLoopBreaker False.  So
 
 
     We "solve" this by making g a "weak" or "rules-only" loop breaker,
     with OccInfo = IAmLoopBreaker True.  A normal "strong" loop breaker
     has IAmLoopBreaker False.  So
 
-                                Inline  postInlineUnconditinoally
+                                Inline  postInlineUnconditionally
         IAmLoopBreaker False    no      no
         IAmLoopBreaker True     yes     no
         other                   yes     yes
         IAmLoopBreaker False    no      no
         IAmLoopBreaker True     yes     no
         other                   yes     yes
@@ -237,14 +246,23 @@ However things are made quite a bit more complicated by RULES.  Remember
   * Note [Rule dependency info]
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~
     The VarSet in a SpecInfo is used for dependency analysis in the
   * Note [Rule dependency info]
     ~~~~~~~~~~~~~~~~~~~~~~~~~~~
     The VarSet in a SpecInfo is used for dependency analysis in the
-    occurrence analyser.  We must track free vars in *both* lhs and rhs.  Why both?
-    Consider
+    occurrence analyser.  We must track free vars in *both* lhs and rhs.  
+    Hence use of idRuleVars, rather than idRuleRhsVars in addRuleUsage.  
+    Why both? Consider
         x = y
         RULE f x = 4
     Then if we substitute y for x, we'd better do so in the
     rule's LHS too, so we'd better ensure the dependency is respected
 
 
         x = y
         RULE f x = 4
     Then if we substitute y for x, we'd better do so in the
     rule's LHS too, so we'd better ensure the dependency is respected
 
 
+  * Note [Inline rules]
+    ~~~~~~~~~~~~~~~~~~~
+    None of the above stuff about RULES applies to Inline Rules,
+    stored in a CoreUnfolding.  The unfolding, if any, is simplified
+    at the same time as the regular RHS of the function, so it should
+    be treated *exactly* like an extra RHS.
+
+
 Example [eftInt]
 ~~~~~~~~~~~~~~~
 Example (from GHC.Enum):
 Example [eftInt]
 ~~~~~~~~~~~~~~~
 Example (from GHC.Enum):
@@ -280,7 +298,7 @@ This showed up when compiling Control.Concurrent.Chan.getChanContents.
 
 
 \begin{code}
 
 
 \begin{code}
-occAnalBind env (Rec pairs) body_usage
+occAnalBind _ env (Rec pairs) body_usage
   = foldr occAnalRec (body_usage, []) sccs
        -- For a recursive group, we 
        --      * occ-analyse all the RHSs
   = foldr occAnalRec (body_usage, []) sccs
        -- For a recursive group, we 
        --      * occ-analyse all the RHSs
@@ -297,11 +315,13 @@ occAnalBind env (Rec pairs) body_usage
     rec_edges = {-# SCC "occAnalBind.assoc" #-}  map make_node pairs
     
     make_node (bndr, rhs)
     rec_edges = {-# SCC "occAnalBind.assoc" #-}  map make_node pairs
     
     make_node (bndr, rhs)
-       = (ND bndr rhs' rhs_usage rhs_fvs, idUnique bndr, out_edges)
+       = (ND bndr rhs' all_rhs_usage rhs_fvs, varUnique bndr, out_edges)
        where
          (rhs_usage, rhs') = occAnalRhs env bndr rhs
        where
          (rhs_usage, rhs') = occAnalRhs env bndr rhs
-         rhs_fvs = intersectUFM_C (\b _ -> b) bndr_set rhs_usage
-         out_edges = keysUFM (rhs_fvs `unionVarSet` idRuleVars bndr)
+         all_rhs_usage = addIdOccs rhs_usage rule_vars -- Note [Rules are extra RHSs]
+         rhs_fvs   = intersectUFM_C (\b _ -> b) bndr_set rhs_usage
+         out_edges = keysUFM (rhs_fvs `unionVarSet` rule_vars)
+          rule_vars = idRuleVars bndr      -- See Note [Rule dependency info]
         -- (a -> b) means a mentions b
         -- Given the usage details (a UFM that gives occ info for each free var of
         -- the RHS) we can get the list of free vars -- or rather their Int keys --
         -- (a -> b) means a mentions b
         -- Given the usage details (a UFM that gives occ info for each free var of
         -- the RHS) we can get the list of free vars -- or rather their Int keys --
@@ -322,7 +342,7 @@ occAnalRec (AcyclicSCC (ND bndr rhs rhs_usage _, _, _)) (body_usage, binds)
   = (body_usage, binds)
 
   | otherwise                  -- It's mentioned in the body
   = (body_usage, binds)
 
   | otherwise                  -- It's mentioned in the body
-  = (body_usage' +++ addRuleUsage rhs_usage bndr,      -- Note [Rules are extra RHSs]
+  = (body_usage' +++ rhs_usage,        
      NonRec tagged_bndr rhs : binds)
   where
     (body_usage', tagged_bndr) = tagBinder body_usage bndr
      NonRec tagged_bndr rhs : binds)
   where
     (body_usage', tagged_bndr) = tagBinder body_usage bndr
@@ -344,8 +364,7 @@ occAnalRec (CyclicSCC nodes) (body_usage, binds)
        ----------------------------
        -- Tag the binders with their occurrence info
     total_usage = foldl add_usage body_usage nodes
        ----------------------------
        -- Tag the binders with their occurrence info
     total_usage = foldl add_usage body_usage nodes
-    add_usage body_usage (ND bndr _ rhs_usage _, _, _)
-       = body_usage +++ addRuleUsage rhs_usage bndr
+    add_usage usage_so_far (ND _ _ rhs_usage _, _, _) = usage_so_far +++ rhs_usage
     (final_usage, tagged_nodes) = mapAccumL tag_node total_usage nodes
 
     tag_node :: UsageDetails -> Node Details -> (UsageDetails, Node Details)
     (final_usage, tagged_nodes) = mapAccumL tag_node total_usage nodes
 
     tag_node :: UsageDetails -> Node Details -> (UsageDetails, Node Details)
@@ -365,10 +384,11 @@ occAnalRec (CyclicSCC nodes) (body_usage, binds)
 
        ----------------------------
        -- Now reconstruct the cycle
 
        ----------------------------
        -- Now reconstruct the cycle
-    pairs | no_rules  = reOrderCycle tagged_nodes
-         | otherwise = concatMap reOrderRec (stronglyConnCompFromEdgedVerticesR loop_breaker_edges)
+    pairs | no_rules  = reOrderCycle 0 tagged_nodes []
+         | otherwise = foldr (reOrderRec 0) [] $
+                       stronglyConnCompFromEdgedVerticesR loop_breaker_edges
 
 
-       -- See Note [Choosing loop breakers] for looop_breaker_edges
+       -- See Note [Choosing loop breakers] for loop_breaker_edges
     loop_breaker_edges = map mk_node tagged_nodes
     mk_node (details@(ND _ _ _ rhs_fvs), k, _) = (details, k, new_ks)
        where
     loop_breaker_edges = map mk_node tagged_nodes
     mk_node (details@(ND _ _ _ rhs_fvs), k, _) = (details, k, new_ks)
        where
@@ -382,6 +402,7 @@ occAnalRec (CyclicSCC nodes) (body_usage, binds)
     no_rules      = null init_rule_fvs
     init_rule_fvs = [(b, rule_fvs)
                     | b <- bndrs
     no_rules      = null init_rule_fvs
     init_rule_fvs = [(b, rule_fvs)
                     | b <- bndrs
+                   , isId b
                     , let rule_fvs = idRuleRhsVars b `intersectVarSet` bndr_set
                     , not (isEmptyVarSet rule_fvs)]
 
                     , let rule_fvs = idRuleRhsVars b `intersectVarSet` bndr_set
                     , not (isEmptyVarSet rule_fvs)]
 
@@ -398,11 +419,6 @@ occAnalRec (CyclicSCC nodes) (body_usage, binds)
                 where
                   new_fvs = extendFvs env emptyVarSet fvs
 
                 where
                   new_fvs = extendFvs env emptyVarSet fvs
 
-idRuleRhsVars :: Id -> VarSet
--- Just the variables free on the *rhs* of a rule
--- See Note [Choosing loop breakers]
-idRuleRhsVars id = foldr (unionVarSet . ruleRhsFreeVars) emptyVarSet (idCoreRules id)
-
 extendFvs :: IdEnv IdSet -> IdSet -> IdSet -> IdSet
 -- (extendFVs env fvs s) returns (fvs `union` env(s))
 extendFvs env fvs id_set
 extendFvs :: IdEnv IdSet -> IdSet -> IdSet -> IdSet
 -- (extendFVs env fvs s) returns (fvs `union` env(s))
 extendFvs env fvs id_set
@@ -453,98 +469,108 @@ type Node details = (details, Unique, [Unique])  -- The Ints are gotten from the
                                                -- which is gotten from the Id.
 data Details = ND Id           -- Binder
                  CoreExpr      -- RHS
                                                -- which is gotten from the Id.
 data Details = ND Id           -- Binder
                  CoreExpr      -- RHS
-                 UsageDetails  -- Full usage from RHS (*not* including rules)
-                 IdSet         -- Other binders from this Rec group mentioned on RHS
-                               -- (derivable from UsageDetails but cached here)
 
 
-reOrderRec :: SCC (Node Details)
-           -> [(Id,CoreExpr)]
+                 UsageDetails  -- Full usage from RHS, 
+                                -- including *both* RULES *and* InlineRule unfolding
+
+                 IdSet         -- Other binders *from this Rec group* mentioned in
+                               --   * the  RHS
+                               --   * any InlineRule unfolding
+                               -- but *excluding* any RULES
+
+reOrderRec :: Int -> SCC (Node Details)
+           -> [(Id,CoreExpr)] -> [(Id,CoreExpr)]
 -- Sorted into a plausible order.  Enough of the Ids have
 --      IAmALoopBreaker pragmas that there are no loops left.
 -- Sorted into a plausible order.  Enough of the Ids have
 --      IAmALoopBreaker pragmas that there are no loops left.
-reOrderRec (AcyclicSCC (ND bndr rhs _ _, _, _)) = [(bndr, rhs)]
-reOrderRec (CyclicSCC cycle)                   = reOrderCycle cycle
+reOrderRec _ (AcyclicSCC (ND bndr rhs _ _, _, _)) pairs = (bndr, rhs) : pairs
+reOrderRec depth (CyclicSCC cycle)               pairs = reOrderCycle depth cycle pairs
 
 
-reOrderCycle :: [Node Details] -> [(Id,CoreExpr)]
-reOrderCycle []
+reOrderCycle :: Int -> [Node Details] -> [(Id,CoreExpr)] -> [(Id,CoreExpr)]
+reOrderCycle _ [] _
   = panic "reOrderCycle"
   = panic "reOrderCycle"
-reOrderCycle [bind]     -- Common case of simple self-recursion
-  = [(makeLoopBreaker False bndr, rhs)]
+reOrderCycle _ [bind] pairs    -- Common case of simple self-recursion
+  = (makeLoopBreaker False bndr, rhs) : pairs
   where
     (ND bndr rhs _ _, _, _) = bind
 
   where
     (ND bndr rhs _ _, _, _) = bind
 
-reOrderCycle (bind : binds)
+reOrderCycle depth (bind : binds) pairs
   =     -- Choose a loop breaker, mark it no-inline,
         -- do SCC analysis on the rest, and recursively sort them out
   =     -- Choose a loop breaker, mark it no-inline,
         -- do SCC analysis on the rest, and recursively sort them out
-    concatMap reOrderRec (stronglyConnCompFromEdgedVerticesR unchosen) ++
-    [(makeLoopBreaker False bndr, rhs)]
-
+--    pprTrace "reOrderCycle" (ppr [b | (ND b _ _ _, _, _) <- bind:binds]) $
+    foldr (reOrderRec new_depth)
+          ([ (makeLoopBreaker False bndr, rhs) 
+           | (ND bndr rhs _ _, _, _) <- chosen_binds] ++ pairs)
+         (stronglyConnCompFromEdgedVerticesR unchosen) 
   where
   where
-    (chosen_bind, unchosen) = choose_loop_breaker bind (score bind) [] binds
-    ND bndr rhs _ _ = chosen_bind
+    (chosen_binds, unchosen) = choose_loop_breaker [bind] (score bind) [] binds
+
+    approximate_loop_breaker = depth >= 2
+    new_depth | approximate_loop_breaker = 0
+             | otherwise                = depth+1
+       -- After two iterations (d=0, d=1) give up
+       -- and approximate, returning to d=0
 
         -- This loop looks for the bind with the lowest score
         -- to pick as the loop  breaker.  The rest accumulate in
 
         -- This loop looks for the bind with the lowest score
         -- to pick as the loop  breaker.  The rest accumulate in
-    choose_loop_breaker (details,_,_) _loop_sc acc []
-        = (details, acc)        -- Done
+    choose_loop_breaker loop_binds _loop_sc acc []
+        = (loop_binds, acc)        -- Done
 
 
-    choose_loop_breaker loop_bind loop_sc acc (bind : binds)
+       -- If approximate_loop_breaker is True, we pick *all*
+       -- nodes with lowest score, else just one
+       -- See Note [Complexity of loop breaking]
+    choose_loop_breaker loop_binds loop_sc acc (bind : binds)
         | sc < loop_sc  -- Lower score so pick this new one
         | sc < loop_sc  -- Lower score so pick this new one
-        = choose_loop_breaker bind sc (loop_bind : acc) binds
+        = choose_loop_breaker [bind] sc (loop_binds ++ acc) binds
 
 
-        | otherwise     -- No lower so don't pick it
-        = choose_loop_breaker loop_bind loop_sc (bind : acc) binds
+       | approximate_loop_breaker && sc == loop_sc
+       = choose_loop_breaker (bind : loop_binds) loop_sc acc binds
+       
+        | otherwise     -- Higher score so don't pick it
+        = choose_loop_breaker loop_binds loop_sc (bind : acc) binds
         where
           sc = score bind
 
     score :: Node Details -> Int        -- Higher score => less likely to be picked as loop breaker
     score (ND bndr rhs _ _, _, _)
         where
           sc = score bind
 
     score :: Node Details -> Int        -- Higher score => less likely to be picked as loop breaker
     score (ND bndr rhs _ _, _, _)
-        | workerExists (idWorkerInfo bndr)      = 10
-                -- Note [Worker inline loop]
-
-        | exprIsTrivial rhs        = 5  -- Practically certain to be inlined
+        | not (isId bndr) = 100            -- A type or cercion varialbe is never a loop breaker
+
+        | isDFunId bndr = 9   -- Never choose a DFun as a loop breaker
+                             -- Note [DFuns should not be loop breakers]
+
+        | Just (inl_source, _) <- isInlineRule_maybe (idUnfolding bndr)
+       = case inl_source of
+            InlineWrapper {} -> 10  -- Note [INLINE pragmas]
+            _other           ->  3  -- Data structures are more important than this
+                                    -- so that dictionary/method recursion unravels
+               -- Note that this case hits all InlineRule things, so we
+               -- never look at 'rhs for InlineRule stuff. That's right, because
+               -- 'rhs' is irrelevant for inlining things with an InlineRule
+                
+        | is_con_app rhs = 5  -- Data types help with cases: Note [Constructor applications]
+                
+        | exprIsTrivial rhs = 10  -- Practically certain to be inlined
                 -- Used to have also: && not (isExportedId bndr)
                 -- But I found this sometimes cost an extra iteration when we have
                 --      rec { d = (a,b); a = ...df...; b = ...df...; df = d }
                 -- where df is the exported dictionary. Then df makes a really
                 -- bad choice for loop breaker
 
                 -- Used to have also: && not (isExportedId bndr)
                 -- But I found this sometimes cost an extra iteration when we have
                 --      rec { d = (a,b); a = ...df...; b = ...df...; df = d }
                 -- where df is the exported dictionary. Then df makes a really
                 -- bad choice for loop breaker
 
-        | is_con_app rhs = 3    -- Data types help with cases
-                -- Note [conapp]
-
+       
 -- If an Id is marked "never inline" then it makes a great loop breaker
 -- The only reason for not checking that here is that it is rare
 -- and I've never seen a situation where it makes a difference,
 -- so it probably isn't worth the time to test on every binder
 --     | isNeverActive (idInlinePragma bndr) = -10
 
 -- If an Id is marked "never inline" then it makes a great loop breaker
 -- The only reason for not checking that here is that it is rare
 -- and I've never seen a situation where it makes a difference,
 -- so it probably isn't worth the time to test on every binder
 --     | isNeverActive (idInlinePragma bndr) = -10
 
-        | inlineCandidate bndr rhs = 2  -- Likely to be inlined
-                -- Note [Inline candidates]
+        | isOneOcc (idOccInfo bndr) = 2  -- Likely to be inlined
 
 
-        | not (neverUnfold (idUnfolding bndr)) = 1
-                -- the Id has some kind of unfolding
+        | canUnfold (realIdUnfolding bndr) = 1
+                -- The Id has some kind of unfolding
+               -- Ignore loop-breaker-ness here because that is what we are setting!
 
         | otherwise = 0
 
 
         | otherwise = 0
 
-    inlineCandidate :: Id -> CoreExpr -> Bool
-    inlineCandidate _  (Note InlineMe _) = True
-    inlineCandidate id _                 = isOneOcc (idOccInfo id)
-
-        -- Note [conapp]
-        --
-        -- It's really really important to inline dictionaries.  Real
-        -- example (the Enum Ordering instance from GHC.Base):
-        --
-        --      rec     f = \ x -> case d of (p,q,r) -> p x
-        --              g = \ x -> case d of (p,q,r) -> q x
-        --              d = (v, f, g)
-        --
-        -- Here, f and g occur just once; but we can't inline them into d.
-        -- On the other hand we *could* simplify those case expressions if
-        -- we didn't stupidly choose d as the loop breaker.
-        -- But we won't because constructor args are marked "Many".
-        -- Inlining dictionaries is really essential to unravelling
-        -- the loops in static numeric dictionaries, see GHC.Float.
-
+       -- Checking for a constructor application
         -- Cheap and cheerful; the simplifer moves casts out of the way
         -- The lambda case is important to spot x = /\a. C (f a)
         -- which comes up when C is a dictionary constructor and
         -- Cheap and cheerful; the simplifer moves casts out of the way
         -- The lambda case is important to spot x = /\a. C (f a)
         -- which comes up when C is a dictionary constructor and
@@ -553,36 +579,119 @@ reOrderCycle (bind : binds)
         --
         -- However we *also* treat (\x. C p q) as a con-app-like thing,
         --      Note [Closure conversion]
         --
         -- However we *also* treat (\x. C p q) as a con-app-like thing,
         --      Note [Closure conversion]
-    is_con_app (Var v)    = isDataConWorkId v
+    is_con_app (Var v)    = isConLikeId v
     is_con_app (App f _)  = is_con_app f
     is_con_app (Lam _ e)  = is_con_app e
     is_con_app (Note _ e) = is_con_app e
     is_con_app _          = False
 
 makeLoopBreaker :: Bool -> Id -> Id
     is_con_app (App f _)  = is_con_app f
     is_con_app (Lam _ e)  = is_con_app e
     is_con_app (Note _ e) = is_con_app e
     is_con_app _          = False
 
 makeLoopBreaker :: Bool -> Id -> Id
--- Set the loop-breaker flag
--- See Note [Weak loop breakers]
-makeLoopBreaker weak bndr = setIdOccInfo bndr (IAmALoopBreaker weak)
+-- Set the loop-breaker flag: see Note [Weak loop breakers]
+makeLoopBreaker weak bndr 
+  = ASSERT2( isId bndr, ppr bndr ) setIdOccInfo bndr (IAmALoopBreaker weak)
 \end{code}
 
 \end{code}
 
-Note [Worker inline loop]
-~~~~~~~~~~~~~~~~~~~~~~~~
-Never choose a wrapper as the loop breaker!  Because
-wrappers get auto-generated inlinings when importing, and
-that can lead to an infinite inlining loop.  For example:
+Note [Complexity of loop breaking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The loop-breaking algorithm knocks out one binder at a time, and 
+performs a new SCC analysis on the remaining binders.  That can
+behave very badly in tightly-coupled groups of bindings; in the
+worst case it can be (N**2)*log N, because it does a full SCC
+on N, then N-1, then N-2 and so on.
+
+To avoid this, we switch plans after 2 (or whatever) attempts:
+  Plan A: pick one binder with the lowest score, make it
+         a loop breaker, and try again
+  Plan B: pick *all* binders with the lowest score, make them
+         all loop breakers, and try again 
+Since there are only a small finite number of scores, this will
+terminate in a constant number of iterations, rather than O(N)
+iterations.
+
+You might thing that it's very unlikely, but RULES make it much
+more likely.  Here's a real example from Trac #1969:
+  Rec { $dm = \d.\x. op d
+       {-# RULES forall d. $dm Int d  = $s$dm1
+                 forall d. $dm Bool d = $s$dm2 #-}
+       
+       dInt = MkD .... opInt ...
+       dInt = MkD .... opBool ...
+       opInt  = $dm dInt
+       opBool = $dm dBool
+
+       $s$dm1 = \x. op dInt
+       $s$dm2 = \x. op dBool }
+The RULES stuff means that we can't choose $dm as a loop breaker
+(Note [Choosing loop breakers]), so we must choose at least (say)
+opInt *and* opBool, and so on.  The number of loop breakders is
+linear in the number of instance declarations.
+
+Note [INLINE pragmas]
+~~~~~~~~~~~~~~~~~~~~~
+Avoid choosing a function with an INLINE pramga as the loop breaker!  
+If such a function is mutually-recursive with a non-INLINE thing,
+then the latter should be the loop-breaker.
+
+Usually this is just a question of optimisation. But a particularly
+bad case is wrappers generated by the demand analyser: if you make
+then into a loop breaker you may get an infinite inlining loop.  For
+example:
   rec {
         $wfoo x = ....foo x....
 
         {-loop brk-} foo x = ...$wfoo x...
   }
   rec {
         $wfoo x = ....foo x....
 
         {-loop brk-} foo x = ...$wfoo x...
   }
-
 The interface file sees the unfolding for $wfoo, and sees that foo is
 strict (and hence it gets an auto-generated wrapper).  Result: an
 infinite inlining in the importing scope.  So be a bit careful if you
 change this.  A good example is Tree.repTree in
 nofib/spectral/minimax. If the repTree wrapper is chosen as the loop
 The interface file sees the unfolding for $wfoo, and sees that foo is
 strict (and hence it gets an auto-generated wrapper).  Result: an
 infinite inlining in the importing scope.  So be a bit careful if you
 change this.  A good example is Tree.repTree in
 nofib/spectral/minimax. If the repTree wrapper is chosen as the loop
-breaker then compiling Game.hs goes into an infinite loop (this
-happened when we gave is_con_app a lower score than inline candidates).
+breaker then compiling Game.hs goes into an infinite loop.  This
+happened when we gave is_con_app a lower score than inline candidates:
+
+  Tree.repTree
+    = __inline_me (/\a. \w w1 w2 -> 
+                   case Tree.$wrepTree @ a w w1 w2 of
+                    { (# ww1, ww2 #) -> Branch @ a ww1 ww2 })
+  Tree.$wrepTree
+    = /\a w w1 w2 -> 
+      (# w2_smP, map a (Tree a) (Tree.repTree a w1 w) (w w2) #)
+
+Here we do *not* want to choose 'repTree' as the loop breaker.
+
+Note [DFuns should not be loop breakers]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's particularly bad to make a DFun into a loop breaker.  See
+Note [How instance declarations are translated] in TcInstDcls
+
+We give DFuns a higher score than ordinary CONLIKE things because 
+if there's a choice we want the DFun to be the non-looop breker. Eg
+rec { sc = /\ a \$dC. $fBWrap (T a) ($fCT @ a $dC)
+
+      $fCT :: forall a_afE. (Roman.C a_afE) => Roman.C (Roman.T a_afE)
+      {-# DFUN #-}
+      $fCT = /\a \$dC. MkD (T a) ((sc @ a $dC) |> blah) ($ctoF @ a $dC)
+    }
+
+Here 'sc' (the superclass) looks CONLIKE, but we'll never get to it
+if we can't unravel the DFun first.
+
+Note [Constructor applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's really really important to inline dictionaries.  Real
+example (the Enum Ordering instance from GHC.Base):
+
+     rec     f = \ x -> case d of (p,q,r) -> p x
+             g = \ x -> case d of (p,q,r) -> q x
+             d = (v, f, g)
+
+Here, f and g occur just once; but we can't inline them into d.
+On the other hand we *could* simplify those case expressions if
+we didn't stupidly choose d as the loop breaker.
+But we won't because constructor args are marked "Many".
+Inlining dictionaries is really essential to unravelling
+the loops in static numeric dictionaries, see GHC.Float.
 
 Note [Closure conversion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Closure conversion]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -624,10 +733,14 @@ occAnalRhs :: OccEnv
                                 -- For non-recs the binder is alrady tagged
                                 -- with occurrence info
            -> (UsageDetails, CoreExpr)
                                 -- For non-recs the binder is alrady tagged
                                 -- with occurrence info
            -> (UsageDetails, CoreExpr)
+             -- Returned usage details includes any INLINE rhs
 
 occAnalRhs env id rhs
 
 occAnalRhs env id rhs
-  = occAnal ctxt rhs
+  | isId id   = (addIdOccs rhs_usage (idUnfoldingVars id), rhs')
+  | otherwise = (rhs_usage, rhs')
+       -- Include occurrences for the "extra RHS" from a CoreUnfolding
   where
   where
+    (rhs_usage, rhs') = occAnal ctxt rhs
     ctxt | certainly_inline id = env
          | otherwise           = rhsCtxt env
         -- Note that we generally use an rhsCtxt.  This tells the occ anal n
     ctxt | certainly_inline id = env
          | otherwise           = rhsCtxt env
         -- Note that we generally use an rhsCtxt.  This tells the occ anal n
@@ -653,14 +766,23 @@ occAnalRhs env id rhs
 
 
 \begin{code}
 
 
 \begin{code}
-addRuleUsage :: UsageDetails -> Id -> UsageDetails
+addRuleUsage :: UsageDetails -> Var -> UsageDetails
 -- Add the usage from RULES in Id to the usage
 -- Add the usage from RULES in Id to the usage
-addRuleUsage usage id
-  = foldVarSet add usage (idRuleVars id)
+addRuleUsage usage var 
+  | isId var  = addIdOccs usage (idRuleVars var)
+  | otherwise = usage
+        -- idRuleVars here: see Note [Rule dependency info]
+
+addIdOccs :: UsageDetails -> VarSet -> UsageDetails
+addIdOccs usage id_set = foldVarSet add usage id_set
   where
   where
-    add v u = addOneOcc u v NoOccInfo           -- Give a non-committal binder info
-                                                -- (i.e manyOcc) because many copies
-                                                -- of the specialised thing can appear
+    add v u | isId v    = addOneOcc u v NoOccInfo
+            | otherwise = u
+       -- Give a non-committal binder info (i.e NoOccInfo) because
+       --   a) Many copies of the specialised thing can appear
+       --   b) We don't want to substitute a BIG expression inside a RULE
+       --      even if that's the only occurrence of the thing
+       --      (Same goes for INLINE.)
 \end{code}
 
 Expressions
 \end{code}
 
 Expressions
@@ -701,11 +823,6 @@ occAnal _   expr@(Lit _) = (emptyDetails, expr)
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
-occAnal env (Note InlineMe body)
-  = case occAnal env body of { (usage, body') ->
-    (mapVarEnv markMany usage, Note InlineMe body')
-    }
-
 occAnal env (Note note@(SCC _) body)
   = case occAnal env body of { (usage, body') ->
     (mapVarEnv markInsideSCC usage, Note note body')
 occAnal env (Note note@(SCC _) body)
   = case occAnal env body of { (usage, body') ->
     (mapVarEnv markInsideSCC usage, Note note body')
@@ -718,7 +835,7 @@ occAnal env (Note note body)
 
 occAnal env (Cast expr co)
   = case occAnal env expr of { (usage, expr') ->
 
 occAnal env (Cast expr co)
   = case occAnal env expr of { (usage, expr') ->
-    (markRhsUds env True usage, Cast expr' co)
+      (markManyIf (isRhsEnv env) usage, Cast expr' co)
         -- If we see let x = y `cast` co
         -- then mark y as 'Many' so that we don't
         -- immediately inline y again.
         -- If we see let x = y `cast` co
         -- then mark y as 'Many' so that we don't
         -- immediately inline y again.
@@ -733,7 +850,7 @@ occAnal env app@(App _ _)
 --   (a) occurrences inside type lambdas only not marked as InsideLam
 --   (b) type variables not in environment
 
 --   (a) occurrences inside type lambdas only not marked as InsideLam
 --   (b) type variables not in environment
 
-occAnal env (Lam x body) | isTyVar x
+occAnal env (Lam x body) | isTyCoVar x
   = case occAnal env body of { (body_usage, body') ->
     (body_usage, Lam x body')
     }
   = case occAnal env body of { (body_usage, body') ->
     (body_usage, Lam x body')
     }
@@ -750,7 +867,9 @@ occAnal env (Lam x body) | isTyVar x
 occAnal env expr@(Lam _ _)
   = case occAnal env_body body of { (body_usage, body') ->
     let
 occAnal env expr@(Lam _ _)
   = case occAnal env_body body of { (body_usage, body') ->
     let
-        (final_usage, tagged_binders) = tagBinders body_usage binders
+        (final_usage, tagged_binders) = tagLamBinders body_usage binders'
+                     -- Use binders' to put one-shot info on the lambdas
+
         --      URGH!  Sept 99: we don't seem to be able to use binders' here, because
         --      we get linear-typed things in the resulting program that we can't handle yet.
         --      (e.g. PrelShow)  TODO
         --      URGH!  Sept 99: we don't seem to be able to use binders' here, because
         --      we get linear-typed things in the resulting program that we can't handle yet.
         --      (e.g. PrelShow)  TODO
@@ -763,7 +882,8 @@ occAnal env expr@(Lam _ _)
     (really_final_usage,
      mkLams tagged_binders body') }
   where
     (really_final_usage,
      mkLams tagged_binders body') }
   where
-    env_body        = vanillaCtxt env        -- Body is (no longer) an RhsContext
+    env_body        = vanillaCtxt (trimOccEnv env binders)
+                       -- Body is (no longer) an RhsContext
     (binders, body) = collectBinders expr
     binders'        = oneShotGroup env binders
     linear          = all is_one_shot binders'
     (binders, body) = collectBinders expr
     binders'        = oneShotGroup env binders
     linear          = all is_one_shot binders'
@@ -774,8 +894,7 @@ occAnal env (Case scrut bndr ty alts)
     case mapAndUnzip occ_anal_alt alts of { (alts_usage_s, alts')   ->
     let
         alts_usage  = foldr1 combineAltsUsageDetails alts_usage_s
     case mapAndUnzip occ_anal_alt alts of { (alts_usage_s, alts')   ->
     let
         alts_usage  = foldr1 combineAltsUsageDetails alts_usage_s
-        alts_usage' = addCaseBndrUsage alts_usage
-        (alts_usage1, tagged_bndr) = tagBinder alts_usage' bndr
+        (alts_usage1, tagged_bndr) = tag_case_bndr alts_usage bndr
         total_usage = scrut_usage +++ alts_usage1
     in
     total_usage `seq` (total_usage, Case scrut' tagged_bndr ty alts') }}
         total_usage = scrut_usage +++ alts_usage1
     in
     total_usage `seq` (total_usage, Case scrut' tagged_bndr ty alts') }}
@@ -789,20 +908,13 @@ occAnal env (Case scrut bndr ty alts)
         --      case x of w { (p,q) -> f w }
         -- into
         --      case x of w { (p,q) -> f (p,q) }
         --      case x of w { (p,q) -> f w }
         -- into
         --      case x of w { (p,q) -> f (p,q) }
-    addCaseBndrUsage usage = case lookupVarEnv usage bndr of
-                                Nothing -> usage
-                                Just _  -> extendVarEnv usage bndr NoOccInfo
+    tag_case_bndr usage bndr
+      = case lookupVarEnv usage bndr of
+          Nothing -> (usage,                  setIdOccInfo bndr IAmDead)
+          Just _  -> (usage `delVarEnv` bndr, setIdOccInfo bndr NoOccInfo)
 
 
-    alt_env = mkAltEnv env bndr_swap
-        -- Consider     x = case v of { True -> (p,q); ... }
-        -- Then it's fine to inline p and q
-
-    bndr_swap = case scrut of
-                 Var v           -> Just (v, Var bndr)
-                 Cast (Var v) co -> Just (v, Cast (Var bndr) (mkSymCoercion co))
-                 _other          -> Nothing
-
-    occ_anal_alt = occAnalAlt alt_env bndr bndr_swap
+    alt_env      = mkAltEnv env scrut bndr
+    occ_anal_alt = occAnalAlt alt_env bndr
 
     occ_anal_scrut (Var v) (alt1 : other_alts)
         | not (null other_alts) || not (isDefaultAlt alt1)
 
     occ_anal_scrut (Var v) (alt1 : other_alts)
         | not (null other_alts) || not (isDefaultAlt alt1)
@@ -813,9 +925,11 @@ occAnal env (Case scrut bndr ty alts)
        = occAnal (vanillaCtxt env) scrut    -- No need for rhsCtxt
 
 occAnal env (Let bind body)
        = occAnal (vanillaCtxt env) scrut    -- No need for rhsCtxt
 
 occAnal env (Let bind body)
-  = case occAnal env body                of { (body_usage, body') ->
-    case occAnalBind env bind body_usage of { (final_usage, new_binds) ->
+  = case occAnal env_body body                    of { (body_usage, body') ->
+    case occAnalBind env env_body bind body_usage of { (final_usage, new_binds) ->
        (final_usage, mkLets new_binds body') }}
        (final_usage, mkLets new_binds body') }}
+  where
+    env_body = trimOccEnv env (bindersOf bind)
 
 occAnalArgs :: OccEnv -> [CoreExpr] -> (UsageDetails, [CoreExpr])
 occAnalArgs env args
 
 occAnalArgs :: OccEnv -> [CoreExpr] -> (UsageDetails, [CoreExpr])
 occAnalArgs env args
@@ -835,13 +949,23 @@ occAnalApp :: OccEnv
 occAnalApp env (Var fun, args)
   = case args_stuff of { (args_uds, args') ->
     let
 occAnalApp env (Var fun, args)
   = case args_stuff of { (args_uds, args') ->
     let
-        final_args_uds = markRhsUds env is_pap args_uds
+       final_args_uds = markManyIf (isRhsEnv env && is_exp) args_uds
+         -- We mark the free vars of the argument of a constructor or PAP
+         -- as "many", if it is the RHS of a let(rec).
+         -- This means that nothing gets inlined into a constructor argument
+         -- position, which is what we want.  Typically those constructor
+         -- arguments are just variables, or trivial expressions.
+         --
+         -- This is the *whole point* of the isRhsEnv predicate
     in
     (fun_uds +++ final_args_uds, mkApps (Var fun) args') }
   where
     fun_uniq = idUnique fun
     fun_uds  = mkOneOcc env fun (valArgCount args > 0)
     in
     (fun_uds +++ final_args_uds, mkApps (Var fun) args') }
   where
     fun_uniq = idUnique fun
     fun_uds  = mkOneOcc env fun (valArgCount args > 0)
-    is_pap = isDataConWorkId fun || valArgCount args < idArity fun
+    is_exp = isExpandableApp fun (valArgCount args)
+          -- See Note [CONLIKE pragma] in BasicTypes
+          -- The definition of is_exp should match that in
+          -- Simplify.prepareRhs
 
                 -- Hack for build, fold, runST
     args_stuff  | fun_uniq == buildIdKey    = appSpecial env 2 [True,True]  args
 
                 -- Hack for build, fold, runST
     args_stuff  | fun_uniq == buildIdKey    = appSpecial env 2 [True,True]  args
@@ -873,21 +997,11 @@ occAnalApp env (fun, args)
     (final_uds, mkApps fun' args') }}
 
 
     (final_uds, mkApps fun' args') }}
 
 
-markRhsUds :: OccEnv            -- Check if this is a RhsEnv
-           -> Bool              -- and this is true
-           -> UsageDetails      -- The do markMany on this
+markManyIf :: Bool              -- If this is true
+           -> UsageDetails      -- Then do markMany on this
            -> UsageDetails
            -> UsageDetails
--- We mark the free vars of the argument of a constructor or PAP
--- as "many", if it is the RHS of a let(rec).
--- This means that nothing gets inlined into a constructor argument
--- position, which is what we want.  Typically those constructor
--- arguments are just variables, or trivial expressions.
---
--- This is the *whole point* of the isRhsEnv predicate
-markRhsUds env is_pap arg_uds
-  | isRhsEnv env && is_pap = mapVarEnv markMany arg_uds
-  | otherwise              = arg_uds
-
+markManyIf True  uds = mapVarEnv markMany uds
+markManyIf False uds = uds
 
 appSpecial :: OccEnv
            -> Int -> CtxtTy     -- Argument number, and context to use for it
 
 appSpecial :: OccEnv
            -> Int -> CtxtTy     -- Argument number, and context to use for it
@@ -912,81 +1026,15 @@ appSpecial env n ctxt args
 \end{code}
 
 
 \end{code}
 
 
-Note [Binder swap]
-~~~~~~~~~~~~~~~~~~
-We do these two transformations right here:
-
- (1)   case x of b { pi -> ri }
-    ==>
-      case x of b { pi -> let x=b in ri }
-
- (2)  case (x |> co) of b { pi -> ri }
-    ==>
-      case (x |> co) of b { pi -> let x = b |> sym co in ri }
-
-    Why (2)?  See Note [Case of cast]
-
-In both cases, in a particular alternative (pi -> ri), we only 
-add the binding if
-  (a) x occurs free in (pi -> ri)
-       (ie it occurs in ri, but is not bound in pi)
-  (b) the pi does not bind b (or the free vars of co)
-We need (a) and (b) for the inserted binding to be correct.
-
-For the alternatives where we inject the binding, we can transfer
-all x's OccInfo to b.  And that is the point.
-
-Notice that 
-  * The deliberate shadowing of 'x'. 
-  * That (a) rapidly becomes false, so no bindings are injected.
-
-The reason for doing these transformations here is because it allows
-us to adjust the OccInfo for 'x' and 'b' as we go.
-
-  * Suppose the only occurrences of 'x' are the scrutinee and in the
-    ri; then this transformation makes it occur just once, and hence
-    get inlined right away.
-
-  * If we do this in the Simplifier, we don't know whether 'x' is used
-    in ri, so we are forced to pessimistically zap b's OccInfo even
-    though it is typically dead (ie neither it nor x appear in the
-    ri).  There's nothing actually wrong with zapping it, except that
-    it's kind of nice to know which variables are dead.  My nose
-    tells me to keep this information as robustly as possible.
-
-The Maybe (Id,CoreExpr) passed to occAnalAlt is the extra let-binding
-{x=b}; it's Nothing if the binder-swap doesn't happen.
-
-Note [Binder swap on GlobalId scrutinees]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When the scrutinee is a GlobalId we must take care in two ways
-
- i) In order to *know* whether 'x' occurs free in the RHS, we need its
-    occurrence info. BUT, we don't gather occurrence info for
-    GlobalIds.  That's what the (small) occ_scrut_ids set in OccEnv is
-    for: it says "gather occurrence info for these.
-
- ii) We must call localiseId on 'x' first, in case it's a GlobalId, or
-     has an External Name. See, for example, SimplEnv Note [Global Ids in
-     the substitution].
-
-Note [Case of cast]
-~~~~~~~~~~~~~~~~~~~
-Consider        case (x `cast` co) of b { I# ->
-                ... (case (x `cast` co) of {...}) ...
-We'd like to eliminate the inner case.  That is the motivation for
-equation (2) in Note [Binder swap].  When we get to the inner case, we
-inline x, cancel the casts, and away we go.
-
 Note [Binders in case alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
     case x of y { (a,b) -> f y }
 We treat 'a', 'b' as dead, because they don't physically occur in the
 case alternative.  (Indeed, a variable is dead iff it doesn't occur in
 Note [Binders in case alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
     case x of y { (a,b) -> f y }
 We treat 'a', 'b' as dead, because they don't physically occur in the
 case alternative.  (Indeed, a variable is dead iff it doesn't occur in
-its scope in the output of OccAnal.)  This invariant is It really
-helpe to know when binders are unused.  See esp the call to
-isDeadBinder in Simplify.mkDupableAlt
+its scope in the output of OccAnal.)  It really helps to know when
+binders are unused.  See esp the call to isDeadBinder in
+Simplify.mkDupableAlt
 
 In this example, though, the Simplifier will bring 'a' and 'b' back to
 life, beause it binds 'y' to (a,b) (imagine got inlined and
 
 In this example, though, the Simplifier will bring 'a' and 'b' back to
 life, beause it binds 'y' to (a,b) (imagine got inlined and
@@ -995,52 +1043,48 @@ scrutinised y).
 \begin{code}
 occAnalAlt :: OccEnv
            -> CoreBndr
 \begin{code}
 occAnalAlt :: OccEnv
            -> CoreBndr
-          -> Maybe (Id, CoreExpr)  -- Note [Binder swap]
            -> CoreAlt
            -> (UsageDetails, Alt IdWithOccInfo)
            -> CoreAlt
            -> (UsageDetails, Alt IdWithOccInfo)
-occAnalAlt env case_bndr mb_scrut_var (con, bndrs, rhs)
-  = case occAnal env rhs of { (rhs_usage, rhs') ->
+occAnalAlt env case_bndr (con, bndrs, rhs)
+  = let 
+        env' = trimOccEnv env bndrs
+    in 
+    case occAnal env' rhs of { (rhs_usage1, rhs1) ->
     let
     let
-        (alt_usg, tagged_bndrs) = tagBinders rhs_usage bndrs
+       proxies = getProxies env' case_bndr 
+       (rhs_usage2, rhs2) = foldrBag wrapProxy (rhs_usage1, rhs1) proxies
+        (alt_usg, tagged_bndrs) = tagLamBinders rhs_usage2 bndrs
         bndrs' = tagged_bndrs      -- See Note [Binders in case alternatives]
     in
         bndrs' = tagged_bndrs      -- See Note [Binders in case alternatives]
     in
-    case mb_scrut_var of
-       Just (scrut_var, scrut_rhs)             -- See Note [Binder swap]
-         | scrut_var `localUsedIn` alt_usg     -- (a) Fast path, usually false
-         , not (any shadowing bndrs)           -- (b) 
-         -> (addOneOcc usg_wo_scrut case_bndr NoOccInfo,
-                       -- See Note [Case binder usage] for the NoOccInfo
-             (con, bndrs', Let (NonRec scrut_var' scrut_rhs) rhs'))
-         where
-          (usg_wo_scrut, scrut_var') = tagBinder alt_usg (localiseId scrut_var)
-                       -- Note the localiseId; we're making a new binding
-                       -- for it, and it might have an External Name, or
-                       -- even be a GlobalId; Note [Binder swap on GlobalId scrutinees]
-          shadowing bndr = bndr `elemVarSet` rhs_fvs
-          rhs_fvs = exprFreeVars scrut_rhs
-
-       _other -> (alt_usg, (con, bndrs', rhs')) }
+    (alt_usg, (con, bndrs', rhs2)) }
+
+wrapProxy :: ProxyBind -> (UsageDetails, CoreExpr) -> (UsageDetails, CoreExpr)
+wrapProxy (bndr, rhs_var, co) (body_usg, body)
+  | not (bndr `usedIn` body_usg) 
+  = (body_usg, body)
+  | otherwise
+  = (body_usg' +++ rhs_usg, Let (NonRec tagged_bndr rhs) body)
+  where
+    (body_usg', tagged_bndr) = tagBinder body_usg bndr
+    rhs_usg = unitVarEnv rhs_var NoOccInfo     -- We don't need exact info
+    rhs = mkCoerceI co (Var rhs_var)
 \end{code}
 
 
 %************************************************************************
 %*                                                                      *
 \end{code}
 
 
 %************************************************************************
 %*                                                                      *
-\subsection[OccurAnal-types]{OccEnv}
+                    OccEnv                                                                     
 %*                                                                      *
 %************************************************************************
 
 \begin{code}
 data OccEnv
 %*                                                                      *
 %************************************************************************
 
 \begin{code}
 data OccEnv
-  = OccEnv { occ_encl     :: !OccEncl      -- Enclosing context information
-          , occ_ctxt      :: !CtxtTy       -- Tells about linearity
-          , occ_scrut_ids :: !GblScrutIds }
+  = OccEnv { occ_encl  :: !OccEncl      -- Enclosing context information
+          , occ_ctxt  :: !CtxtTy       -- Tells about linearity
+          , occ_proxy :: ProxyEnv }
 
 
-type GblScrutIds = IdSet  -- GlobalIds that are scrutinised, and for which
-                         -- we want to gather occurence info; see
-                         -- Note [Binder swap for GlobalId scrutinee]
-                         -- No need to prune this if there's a shadowing binding
-                         -- because it's OK for it to be too big
 
 
+-----------------------------
 -- OccEncl is used to control whether to inline into constructor arguments
 -- For example:
 --      x = (p,q)               -- Don't inline p or q
 -- OccEncl is used to control whether to inline into constructor arguments
 -- For example:
 --      x = (p,q)               -- Don't inline p or q
@@ -1055,6 +1099,10 @@ data OccEncl
   | OccVanilla          -- Argument of function, body of lambda, scruintee of case etc.
                         -- Do inline into constructor args here
 
   | OccVanilla          -- Argument of function, body of lambda, scruintee of case etc.
                         -- Do inline into constructor args here
 
+instance Outputable OccEncl where
+  ppr OccRhs     = ptext (sLit "occRhs")
+  ppr OccVanilla = ptext (sLit "occVanilla")
+
 type CtxtTy = [Bool]
         -- []           No info
         --
 type CtxtTy = [Bool]
         -- []           No info
         --
@@ -1066,29 +1114,18 @@ type CtxtTy = [Bool]
         --                      the CtxtTy inside applies
 
 initOccEnv :: OccEnv
         --                      the CtxtTy inside applies
 
 initOccEnv :: OccEnv
-initOccEnv = OccEnv { occ_encl = OccRhs
-                   , occ_ctxt = []
-                   , occ_scrut_ids = emptyVarSet }
+initOccEnv = OccEnv { occ_encl  = OccVanilla
+                   , occ_ctxt  = []
+                   , occ_proxy = PE emptyVarEnv emptyVarSet }
 
 vanillaCtxt :: OccEnv -> OccEnv
 
 vanillaCtxt :: OccEnv -> OccEnv
-vanillaCtxt env = OccEnv { occ_encl = OccVanilla, occ_ctxt = []
-                        , occ_scrut_ids = occ_scrut_ids env }
+vanillaCtxt env = OccEnv { occ_encl = OccVanilla
+                         , occ_ctxt = []
+                        , occ_proxy = occ_proxy env }
 
 rhsCtxt :: OccEnv -> OccEnv
 rhsCtxt env = OccEnv { occ_encl = OccRhs, occ_ctxt = []
 
 rhsCtxt :: OccEnv -> OccEnv
 rhsCtxt env = OccEnv { occ_encl = OccRhs, occ_ctxt = []
-                    , occ_scrut_ids = occ_scrut_ids env }
-
-mkAltEnv :: OccEnv -> Maybe (Id, CoreExpr) -> OccEnv
--- Does two things: a) makes the occ_ctxt = OccVanilla
---                 b) extends the scrut_ids if necessary
-mkAltEnv env (Just (scrut_id, _))
-  | not (isLocalId scrut_id) 
-  = OccEnv { occ_encl      = OccVanilla
-          , occ_scrut_ids = extendVarSet (occ_scrut_ids env) scrut_id
-          , occ_ctxt      = occ_ctxt env }
-mkAltEnv env _
-  | isRhsEnv env = env { occ_encl = OccVanilla }
-  | otherwise    = env
+                    , occ_proxy = occ_proxy env }
 
 setCtxtTy :: OccEnv -> CtxtTy -> OccEnv
 setCtxtTy env ctxt = env { occ_ctxt = ctxt }
 
 setCtxtTy :: OccEnv -> CtxtTy -> OccEnv
 setCtxtTy env ctxt = env { occ_ctxt = ctxt }
@@ -1123,6 +1160,329 @@ addAppCtxt env@(OccEnv { occ_ctxt = ctxt }) args
 
 %************************************************************************
 %*                                                                      *
 
 %************************************************************************
 %*                                                                      *
+                    ProxyEnv                                                                   
+%*                                                                      *
+%************************************************************************
+
+\begin{code}
+data ProxyEnv 
+   = PE (IdEnv (Id, [(Id,CoercionI)])) VarSet
+       -- Main env, and its free variables (of both range and domain)
+\end{code}
+
+Note [ProxyEnv]
+~~~~~~~~~~~~~~~
+The ProxyEnv keeps track of the connection between case binders and
+scrutinee.  Specifically, if
+     sc |-> (sc, [...(cb, co)...])
+is a binding in the ProxyEnv, then
+     cb = sc |> coi
+Typically we add such a binding when encountering the case expression
+     case (sc |> coi) of cb { ... }
+
+Things to note:
+  * The domain of the ProxyEnv is the variable (or casted variable) 
+    scrutinees of enclosing cases.  This is additionally used
+    to ensure we gather occurrence info even for GlobalId scrutinees;
+    see Note [Binder swap for GlobalId scrutinee]
+
+  * The ProxyEnv is just an optimisation; you can throw away any 
+    element without losing correctness.  And we do so when pushing
+    it inside a binding (see trimProxyEnv).
+
+  * Once scrutinee might map to many case binders:  Eg
+      case sc of cb1 { DEFAULT -> ....case sc of cb2 { ... } .. }
+
+INVARIANTS
+ * If sc1 |-> (sc2, [...(cb, co)...]), then sc1==sc2
+   It's a UniqFM and we sometimes need the domain Id
+
+ * Any particular case binder 'cb' occurs only once in entire range
+
+ * No loops
+
+The Main Reason for having a ProxyEnv is so that when we encounter
+    case e of cb { pi -> ri }
+we can find all the in-scope variables derivable from 'cb', 
+and effectively add let-bindings for them thus:
+    case e of cb { pi -> let { x = ..cb..; y = ...cb.. }
+                         in ri }
+The function getProxies finds these bindings; then we 
+add just the necessary ones, using wrapProxy. 
+
+More info under Note [Binder swap]
+
+Note [Binder swap]
+~~~~~~~~~~~~~~~~~~
+We do these two transformations right here:
+
+ (1)   case x of b { pi -> ri }
+    ==>
+      case x of b { pi -> let x=b in ri }
+
+ (2)  case (x |> co) of b { pi -> ri }
+    ==>
+      case (x |> co) of b { pi -> let x = b |> sym co in ri }
+
+    Why (2)?  See Note [Case of cast]
+
+In both cases, in a particular alternative (pi -> ri), we only 
+add the binding if
+  (a) x occurs free in (pi -> ri)
+       (ie it occurs in ri, but is not bound in pi)
+  (b) the pi does not bind b (or the free vars of co)
+We need (a) and (b) for the inserted binding to be correct.
+
+For the alternatives where we inject the binding, we can transfer
+all x's OccInfo to b.  And that is the point.
+
+Notice that 
+  * The deliberate shadowing of 'x'. 
+  * That (a) rapidly becomes false, so no bindings are injected.
+
+The reason for doing these transformations here is because it allows
+us to adjust the OccInfo for 'x' and 'b' as we go.
+
+  * Suppose the only occurrences of 'x' are the scrutinee and in the
+    ri; then this transformation makes it occur just once, and hence
+    get inlined right away.
+
+  * If we do this in the Simplifier, we don't know whether 'x' is used
+    in ri, so we are forced to pessimistically zap b's OccInfo even
+    though it is typically dead (ie neither it nor x appear in the
+    ri).  There's nothing actually wrong with zapping it, except that
+    it's kind of nice to know which variables are dead.  My nose
+    tells me to keep this information as robustly as possible.
+
+The Maybe (Id,CoreExpr) passed to occAnalAlt is the extra let-binding
+{x=b}; it's Nothing if the binder-swap doesn't happen.
+
+There is a danger though.  Consider
+      let v = x +# y
+      in case (f v) of w -> ...v...v...
+And suppose that (f v) expands to just v.  Then we'd like to
+use 'w' instead of 'v' in the alternative.  But it may be too
+late; we may have substituted the (cheap) x+#y for v in the 
+same simplifier pass that reduced (f v) to v.
+
+I think this is just too bad.  CSE will recover some of it.
+
+Note [Case of cast]
+~~~~~~~~~~~~~~~~~~~
+Consider        case (x `cast` co) of b { I# ->
+                ... (case (x `cast` co) of {...}) ...
+We'd like to eliminate the inner case.  That is the motivation for
+equation (2) in Note [Binder swap].  When we get to the inner case, we
+inline x, cancel the casts, and away we go.
+
+Note [Binder swap on GlobalId scrutinees]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When the scrutinee is a GlobalId we must take care in two ways
+
+ i) In order to *know* whether 'x' occurs free in the RHS, we need its
+    occurrence info. BUT, we don't gather occurrence info for
+    GlobalIds.  That's one use for the (small) occ_proxy env in OccEnv is
+    for: it says "gather occurrence info for these.
+
+ ii) We must call localiseId on 'x' first, in case it's a GlobalId, or
+     has an External Name. See, for example, SimplEnv Note [Global Ids in
+     the substitution].
+
+Note [getProxies is subtle]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The code for getProxies isn't all that obvious. Consider
+
+  case v |> cov  of x { DEFAULT ->
+  case x |> cox1 of y { DEFAULT ->
+  case x |> cox2 of z { DEFAULT -> r
+
+These will give us a ProxyEnv looking like:
+  x |-> (x, [(y, cox1), (z, cox2)])
+  v |-> (v, [(x, cov)])
+
+From this we want to extract the bindings
+    x = z |> sym cox2
+    v = x |> sym cov
+    y = x |> cox1
+
+Notice that later bindings may mention earlier ones, and that
+we need to go "both ways".
+
+Historical note [no-case-of-case]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We *used* to suppress the binder-swap in case expressions when 
+-fno-case-of-case is on.  Old remarks:
+    "This happens in the first simplifier pass,
+    and enhances full laziness.  Here's the bad case:
+            f = \ y -> ...(case x of I# v -> ...(case x of ...) ... )
+    If we eliminate the inner case, we trap it inside the I# v -> arm,
+    which might prevent some full laziness happening.  I've seen this
+    in action in spectral/cichelli/Prog.hs:
+             [(m,n) | m <- [1..max], n <- [1..max]]
+    Hence the check for NoCaseOfCase."
+However, now the full-laziness pass itself reverses the binder-swap, so this
+check is no longer necessary.
+
+Historical note [Suppressing the case binder-swap]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This old note describes a problem that is also fixed by doing the
+binder-swap in OccAnal:
+
+    There is another situation when it might make sense to suppress the
+    case-expression binde-swap. If we have
+
+        case x of w1 { DEFAULT -> case x of w2 { A -> e1; B -> e2 }
+                       ...other cases .... }
+
+    We'll perform the binder-swap for the outer case, giving
+
+        case x of w1 { DEFAULT -> case w1 of w2 { A -> e1; B -> e2 }
+                       ...other cases .... }
+
+    But there is no point in doing it for the inner case, because w1 can't
+    be inlined anyway.  Furthermore, doing the case-swapping involves
+    zapping w2's occurrence info (see paragraphs that follow), and that
+    forces us to bind w2 when doing case merging.  So we get
+
+        case x of w1 { A -> let w2 = w1 in e1
+                       B -> let w2 = w1 in e2
+                       ...other cases .... }
+
+    This is plain silly in the common case where w2 is dead.
+
+    Even so, I can't see a good way to implement this idea.  I tried
+    not doing the binder-swap if the scrutinee was already evaluated
+    but that failed big-time:
+
+            data T = MkT !Int
+
+            case v of w  { MkT x ->
+            case x of x1 { I# y1 ->
+            case x of x2 { I# y2 -> ...
+
+    Notice that because MkT is strict, x is marked "evaluated".  But to
+    eliminate the last case, we must either make sure that x (as well as
+    x1) has unfolding MkT y1.  THe straightforward thing to do is to do
+    the binder-swap.  So this whole note is a no-op.
+
+It's fixed by doing the binder-swap in OccAnal because we can do the
+binder-swap unconditionally and still get occurrence analysis
+information right.
+
+\begin{code}
+extendProxyEnv :: ProxyEnv -> Id -> CoercionI -> Id -> ProxyEnv
+-- (extendPE x co y) typically arises from 
+--               case (x |> co) of y { ... }
+-- It extends the proxy env with the binding 
+--                    y = x |> co
+extendProxyEnv pe scrut co case_bndr
+  | scrut == case_bndr = PE env1 fvs1  -- If case_bndr shadows scrut,
+  | otherwise          = PE env2 fvs2  --   don't extend
+  where
+    PE env1 fvs1 = trimProxyEnv pe [case_bndr]
+    env2 = extendVarEnv_Acc add single env1 scrut1 (case_bndr,co)
+    single cb_co = (scrut1, [cb_co]) 
+    add cb_co (x, cb_cos) = (x, cb_co:cb_cos)
+    fvs2 = fvs1 `unionVarSet`  freeVarsCoI co
+               `extendVarSet` case_bndr
+               `extendVarSet` scrut1
+
+    scrut1 = mkLocalId (localiseName (idName scrut)) (idType scrut)
+       -- Localise the scrut_var before shadowing it; we're making a 
+       -- new binding for it, and it might have an External Name, or
+       -- even be a GlobalId; Note [Binder swap on GlobalId scrutinees]
+       -- Also we don't want any INLILNE or NOINLINE pragmas!
+
+-----------
+type ProxyBind = (Id, Id, CoercionI)
+
+getProxies :: OccEnv -> Id -> Bag ProxyBind
+-- Return a bunch of bindings [...(xi,ei)...] 
+-- such that  let { ...; xi=ei; ... } binds the xi using y alone
+-- See Note [getProxies is subtle]
+getProxies (OccEnv { occ_proxy = PE pe _ }) case_bndr
+  = -- pprTrace "wrapProxies" (ppr case_bndr) $
+    go_fwd case_bndr
+  where
+    fwd_pe :: IdEnv (Id, CoercionI)
+    fwd_pe = foldVarEnv add1 emptyVarEnv pe
+           where
+             add1 (x,ycos) env = foldr (add2 x) env ycos
+             add2 x (y,co) env = extendVarEnv env y (x,co)
+
+    go_fwd :: Id -> Bag ProxyBind
+       -- Return bindings derivable from case_bndr
+    go_fwd case_bndr = -- pprTrace "go_fwd" (vcat [ppr case_bndr, text "fwd_pe =" <+> ppr fwd_pe, 
+                       --                         text "pe =" <+> ppr pe]) $ 
+                       go_fwd' case_bndr
+
+    go_fwd' case_bndr
+        | Just (scrut, co) <- lookupVarEnv fwd_pe case_bndr
+        = unitBag (scrut,  case_bndr, mkSymCoI co)
+         `unionBags` go_fwd scrut
+          `unionBags` go_bwd scrut [pr | pr@(cb,_) <- lookup_bwd scrut
+                                       , cb /= case_bndr]
+        | otherwise 
+        = emptyBag
+
+    lookup_bwd :: Id -> [(Id, CoercionI)]
+       -- Return case_bndrs that are connected to scrut 
+    lookup_bwd scrut = case lookupVarEnv pe scrut of
+                         Nothing          -> []
+                         Just (_, cb_cos) -> cb_cos
+
+    go_bwd :: Id -> [(Id, CoercionI)] -> Bag ProxyBind
+    go_bwd scrut cb_cos = foldr (unionBags . go_bwd1 scrut) emptyBag cb_cos
+
+    go_bwd1 :: Id -> (Id, CoercionI) -> Bag ProxyBind
+    go_bwd1 scrut (case_bndr, co) 
+       = -- pprTrace "go_bwd1" (ppr case_bndr) $
+         unitBag (case_bndr, scrut, co)
+        `unionBags` go_bwd case_bndr (lookup_bwd case_bndr)
+
+-----------
+mkAltEnv :: OccEnv -> CoreExpr -> Id -> OccEnv
+-- Does two things: a) makes the occ_ctxt = OccVanilla
+--                 b) extends the ProxyEnv if possible
+mkAltEnv env scrut cb
+  = env { occ_encl  = OccVanilla, occ_proxy = pe' }
+  where
+    pe  = occ_proxy env
+    pe' = case scrut of
+             Var v           -> extendProxyEnv pe v (IdCo (idType v)) cb
+             Cast (Var v) co -> extendProxyEnv pe v (ACo co)          cb
+            _other          -> trimProxyEnv pe [cb]
+
+-----------
+trimOccEnv :: OccEnv -> [CoreBndr] -> OccEnv
+trimOccEnv env bndrs = env { occ_proxy = trimProxyEnv (occ_proxy env) bndrs }
+
+-----------
+trimProxyEnv :: ProxyEnv -> [CoreBndr] -> ProxyEnv
+-- We are about to push this ProxyEnv inside a binding for 'bndrs'
+-- So dump any ProxyEnv bindings which mention any of the bndrs
+trimProxyEnv (PE pe fvs) bndrs 
+  | not (bndr_set `intersectsVarSet` fvs) 
+  = PE pe fvs
+  | otherwise
+  = PE pe' (fvs `minusVarSet` bndr_set)
+  where
+    pe' = mapVarEnv trim pe
+    bndr_set = mkVarSet bndrs
+    trim (scrut, cb_cos) | scrut `elemVarSet` bndr_set = (scrut, [])
+                        | otherwise = (scrut, filterOut discard cb_cos)
+    discard (cb,co) = bndr_set `intersectsVarSet` 
+                      extendVarSet (freeVarsCoI co) cb
+                             
+-----------
+freeVarsCoI :: CoercionI -> VarSet
+freeVarsCoI (IdCo t) = tyVarsOfType t
+freeVarsCoI (ACo co) = tyVarsOfType co
+\end{code}
+
+
+%************************************************************************
+%*                                                                      *
 \subsection[OccurAnal-types]{OccEnv}
 %*                                                                      *
 %************************************************************************
 \subsection[OccurAnal-types]{OccEnv}
 %*                                                                      *
 %************************************************************************
@@ -1149,23 +1509,26 @@ addOneOcc usage id info
 emptyDetails :: UsageDetails
 emptyDetails = (emptyVarEnv :: UsageDetails)
 
 emptyDetails :: UsageDetails
 emptyDetails = (emptyVarEnv :: UsageDetails)
 
-localUsedIn, usedIn :: Id -> UsageDetails -> Bool
-v `localUsedIn` details = v `elemVarEnv` details
-v `usedIn`      details =  isExportedId v || v `localUsedIn` details
+usedIn :: Id -> UsageDetails -> Bool
+v `usedIn` details = isExportedId v || v `elemVarEnv` details
 
 type IdWithOccInfo = Id
 
 
 type IdWithOccInfo = Id
 
-tagBinders :: UsageDetails          -- Of scope
-           -> [Id]                  -- Binders
-           -> (UsageDetails,        -- Details with binders removed
-              [IdWithOccInfo])    -- Tagged binders
-
-tagBinders usage binders
- = let
-     usage' = usage `delVarEnvList` binders
-     uss    = map (setBinderOcc usage) binders
-   in
-   usage' `seq` (usage', uss)
+tagLamBinders :: UsageDetails          -- Of scope
+              -> [Id]                  -- Binders
+              -> (UsageDetails,        -- Details with binders removed
+                 [IdWithOccInfo])    -- Tagged binders
+-- Used for lambda and case binders
+-- It copes with the fact that lambda bindings can have InlineRule 
+-- unfoldings, used for join points
+tagLamBinders usage binders = usage' `seq` (usage', bndrs')
+  where
+    (usage', bndrs') = mapAccumR tag_lam usage binders
+    tag_lam usage bndr = (usage2, setBinderOcc usage bndr)
+      where
+        usage1 = usage `delVarEnv` bndr
+        usage2 | isId bndr = addIdOccs usage1 (idUnfoldingVars bndr)
+               | otherwise = usage1
 
 tagBinder :: UsageDetails           -- Of scope
           -> Id                     -- Binders
 
 tagBinder :: UsageDetails           -- Of scope
           -> Id                     -- Binders
@@ -1181,7 +1544,7 @@ tagBinder usage binder
 
 setBinderOcc :: UsageDetails -> CoreBndr -> CoreBndr
 setBinderOcc usage bndr
 
 setBinderOcc :: UsageDetails -> CoreBndr -> CoreBndr
 setBinderOcc usage bndr
-  | isTyVar bndr      = bndr
+  | isTyCoVar bndr    = bndr
   | isExportedId bndr = case idOccInfo bndr of
                           NoOccInfo -> bndr
                           _         -> setIdOccInfo bndr NoOccInfo
   | isExportedId bndr = case idOccInfo bndr of
                           NoOccInfo -> bndr
                           _         -> setIdOccInfo bndr NoOccInfo
@@ -1205,8 +1568,9 @@ setBinderOcc usage bndr
 mkOneOcc :: OccEnv -> Id -> InterestingCxt -> UsageDetails
 mkOneOcc env id int_cxt
   | isLocalId id = unitVarEnv id (OneOcc False True int_cxt)
 mkOneOcc :: OccEnv -> Id -> InterestingCxt -> UsageDetails
 mkOneOcc env id int_cxt
   | isLocalId id = unitVarEnv id (OneOcc False True int_cxt)
-  | id `elemVarSet` occ_scrut_ids env = unitVarEnv id NoOccInfo
-  | otherwise                        = emptyDetails
+  | PE env _ <- occ_proxy env
+  , id `elemVarEnv` env = unitVarEnv id NoOccInfo
+  | otherwise           = emptyDetails
 
 markMany, markInsideLam, markInsideSCC :: OccInfo -> OccInfo
 
 
 markMany, markInsideLam, markInsideSCC :: OccInfo -> OccInfo