Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: 6db30500 by Simon Peyton Jones at 2025-12-02T00:11:51+00:00 Use a depth limit in fundeps - - - - - bab28604 by Simon Peyton Jones at 2025-12-02T00:37:48+00:00 wibbles - - - - - 6 changed files: - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Dict.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 Changes: ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -508,6 +508,10 @@ defaultEquality encl_eqs ct = return False where + ev = ctEvidence ct + rws = ctEvRewriters ev + loc = ctEvLoc ev + -- try_default_tv_nom: used for tv ~#N ty try_default_tv_nom lhs_tv rhs_ty | MetaTv { mtv_info = info } <- tcTyVarDetails lhs_tv @@ -546,7 +550,7 @@ defaultEquality encl_eqs ct = do { traceTcS "defaultEquality success:" (ppr rhs_ty) ; unifyTyVar lhs_tv rhs_ty -- NB: unifyTyVar adds to the -- TcS unification counter - ; setEqIfWanted (ctEvidence ct) (mkReflCPH NomEq rhs_ty) + ; setEqIfWanted ev (mkReflCPH NomEq rhs_ty) ; return True } @@ -561,7 +565,7 @@ defaultEquality encl_eqs ct -- This handles cases such as @IO alpha[tau] ~R# IO Int@ -- by defaulting @alpha := Int@, which is useful in practice -- (see Note [Defaulting representational equalities]). - ; (co, new_eqs) <- wrapUnifier (ctEvidence ct) Nominal $ \uenv -> + ; (co, new_eqs) <- wrapUnifier rws loc Nominal $ \uenv -> -- NB: nominal equality! uType uenv z_ty1 z_ty2 @@ -571,7 +575,7 @@ defaultEquality encl_eqs ct -- See Note [Defaulting representational equalities]. ; if null new_eqs then do { traceTcS "defaultEquality ReprEq } (yes)" empty - ; setEqIfWanted (ctEvidence ct) $ + ; setEqIfWanted ev $ CPH { cph_co = mkSubCo co, cph_holes = emptyCoHoleSet } ; return True } else do { traceTcS "defaultEquality ReprEq } (no)" empty ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -4,7 +4,6 @@ -- | Solving Class constraints CDictCan module GHC.Tc.Solver.Dict ( solveDict, solveDictNC, solveCallStack, - checkInstanceOK, matchLocalInst, chooseInstance, makeSuperClasses, mkStrictSuperClasses ) where @@ -857,8 +856,22 @@ chooseInstance work_item@(WantedCt { ctev_dest = dest, ctev_rewriters = rws , cir_mk_ev = mk_ev , cir_canonical = canonical }) = do { traceTcS "doTopReact/found instance for" $ ppr work_item - ; deeper_loc <- checkInstanceOK loc what pred - ; checkReductionDepth deeper_loc pred + + -- Check that the dfun is well-staged in the Template Haskell sense + ; checkWellLevelledDFun loc what pred + + -- zapped_loc: after applying an instance we can set ScOrigin to + -- NotNakedSc, so that prohibitedSuperClassSolve never fires + -- See Note [Solving superclass constraints] in + -- GHC.Tc.TyCl.Instance, (sc1). + ; let zapped_loc | ScOrigin what _ <- ctLocOrigin loc + = setCtLocOrigin loc (ScOrigin what NotNakedSc) + | otherwise + = loc + + -- Deeper location for new constraints + ; deeper_loc <- bumpReductionDepth zapped_loc pred + ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar) (ppr work_item) ; evc_vars <- mapM (newWanted deeper_loc rws) theta @@ -868,27 +881,6 @@ chooseInstance work_item@(WantedCt { ctev_dest = dest, ctev_rewriters = rws chooseInstance work_item lookup_res = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res) -checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc --- Check that it's OK to use this instance: --- (a) the use is well staged in the Template Haskell sense --- Returns the CtLoc to used for sub-goals --- Probably also want to call checkReductionDepth -checkInstanceOK loc what pred - = do { checkWellLevelledDFun loc what pred - ; return deeper_loc } - where - deeper_loc = zap_origin (bumpCtLocDepth loc) - origin = ctLocOrigin loc - - zap_origin loc -- After applying an instance we can set ScOrigin to - -- NotNakedSc, so that prohibitedSuperClassSolve never fires - -- See Note [Solving superclass constraints] in - -- GHC.Tc.TyCl.Instance, (sc1). - | ScOrigin what _ <- origin - = setCtLocOrigin loc (ScOrigin what NotNakedSc) - | otherwise - = loc - matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS ClsInstResult ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -486,7 +486,7 @@ can_eq_nc_forall :: CtEvidence -> EqRel -- See Note [Solving forall equalities] can_eq_nc_forall ev eq_rel s1 s2 - | CtWanted (WantedCt { ctev_dest = orig_dest }) <- ev + | CtWanted (WantedCt { ctev_dest = orig_dest, ctev_rewriters = rws, ctev_loc = loc }) <- ev = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2 flags1 = binderFlags bndrs1 flags2 = binderFlags bndrs2 @@ -550,7 +550,7 @@ can_eq_nc_forall ev eq_rel s1 s2 do { -- Generate constraints (tclvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $ - wrapUnifier ev (eqRelRole eq_rel) $ \uenv -> + wrapUnifier rws loc (eqRelRole eq_rel) $ \uenv -> go uenv skol_tvs init_subst2 bndrs1 bndrs2 ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds) @@ -788,9 +788,8 @@ can_eq_newtype_nc rdr_env envs ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 -- Check for blowing our stack, and increase the depth -- See Note [Newtypes can blow the stack] - ; let loc = ctEvLoc ev - ev' = ev `setCtEvLoc` bumpCtLocDepth loc - ; checkReductionDepth loc ty1 + ; loc' <- bumpReductionDepth (ctEvLoc ev) ty1 + ; let ev' = ev `setCtEvLoc` loc' -- Next, we record uses of newtype constructors, since coercing -- through newtypes is tantamount to using their constructors. @@ -1689,9 +1688,9 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 ; emitWorkNC [CtGiven kind_ev] ; finish emptyCoHoleSet (givenCtEvCoercion kind_ev) } - CtWanted {} + CtWanted (WantedCt { ctev_loc = loc, ctev_rewriters = rws }) -> do { (unifs, (kind_co, eqs)) <- reportFineGrainUnifications $ - wrapUnifier ev Nominal $ \uenv -> + wrapUnifier rws loc Nominal $ \uenv -> let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) in uType uenv' ki2 ki1 -- kind_co :: ki2 ~N ki1 ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -25,7 +25,6 @@ import GHC.Core.FamInstEnv import GHC.Core.Coercion import GHC.Core.Predicate( EqRel(..) ) import GHC.Core.TyCon -import GHC.Core.TyCo.Rep( Type(..) ) import GHC.Core.Unify( tcUnifyTysForInjectivity, typeListsAreApart ) import GHC.Core.Coercion.Axiom import GHC.Core.TyCo.Subst( elemSubst ) @@ -36,7 +35,6 @@ import GHC.Types.Var.Set import GHC.Utils.Outputable import GHC.Utils.Panic -import GHC.Utils.Misc( lengthExceeds ) import GHC.Data.Pair import Data.Maybe( isNothing, isJust, mapMaybe ) @@ -545,25 +543,11 @@ tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eq ----------------------------------------- mkTopClosedFamEqFDs :: CoAxiom Branched -> [TcType] -> Xi -> TcS [FunDepEqns] mkTopClosedFamEqFDs ax work_args work_rhs - | isInformativeType work_rhs -- Does RHS have anything useful to say? = do { let branches = fromBranches (coAxiomBranches ax) ; traceTcS "mkTopClosed" (ppr branches $$ ppr work_args $$ ppr work_rhs) ; case getRelevantBranches ax work_args work_rhs of [eqn] -> return [eqn] -- If there is just one relevant equation, use it _ -> return [] } - | otherwise - = return [] - -isInformativeType :: Type -> Bool --- The type is headed by something generative, not just --- a type variable or a type-family application -isInformativeType ty | Just ty' <- coreView ty = isInformativeType ty' -isInformativeType (CastTy ty _) = isInformativeType ty -isInformativeType (TyVarTy {}) = False -isInformativeType (CoercionTy {}) = False -- Moot -isInformativeType (TyConApp tc tys) = isGenerativeTyCon tc Nominal || - tys `lengthExceeds` tyConArity tc -isInformativeType _ = True -- AppTy, ForAllTy, FunTy, LitTy hasRelevantGiven :: [EqCt] -> [TcType] -> EqCt -> Bool -- A Given is relevant if it is not apart from the Wanted @@ -907,14 +891,17 @@ solveFunDeps work_ev fd_eqns = return False -- Common case no-op | otherwise - = do { (unifs, _res) + = do { loc' <- bumpReductionDepth (ctEvLoc work_ev) (ctEvPred work_ev) + + ; (unifs, _res) <- reportFineGrainUnifications $ nestFunDepsTcS $ TcS.pushTcLevelM_ $ -- pushTcLevelTcM: increase the level so that unification variables -- allocated by the fundep-creation itself don't count as useful unifications -- See Note [Deeper TcLevel for partial improvement unification variables] - do { (_, eqs) <- wrapUnifier work_ev Nominal do_fundeps + do { (_, eqs) <- wrapUnifier (ctEvRewriters work_ev) loc' Nominal $ + do_fundeps ; solveSimpleWanteds eqs } -- Why solveSimpleWanteds? Answer -- (a) We don't want to rely on the eager unifier being clever @@ -938,7 +925,7 @@ instantiateFunDepEqns (FDEqns { fd_qtvs = tvs, fd_eqs = eqs }) | null tvs = return rev_eqs | otherwise - = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs) + = do { TcM.traceTc "instantiateFunDepEqns" (ppr tvs $$ ppr eqs) ; (_, subst) <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution ; return (map (subst_pair subst) rev_eqs) } where ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -58,7 +58,7 @@ module GHC.Tc.Solver.Monad ( setEvBind, setWantedEq, setWantedDict, setEqIfWanted, setDictIfWanted, fillCoercionHole, newEvVar, newGivenEv, emitNewGivens, - emitChildEqs, checkReductionDepth, + emitChildEqs, bumpReductionDepth, getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getLclEnv, setSrcSpan, @@ -1810,8 +1810,6 @@ selectNextWorkItem pick_me ct new_wl = do { writeTcRef wl_var new_wl ; return (Just ct) } - -- NB: no need for checkReductionDepth (ctLoc ct) (ctPred ct) - -- This is done by GHC.Tc.Solver.Dict.chooseInstance -- try_rws looks through rw_eqs to find one that has an empty -- rewriter set, after zonking. If none such, call try_rest. @@ -2184,12 +2182,13 @@ 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. -checkReductionDepth :: CtLoc -> TcType -- ^ type being reduced - -> TcS () -checkReductionDepth loc ty +bumpReductionDepth :: CtLoc -> TcType -- ^ type being reduced + -> TcS CtLoc +bumpReductionDepth loc ty = do { dflags <- getDynFlags ; when (subGoalDepthExceeded (reductionDepth dflags) (ctLocDepth loc)) $ - wrapErrTcS $ solverDepthError loc ty } + wrapErrTcS $ solverDepthError loc ty + ; return (bumpCtLocDepth loc) } matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN) matchFam tycon args = wrapTcS $ matchFamTcM tycon args @@ -2258,7 +2257,8 @@ wrapUnifierAndEmit :: CtEvidence -> Role -- returns a CoHoleSet describing the new unsolved goals wrapUnifierAndEmit ev role do_unifications = do { (unifs, (co, eqs)) <- reportFineGrainUnifications $ - wrapUnifier ev role do_unifications + wrapUnifier (ctEvRewriters ev) (ctEvLoc ev) role $ + do_unifications -- Emit the deferred constraints ; emitChildEqs ev eqs @@ -2268,7 +2268,7 @@ wrapUnifierAndEmit ev role do_unifications ; return (CPH { cph_co = co, cph_holes = rewriterSetFromCts eqs }) } -wrapUnifier :: CtEvidence -> Role +wrapUnifier :: CoHoleSet -> CtLoc -> Role -> (UnifyEnv -> TcM a) -- Some calls to uType -> TcS (a, Bag Ct) -- Invokes the do_unifications argument, with a suitable UnifyEnv. @@ -2276,7 +2276,7 @@ wrapUnifier :: CtEvidence -> Role -- See Note [wrapUnifier] -- The (Bag Ct) are the deferred constraints; we emit them but -- also return them -wrapUnifier ev role do_unifications +wrapUnifier rws loc role do_unifications = do { given_eq_lvl <- getInnermostGivenEqLevel ; what_uni <- getWhatUnifications @@ -2284,8 +2284,8 @@ wrapUnifier ev role do_unifications do { defer_ref <- TcM.newTcRef emptyBag ; let env = UE { u_role = role , u_given_eq_lvl = given_eq_lvl - , u_rewriters = ctEvRewriters ev - , u_loc = ctEvLoc ev + , u_rewriters = rws + , u_loc = loc , u_defer = defer_ref , u_what = what_uni } -- u_rewriters: the rewriter set and location from ===================================== 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, bumpCtLocDepth ) +import GHC.Tc.Types.CtLoc( CtLoc ) import GHC.Core.Predicate import GHC.Tc.Utils.TcType import GHC.Core.Type @@ -125,14 +125,6 @@ getFlavourRole ; eq_rel <- getEqRel ; return (flavour, eq_rel) } -getLoc :: RewriteM CtLoc -getLoc = getRewriteEnvField re_loc - -checkStackDepth :: Type -> RewriteM () -checkStackDepth ty - = do { loc <- getLoc - ; liftTcS $ checkReductionDepth loc ty } - -- | Change the 'EqRel' in a 'RewriteM'. setEqRel :: EqRel -> RewriteM a -> RewriteM a setEqRel new_eq_rel thing_inside @@ -142,12 +134,13 @@ setEqRel new_eq_rel thing_inside else runRewriteM thing_inside (env { re_eq_rel = new_eq_rel }) {-# INLINE setEqRel #-} -bumpDepth :: RewriteM a -> RewriteM a -bumpDepth (RewriteM thing_inside) +bumpReductionDepthRM :: Type -> RewriteM a -> RewriteM a +bumpReductionDepthRM ty (RewriteM thing_inside) = mkRewriteM $ \env -> do - -- bumpDepth can be called a lot during rewriting so we force the - -- new env to avoid accumulating thunks. - { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) } + { loc' <- TcS.bumpReductionDepth (re_loc env) ty + ; let !env' = env { re_loc = loc' } + -- !env: bumpReductionDepth can be called a lot during rewriting + -- so we force the new env to avoid accumulating thunks ; thing_inside env' } recordRewriter :: CtEvidence -> RewriteM () @@ -584,7 +577,7 @@ rewrite_co co = liftTcS $ zonkCo co -- | Rewrite a reduction, composing the resulting coercions. rewrite_reduction :: Reduction -> RewriteM Reduction rewrite_reduction (Reduction co xi) - = do { redn <- bumpDepth $ rewrite_one xi + = do { redn <- rewrite_one xi ; return $ co `mkTransRedn` redn } -- rewrite (nested) AppTys @@ -799,10 +792,9 @@ 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 - = do { checkStackDepth (mkTyConApp tc tys) - - -- Query the typechecking plugins for all their rewriting functions - -- which apply to a type family application headed by the TyCon 'tc'. + = bumpReductionDepthRM (mkTyConApp tc tys) $ + 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 -- STEP 1. Try to reduce without reducing arguments first. View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9106adf35ef38c62d2720b0ed761d35... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/9106adf35ef38c62d2720b0ed761d35... You're receiving this email because of your account on gitlab.haskell.org.