Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: 7121fd75 by Simon Peyton Jones at 2025-09-23T00:26:47+01:00 Progress [skip ci]x - - - - - 7 changed files: - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Utils/TcType.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -395,7 +395,7 @@ tryConstraintDefaulting wc | isEmptyWC wc = return wc | otherwise - = do { (unif_happened, better_wc) <- reportUnifications (go_wc wc) + = do { (unif_happened, better_wc) <- reportCoarseGrainUnifications (go_wc wc) -- We may have done unifications; so solve again ; solveAgainIf unif_happened better_wc } where ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -543,9 +543,14 @@ can_eq_nc_forall ev eq_rel s1 s2 -- Generate the constraints that live in the body of the implication -- See (SF5) in Note [Solving forall equalities] - ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $ - wrapUnifier ev (eqRelRole eq_rel) $ \uenv -> - go uenv skol_tvs init_subst2 bndrs1 bndrs2 + ; (unifs, (lvl, (all_co, wanteds))) + <- reportFindGrainUnifications $ + pushLevelNoWorkList (ppr skol_info) $ + wrapUnifier ev (eqRelRole eq_rel) $ \uenv -> + go uenv skol_tvs init_subst2 bndrs1 bndrs2 + + -- Kick out any inerts constraints that mention unified type variables + ; kickOutAfterUnification unifs -- Solve the implication right away, using `trySolveImplication` -- See (SF6) in Note [Solving forall equalities] @@ -1670,31 +1675,36 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) } CtWanted {} - -> do { (unifs, (kind_co, cts)) <- reportUnifications $ + -> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $ wrapUnifier ev Nominal $ \uenv -> let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) in unSwap swapped (uType uenv') ki1 ki2 -- mkKindEqLoc: any new constraints, arising from the kind -- unification, say they thay come from unifying xi1~xi2 + -- ...AndEmit: emit any unsolved equalities - -- Emit any unsolved kind equalities - ; unless (isEmptyBag cts) $ - updWorkListTcS (extendWorkListChildEqs ev cts) + -- Kick out any inert constraints mentioning the unified variables + ; kickOutAfterUnification unifs - ; if unifs + ; if not (isEmptyVarSet unifs) then -- Unifications happened, so start again to do the zonking -- Otherwise we might put something in the inert set that isn't inert + -- Since we are starting again we can ignore `eqs`, because they will + -- happen again next time round startAgainWith (mkNonCanonical ev) else - assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $ - -- assert: the constraints won't be empty because the two kinds differ, - -- and there are no unifications, so we must have emitted one or - -- more constraints - finish (rewriterSetFromCts cts) kind_co } - -- rewriterSetFromCts: record in the /type/ unification xi1~xi2 that - -- it has been rewritten by any (unsolved) consraints in `cts`; that - -- stops xi1~xi2 from unifying until `cts` are solved. See (EIK2). + -- Emit the deferred constraints + do { emitChildEqs eqs + + ; assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $ + -- assert: the constraints won't be empty because the two kinds differ, + -- and there are no unifications, so we must have emitted one or + -- more constraints + finish (rewriterSetFromCts cts) kind_co }} + -- rewriterSetFromCts: record in the /type/ unification xi1~xi2 that + -- it has been rewritten by any (unsolved) constraints in `cts`; that + -- stops xi1~xi2 from unifying until `cts` are solved. See (EIK2). where xi1 = canEqLHSType lhs1 role = eqRelRole eq_rel @@ -2019,6 +2029,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; setEvBindIfWanted new_ev EvCanonical $ evCoercion (mkNomReflCo final_rhs) + -- Kick out any constraints that can now be rewritten + ; kickOutAfterUnification (unitVarSet tv) + ; return (Stop new_ev (text "Solved by unification")) } --------------------------- ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -198,7 +198,7 @@ The solution is super-simple: * Better still, we solve the [FunDepEqns] with solveFunDeps :: CtEvidence -> [FunDepEqns] -> TcS Bool - It uses `reportUnifications` to see if any unification happened at this + It uses `reportFineGrainUnifications` to see if any unification happened at this level or outside -- that is, it does NOT report unifications to the fresh unification variables. So `solveFunDeps` returns True only if it unifies a variable /other than/ the fresh ones. Bingo. @@ -770,16 +770,20 @@ solveFunDeps work_ev fd_eqns = return False -- Common case no-op | otherwise - = do { (unif_happened, _res) - <- reportUnifications $ - nestFunDepsTcS $ + = do { (unifs, _res) + <- reportFineGrainUnifications $ + nestFunDepsTcS $ do { (_, eqs) <- wrapUnifier work_ev Nominal do_fundeps ; solveSimpleWanteds eqs } -- Why solveSimpleWanteds? Answer -- (a) We don't want to rely on the eager unifier being clever -- (b) F Int alpha ~ Maybe Int where type instance F Int x = Maybe x - ; return unif_happened } + -- Kick out any inert constraints that mention variables + -- that were unified by the fundep + ; kickOutAfterUnification unifs + + ; return (not (isEmptyVarSet unifs)) } where do_fundeps :: UnifyEnv -> TcM () do_fundeps env = mapM_ (do_one env) fd_eqns ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -55,7 +55,7 @@ module GHC.Tc.Solver.Monad ( newWanted, newWantedNC, newWantedEvVarNC, newBoundEvVarId, - unifyTyVar, reportUnifications, + unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications, setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, newEvVar, newGivenEv, emitNewGivens, @@ -448,6 +448,17 @@ kickOutRewritable ko_spec new_fr , text "kicked_out =" <+> ppr kicked_out , text "Residual inerts =" <+> ppr ics' ]) } } +kickOutAfterUnification :: TcTyVarSet -> TcS () +kickOutAfterUnification tv_set + | isEmptyVarSet tv_set + = return () + | otherwise + = do { n_kicked <- kickOutRewritable (KOAfterUnify tv_set) (Given, NomEq) + -- Given because the tv := xi is given; NomEq because + -- only nominal equalities are solved by unification + ; 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] -- in GHC.Tc.Solver.Equality @@ -1764,30 +1775,47 @@ unifyTyVar :: TcTyVar -> TcType -> TcS () unifyTyVar tv ty = assertPpr (isMetaTyVar tv) (ppr tv) $ do { liftZonkTcS (TcM.writeMetaTyVar tv ty) -- Produces a trace message - ; uni_ref <- getWhatUnifications - ; wrapTcS $ recordUnification uni_ref tv } + ; what_uni <- getWhatUnifications + ; wrapTcS $ recordUnification what_uni tv } + +reportFineGrainUnifications :: TcS a -> TcS (TcTyVarSet, a) +reportFineGrainUnifications (TcS thing_inside) + = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_wu }) -> + do { (unif_tvs, res) <- report_fine_grain_unifs env thing_inside + ; recordUnifications outer_wu unif_tvs + ; return (unif_tvs, res) } -reportUnifications :: TcS a -> TcS (Bool, a) +reportCoarseGrainUnifications :: TcS a -> TcS (Bool, a) -- Record whether any useful 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 NoUnificationsYet - - ; 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 - UnificationsDone unif_lvl - | ambient_lvl `deeperThanOrSame` unif_lvl - -> -- Some useful unifications took place - do { recordUnificationLevel outer_ul_var unif_lvl - ; return (True, res) } - - _ -> -- No useful unifications - return (False, res) } +reportCoarseGrainUnifications (TcS thing_inside) + = TcS $ \ env@(TcSEnv { tcs_unif_lvl = outer_what }) -> + case outer_what of + WU_Coarse outer_ul_ref + -> do { inner_ul_ref <- TcM.newTcRef infiniteTcLevel + ; res <- thing_inside (env { tcs_unif_lvl = WU_Coarse inner_ul_ref }) + ; ambient_lvl <- TcM.getTcLevel + ; outer_ul <- TcM.readTcRef outer_ul_ref + ; inner_ul <- TcM.readTcRef inner_ul_ref + ; unless (inner_ul `deeperThanOrSame` outer_ul) $ + writeTcRef outer_ul_ref inner_ul + ; let unif_happened = ambient_lvl `deeperThanOrSame` inner_lvl + ; return (unif_happened, res) } + WU_Fine outer_tvs + -> do { (unif_tvs,res) <- report_fine_grain_unifs env thing_inside + ; return (not (isEmptyVarSet unif_tvs), res) } + +report_fine_grain_unifs :: TcSEnv -> (TcSEnv -> TcM a) -> TcM (TcTyVarSet, a) +report_fine_grain_unifs env thing_inside + = do { unif_tvs_ref <- TcM.newTcRef emptyVarSet + + ; res <- thing_inside (env { tcs_unif_lvl = WU_Fine unif_tvs_ref }) + + ; unif_tvs <- TcM.readTcRef unif_tvs_ref + ; ambient_lvl <- TcM.getTcLevel + ; let interesting unif_tv = ambient_lvl `deeperThanOrSame` tcTyVarLevel tv + interesting_unifs = filterVarSet interesting unif_tvs + ; return (unif_tvs, res) } getWhatUnifications :: TcS (TcRef WhatUnifications) getWhatUnifications @@ -1995,6 +2023,19 @@ emitNewWantedEq loc rewriters role ty1 ty2 ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical $ CtWanted wtd)) ; return co } +emitChildEqs :: Cts -> TcS () +-- Emit a bunch of equalities into the work list +-- See Note [Work-list ordering] in GHC.Tc.Solved.Equality +-- +-- All the constraints in `cts` share the same rewriter set so, +-- rather than looking at it one by one, we pass it to +-- extendWorkListChildEqs; just a small optimisation. +emitChildEqs eqs + | isEmptyBag eqs + = return () + | otherwise + = updWorkListTcS (extendWorkListChildEqs ev cts) + -- | Create a new Wanted constraint holding a coercion hole -- for an equality between the two types at the given 'Role'. newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType @@ -2146,18 +2187,18 @@ uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns wrapUnifierAndEmit :: CtEvidence -> Role -> (UnifyEnv -> TcM a) -- Some calls to uType -> TcS a --- Like wrapUnifier, but emits any unsolved equalities into the work-list +-- Like wrapUnifier, but +-- emits any unsolved equalities into the work-list +-- kicks out any inert constraints that mention unified variables wrapUnifierAndEmit ev role do_unifications - = do { (res, cts) <- wrapUnifier ev role do_unifications + = do { (unifs, (res, eqs)) <- reportFineGrainUnifications $ + wrapUnifier ev role do_unifications -- Emit the deferred constraints - -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality - -- - -- All the constraints in `cts` share the same rewriter set so, - -- rather than looking at it one by one, we pass it to - -- extendWorkListChildEqs; just a small optimisation. - ; unless (isEmptyBag cts) $ - updWorkListTcS (extendWorkListChildEqs ev cts) + ; emitChildEqs eqs + + -- Kick out any inert constraints mentioning the unified variables + ; kickOutAfterUnification unifs ; return res } ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -119,7 +119,7 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (unif_happened, wc1) <- reportUnifications $ -- See Note [Superclass iteration] + ; (unif_happened, wc1) <- reportCoarseGrainUnifications $ -- 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 @@ -1125,19 +1125,11 @@ solveSimpleWanteds simples where do_solve_and_plugins :: IntWithInf -> WantedConstraints -> TcS (Bool,WantedConstraints) do_solve_and_plugins max_iter wc - = do { wc1 <- run_simple_solver max_iter wc + = do { wc1 <- simple_solver wc ; (rerun_plugin, simples2) <- runTcPluginsWanted (wc_simple wc1) ; return (rerun_plugin, wc1 { wc_simple = simples2 }) } - run_simple_solver :: IntWithInf -> WantedConstraints -> TcS WantedConstraints - -- Run `simple_solver` repeatedly until no more unifications happen - -- Try this repeatedly, until no unifications happen - -- This is potentially quadratic, because we might solve just one - -- constraint in each iteration but that seems inevitable - run_simple_solver max_iter - = iterateToFixpoint (max_iter `mulWithInf` 10) simple_solver - - simple_solver :: WantedConstraints -> TcS (Bool, WantedConstraints) + simple_solver :: WantedConstraints -> TcS WantedConstraints -- Try solving the wc_simple part of these constraints, once -- Affects the unification state (of course) but not the inert set -- The result is not necessarily zonked @@ -1145,8 +1137,7 @@ solveSimpleWanteds simples | isEmptyBag simples = return (False, wc) | otherwise - = reportUnifications $ - nestTcS $ + = nestTcS $ do { solveSimples simples ; simples1 <- getUnsolvedInerts -- Now try to solve any Wanted quantified ===================================== compiler/GHC/Tc/Utils/TcType.hs ===================================== @@ -45,6 +45,7 @@ module GHC.Tc.Utils.TcType ( TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, strictlyDeeperThan, deeperThanOrSame, sameDepthAs, tcTypeLevel, tcTyVarLevel, maxTcLevel, minTcLevel, + infiniteTcLevel, -------------------------------- -- MetaDetails @@ -843,6 +844,12 @@ We can unify alpha:=b in the inner implication, because 'alpha' is touchable; but then 'b' has escaped its scope into the outer implication. -} +infiniteTcLevel :: TcLevel +-- It is sometimes helpful to be able to say "infinitely deep" +-- Particularly as a unit for `minTcLevel` +-- Happily QLInstVar behaves like infinity :-) +infiniteTcLevel = QLInstVar + maxTcLevel :: TcLevel -> TcLevel -> TcLevel maxTcLevel (TcLevel a) (TcLevel b) | a > b = TcLevel a ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify ( makeTypeConcrete, UnifyEnv(..), updUEnvLoc, setUEnvRole, - WhatUnifications(..), recordUnification, recordUnificationLevel, + WhatUnifications(..), recordUnification, recordUnifications, minTcTyVarSetLevel, -------------------------------- -- Holes @@ -2316,8 +2316,11 @@ unifyTypeAndEmit t_or_k orig ty1 ty2 **********************************************************************-} data WhatUnifications - = NoUnificationsYet - | UnificationsDone TcLevel + = WU_Coarse -- Track unifications coarsely + (TcRef TcLevel) -- infiniteTcLevel <=> no unifications yet + + | WU_Fine -- Track each unification individually + (TcRef TcTyVarSet) {- Note [WhatUnifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2346,9 +2349,28 @@ Why do all this? * See Note [When to iterate the solver: unifications] in GHC.Tc.Solver.Solve -} -recordUnification :: TcRef WhatUnifications -> TcTyVar -> TcM () -recordUnification what_ref tv = recordUnificationLevel what_ref (tcTyVarLevel tv) +minTcTyVarSetLevel :: TcTyVarSet -> TcLevel +minTcTyVarSetLevel tvs + = nonDetStrictFoldVarSet (minTcLevel . tcTyVarLevel) infiniteTcLevel tvs + +recordUnification :: WhatUnifications -> TcTyVar -> TcM () +recordUnification what tv = recordUnifications what (unitVarSet tv) + +recordUnifications :: WhatUnifications -> TcTyVarSet -> TcM () +recordUnifications (WU_Coarse lvl_ref) tvs + = do { unif_lvl <- readTcRef lvl_ref + ; let tv_lvl = minTcTyVarSetLevel tvs + ; if tv_lvl `deeperThanOrSame` unif_lvl + then do { traceTc "set-uni-flag: no-op" $ + vcat [ text "lvl" <+> ppr tv_lvl, text "unif_lvl" <+> ppr unif_lvl ] + ; return () } + else do { traceTc "set-uni-flag" (ppr tv_lvl) + ; writeTcRef lvl_ref tv_lvl } } + +recordUnifications (WU_Fine tvs_ref) tvs + = updTcRef tvs_ref (`unionVarSet` tvs) +{- recordUnificationLevel :: TcRef WhatUnifications -> TcLevel -> TcM () recordUnificationLevel what_ref tv_lvl = do { what <- readTcRef what_ref @@ -2360,11 +2382,7 @@ recordUnificationLevel what_ref tv_lvl ; return () } _ -> do { traceTc "set-uni-flag" (ppr tv_lvl) ; writeTcRef what_ref (UnificationsDone tv_lvl) } } - - -instance Outputable WhatUnifications where - ppr NoUnificationsYet = text "NoUniYet" - ppr (UnificationsDone lvl) = text "UniDone" <> braces (ppr lvl) +-} {- %************************************************************************ @@ -2416,7 +2434,7 @@ data UnifyEnv -- Which variables are unified; -- if Nothing, we don't care - , u_what :: Maybe (TcRef WhatUnifications) + , u_what :: Maybe WhatUnifications } setUEnvRole :: UnifyEnv -> Role -> UnifyEnv @@ -2698,7 +2716,7 @@ Deferred unifications are of the form or x ~ ... where F is a type function and x is a type variable. E.g. - id :: x ~ y => x -> y + id :: x ~ y => x -> y id e = e involves the unification x = y. It is deferred until we bring into account the View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7121fd7575551a1cc0e5157bd91fda85... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7121fd7575551a1cc0e5157bd91fda85... You're receiving this email because of your account on gitlab.haskell.org.