Simon Peyton Jones pushed to branch wip/T25992 at Glasgow Haskell Compiler / GHC Commits: 4cb8b60a by Simon Peyton Jones at 2025-05-23T17:11:37+01:00 yet more - - - - - 6 changed files: - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -399,13 +399,6 @@ warnRedundantConstraints ctxt env info redundant_evs | null redundant_evs = return () - -- 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 () - | SigSkol user_ctxt _ _ <- info -- When dealing with a user-written type signature, -- we want to add "In the type signature for f". ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -275,7 +275,7 @@ solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implicati solveImplicationUsingUnsatGiven unsat_given@(given_ev,_) impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var - , ic_need_pruned = inner }) + , ic_need_implic = inner }) | isCoEvBindsVar ev_binds_var -- We can't use Unsatisfiable evidence in kinds. -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence. @@ -284,7 +284,7 @@ solveImplicationUsingUnsatGiven = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd ; setImplicationStatus $ impl { ic_wanted = wcs - , ic_need_pruned = inner `extendEvNeedSet` given_ev } } + , ic_need_implic = inner `extendEvNeedSet` given_ev } } -- Record that the Given is needed; I'm not certain why where go_wc :: WantedConstraints -> TcS WantedConstraints ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -2089,18 +2089,8 @@ solveOneFromTheOther. (a) If both are GivenSCOrigin, choose the one that is unblocked if possible according to Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance. - (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. + (b) Prefer constraints that are not superclass selections. See + (TRC3) in Note [Tracking redundant constraints] in GHC.Tc.Solver. (c) If both are GivenSCOrigin, chooose the one with the shallower superclass-selection depth, in the hope of identifying more correct ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -354,84 +354,42 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ---------------------- setImplicationStatus :: Implication -> TcS Implication -- Finalise the implication returned from solveImplication, --- setting the ic_status field +-- * Set the ic_status field +-- * Prune unnecessary evidence bindings +-- * Prune unnecessary child implications -- Precondition: the ic_status field is not already IC_Solved --- Return Nothing if we can discard the implication altogether setImplicationStatus implic@(Implic { ic_status = old_status , ic_info = info , ic_wanted = wc }) - | assertPpr (not (isSolvedStatus old_status)) (ppr info) $ + = assertPpr (not (isSolvedStatus old_status)) (ppr info) $ -- Precondition: we only set the status if it is not already solved - not (isSolvedWC wc) - = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic) + do { traceTcS "setImplicationStatus {" (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) + ; let solved = isSolvedWC wc + ; new_implic <- neededEvVars implic + ; bad_telescope <- if solved then checkBadTelescope implic + else return False - ; (dead_givens, implic) <- neededEvVars implic - - ; bad_telescope <- checkBadTelescope implic + ; 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 - ; let final_status - | bad_telescope = IC_BadTelescope - | otherwise = IC_Solved { ics_dead = dead_givens } - final_implic = pruneImplications (implic { ic_status = final_status }) + final_implic = new_implic { ic_status = new_status } - ; traceTcS "setImplicationStatus(solved) }" (ppr final_implic) + ; traceTcS "setImplicationStatus }" (ppr final_implic) ; return 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 +findRedundantGivens :: Implication -> [EvVar] +findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens }) | not (warnRedundantGivens info) -- Don't report redundant constraints at all - = [] + = [] -- See (TRC4) of Note [Tracking redundant constraints] | not (null unused_givens) -- Some givens are literally unused = unused_givens + -- Only try this if unused_givens is empty: see (TRC2a) | otherwise -- All givens are used, but some might = redundant_givens -- still be redundant e.g. (Eq a, Ord a) @@ -441,11 +399,13 @@ findUnnecessaryGivens info need_inner givens unused_givens = filterOut is_used givens + needed_givens_ignoring_default_methods = ens_fvs need is_used given = is_type_error given - || given `elemVarSet` need_inner + || given `elemVarSet` needed_givens_ignoring_default_methods || (in_instance_decl && is_improving (idType given)) - minimal_givens = mkMinimalBySCs evVarPred givens + minimal_givens = mkMinimalBySCs evVarPred givens -- See (TRC2) + is_minimal = (`elemVarSet` mkVarSet minimal_givens) redundant_givens | in_instance_decl = [] @@ -457,6 +417,26 @@ findUnnecessaryGivens info need_inner givens is_improving pred -- (transSuperClasses p) does not include p = any isImprovementPred (pred : transSuperClasses pred) +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 + {- Note [Redundant constraints in instance decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Instance declarations are special in two ways: @@ -508,21 +488,11 @@ checkBadTelescope (Implic { ic_info = info | otherwise = go (later_skols `extendVarSet` one_skol) earlier_skols -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) +neededEvVars :: Implication -> TcS Implication -- Find all the evidence variables that are "needed", --- and delete dead evidence bindings +-- /and/ delete dead evidence bindings +-- /and/ delete unnecessary child implications +-- -- See Note [Tracking redundant constraints] -- See Note [Delete dead Given evidence bindings] -- @@ -539,78 +509,89 @@ neededEvVars :: Implication -> TcS ([EvVar], Implication) -- -- - 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_given = givens - , ic_info = info - , ic_binds = ev_binds_var - , ic_wanted = WC { wc_impl = implics } - , ic_need_pruned = need_pruned }) +-- - Prune out all child implications that are no longer useful + +neededEvVars implic@(Implic { ic_info = info + , ic_binds = ev_binds_var + , ic_wanted = old_wanted + , ic_need_implic = old_need_implic -- See (TRC1) + }) + | WC { wc_impl = old_implics } <- old_wanted = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var - ; 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 + ; let -- Augment `need_implic` (see (TRC1)) with the variables needed by the implications + new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds }) + = foldr add_implic old_need_implic old_implics -- 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 - -- `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 + 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 - live_ev_binds = filterEvBindMap (needed_ev_bind need_full) ev_binds + -- `new_need`: the Givens from outer scopes that are used in this implication + 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 } + + -- `new_implics`: we have now taken account of the `ic_need` variables + -- of `old_implics`, so we can drop any that are no longer necessary + pruned_implics = filterBag keep_me old_implics + pruned_wanted = old_wanted { wc_impl = pruned_implics } + -- Do not prune holes; these should be reported + + -- Delete dead Given evidence bindings + -- See Note [Delete dead Given evidence bindings] + ; let live_ev_binds = filterEvBindMap (needed_ev_bind need_full) ev_binds ; TcS.setTcEvBindsMap ev_binds_var live_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 } ; traceTcS "neededEvVars" $ - vcat [ text "old need_pruned:" <+> ppr need_pruned + vcat [ text "old_need_implic:" <+> ppr old_need_implic + , text "new_need_implic:" <+> ppr new_need_implic , text "tcvs:" <+> ppr tcvs , text "need_ignoring_dms:" <+> ppr need_ignoring_dms , text "need_from_dms:" <+> ppr need_from_dms - , text "need_outer:" <+> ppr need_outer - , text "dead_givens:" <+> ppr dead_givens + , text "need:" <+> ppr need , text "ev_binds:" <+> ppr ev_binds , text "live_ev_binds:" <+> ppr live_ev_binds ] - - ; return ( dead_givens - , implic { ic_need_outer = need_outer }) } + ; return (implic { ic_need = need + , ic_need_implic = new_need_implic + , ic_wanted = pruned_wanted }) } where - trim :: EvBindMap -> VarSet -> VarSet - -- Delete variables bound by Givens or bindings - trim live_ev_binds needs = (needs `varSetMinusEvBindMap` live_ev_binds) - `delVarSetList` givens + trim :: EvBindMap -> VarSet -> VarSet + -- Delete variables bound by Givens or bindings + trim ev_binds needs = needs `varSetMinusEvBindMap` ev_binds - add_implic_seeds :: Implication -> EvNeedSet -> EvNeedSet - add_implic_seeds (Implic { ic_need_outer = needs }) acc - = needs `unionEvNeedSet` acc + 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 + 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 + 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 + 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 + + 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, @@ -752,133 +733,82 @@ in GHC.Tc.Gen.HsType. Note [Tracking redundant constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -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. +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. -* 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. +This is all tested in typecheck/should_compile/T20602 (among others). ----- How tracking works -(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. +* We maintain the `ic_need` field in an implication: + ic_need: the set of Given evidence variables that are needed somewhere + in this implication; and are bound either by this implication + or by an enclosing one. -(RC3) setImplicationStatus: +* `setImplicationStatus` does all the work: 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). - - - 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 + - `neededEvVars`: computes which evidence variables are needed by an + implication in `setImplicationStatus`. A variable is needed if -*** INCOMPLETE TODO *** + 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` -* Examples: - - f, g, h :: (Eq a, Ord a) => a -> Bool - f x = x == x - g x = x > x - h x = x == x && x > x + 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` - 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. + d) It is free in the RHS of a /Given/ EvBind whose LHS is needed: + see `findNeededGivenEvVars` called from `neededEvVars`. - 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 + - Next, if the final status is IC_Solved, `setImplicationStatus` uses + `findRedunantGivens` to decide which of this implicaion's Givens are redundant. * GHC.Tc.Errors does the actual warning, in warnRedundantConstraints. -* We don't report redundant givens for *every* implication; only - for those which reply True to GHC.Tc.Solver.warnRedundantGivens: + +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 do not recompute `ic_need` from scratch each time; rather, we + simply grow it -- see the use of `old_need` in `neededEvVars`. + + Starting from `old_needs` also means that the transitive closure algorithm in + `findNeededGivenEvVars` will terminate faster + +(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`: - For example, in a class declaration, the default method *can* use the class constraint, but it certainly doesn't *have* to, @@ -897,9 +827,68 @@ others). - GHC.Tc.Gen.Bind.tcSpecPrag - GHC.Tc.Gen.Bind.tcTySig - 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. + - 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 works is 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. ----- Shortcomings ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -67,7 +67,7 @@ module GHC.Tc.Types.Constraint ( ImplicStatus(..), isInsolubleStatus, isSolvedStatus, UserGiven, getUserGivensFromImplics, HasGivenEqs(..), checkImplicationInvariants, - EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, + EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet, -- CtLocEnv CtLocEnv(..), setCtLocEnvLoc, setCtLocEnvLvl, getCtLocEnvLoc, getCtLocEnvLvl, ctLocEnvInGeneratedCode, @@ -1459,14 +1459,17 @@ data Implication -- 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 - -- 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 + -- See Note [Tracking redundant constraints] + -- NB: including stuff used by fully-solved nested implications that have + -- since been discarded + ic_need :: EvNeedSet, -- Includes needed Given evidence + -- /after/ deleting the binders of ic_binds, but + -- /before/ deleting ic_givens + + ic_need_implic :: EvNeedSet, -- Union of of the ic_need of all implications in ic_wanted + -- /including/ any fully-solved implications that have been + -- discarded. This discarding is why we need to keep this + -- field in the first place. ic_status :: ImplicStatus } @@ -1486,6 +1489,11 @@ unionEvNeedSet (ENS { ens_dms = dm1, ens_fvs = fv1 }) extendEvNeedSet :: EvNeedSet -> Var -> EvNeedSet extendEvNeedSet ens@(ENS { ens_fvs = fvs }) v = ens { ens_fvs = fvs `extendVarSet` v } +delGivensFromEvNeedSet :: EvNeedSet -> [Var] -> EvNeedSet +delGivensFromEvNeedSet (ENS { ens_dms = dms, ens_fvs = fvs }) givens + = ENS { ens_dms = dms `delVarSetList` givens + , ens_fvs = fvs `delVarSetList` givens } + implicationPrototype :: CtLocEnv -> Implication implicationPrototype ct_loc_env = Implic { -- These fields must be initialised @@ -1494,15 +1502,17 @@ implicationPrototype ct_loc_env , ic_info = panic "newImplic:info" , ic_warn_inaccessible = panic "newImplic:warn_inaccessible" - , ic_env = ct_loc_env + -- Given by caller + , ic_env = ct_loc_env + -- The rest have sensible default values - , ic_skols = [] - , ic_given = [] - , ic_wanted = emptyWC - , ic_given_eqs = MaybeGivenEqs - , ic_status = IC_Unsolved - , ic_need_pruned = emptyEvNeedSet - , ic_need_outer = emptyEvNeedSet } + , ic_skols = [] + , ic_given = [] + , ic_wanted = emptyWC + , ic_given_eqs = MaybeGivenEqs + , ic_status = IC_Unsolved + , ic_need = emptyEvNeedSet + , ic_need_implic = emptyEvNeedSet } data ImplicStatus = IC_Solved -- All wanteds in the tree are solved, all the way down @@ -1578,7 +1588,7 @@ instance Outputable Implication where , ic_given = given, ic_given_eqs = given_eqs , ic_wanted = wanted, ic_status = status , ic_binds = binds - , ic_need_pruned = need_pruned, ic_need_outer = need_out + , ic_need = need, ic_need_implic = need_implic , ic_info = info }) = hang (text "Implic" <+> lbrace) 2 (sep [ text "TcLevel =" <+> ppr tclvl @@ -1588,8 +1598,8 @@ instance Outputable Implication where , hang (text "Given =") 2 (pprEvVars given) , hang (text "Wanted =") 2 (ppr wanted) , text "Binds =" <+> ppr binds - , whenPprDebug (text "Needed pruned =" <+> ppr need_pruned) - , whenPprDebug (text "Needed outer =" <+> ppr need_out) + , text "need =" <+> ppr need + , text "need_implic =" <+> ppr need_implic , pprSkolInfo info ] <+> rbrace) instance Outputable EvNeedSet where @@ -1684,18 +1694,6 @@ all at once, creating one implication constraint for the lot: implication. TL;DR: an explicit forall should generate an implication quantified only over those explicitly quantified variables. -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. - Note [Shadowing in a constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We assume NO SHADOWING in a constraint. Specifically ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -50,27 +50,30 @@ module GHC.Tc.Types.Evidence ( import GHC.Prelude -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.Core import GHC.Core.Coercion.Axiom import GHC.Core.Coercion import GHC.Core.Ppr () -- Instance OutputableBndr TyVar -import GHC.Tc.Utils.TcType +import GHC.Core.Predicate import GHC.Core.Type import GHC.Core.TyCon import GHC.Core.DataCon ( DataCon, dataConWrapId ) -import GHC.Builtin.Names +import GHC.Core.Class (Class, classSCSelId ) +import GHC.Core.FVs ( exprSomeFreeVars ) +import GHC.Core.InstEnv ( CanonicalEvidence(..) ) + +import GHC.Types.Unique.DFM +import GHC.Types.Unique.FM +import GHC.Types.Var +import GHC.Types.Name( isInternalName ) +import GHC.Types.Id( idScaledType ) import GHC.Types.Var.Env import GHC.Types.Var.Set -import GHC.Core.Predicate import GHC.Types.Basic -import GHC.Core -import GHC.Core.Class (Class, classSCSelId ) -import GHC.Core.FVs ( exprSomeFreeVars ) -import GHC.Core.InstEnv ( CanonicalEvidence(..) ) +import GHC.Builtin.Names import GHC.Utils.Misc import GHC.Utils.Panic @@ -865,8 +868,13 @@ evTermCoercion tm = case evTermCoercion_maybe tm of * * ********************************************************************* -} +relevantEvVar :: Var -> Bool +-- Just returns /local/ free evidence variables; i.e ones with Internal Names +-- Top-level ones (DFuns, dictionary selectors and the like) don't count +relevantEvVar v = isInternalName (varName v) + evVarsOfTerm :: EvTerm -> VarSet -evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e +evVarsOfTerm (EvExpr e) = exprSomeFreeVars relevantEvVar e evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4cb8b60a22f1a3b7227f5f5153e00f3b... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4cb8b60a22f1a3b7227f5f5153e00f3b... You're receiving this email because of your account on gitlab.haskell.org.