Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC Commits: d6fac0a4 by Simon Peyton Jones at 2025-08-08T11:37:43+01:00 More wibbles Need to remove the unification-count stuff entirely and do more tidying up -- this commit is mainly for CI - - - - - 4 changed files: - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -323,9 +323,11 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) = Stage $ do { inerts <- getInertCans + ; traceTcS "doDictFunDepImprovementLocal {" (ppr dict_ct) ; imp <- solveFunDeps $ foldM do_interaction emptyCts $ findDictsByClass (inert_dicts inerts) cls + ; traceTcS "doDictFunDepImprovementLocal }" (text "imp =" <+> ppr imp) ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } @@ -344,15 +346,13 @@ doDictFunDepImprovementLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) = return new_eqs1 | otherwise - = do { traceTcS "doLocalFunDepImprovement" $ - vcat [ ppr work_ev - , pprCtLoc work_loc, ppr (isGivenLoc work_loc) - , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) - , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ] - - ; new_eqs2 <- unifyFunDepWanteds_new work_ev $ + = do { new_eqs2 <- unifyFunDepWanteds_new work_ev $ improveFromAnother (deriv_loc, inert_rewriters) inert_pred work_pred + + ; traceTcS "doDictFunDepImprovementLocal item" $ + vcat [ ppr work_ev, ppr new_eqs2 ] + ; return (new_eqs1 `unionBags` new_eqs2) } where inert_pred = ctEvPred inert_ev @@ -374,10 +374,12 @@ doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = = Stage $ do { inst_envs <- getInstEnvs + ; traceTcS "doDictFunDepImprovementTop {" (ppr dict_ct) ; let eqns :: [FunDepEqn (CtLoc, RewriterSet)] eqns = improveFromInstEnv inst_envs mk_ct_loc cls xis ; imp <- solveFunDeps $ unifyFunDepWanteds_new ev eqns + ; traceTcS "doDictFunDepImprovementTop }" (text "imp =" <+> ppr imp) ; if imp then startAgainWith (CDictCan dict_ct) else continueWith () } ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -44,7 +44,7 @@ module GHC.Tc.Solver.Monad ( panicTcS, traceTcS, tryEarlyAbortTcS, traceFireTcS, bumpStepCountTcS, csTraceTcS, wrapErrTcS, wrapWarnTcS, - getUnificationFlag, + getUnificationFlag, traceUnificationFlag, -- Evidence creation and transformation MaybeNew(..), freshGoals, isFresh, getEvExpr, @@ -454,7 +454,8 @@ kickOutAfterUnification :: [TcTyVar] -> TcS () kickOutAfterUnification tv_list = case nonEmpty tv_list of Nothing -> return () - Just tvs -> setUnificationFlagTo min_tv_lvl + Just tvs -> do { traceTcS "kickOutAfterUnification" (ppr min_tv_lvl $$ ppr tv_list) + ; setUnificationFlagTo min_tv_lvl } where min_tv_lvl = foldr1 minTcLevel (NE.map tcTyVarLevel tvs) @@ -1833,16 +1834,31 @@ reportUnifications (TcS thing_inside) | ambient_lvl `deeperThanOrSame` unif_lvl -> -- Some useful unifications took place do { mb_outer_lvl <- TcM.readTcRef outer_ul_var + ; TcM.traceTc "reportUnifications" $ + vcat [ text "ambient =" <+> ppr ambient_lvl + , text "unif_lvl =" <+> ppr unif_lvl + , text "mb_outer =" <+> ppr mb_outer_lvl ] ; case mb_outer_lvl of - Just outer_unif_lvl | outer_unif_lvl `strictlyDeeperThan` unif_lvl - -> -- Update, because outer_unif_lv > unif_lvl + Just outer_unif_lvl | unif_lvl `deeperThanOrSame` outer_unif_lvl + -> -- No need to update: outer_unif_lvl is already shallower + return () + _ -> -- Update the outer level TcM.writeTcRef outer_ul_var (Just unif_lvl) - _ -> return () ; return (True, res) } _ -> -- No useful unifications return (False, res) } +traceUnificationFlag :: String -> TcS () +traceUnificationFlag str + = TcS $ \env -> + do { ambient_lvl <- TcM.getTcLevel + ; mb_lvl <- TcM.readTcRef (tcs_unif_lvl env) + ; TcM.traceTc ("trace-uni-flag: " ++ str) $ + vcat [ text "ambient =" <+> ppr ambient_lvl + , text "mb_lvl =" <+> ppr mb_lvl ] + ; return () } + getUnificationFlag :: TcS Bool -- We are at ambient level i -- If the unification flag = Just i, reset it to Nothing and return True @@ -1872,8 +1888,11 @@ setUnificationFlagTo lvl ; mb_lvl <- TcM.readTcRef ref ; case mb_lvl of Just unif_lvl | lvl `deeperThanOrSame` unif_lvl - -> return () - _ -> TcM.writeTcRef ref (Just lvl) } + -> do { TcM.traceTc "set-uni-flag skip" $ + vcat [ text "lvl" <+> ppr lvl, text "unif_lvl" <+> ppr unif_lvl ] + ; return () } + _ -> do { TcM.traceTc "set-uni-flag" (ppr lvl) + ; TcM.writeTcRef ref (Just lvl) } } {- ********************************************************************* @@ -2263,14 +2282,16 @@ wrapUnifierX :: CtEvidence -> Role -> TcS (a, Bag Ct, [TcTyVar]) wrapUnifierX ev role do_unifications = do { unif_count_ref <- getUnifiedRef + ; given_eq_lvl <- getInnermostGivenEqLevel ; wrapTcS $ do { defer_ref <- TcM.newTcRef emptyBag ; unified_ref <- TcM.newTcRef [] - ; let env = UE { u_role = role - , u_rewriters = ctEvRewriters ev - , u_loc = ctEvLoc ev - , u_defer = defer_ref - , u_unified = Just unified_ref} + ; let env = UE { u_role = role + , u_given_eq_lvl = given_eq_lvl + , u_rewriters = ctEvRewriters ev + , u_loc = ctEvLoc ev + , u_defer = defer_ref + , u_unified = Just unified_ref} -- u_rewriters: the rewriter set and location from -- the parent constraint `ev` are inherited in any -- new constraints spat out by the unifier ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -1063,8 +1063,10 @@ solveSimpleWanteds simples simples limit (emptyWC { wc_simple = wc }) | otherwise = do { -- Solve - (unif_happened, wc1) <- reportUnifications $ + traceUnificationFlag "solveSimpleWanteds1" + ; (unif_happened, wc1) <- reportUnifications $ solve_simple_wanteds wc + ; traceUnificationFlag "solveSimpleWanteds2" -- Run plugins -- NB: runTcPluginsWanted has a fast path for empty wc1, ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -2063,7 +2063,12 @@ unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN unifyTypeAndEmit t_or_k orig ty1 ty2 = do { ref <- newTcRef emptyBag ; loc <- getCtLocM orig (Just t_or_k) + ; cur_lvl <- getTcLevel + -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles + -- Here we don't know about given equalities; so we treat + -- /any/ level outside this one as untouchable. Hence cur_lvl. ; let env = UE { u_loc = loc, u_role = Nominal + , u_given_eq_lvl = cur_lvl , u_rewriters = emptyRewriterSet -- ToDo: check this , u_defer = ref, u_unified = Nothing } @@ -2112,11 +2117,14 @@ A job for the future. -} data UnifyEnv - = UE { u_role :: Role - , u_loc :: CtLoc - , u_rewriters :: RewriterSet - - -- Deferred constraints + = UE { u_role :: Role + , u_loc :: CtLoc + , u_rewriters :: RewriterSet + , u_given_eq_lvl :: TcLevel -- Just like the inert_given_eq_lvl field + -- of GHC.Tc.Solver.InertSet.InertCans + + -- Deferred constraints; ones that could not be + -- solved by "on the fly" unification , u_defer :: TcRef (Bag Ct) -- Which variables are unified; @@ -2483,15 +2491,22 @@ uUnfilledVar2 :: UnifyEnv -- Precondition: u_role==Nominal -- definitely not a /filled/ meta-tyvar -> TcTauType -- Type 2, zonked -> TcM CoercionN -uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 - = do { cur_lvl <- getTcLevel - -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles - -- Here we don't know about given equalities; so we treat - -- /any/ level outside this one as untouchable. Hence cur_lvl. - ; if simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2 /= SUC_CanUnify - then not_ok_so_defer cur_lvl - else - do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs +uUnfilledVar2 env@(UE { u_defer = def_eq_ref, u_given_eq_lvl = given_eq_lvl }) + swapped tv1 ty2 + | simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2 /= SUC_CanUnify + = -- Simple unification check fails, so defer + do { traceTc "uUnfilledVar2 not ok" $ + vcat [ text "tv1:" <+> ppr tv1 + , text "ty2:" <+> ppr ty2 + , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2) + ] + -- Occurs check or an untouchable: just defer + -- NB: occurs check isn't necessarily fatal: + -- eg tv1 occurred in type family parameter + ; defer } + + | otherwise + = do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs -- Attempt to unify kinds -- When doing so, be careful to preserve orientation; @@ -2524,22 +2539,11 @@ uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 -- Do this dicarding by simply restoring the previous state -- of def_eqs; a bit imperative/yukky but works fine. ; defer } - }} + } where ty1 = mkTyVarTy tv1 defer = unSwap swapped (uType_defer env) ty1 ty2 - not_ok_so_defer cur_lvl = - do { traceTc "uUnfilledVar2 not ok" $ - vcat [ text "tv1:" <+> ppr tv1 - , text "ty2:" <+> ppr ty2 - , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly cur_lvl tv1 ty2) - ] - -- Occurs check or an untouchable: just defer - -- NB: occurs check isn't necessarily fatal: - -- eg tv1 occurred in type family parameter - ; defer } - swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool swapOverTyVars is_given tv1 tv2 -- See Note [Unification variables on the left] View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d6fac0a40955ba971ea2f2cd8c79ab17... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d6fac0a40955ba971ea2f2cd8c79ab17... You're receiving this email because of your account on gitlab.haskell.org.