+      = do impls' <- mapBagM go_impl impls

+      = return impl

+solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implication

+  impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var

+               , ic_need_implic = inner })

+  = return impl

+              , ic_need_implic = inner `extendEvNeedSet` given_ev } }

+                -- Record that the Given is needed; I'm not certain why

+           ; impls <- mapBagM (solveImplicationUsingUnsatGiven unsat_given) impls

+      = do { simples' <- mapMaybeBagM go_simple simples

+           ; implics' <- mapBagM go_implic implics

+           ; return (wc { wc_simple = simples', wc_impl = implics' }) }

+    go_implic :: Implication -> TcS Implication

+      = return implic  -- Nothing to solve inside here

+       (b) Prefer constraints that are not superclass selections. See

+           (TRC3) in Note [Tracking redundant constraints] in GHC.Tc.Solver.

+import GHC.Types.Unique.Set( nonDetStrictFoldUniqSet )

+

+import Data.List( deleteFirstsBy )

+       ; return unsolved_implics }

+solveImplication :: Implication     -- Wanted

+                 -> TcS Implication -- Simplified implication (empty or singleton)

+  = return imp  -- Do nothing

+setImplicationStatus :: Implication -> TcS Implication

+--   * Set the ic_status field

+--   * Prune unnecessary evidence bindings

+--   * Prune unnecessary child implications

+setImplicationStatus implic@(Implic { ic_status = old_status

+                                    , ic_info   = info

+                                    , ic_wanted = wc })

+ = assertPpr (not (isSolvedStatus old_status)) (ppr info) $

+   do { traceTcS "setImplicationStatus {" (ppr implic)

+

+      ; let solved = isSolvedWC wc

+      ; new_implic    <- neededEvVars implic

+      ; bad_telescope <- if solved then checkBadTelescope implic

+                                   else return False

+

+      ; let new_status | insolubleWC wc = IC_Insoluble

+                       | not solved     = IC_Unsolved

+                       | bad_telescope  = IC_BadTelescope

+                       | otherwise      = IC_Solved { ics_dead = dead_givens }

+            dead_givens = findRedundantGivens new_implic

+            new_wc      = pruneImplications wc

+

+            final_implic = new_implic { ic_status = new_status

+                                      , ic_wanted = new_wc }

+

+      ; traceTcS "setImplicationStatus }" (ppr final_implic)

+      ; return final_implic }

+

+pruneImplications :: WantedConstraints -> WantedConstraints

+-- We have now recorded the `ic_need` variables of the child

+-- implications (in `ic_need_implics` of the parent) so we can

+-- delete any unnecessary children.

+pruneImplications wc@(WC { wc_impl = implics })

+  = wc { wc_impl = filterBag keep_me implics }

+         -- Do not prune holes; these should be reported

+  where

+    keep_me :: Implication -> Bool

+    keep_me (Implic { ic_status = status, ic_wanted = wanted })

+      | IC_Solved { ics_dead = dead_givens } <- status -- Fully solved

+      , null dead_givens                               -- No redundant givens to report

+      , isEmptyBag (wc_impl wanted)                    -- No children that might have things to report

+      = False

+      | otherwise

+      = True        -- Otherwise, keep it

+findRedundantGivens :: Implication -> [EvVar]

+findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens })

+  = []                    -- See (TRC4) of Note [Tracking redundant constraints]

+  -- Only try this if unused_givens is empty: see (TRC2a)

+    needed_givens_ignoring_default_methods = ens_fvs need

+                  || given `elemVarSet` needed_givens_ignoring_default_methods

+    minimal_givens = mkMinimalBySCs evVarPred givens  -- See (TRC2)

+

+warnRedundantGivens :: SkolemInfoAnon -> Bool

+warnRedundantGivens (SigSkol ctxt _ _)

+  = case ctxt of

+       FunSigCtxt _ rrc -> reportRedundantConstraints rrc

+       ExprSigCtxt rrc  -> reportRedundantConstraints rrc

+       _                -> False

+

+warnRedundantGivens (InstSkol from _)

+ -- Do not report redundant constraints for quantified constraints

+ -- See (TRC4) in Note [Tracking redundant constraints]

+ -- Fortunately it is easy to spot implications constraints that arise

+ -- from quantified constraints, from their SkolInfo

+ = case from of

+      IsQC {}      -> False

+      IsClsInst {} -> True

+

+  -- To think about: do we want to report redundant givens for

+  -- pattern synonyms, PatSynSigSkol? c.f #9953, comment:21.

+warnRedundantGivens _ = False

+

+-- /and/ delete dead evidence bindings

+--

+

+neededEvVars implic@(Implic { ic_info        = info

+                            , ic_binds       = ev_binds_var

+                            , ic_wanted      = WC { wc_impl = implics }

+                            , ic_need_implic = old_need_implic    -- See (TRC1)

+                    })

+      ; let -- Find the variables needed by `implics`

+            new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds })

+                = foldr add_implic old_need_implic implics

+                  -- Start from old_need_implic!  See (TRC1)

+

+            -- Get the variables needed by the solved bindings

+            -- (It's OK to use a non-deterministic fold here

+            --  because add_wanted is commutative.)

+            seeds_w = nonDetStrictFoldEvBindMap add_wanted tcvs ev_binds

+

+            need_ignoring_dms = findNeededGivenEvVars ev_binds (other_seeds `unionVarSet` seeds_w)

+            need_from_dms     = findNeededGivenEvVars ev_binds dm_seeds

+            need_full         = need_ignoring_dms `unionVarSet` need_from_dms

+

+            -- `need`: the Givens from outer scopes that are used in this implication

+            -- is_dm_skol: see (TRC5)

+            need | is_dm_skol info = ENS { ens_dms = trim ev_binds need_full

+                                         , ens_fvs = emptyVarSet }

+                 | otherwise       = ENS { ens_dms = trim ev_binds need_from_dms

+                                         , ens_fvs = trim ev_binds need_ignoring_dms }

+

+      -- Delete dead Given evidence bindings

+      -- See Note [Delete dead Given evidence bindings]

+      ; let live_ev_binds = filterEvBindMap (needed_ev_bind need_full) ev_binds

+        vcat [ text "old_need_implic:" <+> ppr old_need_implic

+             , text "new_need_implic:" <+> ppr new_need_implic

+             , text "need_ignoring_dms:" <+> ppr need_ignoring_dms

+             , text "need_from_dms:"     <+> ppr need_from_dms

+             , text "need:" <+> ppr need

+      ; return (implic { ic_need        = need

+                       , ic_need_implic = new_need_implic }) }

+    trim :: EvBindMap -> VarSet -> VarSet

+    -- Delete variables bound by Givens or bindings

+    trim ev_binds needs = needs `varSetMinusEvBindMap` ev_binds

+

+    add_implic :: Implication -> EvNeedSet -> EvNeedSet

+    add_implic (Implic { ic_given = givens, ic_need = need }) acc

+       = (need `delGivensFromEvNeedSet` givens) `unionEvNeedSet` acc

+

+    needed_ev_bind needed (EvBind { eb_lhs = ev_var, eb_info = info })

+      | EvBindGiven{} <- info = ev_var `elemVarSet` needed

+      | otherwise             = True   -- Keep all wanted bindings

+

+    add_wanted :: EvBind -> VarSet -> VarSet

+    add_wanted (EvBind { eb_info = info, eb_rhs = rhs }) needs

+      | EvBindGiven{} <- info = needs  -- Add the rhs vars of the Wanted bindings only

+      | otherwise = evVarsOfTerm rhs `unionVarSet` needs

+

+    is_dm_skol :: SkolemInfoAnon -> Bool

+    is_dm_skol (MethSkol _ is_dm) = is_dm

+    is_dm_skol _                  = False

+

+findNeededGivenEvVars :: EvBindMap -> VarSet -> VarSet

+-- Find all the Given evidence needed by seeds,

+-- looking transitively through bindings for Givens (only)

+findNeededGivenEvVars ev_binds seeds

+  = transCloVarSet also_needs seeds

+  where

+   also_needs :: VarSet -> VarSet

+   also_needs needs = nonDetStrictFoldUniqSet add emptyVarSet needs

+     -- It's OK to use a non-deterministic fold here because we immediately

+     -- forget about the ordering by creating a set

+

+   add :: Var -> VarSet -> VarSet

+   add v needs

+     | Just ev_bind <- lookupEvBind ev_binds v

+     , EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind

+       -- Look at Given bindings only

+     = evVarsOfTerm rhs `unionVarSet` needs

+     | otherwise

+     = needs

+With Opt_WarnRedundantConstraints, GHC can report which constraints of a type

+signature (or instance declaration) are redundant, and can be omitted.  Here is

+an overview of how it works.

+This is all tested in typecheck/should_compile/T20602 (among others).

+How tracking works:

+* We maintain the `ic_need` field in an implication:

+     ic_need: the set of Given evidence variables that are needed somewhere

+              inside this implication; and are bound either by this implication

+              or by an enclosing one.

+* `setImplicationStatus` does all the work:

+  - When the constraint solver finishes solving all the wanteds in

+    an implication, it sets its status to IC_Solved

+  - `neededEvVars`: computes which evidence variables are needed by an

+    implication in `setImplicationStatus`.  A variable is needed if

+      a) It is in the ic_need field of this implication, computed in

+         a previous call to `setImplicationStatus`; see (TRC1)

+      b) It is in the ics_need of a nested implication; see `add_implic`

+         in `neededEvVars`

+

+      c) It is free in the RHS of any /Wanted/ EvBind; each such binding

+         solves a Wanted, so we want them all.  See `add_wanted` in

+         `neededEvVars`

+

+      d) It is free in the RHS of a /Given/ EvBind whose LHS is needed:

+         see `findNeededGivenEvVars` called from `neededEvVars`.

+

+  - Next, if the final status is IC_Solved, `setImplicationStatus` uses

+    `findRedundantGivens` to decide which of this implication's Givens

+    are redundant.

+

+  - It also uses `pruneImplications` to discard any now-unnecessary child

+    implications.

+

+* GHC.Tc.Errors does the actual warning, in `warnRedundantConstraints`.

+

+

+Wrinkles:

+

+(TRC1) `pruneImplications` drops any sub-implications of an Implication

+  that are irrelevant for error reporting:

+      - no unsolved wanteds

+      - no sub-implications

+      - no redundant givens to report

+  But in doing so we must not lose track of the variables that those implications

+  needed!  So we track the ic_needs of all child implications in `ic_need_implics`.

+  Crucially, this set includes things need by child implications that have been

+  discarded by `pruneImplications`.

+

+(TRC2) A Given can be redundant because it is implied by other Givens

+         f :: (Eq a, Ord a)     => blah   -- Eq a unnecessary

+         g :: (Eq a, a~b, Eq b) => blah   -- Either Eq a or Eq b unnecessary

+   We nail this by using `mkMinimalBySCs` in `findRedundantGivens`.

+   (TRC2a) But NOTE that we only attempt this mkMinimalBySCs stuff if all Givens

+   used by evidence bindings.  Example:

+      f :: (Eq a, Ord a) => a -> Bool

+      f x = x == x

+   We report (Ord a) as unused because it is. But we must not also report (Eq a)

+   as unused because it is a superclass of Ord!

+(TRC3) When two Givens are the same, prefer one that does not involve superclass

+  selection, or more generally has shallower superclass-selection depth:

+  see 2(b,c) in Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.

+    e.g        f :: (Eq a, Ord a) => a -> Bool

+               f x = x == x

+  Eager superclass expansion gives us two [G] Eq a constraints. We want to keep

+  the one from the user-written Eq a, not the superclass selection. This means

+  we report the Ord a as redundant with -Wredundant-constraints, not the Eq a.

+  Getting this wrong was #20602.

+(TRC4) We don't compute redundant givens for *every* implication; only

+  for those which reply True to `warnRedundantGivens`:

+   - We do not want to report redundant constraints for implications

+     that come from quantified constraints.  Example #23323:

+        data T a

+        instance Show (T a) where ...  -- No context!

+        foo :: forall f c. (forall a. c a => Show (f a)) => Proxy c -> f Int -> Int

+        bar = foo @T @Eq

+

+     The call to `foo` gives us

+       [W] d : (forall a. Eq a => Show (T a))

+     To solve this, GHC.Tc.Solver.Solve.solveForAll makes an implication constraint:

+       forall a. Eq a =>  [W] ds : Show (T a)

+     and because of the degnerate instance for `Show (T a)`, we don't need the `Eq a`

+     constraint.  But we don't want to report it as redundant!

+

+(TRC5) Consider this (#25992), where `op2` has a default method

+        class C a where { op1, op2 :: a -> a

+                        ; op2 = op1 . op1 }

+        instance C a => C [a] where

+          op1 x = x

+

+  Plainly the (C a) constraint is unused; but the expanded decl will look like

+        $dmop2 :: C a => a -> a

+        $dmop2 = op1 . op2

+

+        $fCList :: forall a. C a => C [a]

+        $fCList @a (d::C a) = MkC (\(x:a).x) ($dmop2 @a d)

+

+   Notice that `d` gets passed to `$dmop`: it is "needed".  But it's only

+   /really/ needed if some /other/ method (in this case `op1`) uses it.

+

+   So, rather than one set of "needed Givens" we use `EvNeedSet` to track

+   a /pair/ of sets:

+      ens_dms: needed /only/ by default-method calls

+      ens_fvs: needed by something other than a default-method call

+   It's a bit of a palaver, but not really difficult.

+   All the logic is localised in `neededEvVars`.

+

+

+

+----- Reporting redundant constraints

+

+

+----- Examples

+

+    f, g, h :: (Eq a, Ord a) => a -> Bool

+    f x = x == x

+    g x = x > x

+    h x = x == x && x > x

+

+    All of f,g,h will discover that they have two [G] Eq a constraints: one as

+    given and one extracted from the Ord a constraint. They will both discard

+    the latter; see (TRC3).

+

+    The body of f uses the [G] Eq a, but not the [G] Ord a. It will report a

+    redundant Ord a.

+

+    The body of g uses the [G] Ord a, but not the [G] Eq a. It will report a

+    redundant Eq a.

+

+    The body of h uses both [G] Ord a and [G] Eq a; each is used in a solved

+    Wanted evidence binding.  But (TRC2) kicks in and discovers the Eq a

+    is redundant.

+      thing_inside env

+        ; skol_info <- mkSkolemInfo (InstSkol IsClsInst pSizeZero)

+                       -- pSizeZero: here the size part of InstSkol is irrelevant

+tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys

+      = tcMethodBody False clas tyvars dfun_ev_vars inst_tys

+           ; tcMethodBody True clas tyvars dfun_ev_vars inst_tys

+tcMethodBody :: Bool

+tcMethodBody is_def_meth clas tyvars dfun_ev_vars inst_tys

+       ; let skol_info = MethSkol meth_name is_def_meth

+                                              (idName local_meth_id) }

+       ; spec_prags     <- tcExtendIdEnv1 meth_name global_meth_id $

+    meth_name = idName sel_id

+

+        EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet,