GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

ccda188d

by Simon Peyton Jones at 2025-08-20T11:55:07-04:00

Start with empty inerts in shortcut solving

When short-cut solving we were starting with an inert set that had
unsolved Wanteds.  This caused an infinite loop (#26314), because a
typechecker plugin kept being given that unsolved Wanted.

It's better just to start with an empty inert set

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

@@ -588,22 +588,24 @@ solving fails and we use the superclass of C:
  The moving parts are relatively simple:
  * To attempt to solve the constraint completely, we just recursively
 -  call the constraint solver. See the use of `tryTcS` in
 +  call the constraint solver. See the use of `tryShortCutTcS` in
    `tcShortCutSolver`.
 -* When this attempted recursive solving, we set a special mode
 -  `TcSShortCut`, which signals that we are trying to solve using only
 -  top-level instances.  We switch on `TcSShortCut` mode in
 -  `tryShortCutSolver`.
 +* When this attempted recursive solving, in `tryShortCutTcS`, we
 +  - start with an empty inert set: no Givens and no Wanteds
 +  - set a special mode  `TcSShortCut`, which signals that we are trying to solve
 +    using only top-level instances.
 -* When in TcSShortCut mode, we behave specially in a few places:
 -  - `tryInertDicts`, where we would otherwise look for a Given to solve our Wanted
 -  - `GHC.Tc.Solver.Monad.lookupInertDict` similarly
 -  - `noMatchableGivenDicts`, which also consults the Givens
 -  - `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
 +* When in TcSShortCut mode, since there are no Givens we can short-circuit;
 +  these are all just optimisations:
 +      - `tryInertDicts`
 +      - `GHC.Tc.Solver.Monad.lookupInertDict`
 +      - `noMatchableGivenDicts`
 +      - `matchLocalInst`
 +      - `GHC.Tc.Solver.Solve.runTcPluginsWanted`
++
 +* In `GHC.Tc.Solver.Instance.Class.matchInstEnv`: when short-cut solving,
 +  don't pick overlappable top-level instances
  Some wrinkles:
@@ -770,14 +772,14 @@ tryInertDicts dict_ct
  try_inert_dicts :: TcSMode -> InertCans -> DictCt -> TcS (StopOrContinue ())
  try_inert_dicts mode inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys })
 -  | not (mode == TcSShortCut)   -- Ignore the inerts (esp Givens) in short-cut mode
 -                                -- See Note [Shortcut solving]
 +  | not (mode == TcSShortCut)   -- Optimisation: ignore the inerts (esp Givens) in
 +                                -- short-cut mode. See Note [Shortcut solving]
    , Just dict_i <- lookupInertDict inerts cls tys
    , let ev_i  = dictCtEvidence dict_i
          loc_i = ctEvLoc ev_i
          loc_w = ctEvLoc ev_w
    = -- There is a matching dictionary in the inert set
 -    do { -- First to try to solve it /completely/ from top level instances
 +    do { -- For a Wanted, first to try to solve it /completely/ from top level instances
           -- See Note [Shortcut solving]
         ; short_cut_worked <- tryShortCutSolver (isGiven ev_i) dict_w
@@ -833,11 +835,7 @@ tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w })
              , gopt Opt_SolveConstantDicts dflags
                -- Enabled by the -fsolve-constant-dicts flag
 -            -> tryTcS $  -- tryTcS tries to completely solve some contraints
 -               -- Inherit the current solved_dicts, so that one invocation of
 -               -- tryShortCutSolver can benefit from the work of earlier invocations
 -               -- See wrinkle (SCS3) of Note [Shortcut solving]
 -               setTcSMode TcSShortCut $
 +            -> tryShortCutTcS $  -- tryTcS tries to completely solve some contraints
                 do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w))
                    ; return (isEmptyBag residual) }
@@ -977,7 +975,7 @@ matchClassInst dflags mode inerts clas tys loc
  noMatchableGivenDicts :: TcSMode -> InertSet -> CtLoc -> Class -> [TcType] -> Bool
  noMatchableGivenDicts mode inerts@(IS { inert_cans = inert_cans }) loc_w clas tys
    | TcSShortCut <- mode
 -  = True  -- In TcSShortCut mode we behave as if there were no Givens at all
 +  = True  -- Optimisation: in TcSShortCut mode there are no Givens
    | otherwise
    = not $ anyBag matchable_given $
      findDictsByClass (inert_dicts inert_cans) clas
@@ -1153,8 +1151,7 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
  -- Look up the predicate in Given quantified constraints,
  -- which are effectively just local instance declarations.
  matchLocalInst body_pred loc
 -  = do { -- In TcSShortCut mode we do not look at Givens;
 -         -- c.f. tryInertDicts
 +  = do { -- Optimisation: in TcSShortCut mode there are no Givens (c.f. tryInertDicts)
           mode <- getTcSMode
         ; case mode of
             { TcSShortCut -> do { traceTcS "matchLocalInst:TcSShortCut" (ppr body_pred)

compiler/GHC/Tc/Solver/Monad.hs

@@ -19,7 +19,7 @@ module GHC.Tc.Solver.Monad (
      runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,
      failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
      runTcSEqualities,
 -    nestTcS, nestImplicTcS, tryTcS,
 +    nestTcS, nestImplicTcS, tryShortCutTcS,
      setEvBindsTcS, setTcLevelTcS,
      emitFunDepWanteds,
@@ -1259,20 +1259,31 @@ nestTcS (TcS thing_inside)
         ; return res }
 -tryTcS :: TcS Bool -> TcS Bool
 +tryShortCutTcS :: TcS Bool -> TcS Bool
  -- Like nestTcS, but
 ---   (a) be a no-op if the nested computation returns Nothing
 +--   (a) be a no-op if the nested computation returns False
  --   (b) if (but only if) success, propagate nested bindings to the caller
  -- Use only by the short-cut solver;
  --   see Note [Shortcut solving] in GHC.Tc.Solver.Dict
 -tryTcS (TcS thing_inside)
 +tryShortCutTcS (TcS thing_inside)
    = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var
                          , tcs_ev_binds = old_ev_binds_var }) ->
 -    do { old_inerts       <- TcM.readTcRef inerts_var
 -       ; new_inert_var    <- TcM.newTcRef old_inerts
 +    do { -- Initialise a fresh inert set, with no Givens and no Wanteds
 +         --    (i.e. empty `inert_cans`)
 +         -- But inherit all the InertSet cache fields; in particular
 +         --  * the given_eq_lvl, so we don't accidentally unify a
 +         --    unification variable from outside a GADT match
 +         --  * the `solved_dicts`; see wrinkle (SCS3) of Note [Shortcut solving]
 +         --  * the `famapp_cache`; similarly
 +         old_inerts <- TcM.readTcRef inerts_var
 +       ; let given_eq_lvl = inert_given_eq_lvl (inert_cans old_inerts)
 +             new_inerts   = old_inerts { inert_cans = emptyInertCans given_eq_lvl }
 +       ; new_inert_var <- TcM.newTcRef new_inerts
++
         ; new_wl_var       <- TcM.newTcRef emptyWorkList
         ; new_ev_binds_var <- TcM.cloneEvBindsVar old_ev_binds_var
 -       ; let nest_env = env { tcs_ev_binds = new_ev_binds_var
 +       ; let nest_env = env { tcs_mode     = TcSShortCut
 +                            , tcs_ev_binds = new_ev_binds_var
                              , tcs_inerts   = new_inert_var
                              , tcs_worklist = new_wl_var }

compiler/GHC/Tc/Solver/Solve.hs

@@ -1681,8 +1681,9 @@ runTcPluginsWanted 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)!
 +         -- Optimisation: if TcSMode = TcSShortCut, we are solving with
 +         -- no Givens so don't bother to look (#26258 was a bug in an earlier
 +         -- version when we left the Givens in the inert set)
           -- See Note [Shortcut solving] in GHC.Tc.Solver.Dict
           mode <- getTcSMode
         ; given <- case mode of