GitLab

sheaf pushed to branch wip/T26258 at Glasgow Haskell Compiler / GHC

Commits:

de2cf17c

by Simon Peyton Jones at 2025-08-07T10:37:52+02: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 <simon.peytonjones@gmail.com>
    Date:   Mon Jul 21 10:04:49 2025 +0100

        Improve treatment of SPECIALISE pragmas -- again!

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)