[Git][ghc/ghc][wip/26805] Finally fix the constraints-library bug
Simon Peyton Jones pushed to branch wip/26805 at Glasgow Haskell Compiler / GHC Commits: ed1e2ce4 by Simon Peyton Jones at 2026-01-22T23:28:26+00:00 Finally fix the constraints-library bug - - - - - 4 changed files: - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/Monad.hs Changes: ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -748,7 +748,8 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys = -- There is a matching dictionary in the inert set do { -- For a Wanted, first to try to solve it /completely/ from top level instances -- See Note [Shortcut solving] - ; short_cut_worked <- tryShortCutSolver (isGiven ev_i) dict_w + ; dflags <- getDynFlags + ; short_cut_worked <- tryShortCutSolver dflags (isGiven ev_i) dict_w ; if | short_cut_worked -> stopWith ev_w "shortCutSolver worked(1)" @@ -776,7 +777,8 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys ; continueWith () } -- See Note [Shortcut solving] -tryShortCutSolver :: Bool -- True <=> try the short-cut solver; False <=> don't +tryShortCutSolver :: DynFlags + -> Bool -- True <=> try the short-cut solver; False <=> don't -> DictCt -- Work item -> TcS Bool -- True <=> success -- We are about to solve a [W] constraint from a [G] constraint. We take @@ -784,34 +786,25 @@ tryShortCutSolver :: Bool -- True <=> try the short-cut solver; False <=> -- Note that we only do this for the sake of performance. Exactly the same -- programs should typecheck regardless of whether we take this step or -- not. See Note [Shortcut solving] -tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w }) - | not try_short_cut - = return False - | otherwise - = do { dflags <- getDynFlags - ; if | CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w - - , not (couldBeIPLike pred_w) -- Not for implicit parameters (#18627) +tryShortCutSolver dflags try_short_cut dict_w + | try_short_cut + , DictCt { di_ev = ev_w } <- dict_w + , CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w + , not (couldBeIPLike pred_w) -- Not for implicit parameters (#18627) - , not (xopt LangExt.IncoherentInstances dflags) + , not (xopt LangExt.IncoherentInstances dflags) -- If IncoherentInstances is on then we cannot rely on coherence of proofs -- in order to justify this optimization: The proof provided by the -- [G] constraint's superclass may be different from the top-level proof. -- See Note [Shortcut solving: incoherence] - - , gopt Opt_SolveConstantDicts dflags + , gopt Opt_SolveConstantDicts dflags -- Enabled by the -fsolve-constant-dicts flag - -> tryShortCutTcS $ -- tryTcS tries to completely solve some contraints - do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w)) - ; return (isSolvedWC residual) } - -- NB: isSolvedWC, not isEmptyWC (#26805). We might succeed - -- in fully-solving the constraint but still leave some - -- /solved/ implications in the residual. - -- See (SCS4) in Note [Shortcut solving] + = tryShortCutTcS $ -- tryTcS tries to completely solve some contraints + solveSimpleWanteds (unitBag (CDictCan dict_w)) - | otherwise - -> return False } + | otherwise + = return False {- ******************************************************************* @@ -846,7 +839,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev@(CtWanted wev), di_cls = cls ; case lkup_res of OneInst { cir_what = what } -> do { let is_local_given = case what of { LocalInstance -> True; _ -> False } - ; take_shortcut <- tryShortCutSolver is_local_given work_item + ; take_shortcut <- tryShortCutSolver dflags is_local_given work_item ; if take_shortcut then stopWith ev "shortCutSolver worked(2)" else do { insertSafeOverlapFailureTcS what work_item ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1351,7 +1351,7 @@ nestTcS (TcS thing_inside) ; return res } -tryShortCutTcS :: TcS Bool -> TcS Bool +tryShortCutTcS :: TcS WantedConstraints -> TcS Bool -- Like nestTcS, but -- (a) be a no-op if the nested computation returns False -- (b) if (but only if) success, propagate nested bindings to the caller @@ -1384,28 +1384,38 @@ tryShortCutTcS (TcS thing_inside) vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var , text "new_ev_binds:" <+> ppr new_ev_binds_var , ppr old_inerts ] - ; solved <- thing_inside nest_env + ; residual <- thing_inside nest_env + ; let solved = isSolvedWC residual + -- NB: isSolvedWC, not isEmptyWC (#26805). We might succeed + -- in fully-solving the constraint but still leave some + -- /solved/ implications in the residual. + -- See (SCS4) in Note [Shortcut solving] ; TcM.traceTc "tryShortCutTcS }" (ppr solved) - ; if not solved - then return False - else do { -- Successfully solved - -- Add the new bindings to the existing ones - ; old_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var) + ; when solved $ -- Successfully solved + do { -- Add the new bindings to the existing ones + ; TcM.combineTcEvBinds old_ev_binds_var new_ev_binds_var - ; TcM.combineTcEvBinds old_ev_binds_var new_ev_binds_var + -- We are discarding some implications; we must add their + -- NeededEvIds to the current bindings, lest we fail to r + ; TcM.addNeededEvIds old_ev_binds_var $ + foldr add_implic emptyVarSet $ + wc_impl residual - ; final_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var) - ; TcM.traceTc "update" (text "old" <+> ppr old_ebvs $$ - text "new" <+> ppr final_ebvs) + -- Update the existing inert set + ; new_inerts <- TcM.readTcRef new_inert_var + ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts) } - -- Update the existing inert set - ; new_inerts <- TcM.readTcRef new_inert_var - ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts) - ; TcM.traceTc "tryTcS update" (ppr (inert_solved_dicts new_inerts)) - - ; return True } } + ; return solved + } + where + add_implic :: Implication -> NeededEvIds -> NeededEvIds + add_implic implic@(Implic { ic_status = status }) needs + | IC_Solved { ics_dm = dm, ics_non_dm = non_dm } <- status + = needs `unionVarSet` dm `unionVarSet` non_dm + | otherwise + = pprPanic "tryShortCutTcS" (ppr implic) updateInertsWith :: InertSet -> InertSet -> InertSet -- Update the current inert set with bits from a nested solve, ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -15,7 +15,7 @@ module GHC.Tc.Types.Evidence ( -- * Evidence bindings TcEvBinds(..), EvBindsVar(..), NeededEvIds, - EvBindsState(..), emptyEvBindsState, unionEvBindsState, addCoVarsEBS, + EvBindsState(..), emptyEvBindsState, unionEvBindsState, addNeededEvIdsEBS, EvBindsMap(..), emptyEvBindsMap, extendEvBinds, unionEvBindsMap, lookupEvBind, evBindMapBinds, foldEvBindsMap, nonDetStrictFoldEvBindsMap, @@ -765,8 +765,8 @@ unionEvBindsState (EBS { ebs_binds = bs1, ebs_needs = n1 }) = EBS { ebs_binds = bs1 `unionEvBindsMap` bs2 , ebs_needs = n1 `unionVarSet` n2 } -addCoVarsEBS :: VarSet -> EvBindsState -> EvBindsState -addCoVarsEBS n1 ebs@(EBS { ebs_needs = n2 }) +addNeededEvIdsEBS :: NeededEvIds -> EvBindsState -> EvBindsState +addNeededEvIdsEBS n1 ebs@(EBS { ebs_needs = n2 }) = ebs { ebs_needs = n1 `unionVarSet` n2 } instance Outputable EvBindsState where ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -106,7 +106,7 @@ module GHC.Tc.Utils.Monad( newTcEvBinds, newNoTcEvBinds, cloneEvBindsVar, addTcEvCoBind, addTcEvBind, addTopEvBinds, getTcEvBindsMap, getTcEvBindsState, - setTcEvBindsMap, combineTcEvBinds, + setTcEvBindsMap, combineTcEvBinds, addNeededEvIds, chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitSimple, emitSimples, @@ -2018,7 +2018,7 @@ combineTcEvBinds (EvBindsVar { ebv_binds = old_ebv_ref }) combineTcEvBinds (EvBindsVar { ebv_binds = old_tcv_ref }) (CoEvBindsVar { ebv_needs = new_tcv_ref }) = do { new_tcvs <- readTcRef new_tcv_ref - ; updTcRef old_tcv_ref (addCoVarsEBS new_tcvs) } + ; updTcRef old_tcv_ref (addNeededEvIdsEBS new_tcvs) } combineTcEvBinds (CoEvBindsVar { ebv_needs = old_tcv_ref }) (CoEvBindsVar { ebv_needs = new_tcv_ref }) = do { new_tcvs <- readTcRef new_tcv_ref @@ -2027,16 +2027,17 @@ combineTcEvBinds old_var new_var = pprPanic "combineTcEvBinds" (ppr old_var $$ ppr new_var) -- Terms inside types, no good +addNeededEvIds :: EvBindsVar -> NeededEvIds -> TcM () +addNeededEvIds (EvBindsVar { ebv_binds = bs_ref }) needed + = updTcRef bs_ref (addNeededEvIdsEBS needed) +addNeededEvIds (CoEvBindsVar { ebv_needs = need_ref }) needed + = updTcRef need_ref (unionVarSet needed) + addTcEvCoBind :: EvBindsVar -> CoercionHole -> CoercionPlusHoles -> TcM () addTcEvCoBind ebv hole co_plus_holes@(CPH { cph_co = co }) = do { fillCoercionHole hole co_plus_holes -- Record usage of the free vars of this coercion - ; let fvs = coVarsOfCo co - ; case ebv of - EvBindsVar { ebv_binds = bs_ref } - -> updTcRef bs_ref (addCoVarsEBS fvs) - CoEvBindsVar { ebv_needs = need_ref } - -> updTcRef need_ref (unionVarSet fvs) } + ; addNeededEvIds ebv (coVarsOfCo co) } addTcEvBind :: EvBindsVar -> EvBind -> TcM () -- Add a binding to the TcEvBinds by side effect View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ed1e2ce4564907132f92e484fb0897d0... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ed1e2ce4564907132f92e484fb0897d0... You're receiving this email because of your account on gitlab.haskell.org.
participants (1)
-
Simon Peyton Jones (@simonpj)