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
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:
| ... | ... | @@ -748,7 +748,8 @@ try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys |
| 748 | 748 | = -- There is a matching dictionary in the inert set
|
| 749 | 749 | do { -- For a Wanted, first to try to solve it /completely/ from top level instances
|
| 750 | 750 | -- See Note [Shortcut solving]
|
| 751 | - ; short_cut_worked <- tryShortCutSolver (isGiven ev_i) dict_w
|
|
| 751 | + ; dflags <- getDynFlags
|
|
| 752 | + ; short_cut_worked <- tryShortCutSolver dflags (isGiven ev_i) dict_w
|
|
| 752 | 753 | |
| 753 | 754 | ; if | short_cut_worked
|
| 754 | 755 | -> 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 |
| 776 | 777 | ; continueWith () }
|
| 777 | 778 | |
| 778 | 779 | -- See Note [Shortcut solving]
|
| 779 | -tryShortCutSolver :: Bool -- True <=> try the short-cut solver; False <=> don't
|
|
| 780 | +tryShortCutSolver :: DynFlags
|
|
| 781 | + -> Bool -- True <=> try the short-cut solver; False <=> don't
|
|
| 780 | 782 | -> DictCt -- Work item
|
| 781 | 783 | -> TcS Bool -- True <=> success
|
| 782 | 784 | -- 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 <=> |
| 784 | 786 | -- Note that we only do this for the sake of performance. Exactly the same
|
| 785 | 787 | -- programs should typecheck regardless of whether we take this step or
|
| 786 | 788 | -- not. See Note [Shortcut solving]
|
| 787 | -tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w })
|
|
| 788 | - | not try_short_cut
|
|
| 789 | - = return False
|
|
| 790 | - | otherwise
|
|
| 791 | - = do { dflags <- getDynFlags
|
|
| 792 | - ; if | CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w
|
|
| 793 | - |
|
| 794 | - , not (couldBeIPLike pred_w) -- Not for implicit parameters (#18627)
|
|
| 789 | +tryShortCutSolver dflags try_short_cut dict_w
|
|
| 790 | + | try_short_cut
|
|
| 791 | + , DictCt { di_ev = ev_w } <- dict_w
|
|
| 792 | + , CtWanted (WantedCt { ctev_pred = pred_w }) <- ev_w
|
|
| 793 | + , not (couldBeIPLike pred_w) -- Not for implicit parameters (#18627)
|
|
| 795 | 794 | |
| 796 | - , not (xopt LangExt.IncoherentInstances dflags)
|
|
| 795 | + , not (xopt LangExt.IncoherentInstances dflags)
|
|
| 797 | 796 | -- If IncoherentInstances is on then we cannot rely on coherence of proofs
|
| 798 | 797 | -- in order to justify this optimization: The proof provided by the
|
| 799 | 798 | -- [G] constraint's superclass may be different from the top-level proof.
|
| 800 | 799 | -- See Note [Shortcut solving: incoherence]
|
| 801 | - |
|
| 802 | - , gopt Opt_SolveConstantDicts dflags
|
|
| 800 | + , gopt Opt_SolveConstantDicts dflags
|
|
| 803 | 801 | -- Enabled by the -fsolve-constant-dicts flag
|
| 804 | 802 | |
| 805 | - -> tryShortCutTcS $ -- tryTcS tries to completely solve some contraints
|
|
| 806 | - do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w))
|
|
| 807 | - ; return (isSolvedWC residual) }
|
|
| 808 | - -- NB: isSolvedWC, not isEmptyWC (#26805). We might succeed
|
|
| 809 | - -- in fully-solving the constraint but still leave some
|
|
| 810 | - -- /solved/ implications in the residual.
|
|
| 811 | - -- See (SCS4) in Note [Shortcut solving]
|
|
| 803 | + = tryShortCutTcS $ -- tryTcS tries to completely solve some contraints
|
|
| 804 | + solveSimpleWanteds (unitBag (CDictCan dict_w))
|
|
| 812 | 805 | |
| 813 | - | otherwise
|
|
| 814 | - -> return False }
|
|
| 806 | + | otherwise
|
|
| 807 | + = return False
|
|
| 815 | 808 | |
| 816 | 809 | |
| 817 | 810 | {- *******************************************************************
|
| ... | ... | @@ -846,7 +839,7 @@ try_instances inerts work_item@(DictCt { di_ev = ev@(CtWanted wev), di_cls = cls |
| 846 | 839 | ; case lkup_res of
|
| 847 | 840 | OneInst { cir_what = what }
|
| 848 | 841 | -> do { let is_local_given = case what of { LocalInstance -> True; _ -> False }
|
| 849 | - ; take_shortcut <- tryShortCutSolver is_local_given work_item
|
|
| 842 | + ; take_shortcut <- tryShortCutSolver dflags is_local_given work_item
|
|
| 850 | 843 | ; if take_shortcut
|
| 851 | 844 | then stopWith ev "shortCutSolver worked(2)"
|
| 852 | 845 | else do { insertSafeOverlapFailureTcS what work_item
|
| ... | ... | @@ -1351,7 +1351,7 @@ nestTcS (TcS thing_inside) |
| 1351 | 1351 | |
| 1352 | 1352 | ; return res }
|
| 1353 | 1353 | |
| 1354 | -tryShortCutTcS :: TcS Bool -> TcS Bool
|
|
| 1354 | +tryShortCutTcS :: TcS WantedConstraints -> TcS Bool
|
|
| 1355 | 1355 | -- Like nestTcS, but
|
| 1356 | 1356 | -- (a) be a no-op if the nested computation returns False
|
| 1357 | 1357 | -- (b) if (but only if) success, propagate nested bindings to the caller
|
| ... | ... | @@ -1384,28 +1384,38 @@ tryShortCutTcS (TcS thing_inside) |
| 1384 | 1384 | vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var
|
| 1385 | 1385 | , text "new_ev_binds:" <+> ppr new_ev_binds_var
|
| 1386 | 1386 | , ppr old_inerts ]
|
| 1387 | - ; solved <- thing_inside nest_env
|
|
| 1387 | + ; residual <- thing_inside nest_env
|
|
| 1388 | + ; let solved = isSolvedWC residual
|
|
| 1389 | + -- NB: isSolvedWC, not isEmptyWC (#26805). We might succeed
|
|
| 1390 | + -- in fully-solving the constraint but still leave some
|
|
| 1391 | + -- /solved/ implications in the residual.
|
|
| 1392 | + -- See (SCS4) in Note [Shortcut solving]
|
|
| 1388 | 1393 | ; TcM.traceTc "tryShortCutTcS }" (ppr solved)
|
| 1389 | 1394 | |
| 1390 | - ; if not solved
|
|
| 1391 | - then return False
|
|
| 1392 | - else do { -- Successfully solved
|
|
| 1393 | - -- Add the new bindings to the existing ones
|
|
| 1394 | - ; old_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var)
|
|
| 1395 | + ; when solved $ -- Successfully solved
|
|
| 1396 | + do { -- Add the new bindings to the existing ones
|
|
| 1397 | + ; TcM.combineTcEvBinds old_ev_binds_var new_ev_binds_var
|
|
| 1395 | 1398 | |
| 1396 | - ; TcM.combineTcEvBinds old_ev_binds_var new_ev_binds_var
|
|
| 1399 | + -- We are discarding some implications; we must add their
|
|
| 1400 | + -- NeededEvIds to the current bindings, lest we fail to r
|
|
| 1401 | + ; TcM.addNeededEvIds old_ev_binds_var $
|
|
| 1402 | + foldr add_implic emptyVarSet $
|
|
| 1403 | + wc_impl residual
|
|
| 1397 | 1404 | |
| 1398 | - ; final_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var)
|
|
| 1399 | - ; TcM.traceTc "update" (text "old" <+> ppr old_ebvs $$
|
|
| 1400 | - text "new" <+> ppr final_ebvs)
|
|
| 1405 | + -- Update the existing inert set
|
|
| 1406 | + ; new_inerts <- TcM.readTcRef new_inert_var
|
|
| 1407 | + ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts) }
|
|
| 1401 | 1408 | |
| 1402 | - -- Update the existing inert set
|
|
| 1403 | - ; new_inerts <- TcM.readTcRef new_inert_var
|
|
| 1404 | - ; TcM.updTcRef inerts_var (`updateInertsWith` new_inerts)
|
|
| 1405 | 1409 | |
| 1406 | - ; TcM.traceTc "tryTcS update" (ppr (inert_solved_dicts new_inerts))
|
|
| 1407 | - |
|
| 1408 | - ; return True } }
|
|
| 1410 | + ; return solved
|
|
| 1411 | + }
|
|
| 1412 | + where
|
|
| 1413 | + add_implic :: Implication -> NeededEvIds -> NeededEvIds
|
|
| 1414 | + add_implic implic@(Implic { ic_status = status }) needs
|
|
| 1415 | + | IC_Solved { ics_dm = dm, ics_non_dm = non_dm } <- status
|
|
| 1416 | + = needs `unionVarSet` dm `unionVarSet` non_dm
|
|
| 1417 | + | otherwise
|
|
| 1418 | + = pprPanic "tryShortCutTcS" (ppr implic)
|
|
| 1409 | 1419 | |
| 1410 | 1420 | updateInertsWith :: InertSet -> InertSet -> InertSet
|
| 1411 | 1421 | -- Update the current inert set with bits from a nested solve,
|
| ... | ... | @@ -15,7 +15,7 @@ module GHC.Tc.Types.Evidence ( |
| 15 | 15 | |
| 16 | 16 | -- * Evidence bindings
|
| 17 | 17 | TcEvBinds(..), EvBindsVar(..), NeededEvIds,
|
| 18 | - EvBindsState(..), emptyEvBindsState, unionEvBindsState, addCoVarsEBS,
|
|
| 18 | + EvBindsState(..), emptyEvBindsState, unionEvBindsState, addNeededEvIdsEBS,
|
|
| 19 | 19 | EvBindsMap(..), emptyEvBindsMap, extendEvBinds, unionEvBindsMap,
|
| 20 | 20 | lookupEvBind, evBindMapBinds,
|
| 21 | 21 | foldEvBindsMap, nonDetStrictFoldEvBindsMap,
|
| ... | ... | @@ -765,8 +765,8 @@ unionEvBindsState (EBS { ebs_binds = bs1, ebs_needs = n1 }) |
| 765 | 765 | = EBS { ebs_binds = bs1 `unionEvBindsMap` bs2
|
| 766 | 766 | , ebs_needs = n1 `unionVarSet` n2 }
|
| 767 | 767 | |
| 768 | -addCoVarsEBS :: VarSet -> EvBindsState -> EvBindsState
|
|
| 769 | -addCoVarsEBS n1 ebs@(EBS { ebs_needs = n2 })
|
|
| 768 | +addNeededEvIdsEBS :: NeededEvIds -> EvBindsState -> EvBindsState
|
|
| 769 | +addNeededEvIdsEBS n1 ebs@(EBS { ebs_needs = n2 })
|
|
| 770 | 770 | = ebs { ebs_needs = n1 `unionVarSet` n2 }
|
| 771 | 771 | |
| 772 | 772 | instance Outputable EvBindsState where
|
| ... | ... | @@ -106,7 +106,7 @@ module GHC.Tc.Utils.Monad( |
| 106 | 106 | newTcEvBinds, newNoTcEvBinds, cloneEvBindsVar,
|
| 107 | 107 | addTcEvCoBind, addTcEvBind, addTopEvBinds,
|
| 108 | 108 | getTcEvBindsMap, getTcEvBindsState,
|
| 109 | - setTcEvBindsMap, combineTcEvBinds,
|
|
| 109 | + setTcEvBindsMap, combineTcEvBinds, addNeededEvIds,
|
|
| 110 | 110 | chooseUniqueOccTc,
|
| 111 | 111 | getConstraintVar, setConstraintVar,
|
| 112 | 112 | emitConstraints, emitSimple, emitSimples,
|
| ... | ... | @@ -2018,7 +2018,7 @@ combineTcEvBinds (EvBindsVar { ebv_binds = old_ebv_ref }) |
| 2018 | 2018 | combineTcEvBinds (EvBindsVar { ebv_binds = old_tcv_ref })
|
| 2019 | 2019 | (CoEvBindsVar { ebv_needs = new_tcv_ref })
|
| 2020 | 2020 | = do { new_tcvs <- readTcRef new_tcv_ref
|
| 2021 | - ; updTcRef old_tcv_ref (addCoVarsEBS new_tcvs) }
|
|
| 2021 | + ; updTcRef old_tcv_ref (addNeededEvIdsEBS new_tcvs) }
|
|
| 2022 | 2022 | combineTcEvBinds (CoEvBindsVar { ebv_needs = old_tcv_ref })
|
| 2023 | 2023 | (CoEvBindsVar { ebv_needs = new_tcv_ref })
|
| 2024 | 2024 | = do { new_tcvs <- readTcRef new_tcv_ref
|
| ... | ... | @@ -2027,16 +2027,17 @@ combineTcEvBinds old_var new_var |
| 2027 | 2027 | = pprPanic "combineTcEvBinds" (ppr old_var $$ ppr new_var)
|
| 2028 | 2028 | -- Terms inside types, no good
|
| 2029 | 2029 | |
| 2030 | +addNeededEvIds :: EvBindsVar -> NeededEvIds -> TcM ()
|
|
| 2031 | +addNeededEvIds (EvBindsVar { ebv_binds = bs_ref }) needed
|
|
| 2032 | + = updTcRef bs_ref (addNeededEvIdsEBS needed)
|
|
| 2033 | +addNeededEvIds (CoEvBindsVar { ebv_needs = need_ref }) needed
|
|
| 2034 | + = updTcRef need_ref (unionVarSet needed)
|
|
| 2035 | + |
|
| 2030 | 2036 | addTcEvCoBind :: EvBindsVar -> CoercionHole -> CoercionPlusHoles -> TcM ()
|
| 2031 | 2037 | addTcEvCoBind ebv hole co_plus_holes@(CPH { cph_co = co })
|
| 2032 | 2038 | = do { fillCoercionHole hole co_plus_holes
|
| 2033 | 2039 | -- Record usage of the free vars of this coercion
|
| 2034 | - ; let fvs = coVarsOfCo co
|
|
| 2035 | - ; case ebv of
|
|
| 2036 | - EvBindsVar { ebv_binds = bs_ref }
|
|
| 2037 | - -> updTcRef bs_ref (addCoVarsEBS fvs)
|
|
| 2038 | - CoEvBindsVar { ebv_needs = need_ref }
|
|
| 2039 | - -> updTcRef need_ref (unionVarSet fvs) }
|
|
| 2040 | + ; addNeededEvIds ebv (coVarsOfCo co) }
|
|
| 2040 | 2041 | |
| 2041 | 2042 | addTcEvBind :: EvBindsVar -> EvBind -> TcM ()
|
| 2042 | 2043 | -- Add a binding to the TcEvBinds by side effect
|