Drop dead Given bindings in setImplicationStatus

Trac #13032 pointed out that we sometimes generate unused
bindings for Givens, and (worse still) we can't always discard
them later (we don't drop a case binding unless we can prove
that the scrutinee is non-bottom.

It looks as if this may be a major reason for the performace
problems in #14338 (see comment:29).

This patch fixes the problem at source, by pruning away all the
dead Givens.  See Note [Delete dead Given evidence bindings]

Remarkably, compiler allocation falls by 23% in
perf/compiler/T12227!

I have not confirmed whether this change actualy helps with

14 files changed, 270 insertions, 182 deletions

diff --git a/compiler/basicTypes/VarEnv.hs b/compiler/basicTypes/VarEnv.hs
index f8ab574bc5..2c50e8dcbf 100644
--- a/compiler/basicTypes/VarEnv.hs
+++ b/compiler/basicTypes/VarEnv.hs
@@ -34,7 +34,7 @@ module VarEnv (
         extendDVarEnvList,
         lookupDVarEnv, elemDVarEnv,
         isEmptyDVarEnv, foldDVarEnv,
-        mapDVarEnv,
+        mapDVarEnv, filterDVarEnv,
         modifyDVarEnv,
         alterDVarEnv,
         plusDVarEnv, plusDVarEnv_C,
@@ -557,6 +557,9 @@ foldDVarEnv = foldUDFM
 mapDVarEnv :: (a -> b) -> DVarEnv a -> DVarEnv b
 mapDVarEnv = mapUDFM
 
+filterDVarEnv      :: (a -> Bool) -> DVarEnv a -> DVarEnv a
+filterDVarEnv = filterUDFM
+
 alterDVarEnv :: (Maybe a -> Maybe a) -> DVarEnv a -> Var -> DVarEnv a
 alterDVarEnv = alterUDFM
 
diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs
index 0287818b44..249362dde5 100644
--- a/compiler/typecheck/TcEvidence.hs
+++ b/compiler/typecheck/TcEvidence.hs
@@ -13,7 +13,8 @@ module TcEvidence (
   -- Evidence bindings
   TcEvBinds(..), EvBindsVar(..),
   EvBindMap(..), emptyEvBindMap, extendEvBinds,
-  lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap,
+  lookupEvBind, evBindMapBinds, foldEvBindMap, filterEvBindMap,
+  isEmptyEvBindMap,
   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
   sccEvBinds, evBindVar,
   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
@@ -442,6 +443,10 @@ evBindMapBinds = foldEvBindMap consBag emptyBag
 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
 
+filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
+filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
+  = EvBindMap { ev_bind_varenv = filterDVarEnv k env }
+
 instance Outputable EvBindMap where
   ppr (EvBindMap m) = ppr m
 
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 6580758788..e5960cb1b1 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -843,16 +843,14 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
                             , sc_implics `unionBags` meth_implics ) }
 
        ; env <- getLclEnv
-       ; emitImplication $ Implic { ic_tclvl  = tclvl
-                                  , ic_skols  = inst_tyvars
-                                  , ic_no_eqs = False
-                                  , ic_given  = dfun_ev_vars
-                                  , ic_wanted = mkImplicWC sc_meth_implics
-                                  , ic_status = IC_Unsolved
-                                  , ic_binds  = dfun_ev_binds_var
-                                  , ic_needed = emptyVarSet
-                                  , ic_env    = env
-                                  , ic_info   = InstSkol }
+       ; emitImplication $
+         newImplication { ic_tclvl  = tclvl
+                        , ic_skols  = inst_tyvars
+                        , ic_given  = dfun_ev_vars
+                        , ic_wanted = mkImplicWC sc_meth_implics
+                        , ic_binds  = dfun_ev_binds_var
+                        , ic_env    = env
+                        , ic_info   = InstSkol }
 
        -- Create the result bindings
        ; self_dict <- newDict clas inst_tys
@@ -1062,16 +1060,11 @@ checkInstConstraints thing_inside
 
        ; ev_binds_var <- newTcEvBinds
        ; env <- getLclEnv
-       ; let implic = Implic { ic_tclvl  = tclvl
-                             , ic_skols  = []
-                             , ic_no_eqs = False
-                             , ic_given  = []
-                             , ic_wanted = wanted
-                             , ic_status = IC_Unsolved
-                             , ic_binds  = ev_binds_var
-                             , ic_needed = emptyVarSet
-                             , ic_env    = env
-                             , ic_info   = InstSkol }
+       ; let implic = newImplication { ic_tclvl  = tclvl
+                                     , ic_wanted = wanted
+                                     , ic_binds  = ev_binds_var
+                                     , ic_env    = env
+                                     , ic_info   = InstSkol }
 
        ; return (implic, ev_binds_var, result) }
 
diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs
index 5bc200c1a0..184093f066 100644
--- a/compiler/typecheck/TcRnMonad.hs
+++ b/compiler/typecheck/TcRnMonad.hs
@@ -90,7 +90,7 @@ module TcRnMonad(
   -- * Type constraints
   newTcEvBinds,
   addTcEvBind,
-  getTcEvTyCoVars, getTcEvBindsMap,
+  getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
   chooseUniqueOccTc,
   getConstraintVar, setConstraintVar,
   emitConstraints, emitStaticConstraints, emitSimple, emitSimples,
@@ -1372,6 +1372,10 @@ getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap
 getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref })
   = readTcRef ev_ref
 
+setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcM ()
+setTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) binds
+  = writeTcRef ev_ref binds
+
 addTcEvBind :: EvBindsVar -> EvBind -> TcM ()
 -- Add a binding to the TcEvBinds by side effect
 addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 4d7a8e8390..7766a38aa1 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -90,7 +90,8 @@ module TcRnTypes(
         isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic,
         arisesFromGivens,
 
-        Implication(..), ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
+        Implication(..), newImplication,
+        ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
         SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
         bumpSubGoalDepth, subGoalDepthExceeded,
         CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
@@ -2414,17 +2415,38 @@ data Implication
       ic_binds  :: EvBindsVar,    -- Points to the place to fill in the
                                   -- abstraction and bindings.
 
-      ic_needed   :: VarSet,      -- Union of the ics_need fields of any /discarded/
-                                  -- solved implications in ic_wanted
+      -- The ic_need fields keep track of which Given evidence
+      -- is used by this implication or its children
+      -- NB: including stuff used by nested implications that have since
+      --     been discarded
+      ic_need_inner :: VarSet,    -- Includes all used Given evidence
+      ic_need_outer :: VarSet,    -- Includes only the free Given evidence
+                                  --  i.e. ic_need_inner after deleting
+                                  --       (a) givens (b) binders of ic_binds
 
       ic_status   :: ImplicStatus
     }
 
+newImplication :: Implication
+newImplication
+  = Implic { -- These fields must be initialisad
+             ic_tclvl = panic "newImplic:tclvl"
+           , ic_binds = panic "newImplic:binds"
+           , ic_info  = panic "newImplic:info"
+           , ic_env   = panic "newImplic:env"
+
+             -- The rest have sensible default values
+           , ic_skols      = []
+           , ic_given      = []
+           , ic_wanted     = emptyWC
+           , ic_no_eqs     = False
+           , ic_status     = IC_Unsolved
+           , ic_need_inner = emptyVarSet
+           , ic_need_outer = emptyVarSet }
+
 data ImplicStatus
   = IC_Solved     -- All wanteds in the tree are solved, all the way down
-       { ics_need :: VarSet     -- Evidence variables bound further out,
-                                -- but needed by this solved implication
-       , ics_dead :: [EvVar] }  -- Subset of ic_given that are not needed
+       { ics_dead :: [EvVar] }  -- Subset of ic_given that are not needed
          -- See Note [Tracking redundant constraints] in TcSimplify
 
   | IC_Insoluble  -- At least one insoluble constraint in the tree
@@ -2435,7 +2457,8 @@ instance Outputable Implication where
   ppr (Implic { ic_tclvl = tclvl, ic_skols = skols
               , ic_given = given, ic_no_eqs = no_eqs
               , ic_wanted = wanted, ic_status = status
-              , ic_binds = binds, ic_needed = needed , ic_info = info })
+              , ic_binds = binds, ic_need_inner = need_in
+              , ic_need_outer = need_out, ic_info = info })
    = hang (text "Implic" <+> lbrace)
         2 (sep [ text "TcLevel =" <+> ppr tclvl
                , text "Skolems =" <+> pprTyVars skols
@@ -2444,16 +2467,15 @@ instance Outputable Implication where
                , hang (text "Given =")  2 (pprEvVars given)
                , hang (text "Wanted =") 2 (ppr wanted)
                , text "Binds =" <+> ppr binds
-               , text "Needed =" <+> ppr needed
+               , text "Needed inner =" <+> ppr need_in
+               , text "Needed outer =" <+> ppr need_out
                , pprSkolInfo info ] <+> rbrace)
 
 instance Outputable ImplicStatus where
   ppr IC_Insoluble   = text "Insoluble"
   ppr IC_Unsolved    = text "Unsolved"
-  ppr (IC_Solved { ics_need = vs, ics_dead = dead })
-    = text "Solved"
-      <+> (braces $ vcat [ text "Dead givens =" <+> ppr dead
-                         , text "Needed =" <+> ppr vs ])
+  ppr (IC_Solved { ics_dead = dead })
+    = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead))
 
 {-
 Note [Needed evidence variables]
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 41a50976a0..d79a8a465a 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -42,9 +42,8 @@ module TcSMonad (
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
     getTopEnv, getGblEnv, getLclEnv,
     getTcEvBindsVar, getTcLevel,
-    getTcEvBindsAndTCVs, getTcEvBindsMap,
-    tcLookupClass,
-    tcLookupId,
+    getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap,
+    tcLookupClass, tcLookupId,
 
     -- Inerts
     InertSet(..), InertCans(..),
@@ -2636,16 +2635,13 @@ buildImplication skol_info skol_tvs givens (TcS thing_inside)
                             null (wl_deriv wl) && null (wl_implics wl), ppr wl )
                    WC { wc_simple = listToCts eqs
                       , wc_impl   = emptyBag }
-             imp = Implic { ic_tclvl  = new_tclvl
-                          , ic_skols  = skol_tvs
-                          , ic_no_eqs = True
-                          , ic_given  = givens
-                          , ic_wanted = wc
-                          , ic_status = IC_Unsolved
-                          , ic_binds  = ev_binds_var
-                          , ic_env    = env
-                          , ic_needed = emptyVarSet
-                          , ic_info   = skol_info }
+             imp = newImplication { ic_tclvl  = new_tclvl
+                                  , ic_skols  = skol_tvs
+                                  , ic_given  = givens
+                                  , ic_wanted = wc
+                                  , ic_binds  = ev_binds_var
+                                  , ic_env    = env
+                                  , ic_info   = skol_info }
       ; return (unitBag imp, TcEvBinds ev_binds_var, res) } }
 
 {-
@@ -2718,16 +2714,18 @@ getTcEvBindsVar = TcS (return . tcs_ev_binds)
 getTcLevel :: TcS TcLevel
 getTcLevel = wrapTcS TcM.getTcLevel
 
-getTcEvBindsAndTCVs :: EvBindsVar -> TcS (EvBindMap, TyCoVarSet)
-getTcEvBindsAndTCVs ev_binds_var
-  = wrapTcS $ do { bnds <- TcM.getTcEvBindsMap ev_binds_var
-                 ; tcvs <- TcM.getTcEvTyCoVars ev_binds_var
-                 ; return (bnds, tcvs) }
+getTcEvTyCoVars :: EvBindsVar -> TcS TyCoVarSet
+getTcEvTyCoVars ev_binds_var
+  = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var
 
 getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap
 getTcEvBindsMap ev_binds_var
   = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var
 
+setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
+setTcEvBindsMap ev_binds_var binds
+  = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
+
 unifyTyVar :: TcTyVar -> TcType -> TcS ()
 -- Unify a meta-tyvar with a type
 -- We keep track of how many unifications have happened in tcs_unified,
@@ -2883,7 +2881,7 @@ newFlattenSkolem flav loc tc xis
 ----------------------------
 unflattenGivens :: IORef InertSet -> TcM ()
 -- Unflatten all the fsks created by flattening types in Given
--- constraints We must be sure to do this, else we end up with
+-- constraints. We must be sure to do this, else we end up with
 -- flatten-skolems buried in any residual Wanteds
 --
 -- NB: this is the /only/ way that a fsk (MetaDetails = FlatSkolTv)
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index f1d7e9ade8..76765f7396 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -28,7 +28,6 @@ import DynFlags      ( WarningFlag ( Opt_WarnMonomorphism )
 import Id            ( idType )
 import Inst
 import ListSetOps
-import Maybes
 import Name
 import Outputable
 import PrelInfo
@@ -722,16 +721,13 @@ emitResidualConstraints rhs_tclvl tc_lcl_env ev_binds_var
      }
   where
     mk_implic inner_wanted
-       = Implic { ic_tclvl    = rhs_tclvl
-                , ic_skols    = qtvs
-                , ic_no_eqs   = False
-                , ic_given    = full_theta_vars
-                , ic_wanted   = inner_wanted
-                , ic_status   = IC_Unsolved
-                , ic_binds    = ev_binds_var
-                , ic_info     = skol_info
-                , ic_needed   = emptyVarSet
-                , ic_env      = tc_lcl_env }
+       = newImplication { ic_tclvl    = rhs_tclvl
+                        , ic_skols    = qtvs
+                        , ic_given    = full_theta_vars
+                        , ic_wanted   = inner_wanted
+                        , ic_binds    = ev_binds_var
+                        , ic_info     = skol_info
+                        , ic_env      = tc_lcl_env }
 
     full_theta = map idType full_theta_vars
     skol_info  = InferSkol [ (name, mkSigmaTy [] full_theta ty)
@@ -1540,7 +1536,8 @@ solveImplication imp@(Implic { ic_tclvl  = tclvl
        ; res_implic <- setImplicationStatus (imp { ic_no_eqs = no_given_eqs
                                                  , ic_wanted = final_wanted })
 
-       ; (evbinds, tcvs) <- TcS.getTcEvBindsAndTCVs ev_binds_var
+       ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
+       ; tcvs    <- TcS.getTcEvTyCoVars ev_binds_var
        ; traceTcS "solveImplication end }" $ vcat
              [ text "no_given_eqs =" <+> ppr no_given_eqs
              , text "floated_eqs =" <+> ppr floated_eqs
@@ -1557,97 +1554,75 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
 --    * Trim the ic_wanted field to remove Derived constraints
 -- Precondition: the ic_status field is not already IC_Solved
 -- Return Nothing if we can discard the implication altogether
-setImplicationStatus implic@(Implic { ic_binds  = ev_binds_var
-                                    , ic_status = status
+setImplicationStatus implic@(Implic { ic_status = status
                                     , ic_info   = info
                                     , ic_wanted = wc
-                                    , ic_needed = old_discarded_needs
                                     , ic_given  = givens })
  | ASSERT2( not (isSolvedStatus status ), ppr info )
    -- Precondition: we only set the status if it is not already solved
-   some_insoluble
- = return $ Just $
-   implic { ic_status = IC_Insoluble
-          , ic_needed = new_discarded_needs
-          , ic_wanted = pruned_wc }
-
- | some_unsolved
- = do { traceTcS "setImplicationStatus" $
-        vcat [ppr givens $$ ppr simples $$ ppr mb_implic_needs]
-      ; return $ Just $
-        implic { ic_status = IC_Unsolved
-               , ic_needed = new_discarded_needs
-               , ic_wanted = pruned_wc }
-   }
-
- | otherwise  -- Everything is solved; look at the implications
+   not all_solved
+ = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
+
+      ; implic <- neededEvVars implic
+
+      ; let new_status | insolubleWC pruned_wc = IC_Insoluble
+                       | otherwise             = IC_Unsolved
+            new_implic = implic { ic_status = new_status
+                                , ic_wanted = pruned_wc }
+
+      ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
+
+      ; return $ Just new_implic }
+
+ | otherwise  -- Everything is solved
+              -- Set status to IC_Solved,
+              -- and compute the dead givens and outer needs
               -- See Note [Tracking redundant constraints]
- = do { ev_binds <- TcS.getTcEvBindsAndTCVs ev_binds_var
-      ; let all_needs = neededEvVars ev_binds $
-                        solved_implic_needs `unionVarSet` new_discarded_needs
+ = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
 
-            dead_givens | warnRedundantGivens info
-                        = filterOut (`elemVarSet` all_needs) givens
-                        | otherwise = []   -- None to report
+      ; implic <- neededEvVars implic
 
-            final_needs = all_needs `delVarSetList` givens
+      ; let dead_givens | warnRedundantGivens info
+                        = filterOut (`elemVarSet` ic_need_inner implic) givens
+                        | otherwise = []   -- None to report
 
             discard_entire_implication  -- Can we discard the entire implication?
               =  null dead_givens           -- No warning from this implication
               && isEmptyBag pruned_implics  -- No live children
-              && isEmptyVarSet final_needs  -- No needed vars to pass up to parent
+              && isEmptyVarSet (ic_need_outer implic) -- No needed vars to pass up to parent
 
-            final_status = IC_Solved { ics_need = final_needs
-                                     , ics_dead = dead_givens }
+            final_status = IC_Solved { ics_dead = dead_givens }
             final_implic = implic { ic_status = final_status
-                                  , ic_needed = emptyVarSet -- Irrelevant for IC_Solved
                                   , ic_wanted = pruned_wc }
 
-        -- Check that there are no term-level evidence bindings
-        -- in the cases where we have no place to put them
-      ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap (fst ev_binds)
-                , ppr info $$ ppr ev_binds )
+      ; traceTcS "setImplicationStatus(all-solved) }" $
+        vcat [ text "discard:" <+> ppr discard_entire_implication
+             , text "new_implic:" <+> ppr final_implic ]
 
-      ; traceTcS "setImplicationStatus 2" $
-        vcat [ppr givens $$ ppr ev_binds $$ ppr all_needs]
       ; return $ if discard_entire_implication
                  then Nothing
                  else Just final_implic }
  where
    WC { wc_simple = simples, wc_impl = implics } = wc
 
-   some_insoluble = insolubleWC wc
-   some_unsolved = not (isEmptyBag simples)
-                 || isNothing mb_implic_needs
-
    pruned_simples = dropDerivedSimples simples
-   (pruned_implics, discarded_needs) = partitionBagWith discard_me implics
-   pruned_wc = wc { wc_simple = pruned_simples
+   pruned_implics = filterBag keep_me implics
+   pruned_wc = WC { wc_simple = pruned_simples
                   , wc_impl   = pruned_implics }
-   new_discarded_needs = foldrBag unionVarSet old_discarded_needs discarded_needs
-
-   mb_implic_needs :: Maybe VarSet
-        -- Just vs => all implics are IC_Solved, with 'vs' needed
-        -- Nothing => at least one implic is not IC_Solved
-   mb_implic_needs   = foldrBag add_implic (Just emptyVarSet) pruned_implics
-   Just solved_implic_needs = mb_implic_needs
-
-   add_implic implic acc
-      | Just vs_acc <- acc
-      , IC_Solved { ics_need = vs } <- ic_status implic
-      = Just (vs `unionVarSet` vs_acc)
-      | otherwise = Nothing
-
-   discard_me :: Implication -> Either Implication VarSet
-   discard_me ic
-     | IC_Solved { ics_dead = dead_givens, ics_need = needed } <- ic_status ic
+
+   all_solved = isEmptyBag pruned_simples
+             && allBag (isSolvedStatus . ic_status) pruned_implics
+
+   keep_me :: Implication -> Bool
+   keep_me ic
+     | IC_Solved { ics_dead = dead_givens } <- ic_status ic
                           -- Fully solved
      , null dead_givens   -- No redundant givens to report
      , isEmptyBag (wc_impl (ic_wanted ic))
            -- And no children that might have things to report
-     = Right needed
+     = False       -- Tnen we don't need to keep it
      | otherwise
-     = Left ic
+     = True        -- Otherwise, keep it
 
 warnRedundantGivens :: SkolemInfo -> Bool
 warnRedundantGivens (SigSkol ctxt _ _)
@@ -1661,38 +1636,82 @@ warnRedundantGivens (SigSkol ctxt _ _)
 warnRedundantGivens (InstSkol {}) = True
 warnRedundantGivens _             = False
 
-neededEvVars :: (EvBindMap, TcTyVarSet) -> VarSet -> VarSet
+neededEvVars :: Implication -> TcS Implication
 -- Find all the evidence variables that are "needed",
---    and then delete all those bound by the evidence bindings
--- See Note [Tracking redundant constraints]
+-- and delete dead evidence bindings
+--   See Note [Tracking redundant constraints]
+--   See Note [Delete dead Given evidence bindings]
 --
 --   - Start from initial_seeds (from nested implications)
+--
 --   - Add free vars of RHS of all Wanted evidence bindings
 --     and coercion variables accumulated in tcvs (all Wanted)
---   - Do transitive closure through Given bindings
---     e.g.   Neede {a,b}
+--
+--   - Generate 'needed', the needed set of EvVars, by doing transitive
+--     closure through Given bindings
+--     e.g.   Needed {a,b}
 --            Given  a = sc_sel a2
 --            Then a2 is needed too
---   - Finally delete all the binders of the evidence bindings
 --
-neededEvVars (ev_binds, tcvs) initial_seeds
- = needed `minusVarSet` bndrs
+--   - Prune out all Given bindings that are not needed
+--
+--   - From the 'needed' set, delete ev_bndrs, the binders of the
+--     evidence bindings, to give the final needed variables
+--
+neededEvVars implic@(Implic { ic_info = info
+                            , ic_given = givens
+                            , ic_binds = ev_binds_var
+                            , ic_wanted = WC { wc_impl = implics }
+                            , ic_need_inner = old_needs })
+ = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
+      ; tcvs     <- TcS.getTcEvTyCoVars ev_binds_var
+
+        -- Check that there are no term-level evidence bindings
+        -- in the cases where we have no place to put them
+      ; MASSERT2( termEvidenceAllowed info || isEmptyEvBindMap ev_binds
+                , ppr info $$ ppr ev_binds )
+
+      ; let seeds1        = foldrBag add_implic_seeds old_needs implics
+            seeds2        = foldEvBindMap add_wanted seeds1 ev_binds
+            seeds3        = seeds2 `unionVarSet` tcvs
+            need_inner    = transCloVarSet (also_needs ev_binds) seeds3
+            live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
+            need_outer    = foldEvBindMap del_ev_bndr need_inner live_ev_binds
+                            `delVarSetList` givens
+
+      ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
+           -- See Note [Delete dead Given evidence bindings]
+
+      ; traceTcS "neededEvVars" $
+        vcat [ text "old_needs:" <+> ppr old_needs
+             , text "seeds3:" <+> ppr seeds3
+             , text "ev_binds:" <+> ppr ev_binds
+             , text "live_ev_binds:" <+> ppr live_ev_binds ]
+
+      ; return (implic { ic_need_inner = need_inner
+                       , ic_need_outer = need_outer }) }
  where
-   needed = transCloVarSet also_needs seeds
-   seeds  = foldEvBindMap add_wanted initial_seeds ev_binds
-            `unionVarSet` tcvs
-   bndrs  = foldEvBindMap add_bndr emptyVarSet ev_binds
+   add_implic_seeds (Implic { ic_need_outer = needs, ic_given = givens }) acc
+      = (needs `delVarSetList` givens) `unionVarSet` acc
+
+   needed_ev_bind needed (EvBind { eb_lhs = ev_var
+                                 , eb_is_given = is_given })
+     | is_given  = ev_var `elemVarSet` needed
+     | otherwise = True   -- Keep all wanted bindings
+
+   del_ev_bndr :: EvBind -> VarSet -> VarSet
+   del_ev_bndr (EvBind { eb_lhs = v }) needs = delVarSet needs v
 
    add_wanted :: EvBind -> VarSet -> VarSet
    add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
      | is_given  = needs  -- Add the rhs vars of the Wanted bindings only
      | otherwise = evVarsOfTerm rhs `unionVarSet` needs
 
-   also_needs :: VarSet -> VarSet
-   also_needs needs
+   also_needs :: EvBindMap -> VarSet -> VarSet
+   also_needs ev_binds needs
      = nonDetFoldUniqSet add emptyVarSet needs
-     -- It's OK to use nonDetFoldUFM here because we immediately forget
-     -- about the ordering by creating a set
+     -- It's OK to use nonDetFoldUFM here because we immediately
+     -- forget about the ordering by creating a set
      where
        add v needs
         | Just ev_bind <- lookupEvBind ev_binds v
@@ -1702,11 +1721,43 @@ neededEvVars (ev_binds, tcvs) initial_seeds
         | otherwise
         = needs
 
-   add_bndr :: EvBind -> VarSet -> VarSet
-   add_bndr (EvBind { eb_lhs = v }) vs = extendVarSet vs v
-
+{- Note [Delete dead Given evidence bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As a result of superclass expansion, we speculatively
+generate evidence bindings for Givens. E.g.
+   f :: (a ~ b) => a -> b -> Bool
+   f x y = ...
+We'll have
+   [G] d1 :: (a~b)
+and we'll specuatively generate the evidence binding
+   [G] d2 :: (a ~# b) = sc_sel d
+
+Now d2 is available for solving.  But it may not be needed!  Usually
+such dead superclass selections will eventually be dropped as dead
+code, but:
+
+ * It won't always be dropped (Trac #13032).  In the case of an
+   unlifted-equality superclass like d2 above, we generate
+       case heq_sc d1 of d2 -> ...
+   and we can't (in general) drop that case exrpession in case
+   d1 is bottom.  So it's technically unsound to have added it
+   in the first place.
+
+ * Simply generating all those extra superclasses can generate lots of
+   code that has to be zonked, only to be discarded later.  Better not
+   to generate it in the first place.
+
+   Moreover, if we simplify this implication more than once
+   (e.g. because we can't solve it completely on the first iteration
+   of simpl_looop), we'll generate all the same bindings AGAIN!
+
+Easy solution: take advantage of the work we are doing to track dead
+(unused) Givens, and use it to prune the Given bindings too.  This is
+all done by neededEvVars.
+
+This led to a remarkable 25% overall compiler allocation decrease in
+test T12227.
 
-{-
 Note [Tracking redundant constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 With Opt_WarnRedundantConstraints, GHC can report which
@@ -1743,18 +1794,16 @@ works:
 
 ----- How tracking works
 
+* The ic_need fields of an Implic records in-scope (given) evidence
+  variables bound by the context, that were needed to solve this
+  implication (so far).  See the declaration of Implication.
+
 * When the constraint solver finishes solving all the wanteds in
   an implication, it sets its status to IC_Solved
 
   - The ics_dead field, of IC_Solved, records the subset of this
     implication's ic_given that are redundant (not needed).
 
-  - The ics_need field of IC_Solved then records all the
-    in-scope (given) evidence variables bound by the context, that
-    were needed to solve this implication, including all its nested
-    implications.  (We remove the ic_given of this implication from
-    the set, of course.)
-
 * We compute which evidence variables are needed by an implication
   in setImplicationStatus.  A variable is needed if
     a) it is free in the RHS of a Wanted EvBind,
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index fc2763ab1b..2c374285fc 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1186,16 +1186,13 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
     do { ev_binds_var <- newTcEvBinds
        ; env <- getLclEnv
-       ; let implic = Implic { ic_tclvl = tclvl
-                             , ic_skols = skol_tvs
-                             , ic_no_eqs = False
-                             , ic_given = given
-                             , ic_wanted = wanted
-                             , ic_status  = IC_Unsolved
-                             , ic_binds = ev_binds_var
-                             , ic_env = env
-                             , ic_needed = emptyVarSet
-                             , ic_info = skol_info }
+       ; let implic = newImplication { ic_tclvl  = tclvl
+                                     , ic_skols  = skol_tvs
+                                     , ic_given  = given
+                                     , ic_wanted = wanted
+                                     , ic_binds  = ev_binds_var
+                                     , ic_env    = env
+                                     , ic_info   = skol_info }
 
        ; return (unitBag implic, TcEvBinds ev_binds_var) }
 
diff --git a/testsuite/tests/indexed-types/should_compile/T7837.stderr b/testsuite/tests/indexed-types/should_compile/T7837.stderr
index 44b894e5fd..6e0720e8d0 100644
--- a/testsuite/tests/indexed-types/should_compile/T7837.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T7837.stderr
@@ -2,4 +2,3 @@ Rule fired: Class op signum (BUILTIN)
 Rule fired: Class op abs (BUILTIN)
 Rule fired: Class op heq_sel (BUILTIN)
 Rule fired: normalize/Double (T7837)
-Rule fired: Class op heq_sel (BUILTIN)
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index b161829546..61b61ae78a 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -1010,12 +1010,13 @@ test('T10547',
 test('T12227',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 1060158624, 5),
+          [(wordsize(64), 812869424, 5),
           # 2016-07-11    5650186880 (Windows) before fix for #12227
           # 2016-07-11    1822822016 (Windows) after fix for #12227
           # 2016-12-20    1715827784 after d250d493 (INLINE in Traversable dms)
           #                          (or thereabouts in the commit history)
           # 2017-02-14    1060158624  Early inlining: 35% improvement
+          # 2018-01-04    812869424   Drop unused givens (#13032): 23% better
           ]),
      ],
      compile,
diff --git a/testsuite/tests/simplCore/should_compile/T4398.stderr b/testsuite/tests/simplCore/should_compile/T4398.stderr
index e1fa710a43..c9b89ca6b4 100644
--- a/testsuite/tests/simplCore/should_compile/T4398.stderr
+++ b/testsuite/tests/simplCore/should_compile/T4398.stderr
@@ -2,21 +2,5 @@
 T4398.hs:6:11: warning:
     Forall'd constraint ‘Ord a’ is not bound in RULE lhs
       Orig bndrs: [a, $dOrd, x, y]
-      Orig lhs: let {
-                  $dEq :: Eq a
-                  [LclId]
-                  $dEq = GHC.Classes.$p1Ord @ a $dOrd } in
-                f @ a
-                  ((\ ($dOrd :: Ord a) ->
-                      let {
-                        $dEq :: Eq a
-                        [LclId]
-                        $dEq = GHC.Classes.$p1Ord @ a $dOrd } in
-                      let {
-                        $dEq :: Eq a
-                        [LclId]
-                        $dEq = GHC.Classes.$p1Ord @ a $dOrd } in
-                      x)
-                     $dOrd)
-                  y
+      Orig lhs: f @ a ((\ ($dOrd :: Ord a) -> x) $dOrd) y
       optimised lhs: f @ a x y
diff --git a/testsuite/tests/typecheck/should_compile/T13032.hs b/testsuite/tests/typecheck/should_compile/T13032.hs
new file mode 100644
index 0000000000..065656e20c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13032.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -ddump-ds -dsuppress-uniques #-}
+{-# LANGUAGE GADTs #-}
+
+module T13032 where
+
+f :: (a ~ b) => a -> b -> Bool
+f x y = True
+
+-- The point of the test is to check that we don't
+-- get a redundant superclass selection to fetch an
+-- equality constraint out of the (a~b) dictionary
+-- Hence -ddump-ds
diff --git a/testsuite/tests/typecheck/should_compile/T13032.stderr b/testsuite/tests/typecheck/should_compile/T13032.stderr
new file mode 100644
index 0000000000..f7620c75a2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T13032.stderr
@@ -0,0 +1,20 @@
+
+==================== Desugar (after optimization) ====================
+Result size of Desugar (after optimization)
+  = {terms: 13, types: 24, coercions: 0, joins: 0/0}
+
+-- RHS size: {terms: 6, types: 11, coercions: 0, joins: 0/0}
+f :: forall a b. ((a :: *) ~ (b :: *)) => a -> b -> Bool
+[LclIdX]
+f = \ (@ a) (@ b) _ [Occ=Dead] _ [Occ=Dead] _ [Occ=Dead] ->
+      GHC.Types.True
+
+-- RHS size: {terms: 5, types: 0, coercions: 0, joins: 0/0}
+T13032.$trModule :: GHC.Types.Module
+[LclIdX]
+T13032.$trModule
+  = GHC.Types.Module
+      (GHC.Types.TrNameS "main"#) (GHC.Types.TrNameS "T13032"#)
+
+
+
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index e516d36f6c..2a89eb3931 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -587,3 +587,4 @@ test('MissingExportList01', normal, compile, [''])
 test('MissingExportList02', normal, compile, [''])
 test('T14488', normal, compile, [''])
 test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
+test('T13032', normal, compile, [''])