GitLab

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC

Commits:

a5170b29
by Simon Peyton Jones at 2025-08-08T00:44:10+01:00
```
Kill off kickOutAfterUnification
```

4 changed files:

compiler/GHC/Tc/Solver/Default.hs
compiler/GHC/Tc/Solver/FunDeps.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Solver/Solve.hs

Changes:

@@ -395,9 +395,9 @@ tryConstraintDefaulting wc
    | isEmptyWC wc
    = return wc
    | otherwise
 -  = do { (n_unifs, better_wc) <- reportUnifications (go_wc wc)
 +  = do { (unif_happened, better_wc) <- reportUnifications (go_wc wc)
           -- We may have done unifications; so solve again
 -       ; solveAgainIf (n_unifs > 0) better_wc }
 +       ; solveAgainIf unif_happened better_wc }
    where
      go_wc :: WantedConstraints -> TcS WantedConstraints
      go_wc wc@(WC { wc_simple = simples, wc_impl = implics })

compiler/GHC/Tc/Solver/FunDeps.hs

@@ -397,12 +397,12 @@ doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys =
          new_orig  = FunDepOrigin2 dict_pred dict_origin
                                    inst_pred inst_loc
+-
  solveFunDeps :: TcS Cts -> TcS Bool
  solveFunDeps generate_eqs
 -  = nestFunDepsTcS $
 -    do { eqs <- generate_eqs
 -       ; solveSimpleWanteds eqs }
 +  = do { (unif_happened, _res) <- nestFunDepsTcS $
 +                                  do { eqs <- generate_eqs
 +                                     ; solveSimpleWanteds eqs }
 +       ; return unif_happened }
  {- Note [No Given/Given fundeps]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/GHC/Tc/Solver/Monad.hs

@@ -451,9 +451,14 @@ kickOutRewritable ko_spec new_fr
                           , text "Residual inerts =" <+> ppr ics' ]) } }
  kickOutAfterUnification :: [TcTyVar] -> TcS ()
 -kickOutAfterUnification tv_list = case nonEmpty tv_list of
 -    Nothing -> return ()
 -    Just tvs -> do
 +kickOutAfterUnification tv_list
 +  = case nonEmpty tv_list of
 +      Nothing  -> return ()
 +      Just tvs -> setUnificationFlagTo min_tv_lvl
 +         where
 +           min_tv_lvl = foldr1 minTcLevel (NE.map tcTyVarLevel tvs)
++
 +{-
         { let tv_set = mkVarSet tv_list
         ; n_kicked <- kickOutRewritable (KOAfterUnify tv_set) (Given, NomEq)
@@ -469,6 +474,7 @@ kickOutAfterUnification tv_list = case nonEmpty tv_list of
         ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked)
         ; return n_kicked }
 +-}
  kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
  -- See Wrinkle (URW2) in Note [Unify only if the rewriter set is empty]
@@ -1286,43 +1292,23 @@ tryTcS (TcS thing_inside)
                   ; return True } }
 -nestFunDepsTcS :: TcS a -> TcS Bool
 +nestFunDepsTcS :: TcS a -> TcS (Bool, a)
  nestFunDepsTcS (TcS thing_inside)
 -  = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var
 -                        , tcs_unif_lvl = unif_lvl_var }) ->
 +  = reportUnifications $
 +    TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var }) ->
 +    TcM.pushTcLevelM_  $
 +         -- pushTcLevelTcM: increase the level so that unification variables
 +         -- allocated by the fundep-creation itself don't count as useful unifications
      do { inerts <- TcM.readTcRef inerts_var
         ; new_inert_var    <- TcM.newTcRef inerts
         ; new_wl_var       <- TcM.newTcRef emptyWorkList
 -       ; new_unif_lvl_var <- TcM.newTcRef Nothing
         ; let nest_env = env { tcs_inerts   = new_inert_var
 -                            , tcs_worklist = new_wl_var
 -                            , tcs_unif_lvl = new_unif_lvl_var }
 +                            , tcs_worklist = new_wl_var }
         ; TcM.traceTc "nestFunDepsTcS {" empty
 -       ; (inner_lvl, _res) <- TcM.pushTcLevelM $
 -                              thing_inside nest_env
 -           -- Increase the level so that unification variables allocated by
 -           -- the fundep-creation itself don't count as useful unifications
 +       ; res <- thing_inside nest_env
         ; TcM.traceTc "nestFunDepsTcS }" empty
+-
 -       -- Figure out whether the fundeps did any useful unifications,
 -       -- and if so update the tcs_unif_lvl
 -       ; mb_new_lvl <- TcM.readTcRef new_unif_lvl_var
 -       ; case mb_new_lvl of
 -           Just unif_lvl
 -             | inner_lvl `deeperThanOrSame` unif_lvl
 -             -> -- Some useful unifications took place
 -                do { mb_old_lvl <- TcM.readTcRef unif_lvl_var
 -                   ; case mb_old_lvl of
 -                       Just old_lvl | unif_lvl `deeperThanOrSame` old_lvl
 -                                    -> return ()
 -                       _ -> TcM.writeTcRef unif_lvl_var (Just unif_lvl)
 -                   ; return True }
+-
 -           _  -> return False   -- No unifications (except of vars
 -                                -- generated in the fundep stuff itself)
 -       }
+-
 +       ; return res }
  updateInertsWith :: InertSet -> InertSet -> InertSet
  -- Update the current inert set with bits from a nested solve,
@@ -1403,30 +1389,6 @@ setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS ()
  setTcEvBindsMap ev_binds_var binds
    = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
 -unifyTyVar :: TcTyVar -> TcType -> TcS ()
 --- Unify a meta-tyvar with a type
 --- We keep track of how many unifications have happened in tcs_unified,
 ---
 --- We should never unify the same variable twice!
 -unifyTyVar tv ty
 -  = assertPpr (isMetaTyVar tv) (ppr tv) $
 -    TcS $ \ env ->
 -    do { TcM.traceTc "unifyTyVar" (ppr tv <+> text ":=" <+> ppr ty)
 -       ; TcM.liftZonkM $ TcM.writeMetaTyVar tv ty
 -       ; TcM.updTcRef (tcs_unified env) (+1) }
+-
 -reportUnifications :: TcS a -> TcS (Int, a)
 --- Record how many unifications are done by thing_inside
 --- We could return a Bool instead of an Int;
 --- all that matters is whether it is no-zero
 -reportUnifications (TcS thing_inside)
 -  = TcS $ \ env ->
 -    do { inner_unified <- TcM.newTcRef 0
 -       ; res <- thing_inside (env { tcs_unified = inner_unified })
 -       ; n_unifs <- TcM.readTcRef inner_unified
 -       ; TcM.updTcRef (tcs_unified env) (+ n_unifs)
 -       ; return (n_unifs, res) }
+-
  getDefaultInfo ::  TcS (DefaultEnv, Bool)
  getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
@@ -1844,6 +1806,43 @@ produced the same Derived constraint.)
  -}
 +unifyTyVar :: TcTyVar -> TcType -> TcS ()
 +-- Unify a meta-tyvar with a type
 +-- We keep track of how many unifications have happened in tcs_unified,
 +--
 +-- We should never unify the same variable twice!
 +unifyTyVar tv ty
 +  = assertPpr (isMetaTyVar tv) (ppr tv) $
 +    do { liftZonkTcS (TcM.writeMetaTyVar tv ty)  -- Produces a trace message
 +       ; setUnificationFlagTo (tcTyVarLevel tv) }
++
 +reportUnifications :: TcS a -> TcS (Bool, a)
 +-- Record whether any unifications are done by thing_inside
 +-- Remember to propagate the information to the enclosing context
 +reportUnifications (TcS thing_inside)
 +  = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_ul_var }) ->
 +    do { inner_ul_var <- TcM.newTcRef Nothing
++
 +       ; res <- thing_inside (env { tcs_unif_lvl = inner_ul_var })
++
 +       ; ambient_lvl  <- TcM.getTcLevel
 +       ; mb_inner_lvl <- TcM.readTcRef inner_ul_var
++
 +       ; case mb_inner_lvl of
 +           Just unif_lvl
 +             | ambient_lvl `deeperThanOrSame` unif_lvl
 +             -> -- Some useful unifications took place
 +                do { mb_outer_lvl <- TcM.readTcRef outer_ul_var
 +                   ; case mb_outer_lvl of
 +                       Just outer_unif_lvl | outer_unif_lvl `strictlyDeeperThan` unif_lvl
 +                         -> -- Update, because outer_unif_lv > unif_lvl
 +                            TcM.writeTcRef outer_ul_var (Just unif_lvl)
 +                       _ -> return ()
 +                   ; return (True, res) }
++
 +           _  -> -- No useful unifications
 +                 return (False, res) }
++
  getUnificationFlag :: TcS Bool
  -- We are at ambient level i
  -- If the unification flag = Just i, reset it to Nothing and return True
@@ -2226,7 +2225,7 @@ unifyForAllBody ev role unify_body
    = do { (res, cts, unified) <- wrapUnifierX ev role unify_body
         -- Kick out any inert constraint that we have unified
 -       ; _ <- kickOutAfterUnification unified
 +       ; kickOutAfterUnification unified
         ; return (res, cts) }
@@ -2255,7 +2254,7 @@ wrapUnifierTcS ev role do_unifications
           updWorkListTcS (extendWorkListChildEqs ev cts)
         -- And kick out any inert constraint that we have unified
 -       ; _ <- kickOutAfterUnification unified
 +       ; kickOutAfterUnification unified
         ; return (res, cts, unified) }

compiler/GHC/Tc/Solver/Solve.hs

@@ -120,13 +120,13 @@ simplify_loop n limit definitely_redo_implications
                              , int (lengthBag simples) <+> text "simples to solve" ])
         ; traceTcS "simplify_loop: wc =" (ppr wc)
 -       ; (n_unifs1, simples1) <- reportUnifications $  -- See Note [Superclass iteration]
 -                                 solveSimpleWanteds simples
 +       ; (unif_happened, simples1) <- reportUnifications $  -- See Note [Superclass iteration]
 +                                      solveSimpleWanteds simples
                  -- Any insoluble constraints are in 'simples' and so get rewritten
                  -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
 -       ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]
 -                   && n_unifs1 == 0                  -- for this conditional
 +       ; wc2 <- if not (definitely_redo_implications  -- See Note [Superclass iteration]
 +                        || unif_happened)             -- for this conditional
                  then return (wc { wc_simple = simples1 })  -- Short cut
                  else do { implics1 <- solveNestedImplications implics
                          ; return (wc { wc_simple = simples1
@@ -1063,15 +1063,16 @@ solveSimpleWanteds simples
                           simples limit (emptyWC { wc_simple = wc })
        | otherwise
        = do { -- Solve
 -             wc1 <- solve_simple_wanteds wc
 +             (unif_happened, wc1) <- reportUnifications $
 +                                     solve_simple_wanteds wc
               -- Run plugins
               -- NB: runTcPluginsWanted has a fast path for empty wc1,
               --     which is the common case
             ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
 -           ; if rerun_plugin
 -             then do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
 +           ; if unif_happened || rerun_plugin
 +             then do { traceTcS "solveSimple going round again:" empty
                       ; go (n+1) limit wc2 }   -- Loop
               else return (n, wc2) }           -- Done