Simon Peyton Jones pushed to branch wip/T26315 at Glasgow Haskell Compiler / GHC
Commits:
-
04f3db59
by Simon Peyton Jones at 2025-09-02T01:01:25+01:00
5 changed files:
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Utils/Monad.hs
Changes:
| ... | ... | @@ -39,7 +39,7 @@ import GHC.Tc.Gen.HsType |
| 39 | 39 | import GHC.Tc.Solver( reportUnsolvedEqualities, pushLevelAndSolveEqualitiesX
|
| 40 | 40 | , emitResidualConstraints )
|
| 41 | 41 | import GHC.Tc.Solver.Solve( solveWanteds )
|
| 42 | -import GHC.Tc.Solver.Monad( runTcS, setTcSMode, TcSMode(..), runTcSWithEvBinds )
|
|
| 42 | +import GHC.Tc.Solver.Monad( runTcS, setTcSMode, TcSMode(..), vanillaTcSMode, runTcSWithEvBinds )
|
|
| 43 | 43 | import GHC.Tc.Validity ( checkValidType )
|
| 44 | 44 | |
| 45 | 45 | import GHC.Tc.Utils.Monad
|
| ... | ... | @@ -1146,12 +1146,12 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult |
| 1146 | 1146 | -- Look up the predicate in Given quantified constraints,
|
| 1147 | 1147 | -- which are effectively just local instance declarations.
|
| 1148 | 1148 | matchLocalInst body_pred loc
|
| 1149 | - = odo { -- Look in the inert set for a matching Given quantified constraint
|
|
| 1149 | + = do { -- Look in the inert set for a matching Given quantified constraint
|
|
| 1150 | 1150 | inerts@(IS { inert_cans = ics }) <- getInertSet
|
| 1151 | 1151 | ; case match_local_inst inerts (inert_qcis ics) of
|
| 1152 | - { ([], []) -> do { traceTcS "No local instance for" (ppr body_pred)
|
|
| 1153 | - ; return NoInstance }
|
|
| 1154 | - ; (matches, unifs) ->
|
|
| 1152 | + { ([], []) -> do { traceTcS "No local instance for" (ppr body_pred)
|
|
| 1153 | + ; return NoInstance }
|
|
| 1154 | + ; (matches, unifs) ->
|
|
| 1155 | 1155 | |
| 1156 | 1156 | do { -- Find the best match
|
| 1157 | 1157 | -- See Note [Use only the best matching quantified constraint]
|
| ... | ... | @@ -909,19 +909,19 @@ data TcSMode |
| 909 | 909 | -- ^ Do not select an OVERLAPPABLE instance
|
| 910 | 910 | , tcsmFullySolveQCIs :: Bool
|
| 911 | 911 | -- ^ Fully solve all constraints, without using local Givens
|
| 912 | - deriving (Eq)
|
|
| 912 | + }
|
|
| 913 | 913 | |
| 914 | 914 | vanillaTcSMode :: TcSMode
|
| 915 | -vanillaTcSMode = TcSMode { tcs_pm_check = False
|
|
| 915 | +vanillaTcSMode = TcSMode { tcsmPmCheck = False
|
|
| 916 | 916 | , tcsmEarlyAbort = False
|
| 917 | 917 | , tcsmSkipOverlappable = False
|
| 918 | 918 | , tcsmFullySolveQCIs = False }
|
| 919 | 919 | |
| 920 | 920 | instance Outputable TcSMode where
|
| 921 | - ppr (TcSMode { tcs_pm_check = pm, tcsmEarlyAbort = ea
|
|
| 921 | + ppr (TcSMode { tcsmPmCheck = pm, tcsmEarlyAbort = ea
|
|
| 922 | 922 | , tcsmSkipOverlappable = so, tcsmFullySolveQCIs = fs })
|
| 923 | 923 | = text "TcSMode" <> (braces $
|
| 924 | - text "pm=" <> ppr pmc <> comma <>
|
|
| 924 | + text "pm=" <> ppr pm <> comma <>
|
|
| 925 | 925 | text "ea=" <> ppr ea <> comma <>
|
| 926 | 926 | text "so=" <> ppr so <> comma <>
|
| 927 | 927 | text "fs=" <> ppr fs)
|
| ... | ... | @@ -1111,9 +1111,9 @@ runTcS tcs |
| 1111 | 1111 | runTcSEarlyAbort :: TcS a -> TcM a
|
| 1112 | 1112 | runTcSEarlyAbort tcs
|
| 1113 | 1113 | = do { ev_binds_var <- TcM.newTcEvBinds
|
| 1114 | - ; runTcSWithEvBinds' TcSEarlyAbort ev_binds_var tcs }
|
|
| 1114 | + ; runTcSWithEvBinds' mode ev_binds_var tcs }
|
|
| 1115 | 1115 | where
|
| 1116 | - mode = vanillaTcSMode { tcsmEarlyAbort = True ]
|
|
| 1116 | + mode = vanillaTcSMode { tcsmEarlyAbort = True }
|
|
| 1117 | 1117 | |
| 1118 | 1118 | -- | This can deal only with equality constraints.
|
| 1119 | 1119 | runTcSEqualities :: TcS a -> TcM a
|
| ... | ... | @@ -1124,9 +1124,9 @@ runTcSEqualities thing_inside |
| 1124 | 1124 | -- | A variant of 'runTcS' that takes and returns an 'InertSet' for
|
| 1125 | 1125 | -- later resumption of the 'TcS' session.
|
| 1126 | 1126 | runTcSInerts :: InertSet -> TcS a -> TcM (a, InertSet)
|
| 1127 | -runTcSInerts inerts tcs = do
|
|
| 1127 | +runTcSInerts inerts tcs
|
|
| 1128 | 1128 | = do { ev_binds_var <- TcM.newTcEvBinds
|
| 1129 | - ; runTcSWithEvBinds' (vanillaTcMode { tcsmPmCheck = True })
|
|
| 1129 | + ; runTcSWithEvBinds' (vanillaTcSMode { tcsmPmCheck = True })
|
|
| 1130 | 1130 | ev_binds_var $
|
| 1131 | 1131 | do { setInertSet inerts
|
| 1132 | 1132 | ; a <- tcs
|
| ... | ... | @@ -1136,7 +1136,7 @@ runTcSInerts inerts tcs = do |
| 1136 | 1136 | runTcSWithEvBinds :: EvBindsVar
|
| 1137 | 1137 | -> TcS a
|
| 1138 | 1138 | -> TcM a
|
| 1139 | -runTcSWithEvBinds = runTcSWithEvBinds' TcSVanilla
|
|
| 1139 | +runTcSWithEvBinds = runTcSWithEvBinds' vanillaTcSMode
|
|
| 1140 | 1140 | |
| 1141 | 1141 | runTcSWithEvBinds' :: TcSMode
|
| 1142 | 1142 | -> EvBindsVar
|
| ... | ... | @@ -1917,7 +1917,7 @@ matchGlobalInst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS TcM.ClsInstResult |
| 1917 | 1917 | matchGlobalInst dflags cls tys loc
|
| 1918 | 1918 | = do { mode <- getTcSMode
|
| 1919 | 1919 | ; let skip_overlappable = tcsmSkipOverlappable mode
|
| 1920 | - ; wrapTcS $ TcM.matchGlobalInst dflags short_cut cls tys (Just loc) }
|
|
| 1920 | + ; wrapTcS $ TcM.matchGlobalInst dflags skip_overlappable cls tys (Just loc) }
|
|
| 1921 | 1921 | |
| 1922 | 1922 | tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])
|
| 1923 | 1923 | tcInstSkolTyVarsX skol_info subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX skol_info subst tvs
|
| ... | ... | @@ -362,6 +362,12 @@ solveImplication imp@(Implic { ic_tclvl = tclvl |
| 362 | 362 | |
| 363 | 363 | ; traceTcS "solveImplication 2"
|
| 364 | 364 | (ppr given_insols $$ ppr residual_wanted)
|
| 365 | + |
|
| 366 | + ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
|
|
| 367 | + ; traceTcS "solveImplication 3" $ vcat
|
|
| 368 | + [ text "ev_binds_var" <+> ppr ev_binds_var
|
|
| 369 | + , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) ]
|
|
| 370 | + |
|
| 365 | 371 | ; let final_wanted = residual_wanted `addInsols` given_insols
|
| 366 | 372 | -- Don't lose track of the insoluble givens,
|
| 367 | 373 | -- which signal unreachable code; put them in ic_wanted
|
| ... | ... | @@ -1504,7 +1510,7 @@ solveWantedQCI :: TcSMode |
| 1504 | 1510 | -> TcS (Maybe (Either Ct Implication))
|
| 1505 | 1511 | -- Try to solve a quantified constraint.
|
| 1506 | 1512 | -- In TcSChortCut mode, insist on solving it fully or not at all
|
| 1507 | --- Returns
|
|
| 1513 | +-- Returns
|
|
| 1508 | 1514 | -- No-op on all Cts other than CQuantCan
|
| 1509 | 1515 | -- See Note [Solving a Wanted forall-constraint]
|
| 1510 | 1516 | solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev = ev, qci_tvs = tvs
|
| ... | ... | @@ -1548,22 +1554,23 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev = ev, qci_tvs = tvs |
| 1548 | 1554 | |
| 1549 | 1555 | ; imp' <- solveImplication imp
|
| 1550 | 1556 | |
| 1551 | - ; let do_update_evidence = setWantedEvTerm dest EvCanonical $
|
|
| 1552 | - EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
|
|
| 1553 | - , et_binds = TcEvBinds ev_binds_var
|
|
| 1554 | - , et_body = wantedCtEvEvId wanted_ev }
|
|
| 1555 | - |
|
| 1556 | - ; if | isSolvedStatus (ic_status imp')
|
|
| 1557 | - -> -- Fully solved, we are all done!
|
|
| 1558 | - do { do_update_evidence; return Nothing }
|
|
| 1559 | - |
|
| 1560 | - | tcsmFullySolveQCIs mode
|
|
| 1561 | - -> -- No-op if we must fully solve quantified constraints
|
|
| 1557 | + ; if | tcsmFullySolveQCIs mode
|
|
| 1558 | + , not (isSolvedStatus (ic_status imp'))
|
|
| 1559 | + -> -- Not fully solved, but mode says that we must fully
|
|
| 1560 | + -- solve quantified constraints; so abandon the attempt
|
|
| 1562 | 1561 | return (Just (Left ct))
|
| 1563 | 1562 | |
| 1564 | 1563 | | otherwise
|
| 1565 | - -> -- Otherwise return partly-solved implication
|
|
| 1566 | - do { do_update_evidence; return (Just (Right imp')) }
|
|
| 1564 | + -> -- Record evidence and return residual implication
|
|
| 1565 | + -- NB: even if it is fully solved we must return it, because it is
|
|
| 1566 | + -- carrying a record of which evidence variables are used
|
|
| 1567 | + -- See Note [Free vars of EvFun] in GHC.Tc.Types.Evidence
|
|
| 1568 | + do { setWantedEvTerm dest EvCanonical $
|
|
| 1569 | + EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
|
|
| 1570 | + , et_binds = TcEvBinds ev_binds_var
|
|
| 1571 | + , et_body = wantedCtEvEvId wanted_ev }
|
|
| 1572 | + |
|
| 1573 | + ; return (Just (Right imp')) }
|
|
| 1567 | 1574 | }
|
| 1568 | 1575 | |
| 1569 | 1576 | | otherwise -- A Given QCInst
|
| ... | ... | @@ -1840,10 +1840,14 @@ updTcEvBinds old_var new_var |
| 1840 | 1840 | addTcEvBind :: EvBindsVar -> EvBind -> TcM ()
|
| 1841 | 1841 | -- Add a binding to the TcEvBinds by side effect
|
| 1842 | 1842 | addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind
|
| 1843 | - = do { traceTc "addTcEvBind" $ ppr u $$
|
|
| 1844 | - ppr ev_bind
|
|
| 1845 | - ; bnds <- readTcRef ev_ref
|
|
| 1846 | - ; writeTcRef ev_ref (extendEvBinds bnds ev_bind) }
|
|
| 1843 | + = do { bnds <- readTcRef ev_ref
|
|
| 1844 | + ; let bnds' = extendEvBinds bnds ev_bind
|
|
| 1845 | + ; traceTc "addTcEvBind" $
|
|
| 1846 | + vcat [ text "EvBindsVar:" <+> ppr u
|
|
| 1847 | + , text "ev_bind:" <+> ppr ev_bind
|
|
| 1848 | + , text "bnds:" <+> ppr bnds
|
|
| 1849 | + , text "bnds':" <+> ppr bnds' ]
|
|
| 1850 | + ; writeTcRef ev_ref bnds' }
|
|
| 1847 | 1851 | addTcEvBind (CoEvBindsVar { ebv_uniq = u }) ev_bind
|
| 1848 | 1852 | = pprPanic "addTcEvBind CoEvBindsVar" (ppr ev_bind $$ ppr u)
|
| 1849 | 1853 |