- -- Do not report redundant constraints for quantified constraints

- -- See (RC4) in Note [Tracking redundant constraints]

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

- -- from quantified constraints, from their SkolInfo

- | InstSkol (IsQC {}) _ <- info

- = return ()

-

-               , ic_need_pruned = inner })

-              , ic_need_pruned = inner `extendEvNeedSet` given_ev } }

-       (b) Prefer constraints that are not superclass selections. Example:

-

-             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. See also

-           Note [Tracking redundant constraints] in GHC.Tc.Solver.

--- setting the ic_status field

--- Return Nothing if we can discard the implication altogether

- | assertPpr (not (isSolvedStatus old_status)) (ppr info) $

-   not (isSolvedWC wc)

- = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)

-      ; let new_status | insolubleWC wc = IC_Insoluble

-                       | otherwise      = IC_Unsolved

-            new_implic = pruneImplications (implic { ic_status = new_status })

-

-      ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)

-

-      ; return new_implic }

-

- | otherwise

- = do { traceTcS "setImplicationStatus(solved) {" (ppr implic)

-      ; (dead_givens, implic) <- neededEvVars implic

-

-      ; bad_telescope <- checkBadTelescope implic

-      ; let final_status

-              | bad_telescope = IC_BadTelescope

-              | otherwise     = IC_Solved { ics_dead = dead_givens }

-            final_implic = pruneImplications (implic { ic_status = final_status })

-      ; traceTcS "setImplicationStatus(solved) }" (ppr final_implic)

-pruneImplications :: Implication -> Implication

--- We have now taken account of the `needs_outer` variables of these

--- implications, so we can drop any that are no longer necessary

-pruneImplications implic@(Implic { ic_wanted      = wc

-                                 , ic_need_pruned = old_needs })

-  = implic { ic_need_pruned = new_needs

-           , ic_wanted      = wc { wc_impl = new_implics } }

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

-  where

-    (new_needs, new_implics) = foldr do_one (old_needs, emptyBag) (wc_impl wc)

-

-    do_one :: Implication -> (EvNeedSet, Bag Implication) -> (EvNeedSet, Bag Implication)

-    do_one implic (ens, implics)

-      | keep_me implic = (ens, implic `consBag` implics)

-      | otherwise      = (add_needs ens implic, implics)

-

-    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

-

-    add_needs :: EvNeedSet -> Implication -> EvNeedSet

-    -- For a default-method implication, add all its needed vars to ens_dms

-    -- For anything else, just propagate

-    add_needs (ENS { ens_dms = dms, ens_fvs = fvs })

-              (Implic { ic_need_outer = ENS { ens_dms = dms1, ens_fvs = fvs1 }

-                      , ic_info = info })

-      | is_dm_skol info = ENS { ens_dms = dms `unionVarSet` dms1 `unionVarSet` fvs1

-                              , ens_fvs = fvs }

-      | otherwise       = ENS { ens_dms = dms `unionVarSet` dms1

-                              , ens_fvs = fvs `unionVarSet` fvs1 }

-

-findUnnecessaryGivens :: SkolemInfoAnon -> VarSet -> [EvVar] -> [EvVar]

-findUnnecessaryGivens info need_inner givens

-  = []

-                  || given `elemVarSet` need_inner

-    minimal_givens = mkMinimalBySCs evVarPred givens

-warnRedundantGivens :: SkolemInfoAnon -> Bool

-warnRedundantGivens (SigSkol ctxt _ _)

-  = case ctxt of

-       FunSigCtxt _ rrc -> reportRedundantConstraints rrc

-       ExprSigCtxt rrc  -> reportRedundantConstraints rrc

-       _                -> False

-

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

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

-warnRedundantGivens (InstSkol {}) = True

-warnRedundantGivens _             = False

-

-neededEvVars :: Implication -> TcS ([EvVar], Implication)

---   - From the 'needed' set, delete ev_bndrs, the binders of the

---     evidence bindings, to give the final needed variables

---

-neededEvVars implic@(Implic { ic_given = givens

-                            , ic_info  = info

-                            , ic_binds = ev_binds_var

-                            , ic_wanted = WC { wc_impl = implics }

-                            , ic_need_pruned = need_pruned })

-      ; let -- Get the variables needed by the implications

-            ENS { ens_dms = implic_dm_seeds, ens_fvs = implic_other_seeds }

-              = foldr add_implic_seeds need_pruned implics

-                        -- `seeds_w` are the vars mentioned by all the solved Wanted bindings

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

-                        --  because add_wanted is commutative.)

-            need_ignoring_dms = findNeededGivenEvVars ev_binds (implic_other_seeds `unionVarSet` seeds_w)

-            need_from_dms     = findNeededGivenEvVars ev_binds implic_dm_seeds

-            live_ev_binds = filterEvBindMap (needed_ev_bind need_full) ev_binds

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

-

-      ; let -- `dead_givens` are the Givens from this implication that are unused

-            dead_givens = findUnnecessaryGivens info need_ignoring_dms givens

-            -- `need_outer` are the Givens from outer scopes that are used in this implication

-            need_outer

-              | is_dm_skol info = ENS { ens_dms = trim live_ev_binds need_full

-                                      , ens_fvs = emptyVarSet }

-              | otherwise       = ENS { ens_dms = trim live_ev_binds need_from_dms

-                                      , ens_fvs = trim live_ev_binds need_ignoring_dms }

-        vcat [ text "old need_pruned:" <+> ppr need_pruned

-             , text "need_outer:" <+> ppr need_outer

-             , text "dead_givens:" <+> ppr dead_givens

-

-      ; return ( dead_givens

-               , implic { ic_need_outer = need_outer }) }

-   trim :: EvBindMap -> VarSet -> VarSet

-   -- Delete variables bound by Givens or bindings

-   trim live_ev_binds needs = (needs `varSetMinusEvBindMap` live_ev_binds)

-                              `delVarSetList` givens

-   add_implic_seeds :: Implication -> EvNeedSet -> EvNeedSet

-   add_implic_seeds (Implic { ic_need_outer = needs }) acc

-      = needs `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

-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).

-

------ What is a redundant constraint?

-

-* The things that can be redundant are precisely the Given

-  constraints of an implication.

-* A constraint can be redundant in two different ways:

-  a) It is not needed by the Wanted constraints covered by the

-     implication E.g.

-       f :: Eq a => a -> Bool

-       f x = True  -- Equality not used

-  b) It is implied by other givens.  E.g.

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

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

-

-*  To find (a) we need to know which evidence bindings are 'wanted';

-   hence the eb_is_given field on an EvBind.

-

-*  To find (b), we use mkMinimalBySCs on the Givens to see if any

-   are unnecessary.

-(RC1) When two Givens are the same, we drop the evidence for the one

-  that requires more superclass selectors. This is done

-  according to 2(c) of Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.

-

-(RC2) 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.

-(RC3) setImplicationStatus:

-  - The ics_dead field, of IC_Solved, records the subset of this

-    implication's ic_given that are redundant (not needed).

-

-  - 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,

-    b) it is free in the RHS of an EvBind whose LHS is needed, or

-    c) it is in the ics_need of a nested implication.

-

-  - After computing which variables are needed, we then look at the

-    remaining variables for internal redundancies. This is case (b)

-    from above. This is also done in setImplicationStatus.

-    Note that we only look for case (b) if case (a) shows up empty,

-    as exemplified below.

-

-  - We need to be careful not to discard an implication

-    prematurely, even one that is fully solved, because we might

-    thereby forget which variables it needs, and hence wrongly

-    report a constraint as redundant.  But we can discard it once

-    its free vars have been incorporated into its parent; or if it

-    simply has no free vars. This careful discarding is also

-    handled in setImplicationStatus.

-

-(RC4) 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!

-

-(RC5) 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

-

-        instance C a = C [a] b

-*** INCOMPLETE TODO ***

-* 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 three 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, as noted above and in

-    Note [Replacement vs keeping] in GHC.Tc.Solver.InertSet.

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

-    report a redundant Ord a using the logic for case (a).

-

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

-    report a redundant Eq a using the logic for case (a).

-

-    The body of h uses both [G] Ord a and [G] Eq a. Case (a) will

-    thus come up with nothing redundant. But then, the case (b)

-    check will discover that Eq a is redundant and report this.

-

-    If we did case (b) even when case (a) reports something, then

-    we would report both constraints as redundant for f, which is

-    terrible.

-

------ Reporting redundant constraints

-* We don't report redundant givens for *every* implication; only

-  for those which reply True to GHC.Tc.Solver.warnRedundantGivens:

-  This decision is taken in setImplicationStatus, rather than GHC.Tc.Errors

-  so that we can discard implication constraints that we don't need.

-  So ics_dead consists only of the *reportable* redundant givens.

-        EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet,

-      -- NB: including stuff used by nested implications that have since

-      --     been discarded

-      -- See Note [Needed evidence variables]

-      -- and (RC2) in Note [Tracking redundant constraints]a

-      ic_need_outer  :: EvNeedSet,  -- Includes only the free Given evidence

-                                    -- i.e. after deleting (a) ic_givens (b) binders of ic_binds

-      ic_need_pruned :: EvNeedSet,  -- Union of the ic_need_outer EvNeedSets of implications that

-                                    -- have been pruned from wc_impl.ic_wanted

-            , ic_env        = ct_loc_env

-            , ic_skols      = []

-            , ic_given      = []

-            , ic_wanted     = emptyWC

-            , ic_given_eqs  = MaybeGivenEqs

-            , ic_status     = IC_Unsolved

-            , ic_need_pruned = emptyEvNeedSet

-            , ic_need_outer  = emptyEvNeedSet }

-              , ic_need_pruned = need_pruned, ic_need_outer = need_out

-               , whenPprDebug (text "Needed pruned =" <+> ppr need_pruned)

-               , whenPprDebug (text "Needed outer =" <+> ppr need_out)

-Note [Needed evidence variables]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-Th ic_need_evs field holds the free vars of ic_binds, and all the

-ic_binds in nested implications.

-

-  * Main purpose: if one of the ic_givens is not mentioned in here, it

-    is redundant.

-

-  * solveImplication may drop an implication altogether if it has no

-    remaining 'wanteds'. But we still track the free vars of its

-    evidence binds, even though it has now disappeared.

-

-import GHC.Types.Unique.DFM

-import GHC.Types.Unique.FM

-import GHC.Types.Var

-import GHC.Types.Id( idScaledType )

-import GHC.Tc.Utils.TcType

-import GHC.Builtin.Names

-import GHC.Core.Predicate

-import GHC.Core

-import GHC.Core.Class (Class, classSCSelId )

-import GHC.Core.FVs   ( exprSomeFreeVars )

-import GHC.Core.InstEnv ( CanonicalEvidence(..) )

-evVarsOfTerm (EvExpr e)         = exprSomeFreeVars isEvVar e