Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: b261357e by Simon Peyton Jones at 2025-12-02T15:46:07+00:00 Wibbles to depth bound - - - - - 6 changed files: - compiler/GHC/Tc/Errors/Ppr.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/FunDeps.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Rewrite.hs - compiler/GHC/Tc/Types/CtLoc.hs Changes: ===================================== compiler/GHC/Tc/Errors/Ppr.hs ===================================== @@ -167,9 +167,11 @@ instance Diagnostic TcRnMessage where -> mkSimpleDecorated $ pprSolverReportWithCtxt msg TcRnSolverDepthError ty depth -> mkSimpleDecorated msg where + pp_type_or_constraint | isConstraintLikeKind (typeKind ty) = text "constraint" + | otherwise = text "type" msg = vcat [ text "Reduction stack overflow; size =" <+> ppr depth - , hang (text "When simplifying the following type:") + , hang (text "When simplifying the following" <+> pp_type_or_constraint <> colon) 2 (ppr ty) ] TcRnRedundantConstraints redundants (info, show_info) -> mkSimpleDecorated $ ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -349,11 +349,11 @@ can_eq_nc True _rdr_env _envs ev ReprEq ty1 _ ty2 _ can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | ReprEq <- eq_rel , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 - = can_eq_newtype_nc rdr_env envs ev NotSwapped ty1 stuff1 ty2 ps_ty2 + = can_eq_newtype_nc rdr_env envs ev NotSwapped stuff1 ty2 ps_ty2 | ReprEq <- eq_rel , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2 - = can_eq_newtype_nc rdr_env envs ev IsSwapped ty2 stuff2 ty1 ps_ty1 + = can_eq_newtype_nc rdr_env envs ev IsSwapped stuff2 ty1 ps_ty1 -- Then, get rid of casts can_eq_nc rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 @@ -777,18 +777,17 @@ though, because we check our depth in `can_eq_newtype_nc`. can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs -> CtEvidence -- ^ :: ty1 ~ ty2 -> SwapFlag - -> TcType -- ^ ty1 -> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1' -> TcType -- ^ ty2 -> TcType -- ^ ty2, with type synonyms -> TcS (StopOrContinue (Either IrredCt EqCt)) -can_eq_newtype_nc rdr_env envs ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 +can_eq_newtype_nc rdr_env envs ev swapped ((gres, co1), ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] - ; loc' <- bumpReductionDepth (ctEvLoc ev) ty1 + ; loc' <- bumpReductionDepth (ctEvLoc ev) (ctEvPred ev) ; let ev' = ev `setCtEvLoc` loc' -- Next, we record uses of newtype constructors, since coercing ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -38,6 +38,7 @@ import GHC.Utils.Panic import GHC.Data.Pair import Data.Maybe( isNothing, isJust, mapMaybe ) +import Control.Monad( void ) {- Note [Overview of functional dependencies in type inference] @@ -303,17 +304,20 @@ tryDictFunDeps :: DictCt -> SolverStage () tryDictFunDeps dict_ct = do { -- Note [Do local fundeps before top-level instances] - tryDictFunDepsLocal dict_ct - ; tryDictFunDepsTop dict_ct } + insoluble <- tryDictFunDepsLocal dict_ct + ; if insoluble + then nopStage () + else tryDictFunDepsTop dict_ct } -tryDictFunDepsLocal :: DictCt -> SolverStage () +tryDictFunDepsLocal :: DictCt -> SolverStage Bool -- Using functional dependencies, interact the DictCt with the -- inert Givens and Wanteds, to produce new equalities +-- Returns True if the fundeps are insoluble tryDictFunDepsLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) | isGiven work_ev = -- If work_ev is Given, there could in principle be some inert Wanteds -- but in practice there never are because we solve Givens first - nopStage () + nopStage False | otherwise = Stage $ @@ -324,14 +328,15 @@ tryDictFunDepsLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev }) ; let eqns :: [FunDepEqns] eqns = foldr ((++) . do_interaction) [] $ findDictsByClass (inert_dicts inerts) cls - ; imp <- solveFunDeps work_ev eqns + ; (insoluble, unif_happened) <- solveFunDeps work_ev eqns ; traceTcS "tryDictFunDepsLocal }" $ - text "imp =" <+> ppr imp $$ text "eqns = " <+> ppr eqns + text "unif =" <+> ppr unif_happened $$ text "eqns = " <+> ppr eqns - ; if imp then startAgainWith (CDictCan dict_ct) - -- See (DFL1) of Note [Do fundeps last] - else continueWith () } + -- See (DFL1) of Note [Do fundeps last] + ; if insoluble then continueWith True + else if unif_happened then startAgainWith (CDictCan dict_ct) + else continueWith False } where work_pred = ctEvPred work_ev work_is_given = isGiven work_ev @@ -356,11 +361,12 @@ tryDictFunDepsTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis }) ; traceTcS "tryDictFunDepsTop {" (ppr dict_ct) ; let eqns :: [FunDepEqns] eqns = improveFromInstEnv inst_envs cls xis - ; imp <- solveFunDeps ev eqns - ; traceTcS "tryDictFunDepsTop }" (text "imp =" <+> ppr imp) + ; (insoluble, unif_happened) <- solveFunDeps ev eqns + ; traceTcS "tryDictFunDepsTop }" (text "unif =" <+> ppr unif_happened) - ; if imp then startAgainWith (CDictCan dict_ct) - else continueWith () } + ; if not insoluble && unif_happened + then startAgainWith (CDictCan dict_ct) + else continueWith () } {- Note [No Given/Given fundeps] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -481,12 +487,12 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args = if isGiven ev then tryGivenBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_item else do { -- Note [Do local fundeps before top-level instances] - tryFDEqns fam_tc work_args work_item $ - mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs + insoluble <- tryFDEqns fam_tc work_args work_item $ + mkLocalBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_rhs - ; if hasRelevantGiven eqs_for_me work_args work_item + ; if insoluble || hasRelevantGiven eqs_for_me work_args work_item ; then nopStage () - else tryFDEqns fam_tc work_args work_item $ + else void $ tryFDEqns fam_tc work_args work_item $ mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs } | isGiven ev -- See (INJFAM:Given) @@ -496,15 +502,16 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args | otherwise -- Wanted, user-defined type families = do { -- Note [Do local fundeps before top-level instances] - case tyConInjectivityInfo fam_tc of - NotInjective -> nopStage() + insoluble <- case tyConInjectivityInfo fam_tc of + NotInjective -> nopStage False Injective inj -> tryFDEqns fam_tc work_args work_item $ mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs - ; if hasRelevantGiven eqs_for_me work_args work_item + ; if insoluble || hasRelevantGiven eqs_for_me work_args work_item then nopStage () - else tryFDEqns fam_tc work_args work_item $ - mkTopFamEqFDs fam_tc work_args work_rhs } + else void $ tryFDEqns fam_tc work_args work_item $ + mkTopFamEqFDs fam_tc work_args work_rhs + ; nopStage () } mkTopFamEqFDs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqns] mkTopFamEqFDs fam_tc work_args work_rhs @@ -526,17 +533,19 @@ mkTopFamEqFDs fam_tc work_args work_rhs -- closed type families with no equations (isClosedFamilyTyCon_maybe returns Nothing) return [] -tryFDEqns :: TyCon -> [TcType] -> EqCt -> TcS [FunDepEqns] -> SolverStage () +tryFDEqns :: TyCon -> [TcType] -> EqCt -> TcS [FunDepEqns] -> SolverStage Bool +-- Returns True <=> some of the fundep eqns were insoluble tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eqns = Stage $ do { fd_eqns <- mk_fd_eqns ; traceTcS "tryFDEqns" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr work_args , text "rhs:" <+> ppr rhs , text "eqns:" <+> ppr fd_eqns ]) - ; imp <- solveFunDeps ev fd_eqns + ; (insoluble, unif_happened) <- solveFunDeps ev fd_eqns - ; if imp then startAgainWith (CEqCan work_item) - else continueWith () } + ; if insoluble then continueWith True + else if unif_happened then startAgainWith (CEqCan work_item) + else continueWith False } ----------------------------------------- -- User-defined type families @@ -878,7 +887,8 @@ solving. solveFunDeps :: CtEvidence -- The work item -> [FunDepEqns] - -> TcS Bool + -> TcS ( Bool -- True <=> some insoluble fundeps + , Bool ) -- True <=> unifications happened -- Solve a bunch of type-equality equations, generated by functional dependencies -- By "solve" we mean: (only) do unifications. We do not generate evidence, and -- other than unifications there should be no effects whatsoever @@ -888,12 +898,13 @@ solveFunDeps :: CtEvidence -- The work item -- See (SOLVE-FD) in Note [Overview of functional dependencies in type inference] solveFunDeps work_ev fd_eqns | null fd_eqns - = return False -- Common case no-op + = return (False, False) -- Common case no-op | otherwise - = do { loc' <- bumpReductionDepth (ctEvLoc work_ev) (ctEvPred work_ev) + = do { traceTcS "bumping" (ppr work_ev) + ; loc' <- bumpReductionDepth (ctEvLoc work_ev) (ctEvPred work_ev) - ; (unifs, _res) + ; (unifs, residual) <- reportFineGrainUnifications $ nestFunDepsTcS $ TcS.pushTcLevelM_ $ @@ -911,7 +922,7 @@ solveFunDeps work_ev fd_eqns -- that were unified by the fundep ; kickOutAfterUnification unifs - ; return (not (isEmptyVarSet unifs)) } + ; return (insolubleWC residual, not (isEmptyVarSet unifs)) } where do_fundeps :: UnifyEnv -> TcM () do_fundeps env = mapM_ (do_one env) fd_eqns ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -2182,7 +2182,8 @@ newWantedNC loc rewriters pty -- | Checks if the depth of the given location is too much. Fails if -- it's too big, with an appropriate error message. -bumpReductionDepth :: CtLoc -> TcType -- ^ type being reduced +bumpReductionDepth :: CtLoc + -> TcType -- ^ type or constraint being reduced -> TcS CtLoc bumpReductionDepth loc ty = do { dflags <- getDynFlags ===================================== compiler/GHC/Tc/Solver/Rewrite.hs ===================================== @@ -11,7 +11,7 @@ import GHC.Tc.Types ( TcGblEnv(tcg_tc_plugin_rewriters), RewriteEnv(..), runTcPluginM ) import GHC.Tc.Types.Constraint -import GHC.Tc.Types.CtLoc( CtLoc ) +import GHC.Tc.Types.CtLoc( CtLoc, resetCtLocDepth ) import GHC.Core.Predicate import GHC.Tc.Utils.TcType import GHC.Core.Type @@ -90,7 +90,8 @@ runRewriteCtEv ev runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, CoHoleSet) runRewrite loc flav eq_rel thing_inside = do { rewriters_ref <- newTcRef emptyCoHoleSet - ; let fmode = RE { re_loc = loc + ; let fmode = RE { re_loc = resetCtLocDepth loc + -- Start reducing from zero , re_flavour = flav , re_eq_rel = eq_rel , re_rewriters = rewriters_ref } @@ -792,8 +793,7 @@ rewrite_fam_app tc tys -- Can be over-saturated -- See Note [How to normalise a family application] rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_exact_fam_app tc tys - = bumpReductionDepthRM (mkTyConApp tc tys) $ - do { -- Query the typechecking plugins for all their rewriting functions + = do { -- Query the typechecking plugins for all their rewriting functions -- which apply to a type family application headed by the TyCon 'tc'. ; tc_rewriters <- getTcPluginRewritersForTyCon tc @@ -876,7 +876,8 @@ rewrite_exact_fam_app tc tys -> Reduction -> RewriteM Reduction finish use_cache redn = do { -- rewrite the result: FINISH 1 - final_redn <- rewrite_reduction redn + final_redn <- bumpReductionDepthRM (mkTyConApp tc tys) $ + rewrite_reduction redn ; eq_rel <- getEqRel -- extend the cache: FINISH 2 ===================================== compiler/GHC/Tc/Types/CtLoc.hs ===================================== @@ -3,7 +3,8 @@ module GHC.Tc.Types.CtLoc ( -- * CtLoc CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin, ctLocTypeOrKind_maybe, toInvisibleLoc, - ctLocDepth, bumpCtLocDepth, isGivenLoc, mkGivenLoc, mkKindEqLoc, + ctLocDepth, bumpCtLocDepth, resetCtLocDepth, + isGivenLoc, mkGivenLoc, mkKindEqLoc, setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder, @@ -196,6 +197,9 @@ setCtLocSpan ctl@(CtLoc { ctl_env = lcl }) loc = setCtLocEnv ctl (setCtLocRealLo bumpCtLocDepth :: CtLoc -> CtLoc bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d } +resetCtLocDepth :: CtLoc -> CtLoc +resetCtLocDepth loc = loc { ctl_depth = initialSubGoalDepth } + setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc setCtLocOrigin ctl orig = ctl { ctl_origin = orig } View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b261357e6067ca0717371d8ebdeeb301... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b261357e6067ca0717371d8ebdeeb301... You're receiving this email because of your account on gitlab.haskell.org.