Ben Gamari pushed to branch wip/backports-9.14 at Glasgow Haskell Compiler / GHC
Commits:
-
13f32328
by Simon Peyton Jones at 2025-08-12T12:33:03-04:00
3 changed files:
Changes:
| ... | ... | @@ -496,11 +496,15 @@ We could use the Eq [a] superclass of the Ord [a], or we could use the top-level |
| 496 | 496 | instance `Eq a => Eq [a]`. But if we did the latter we'd be stuck with an
|
| 497 | 497 | insoluble constraint (Eq a).
|
| 498 | 498 | |
| 499 | -So the ShortCutSolving rule is this:
|
|
| 499 | +-----------------------------------
|
|
| 500 | +So the ShortCutSolving plan is this:
|
|
| 500 | 501 | If we could solve a constraint from a local Given,
|
| 501 | - try first to /completely/ solve the constraint using only top-level instances.
|
|
| 502 | + try first to /completely/ solve the constraint
|
|
| 503 | + using only top-level instances,
|
|
| 504 | + /without/ using any local Givens.
|
|
| 502 | 505 | - If that succeeds, use it
|
| 503 | 506 | - If not, use the local Given
|
| 507 | +-----------------------------------
|
|
| 504 | 508 | |
| 505 | 509 | An example that succeeds:
|
| 506 | 510 | |
| ... | ... | @@ -555,7 +559,7 @@ The moving parts are relatively simple: |
| 555 | 559 | - `matchLocalInst`, which would otherwise consult Given quantified constraints
|
| 556 | 560 | - `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving, don't
|
| 557 | 561 | pick overlappable top-level instances
|
| 558 | - |
|
| 562 | + - `GHC.Tc.Solver.Solve.runTcPluginsWanted`: don't pass any Givens to the plugin
|
|
| 559 | 563 | |
| 560 | 564 | Some wrinkles:
|
| 561 | 565 |
| ... | ... | @@ -897,7 +897,9 @@ for it, so TcS carries a mutable location where the binding can be |
| 897 | 897 | added. This is initialised from the innermost implication constraint.
|
| 898 | 898 | -}
|
| 899 | 899 | |
| 900 | --- | See Note [TcSMode]
|
|
| 900 | +-- | The mode for the constraint solving monad.
|
|
| 901 | +--
|
|
| 902 | +-- See Note [TcSMode], where each constructor is documented
|
|
| 901 | 903 | data TcSMode
|
| 902 | 904 | = TcSVanilla -- ^ Normal constraint solving
|
| 903 | 905 | | TcSPMCheck -- ^ Used when doing patterm match overlap checks
|
| ... | ... | @@ -905,6 +907,12 @@ data TcSMode |
| 905 | 907 | | TcSShortCut -- ^ Fully solve all constraints, without using local Givens
|
| 906 | 908 | deriving (Eq)
|
| 907 | 909 | |
| 910 | +instance Outputable TcSMode where
|
|
| 911 | + ppr TcSVanilla = text "TcSVanilla"
|
|
| 912 | + ppr TcSPMCheck = text "TcSPMCheck"
|
|
| 913 | + ppr TcSEarlyAbort = text "TcSEarlyAbort"
|
|
| 914 | + ppr TcSShortCut = text "TcSShortcut"
|
|
| 915 | + |
|
| 908 | 916 | {- Note [TcSMode]
|
| 909 | 917 | ~~~~~~~~~~~~~~~~~
|
| 910 | 918 | The constraint solver can operate in different modes:
|
| ... | ... | @@ -1011,9 +1011,17 @@ solveSimpleGivens givens |
| 1011 | 1011 | solveSimpleWanteds :: Cts -> TcS Cts
|
| 1012 | 1012 | -- The result is not necessarily zonked
|
| 1013 | 1013 | solveSimpleWanteds simples
|
| 1014 | - = do { traceTcS "solveSimpleWanteds {" (ppr simples)
|
|
| 1014 | + = do { mode <- getTcSMode
|
|
| 1015 | 1015 | ; dflags <- getDynFlags
|
| 1016 | + ; inerts <- getInertSet
|
|
| 1017 | + |
|
| 1018 | + ; traceTcS "solveSimpleWanteds {" $
|
|
| 1019 | + vcat [ text "Mode:" <+> ppr mode
|
|
| 1020 | + , text "Inerts:" <+> ppr inerts
|
|
| 1021 | + , text "Wanteds to solve:" <+> ppr simples ]
|
|
| 1022 | + |
|
| 1016 | 1023 | ; (n,wc) <- go 1 (solverIterations dflags) simples
|
| 1024 | + |
|
| 1017 | 1025 | ; traceTcS "solveSimpleWanteds end }" $
|
| 1018 | 1026 | vcat [ text "iterations =" <+> ppr n
|
| 1019 | 1027 | , text "residual =" <+> ppr wc ]
|
| ... | ... | @@ -1663,19 +1671,28 @@ runTcPluginsGiven |
| 1663 | 1671 | -- 'solveSimpleWanteds' should feed the updated wanteds back into the
|
| 1664 | 1672 | -- main solver.
|
| 1665 | 1673 | runTcPluginsWanted :: Cts -> TcS (Bool, Cts)
|
| 1666 | -runTcPluginsWanted simples1
|
|
| 1667 | - | isEmptyBag simples1
|
|
| 1668 | - = return (False, simples1)
|
|
| 1674 | +runTcPluginsWanted wanted
|
|
| 1675 | + | isEmptyBag wanted
|
|
| 1676 | + = return (False, wanted)
|
|
| 1669 | 1677 | | otherwise
|
| 1670 | 1678 | = do { solvers <- getTcPluginSolvers
|
| 1671 | - ; if null solvers then return (False, simples1) else
|
|
| 1672 | - |
|
| 1673 | - do { given <- getInertGivens
|
|
| 1674 | - ; wanted <- TcS.zonkSimples simples1 -- Plugin requires zonked inputs
|
|
| 1675 | - |
|
| 1676 | - ; traceTcS "Running plugins (" (vcat [ text "Given:" <+> ppr given
|
|
| 1677 | - , text "Wanted:" <+> ppr wanted ])
|
|
| 1678 | - ; p <- runTcPluginSolvers solvers (given, bagToList wanted)
|
|
| 1679 | + ; if null solvers then return (False, wanted) else
|
|
| 1680 | + |
|
| 1681 | + do { -- Find the set of Givens to give to the plugin.
|
|
| 1682 | + -- If TcSMode = TcSShortCut, we are solving with
|
|
| 1683 | + -- no Givens so don't return any (#26258)!
|
|
| 1684 | + -- See Note [Shortcut solving] in GHC.Tc.Solver.Dict
|
|
| 1685 | + mode <- getTcSMode
|
|
| 1686 | + ; given <- case mode of
|
|
| 1687 | + TcSShortCut -> return []
|
|
| 1688 | + _ -> getInertGivens
|
|
| 1689 | + |
|
| 1690 | + -- Plugin requires zonked input wanteds
|
|
| 1691 | + ; zonked_wanted <- TcS.zonkSimples wanted
|
|
| 1692 | + |
|
| 1693 | + ; traceTcS "Running plugins {" (vcat [ text "Given:" <+> ppr given
|
|
| 1694 | + , text "Wanted:" <+> ppr zonked_wanted ])
|
|
| 1695 | + ; p <- runTcPluginSolvers solvers (given, bagToList zonked_wanted)
|
|
| 1679 | 1696 | ; let (_, solved_wanted) = pluginSolvedCts p
|
| 1680 | 1697 | (_, unsolved_wanted) = pluginInputCts p
|
| 1681 | 1698 | new_wanted = pluginNewCts p
|
| ... | ... | @@ -1684,9 +1701,6 @@ runTcPluginsWanted simples1 |
| 1684 | 1701 | listToBag unsolved_wanted `andCts`
|
| 1685 | 1702 | listToBag insols
|
| 1686 | 1703 | |
| 1687 | --- SLPJ: I'm deeply suspicious of this
|
|
| 1688 | --- ; updInertCans (removeInertCts $ solved_givens)
|
|
| 1689 | - |
|
| 1690 | 1704 | ; mapM_ setEv solved_wanted
|
| 1691 | 1705 | |
| 1692 | 1706 | ; traceTcS "Finished plugins }" (ppr new_wanted)
|