Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: 19f20861 by Simon Peyton Jones at 2025-06-13T09:51:11-04:00 Improve redundant constraints for instance decls Addresses #25992, which showed that the default methods of an instance decl could make GHC fail to report redundant constraints. Figuring out how to do this led me to refactor the computation of redundant constraints. See the entirely rewritten Note [Tracking redundant constraints] in GHC.Tc.Solver.Solve - - - - - 14 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/TyCl/Instance.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Types/Origin.hs - compiler/GHC/Tc/Utils/Instantiate.hs - testsuite/tests/dependent/should_fail/T13135_simple.stderr - + testsuite/tests/typecheck/should_compile/T25992.hs - + testsuite/tests/typecheck/should_compile/T25992.stderr - testsuite/tests/typecheck/should_compile/all.T - testsuite/tests/typecheck/should_fail/tcfail097.stderr 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 ===================================== @@ -247,11 +247,11 @@ tryUnsatisfiableGivens wc = ; solveAgainIf did_work final_wc } where go_wc (WC { wc_simple = wtds, wc_impl = impls, wc_errors = errs }) - = do impls' <- mapMaybeBagM go_impl impls + = do impls' <- mapBagM go_impl impls return $ WC { wc_simple = wtds, wc_impl = impls', wc_errors = errs } go_impl impl | isSolvedStatus (ic_status impl) - = return $ Just impl + = return impl -- Is there a Given with type "Unsatisfiable msg"? -- If so, use it to solve all other Wanteds. | unsat_given:_ <- mapMaybe unsatisfiableEv_maybe (ic_given impl) @@ -271,24 +271,26 @@ unsatisfiableEv_maybe v = (v,) <$> isUnsatisfiableCt_maybe (idType v) -- | We have an implication with an 'Unsatisfiable' Given; use that Given to -- solve all the other Wanted constraints, including those nested within -- deeper implications. -solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS (Maybe Implication) +solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implication solveImplicationUsingUnsatGiven unsat_given@(given_ev,_) - impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var, ic_need_inner = inner }) + impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var + , 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. - = return $ Just impl + = return impl | otherwise = do { wcs <- nestImplicTcS ev_binds_var tclvl $ go_wc wtd ; setImplicationStatus $ impl { ic_wanted = wcs - , ic_need_inner = inner `extendVarSet` 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 go_wc wc@(WC { wc_simple = wtds, wc_impl = impls }) = do { mapBagM_ go_simple wtds - ; impls <- mapMaybeBagM (solveImplicationUsingUnsatGiven unsat_given) impls + ; impls <- mapBagM (solveImplicationUsingUnsatGiven unsat_given) impls ; return $ wc { wc_simple = emptyBag, wc_impl = impls } } go_simple :: Ct -> TcS () go_simple ct = case ctEvidence ct of @@ -399,21 +401,21 @@ tryConstraintDefaulting wc where go_wc :: WantedConstraints -> TcS WantedConstraints go_wc wc@(WC { wc_simple = simples, wc_impl = implics }) - = do { simples' <- mapMaybeBagM go_simple simples - ; mb_implics <- mapMaybeBagM go_implic implics - ; return (wc { wc_simple = simples', wc_impl = mb_implics }) } + = do { simples' <- mapMaybeBagM go_simple simples + ; implics' <- mapBagM go_implic implics + ; return (wc { wc_simple = simples', wc_impl = implics' }) } go_simple :: Ct -> TcS (Maybe Ct) go_simple ct = do { solved <- tryCtDefaultingStrategy ct ; if solved then return Nothing else return (Just ct) } - go_implic :: Implication -> TcS (Maybe Implication) + go_implic :: Implication -> TcS Implication -- The Maybe is because solving the CallStack constraint -- may well allow us to discard the implication entirely go_implic implic | isSolvedStatus (ic_status implic) - = return (Just implic) -- Nothing to solve inside here + = return implic -- Nothing to solve inside here | otherwise = do { wanteds <- setEvBindsTcS (ic_binds implic) $ -- defaultCallStack sets a binding, so ===================================== 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 ===================================== @@ -42,6 +42,7 @@ import GHC.Types.Var( EvVar, tyVarKind ) import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Types.Basic ( IntWithInf, intGtLimit ) +import GHC.Types.Unique.Set( nonDetStrictFoldUniqSet ) import GHC.Data.Bag @@ -51,9 +52,10 @@ import GHC.Utils.Misc import GHC.Driver.Session -import Data.List( deleteFirstsBy ) import Control.Monad + +import Data.List( deleteFirstsBy ) import Data.Foldable ( traverse_ ) import Data.Maybe ( mapMaybe ) import qualified Data.Semigroup as S @@ -277,10 +279,10 @@ solveNestedImplications implics ; traceTcS "solveNestedImplications end }" $ vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ] - ; return (catBagMaybes unsolved_implics) } + ; return unsolved_implics } -solveImplication :: Implication -- Wanted - -> TcS (Maybe Implication) -- Simplified implication (empty or singleton) +solveImplication :: Implication -- Wanted + -> TcS Implication -- Simplified implication (empty or singleton) -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value solveImplication imp@(Implic { ic_tclvl = tclvl @@ -290,7 +292,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl , ic_info = info , ic_status = status }) | isSolvedStatus status - = return (Just imp) -- Do nothing + = return imp -- Do nothing | otherwise -- Even for IC_Insoluble it is worth doing more work -- The insoluble stuff might be in one sub-implication @@ -350,90 +352,63 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -} ---------------------- -setImplicationStatus :: Implication -> TcS (Maybe Implication) +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 - , ic_given = givens }) - | assertPpr (not (isSolvedStatus old_status)) (ppr info) $ +setImplicationStatus implic@(Implic { ic_status = old_status + , ic_info = info + , ic_wanted = wc }) + = assertPpr (not (isSolvedStatus old_status)) (ppr info) $ -- Precondition: we only set the status if it is not already solved - not (isSolvedWC pruned_wc) - = 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 { traceTcS "setImplicationStatus(all-solved) {" (ppr implic) - - ; implic@(Implic { ic_need_inner = need_inner - , ic_need_outer = need_outer }) <- neededEvVars implic - - ; bad_telescope <- checkBadTelescope implic - - ; let warn_givens = findUnnecessaryGivens info need_inner givens - - discard_entire_implication -- Can we discard the entire implication? - = null warn_givens -- No warning from this implication - && not bad_telescope - && isEmptyWC pruned_wc -- No live children - && isEmptyVarSet need_outer -- No needed vars to pass up to parent - - final_status - | bad_telescope = IC_BadTelescope - | otherwise = IC_Solved { ics_dead = warn_givens } - final_implic = implic { ic_status = final_status - , ic_wanted = pruned_wc } - - ; traceTcS "setImplicationStatus(all-solved) }" $ - vcat [ text "discard:" <+> ppr discard_entire_implication - , text "new_implic:" <+> ppr final_implic ] - - ; return $ if discard_entire_implication - then Nothing - else Just final_implic } - where - WC { wc_simple = simples, wc_impl = implics, wc_errors = errs } = wc - - pruned_implics = filterBag keep_me implics - pruned_wc = WC { wc_simple = simples - , wc_impl = pruned_implics - , wc_errors = errs } -- do not prune holes; these should be reported - - 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 - = False -- Tnen we don't need to keep it - | otherwise - = True -- Otherwise, keep it + 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 -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) @@ -443,11 +418,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 = [] @@ -459,6 +436,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: @@ -510,21 +507,10 @@ 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 Implication -- Find all the evidence variables that are "needed", --- and delete dead evidence bindings +-- /and/ delete dead evidence bindings +-- -- See Note [Tracking redundant constraints] -- See Note [Delete dead Given evidence bindings] -- @@ -540,52 +526,93 @@ neededEvVars :: Implication -> TcS Implication -- Then a2 is needed too -- -- - 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_binds = ev_binds_var - , ic_wanted = WC { wc_impl = implics } - , ic_need_inner = old_needs }) + +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) + }) = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var - ; let seeds1 = foldr add_implic_seeds old_needs implics - seeds2 = nonDetStrictFoldEvBindMap add_wanted seeds1 ev_binds - -- It's OK to use a non-deterministic fold here - -- because add_wanted is commutative - seeds3 = seeds2 `unionVarSet` tcvs - need_inner = findNeededEvVars ev_binds seeds3 - live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds - need_outer = varSetMinusEvBindMap need_inner live_ev_binds - `delVarSetList` givens - + ; 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 ; 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 + 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:" <+> ppr need , 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 }) } + ; return (implic { ic_need = need + , ic_need_implic = new_need_implic }) } where - add_implic_seeds (Implic { ic_need_outer = needs }) acc - = needs `unionVarSet` 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 + 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 ------------------------------------------------- simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError) @@ -707,117 +734,84 @@ 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. - -* 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. - ------ 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. - -(RC3) setImplicationStatus: - 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! - -* Examples: +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. - f, g, h :: (Eq a, Ord a) => a -> Bool - f x = x == x - g x = x > x - h x = x == x && x > x +This is all tested in typecheck/should_compile/T20602 (among others). - 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. +How tracking works: - 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). +* 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. - 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). +* `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 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. + - `neededEvVars`: computes which evidence variables are needed by an + implication in `setImplicationStatus`. A variable is needed if - If we did case (b) even when case (a) reports something, then - we would report both constraints as redundant for f, which is - terrible. + a) It is in the ic_need field of this implication, computed in + a previous call to `setImplicationStatus`; see (TRC1) ------ Reporting redundant constraints + 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! -* GHC.Tc.Errors does the actual warning, in warnRedundantConstraints. +(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. -* We don't report redundant givens for *every* implication; only - for those which reply True to GHC.Tc.Solver.warnRedundantGivens: +(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, @@ -836,9 +830,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 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. ----- Shortcomings @@ -1732,4 +1785,4 @@ solveCompletelyIfRequired ct (TcS thing_inside) ; return $ Stop (ctEvidence ct) (text "Not fully solved; kept as inert:" <+> ppr ct) } } _notFullySolveMode -> - thing_inside env \ No newline at end of file + thing_inside env ===================================== compiler/GHC/Tc/TyCl/Instance.hs ===================================== @@ -495,7 +495,8 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_ext = lwarn do { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty -- NB: tcHsClsInstType does checkValidInstance - ; skol_info <- mkSkolemInfo (mkClsInstSkol clas inst_tys) + ; skol_info <- mkSkolemInfo (InstSkol IsClsInst pSizeZero) + -- pSizeZero: here the size part of InstSkol is irrelevant ; (subst, skol_tvs) <- tcInstSkolTyVars skol_info tyvars ; let tv_skol_prs = [ (tyVarName tv, skol_tv) | (tv, skol_tv) <- tyvars `zip` skol_tvs ] @@ -1816,7 +1817,7 @@ tcMethods :: SkolemInfoAnon -> DFunId -> Class -> TcM ([Id], LHsBinds GhcTc, Bag Implication) -- The returned inst_meth_ids all have types starting -- forall tvs. theta => ... -tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys +tcMethods _skol_info dfun_id clas tyvars dfun_ev_vars inst_tys dfun_ev_binds (spec_inst_prags, prag_fn) op_items (InstBindings { ib_binds = binds , ib_tyvars = lexical_tvs @@ -1852,7 +1853,7 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys tc_item :: ClassOpItem -> TcM (Id, LHsBind GhcTc, Maybe Implication) tc_item (sel_id, dm_info) | Just (user_bind, bndr_loc, prags) <- findMethodBind (idName sel_id) binds prag_fn - = tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys + = tcMethodBody False clas tyvars dfun_ev_vars inst_tys dfun_ev_binds is_derived hs_sig_fn spec_inst_prags prags sel_id user_bind bndr_loc @@ -1888,7 +1889,7 @@ tcMethods skol_info dfun_id clas tyvars dfun_ev_vars inst_tys Just (dm_name, dm_spec) -> do { (meth_bind, inline_prags) <- mkDefMethBind inst_loc dfun_id clas sel_id dm_name dm_spec - ; tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys + ; tcMethodBody True clas tyvars dfun_ev_vars inst_tys dfun_ev_binds is_derived hs_sig_fn spec_inst_prags inline_prags sel_id meth_bind inst_loc } @@ -2013,25 +2014,26 @@ Instead, we take the following approach: -} ------------------------ -tcMethodBody :: SkolemInfoAnon +tcMethodBody :: Bool -> Class -> [TcTyVar] -> [EvVar] -> [TcType] -> TcEvBinds -> Bool -> HsSigFun -> [LTcSpecPrag] -> [LSig GhcRn] -> Id -> LHsBind GhcRn -> SrcSpan -> TcM (TcId, LHsBind GhcTc, Maybe Implication) -tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys +tcMethodBody is_def_meth clas tyvars dfun_ev_vars inst_tys dfun_ev_binds is_derived sig_fn spec_inst_prags prags sel_id (L bind_loc meth_bind) bndr_loc = add_meth_ctxt $ do { traceTc "tcMethodBody" (ppr sel_id <+> ppr (idType sel_id) $$ ppr bndr_loc) + ; let skol_info = MethSkol meth_name is_def_meth ; (global_meth_id, local_meth_id) <- setSrcSpan bndr_loc $ mkMethIds clas tyvars dfun_ev_vars inst_tys sel_id ; let lm_bind = meth_bind { fun_id = L (noAnnSrcSpan bndr_loc) - (idName local_meth_id) } + (idName local_meth_id) } -- Substitute the local_meth_name for the binder -- NB: the binding is always a FunBind @@ -2042,7 +2044,7 @@ tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys tcMethodBodyHelp sig_fn sel_id local_meth_id (L bind_loc lm_bind) ; global_meth_id <- addInlinePrags global_meth_id prags - ; spec_prags <- tcExtendIdEnv1 (idName sel_id) global_meth_id $ + ; spec_prags <- tcExtendIdEnv1 meth_name global_meth_id $ -- tcExtendIdEnv1: tricky point: a SPECIALISE pragma in prags -- mentions sel_name but the pragma is really for global_meth_id. -- So we bind sel_name to global_meth_id, just in the pragmas. @@ -2071,6 +2073,8 @@ tcMethodBody skol_info clas tyvars dfun_ev_vars inst_tys ; return (global_meth_id, L bind_loc full_bind, Just meth_implic) } where + meth_name = idName sel_id + -- For instance decls that come from deriving clauses -- we want to print out the full source code if there's an error -- because otherwise the user won't see the code at all ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -67,6 +67,7 @@ module GHC.Tc.Types.Constraint ( ImplicStatus(..), isInsolubleStatus, isSolvedStatus, UserGiven, getUserGivensFromImplics, HasGivenEqs(..), checkImplicationInvariants, + EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet, -- CtLocEnv CtLocEnv(..), setCtLocEnvLoc, setCtLocEnvLvl, getCtLocEnvLoc, getCtLocEnvLvl, ctLocEnvInGeneratedCode, @@ -1458,18 +1459,43 @@ 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_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 + -- See Note [Tracking redundant constraints] + -- NB: these sets include stuff used by fully-solved nested implications + -- that have since been discarded + ic_need :: EvNeedSet, -- All needed Given evidence, from this implication + -- or outer ones + -- That is, /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 by `pruneImplications`. This discarding is why + -- we need to keep this field in the first place. ic_status :: ImplicStatus } +data EvNeedSet = ENS { ens_dms :: VarSet -- Needed only by default methods + , ens_fvs :: VarSet -- Needed by things /other than/ default methods + -- See (TRC5) in Note [Tracking redundant constraints] + } + +emptyEvNeedSet :: EvNeedSet +emptyEvNeedSet = ENS { ens_dms = emptyVarSet, ens_fvs = emptyVarSet } + +unionEvNeedSet :: EvNeedSet -> EvNeedSet -> EvNeedSet +unionEvNeedSet (ENS { ens_dms = dm1, ens_fvs = fv1 }) + (ENS { ens_dms = dm2, ens_fvs = fv2 }) + = ENS { ens_dms = dm1 `unionVarSet` dm2, ens_fvs = fv1 `unionVarSet` fv2 } + +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 @@ -1478,15 +1504,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_inner = emptyVarSet - , ic_need_outer = emptyVarSet } + , 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 @@ -1562,7 +1590,7 @@ instance Outputable Implication where , ic_given = given, ic_given_eqs = given_eqs , ic_wanted = wanted, ic_status = status , ic_binds = binds - , ic_need_inner = need_in, 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 @@ -1572,10 +1600,15 @@ instance Outputable Implication where , hang (text "Given =") 2 (pprEvVars given) , hang (text "Wanted =") 2 (ppr wanted) , text "Binds =" <+> ppr binds - , whenPprDebug (text "Needed inner =" <+> ppr need_in) - , whenPprDebug (text "Needed outer =" <+> ppr need_out) + , text "need =" <+> ppr need + , text "need_implic =" <+> ppr need_implic , pprSkolInfo info ] <+> rbrace) +instance Outputable EvNeedSet where + ppr (ENS { ens_dms = dms, ens_fvs = fvs }) + = text "ENS" <> braces (sep [text "ens_dms =" <+> ppr dms + , text "ens_fvs =" <+> ppr fvs]) + instance Outputable ImplicStatus where ppr IC_Insoluble = text "Insoluble" ppr IC_BadTelescope = text "Bad telescope" @@ -1663,18 +1696,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 @@ -2012,6 +2033,7 @@ checkSkolInfoAnon sk1 sk2 = go sk1 sk2 go (TyConSkol f1 n1) (TyConSkol f2 n2) = f1==f2 && n1==n2 go (DataConSkol n1) (DataConSkol n2) = n1==n2 go (InstSkol {}) (InstSkol {}) = True + go (MethSkol n1 d1) (MethSkol n2 d2) = n1==n2 && d1==d2 go FamInstSkol FamInstSkol = True go BracketSkol BracketSkol = True go (RuleSkol n1) (RuleSkol n2) = n1==n2 ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -28,7 +28,7 @@ module GHC.Tc.Types.Evidence ( -- * EvTerm (already a CoreExpr) EvTerm(..), EvExpr, evId, evCoercion, evCast, evDFunApp, evDataConApp, evSelector, - mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars, + mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, evTermCoercion, evTermCoercion_maybe, EvCallStack(..), @@ -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,27 +868,13 @@ evTermCoercion tm = case evTermCoercion_maybe tm of * * ********************************************************************* -} -findNeededEvVars :: EvBindMap -> VarSet -> VarSet --- Find all the Given evidence needed by seeds, --- looking transitively through binds -findNeededEvVars 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 - = evVarsOfTerm rhs `unionVarSet` needs - | otherwise - = needs +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] ===================================== compiler/GHC/Tc/Types/Origin.hs ===================================== @@ -15,7 +15,7 @@ module GHC.Tc.Types.Origin ( -- * SkolemInfo SkolemInfo(..), SkolemInfoAnon(..), mkSkolemInfo, getSkolemInfo, pprSigSkolInfo, pprSkolInfo, - unkSkol, unkSkolAnon, mkClsInstSkol, + unkSkol, unkSkolAnon, -- * CtOrigin CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin, @@ -58,7 +58,6 @@ import GHC.Hs import GHC.Core.DataCon import GHC.Core.ConLike import GHC.Core.TyCon -import GHC.Core.Class import GHC.Core.InstEnv import GHC.Core.PatSyn import GHC.Core.Multiplicity ( scaledThing ) @@ -288,6 +287,10 @@ data SkolemInfoAnon ClsInstOrQC -- Whether class instance or quantified constraint PatersonSize -- Head has the given PatersonSize + | MethSkol Name Bool -- Bound by the type of class method op + -- True <=> it's a default method + -- False <=> it's a user-written method + | FamInstSkol -- Bound at a family instance decl | PatSkol -- An existential type variable bound by a pattern for ConLike -- a data constructor with an existential type. @@ -348,9 +351,6 @@ mkSkolemInfo sk_anon = do getSkolemInfo :: SkolemInfo -> SkolemInfoAnon getSkolemInfo (SkolemInfo _ skol_anon) = skol_anon -mkClsInstSkol :: Class -> [Type] -> SkolemInfoAnon -mkClsInstSkol cls tys = InstSkol IsClsInst (pSizeClassPred cls tys) - instance Outputable SkolemInfo where ppr (SkolemInfo _ sk_info ) = ppr sk_info @@ -369,6 +369,8 @@ pprSkolInfo (InstSkol IsClsInst sz) = vcat [ text "the instance declaration" , whenPprDebug (braces (ppr sz)) ] pprSkolInfo (InstSkol (IsQC {}) sz) = vcat [ text "a quantified context" , whenPprDebug (braces (ppr sz)) ] +pprSkolInfo (MethSkol name d) = text "the" <+> ppWhen d (text "default") + <+> text "method declaration for" <+> ppr name pprSkolInfo FamInstSkol = text "a family instance declaration" pprSkolInfo BracketSkol = text "a Template Haskell bracket" pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name ===================================== compiler/GHC/Tc/Utils/Instantiate.hs ===================================== @@ -582,8 +582,11 @@ tcSkolDFunType dfun_ty -- We instantiate the dfun_tyd with superSkolems. -- See Note [Subtle interaction of recursion and overlap] -- and Note [Super skolems: binding when looking up instances] - ; let inst_tys = substTys subst tys - skol_info_anon = mkClsInstSkol cls inst_tys } + ; let inst_tys = substTys subst tys + skol_info_anon = InstSkol IsClsInst (pSizeClassPred cls inst_tys) + -- We need to take the size of `inst_tys` (not `tys`) because + -- Paterson sizes mention the free type variables + } ; let inst_theta = substTheta subst theta ; return (skol_info_anon, inst_tvs, inst_theta, cls, inst_tys) } ===================================== testsuite/tests/dependent/should_fail/T13135_simple.stderr ===================================== @@ -1,8 +1,8 @@ - T13135_simple.hs:34:11: error: [GHC-83865] - • Couldn't match type ‘SmartFun sig’ with ‘Bool’ + • Couldn't match type ‘SmartFun sig1’ with ‘Bool’ Expected: Int -> Bool - Actual: SmartFun (SigFun Int sig) - The type variable ‘sig’ is ambiguous + Actual: SmartFun (SigFun Int sig1) + The type variable ‘sig1’ is ambiguous • In the expression: smartSym In an equation for ‘problem’: problem = smartSym + ===================================== testsuite/tests/typecheck/should_compile/T25992.hs ===================================== @@ -0,0 +1,8 @@ +{-# OPTIONS_GHC -Wredundant-constraints #-} + +module T25992 where + +data P a = P + +instance Eq a => Semigroup (P a) where + P <> P = P ===================================== testsuite/tests/typecheck/should_compile/T25992.stderr ===================================== @@ -0,0 +1,4 @@ +T25992.hs:7:10: warning: [GHC-30606] [-Wredundant-constraints] + • Redundant constraint: Eq a + • In the instance declaration for ‘Semigroup (P a)’ + ===================================== testsuite/tests/typecheck/should_compile/all.T ===================================== @@ -941,3 +941,4 @@ test('T25597', normal, compile, ['']) test('T25960', normal, compile, ['']) test('T26020', normal, compile, ['']) test('T26020a', [extra_files(['T26020a_help.hs'])], multimod_compile, ['T26020a', '-v0']) +test('T25992', normal, compile, ['']) ===================================== testsuite/tests/typecheck/should_fail/tcfail097.stderr ===================================== @@ -7,8 +7,8 @@ tcfail097.hs:5:6: error: [GHC-39999] The type variable ‘a0’ is ambiguous Potentially matching instances: instance Eq Ordering -- Defined in ‘GHC.Internal.Classes’ - instance Eq a => Eq (Solo a) -- Defined in ‘GHC.Internal.Classes’ - ...plus 22 others + instance Eq Integer -- Defined in ‘GHC.Internal.Bignum.Integer’ + ...plus 23 others ...plus five instances involving out-of-scope types (use -fprint-potential-instances to see them all) • In the ambiguity check for ‘f’ View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/19f20861b7462c6224d4ebdaeaa5d1e0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/19f20861b7462c6224d4ebdaeaa5d1e0... You're receiving this email because of your account on gitlab.haskell.org.