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
In TcSShortCut, typechecker plugins should get empty Givens
Solving in TcShortCut mode means /ignoring the Givens/. So we
should not pass them to typechecker plugins!
Fixes #26258.
This is a fixup to the earlier MR:
commit 1bd12371feacc52394a0e660ef9349f9e8ee1c06
Author: Simon Peyton Jones
Date: Mon Jul 21 10:04:49 2025 +0100
Improve treatment of SPECIALISE pragmas -- again!
(cherry picked from commit 2860a9a5d657eacd711a7df4a231dc9fe81402c2)
- - - - -
3 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
Changes:
=====================================
compiler/GHC/Tc/Solver/Dict.hs
=====================================
@@ -496,11 +496,15 @@ We could use the Eq [a] superclass of the Ord [a], or we could use the top-level
instance `Eq a => Eq [a]`. But if we did the latter we'd be stuck with an
insoluble constraint (Eq a).
-So the ShortCutSolving rule is this:
+-----------------------------------
+So the ShortCutSolving plan is this:
If we could solve a constraint from a local Given,
- try first to /completely/ solve the constraint using only top-level instances.
+ try first to /completely/ solve the constraint
+ using only top-level instances,
+ /without/ using any local Givens.
- If that succeeds, use it
- If not, use the local Given
+-----------------------------------
An example that succeeds:
@@ -555,7 +559,7 @@ The moving parts are relatively simple:
- `matchLocalInst`, which would otherwise consult Given quantified constraints
- `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving, don't
pick overlappable top-level instances
-
+ - `GHC.Tc.Solver.Solve.runTcPluginsWanted`: don't pass any Givens to the plugin
Some wrinkles:
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -897,7 +897,9 @@ for it, so TcS carries a mutable location where the binding can be
added. This is initialised from the innermost implication constraint.
-}
--- | See Note [TcSMode]
+-- | The mode for the constraint solving monad.
+--
+-- See Note [TcSMode], where each constructor is documented
data TcSMode
= TcSVanilla -- ^ Normal constraint solving
| TcSPMCheck -- ^ Used when doing patterm match overlap checks
@@ -905,6 +907,12 @@ data TcSMode
| TcSShortCut -- ^ Fully solve all constraints, without using local Givens
deriving (Eq)
+instance Outputable TcSMode where
+ ppr TcSVanilla = text "TcSVanilla"
+ ppr TcSPMCheck = text "TcSPMCheck"
+ ppr TcSEarlyAbort = text "TcSEarlyAbort"
+ ppr TcSShortCut = text "TcSShortcut"
+
{- Note [TcSMode]
~~~~~~~~~~~~~~~~~
The constraint solver can operate in different modes:
=====================================
compiler/GHC/Tc/Solver/Solve.hs
=====================================
@@ -1011,9 +1011,17 @@ solveSimpleGivens givens
solveSimpleWanteds :: Cts -> TcS Cts
-- The result is not necessarily zonked
solveSimpleWanteds simples
- = do { traceTcS "solveSimpleWanteds {" (ppr simples)
+ = do { mode <- getTcSMode
; dflags <- getDynFlags
+ ; inerts <- getInertSet
+
+ ; traceTcS "solveSimpleWanteds {" $
+ vcat [ text "Mode:" <+> ppr mode
+ , text "Inerts:" <+> ppr inerts
+ , text "Wanteds to solve:" <+> ppr simples ]
+
; (n,wc) <- go 1 (solverIterations dflags) simples
+
; traceTcS "solveSimpleWanteds end }" $
vcat [ text "iterations =" <+> ppr n
, text "residual =" <+> ppr wc ]
@@ -1663,19 +1671,28 @@ runTcPluginsGiven
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
-- main solver.
runTcPluginsWanted :: Cts -> TcS (Bool, Cts)
-runTcPluginsWanted simples1
- | isEmptyBag simples1
- = return (False, simples1)
+runTcPluginsWanted wanted
+ | isEmptyBag wanted
+ = return (False, wanted)
| otherwise
= do { solvers <- getTcPluginSolvers
- ; if null solvers then return (False, simples1) else
-
- do { given <- getInertGivens
- ; wanted <- TcS.zonkSimples simples1 -- Plugin requires zonked inputs
-
- ; traceTcS "Running plugins (" (vcat [ text "Given:" <+> ppr given
- , text "Wanted:" <+> ppr wanted ])
- ; p <- runTcPluginSolvers solvers (given, bagToList wanted)
+ ; if null solvers then return (False, wanted) else
+
+ do { -- Find the set of Givens to give to the plugin.
+ -- If TcSMode = TcSShortCut, we are solving with
+ -- no Givens so don't return any (#26258)!
+ -- See Note [Shortcut solving] in GHC.Tc.Solver.Dict
+ mode <- getTcSMode
+ ; given <- case mode of
+ TcSShortCut -> return []
+ _ -> getInertGivens
+
+ -- Plugin requires zonked input wanteds
+ ; zonked_wanted <- TcS.zonkSimples wanted
+
+ ; traceTcS "Running plugins {" (vcat [ text "Given:" <+> ppr given
+ , text "Wanted:" <+> ppr zonked_wanted ])
+ ; p <- runTcPluginSolvers solvers (given, bagToList zonked_wanted)
; let (_, solved_wanted) = pluginSolvedCts p
(_, unsolved_wanted) = pluginInputCts p
new_wanted = pluginNewCts p
@@ -1684,9 +1701,6 @@ runTcPluginsWanted simples1
listToBag unsolved_wanted `andCts`
listToBag insols
--- SLPJ: I'm deeply suspicious of this
--- ; updInertCans (removeInertCts $ solved_givens)
-
; mapM_ setEv solved_wanted
; traceTcS "Finished plugins }" (ppr new_wanted)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/13f323286857f69417f2d4ae4e38b218...
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/13f323286857f69417f2d4ae4e38b218...
You're receiving this email because of your account on gitlab.haskell.org.
