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: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -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 View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a5170b29fdc328a3b9325cc4bfa16101... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/a5170b29fdc328a3b9325cc4bfa16101... You're receiving this email because of your account on gitlab.haskell.org.