Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC Commits: f459ecc1 by Adam Gundry at 2025-06-09T21:13:49+02:00 WIP: store CoVarSet instead of [Coercion] in ZCoercion - - - - - 34eae6a1 by Adam Gundry at 2025-06-09T20:31:23+01:00 WIP: use castCoToCo in arity and occurrence analysis - - - - - 030a1d36 by Adam Gundry at 2025-06-09T20:31:37+01:00 WIP: use castCoToCo in rule matching - - - - - 967543c7 by Adam Gundry at 2025-06-09T20:34:10+01:00 WIP: use castCoToCo in SimpleOpt - - - - - 3734e3b9 by Adam Gundry at 2025-06-09T20:51:34+01:00 Tidy up mkCastZ - - - - - 64177f47 by Adam Gundry at 2025-06-09T20:51:42+01:00 Improve Note [Zapped casts] - - - - - 8cf3d717 by Adam Gundry at 2025-06-09T20:56:50+01:00 Tidy up utilities - - - - - 3fb84e30 by Adam Gundry at 2025-06-09T21:16:39+01:00 Document that -fzap-casts is enabled by default - - - - - 32459579 by Adam Gundry at 2025-06-09T21:24:20+01:00 Tidy up pprOptCastCoercion - - - - - 21 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/FVs.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/DmdAnal.hs - compiler/GHC/Core/Opt/OccurAnal.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/Opt/Simplify/Utils.hs - compiler/GHC/Core/Ppr.hs - compiler/GHC/Core/Rules.hs - compiler/GHC/Core/SimpleOpt.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Ppr.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/TyCo/Tidy.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/CoreToIface.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Zonk/Type.hs - docs/users_guide/debugging.rst Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -54,10 +54,7 @@ module GHC.Core.Coercion ( -- ** Cast coercions castCoToCo, - mkSymCastCo, mkTransCastCo, mkTransCastCoCo, mkTransCoCastCo, - mkPisCastCo, - zapCo, zapCos, zapCastCo, -- ** Decomposition instNewTyCon_maybe, @@ -76,7 +73,7 @@ module GHC.Core.Coercion ( pickLR, isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe, - isReflCastCo, isReflexiveCastCo, + isReflexiveCastCo, isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo, mkCoherenceRightMCo, @@ -2421,7 +2418,7 @@ seqMCo (MCo co) = seqCo co seqCastCoercion :: CastCoercion -> () seqCastCoercion (CCoercion co) = seqCo co -seqCastCoercion (ZCoercion ty cos) = seqType ty `seq` seqCos cos +seqCastCoercion (ZCoercion ty cos) = seqType ty `seq` seqVarSet cos seqCo :: Coercion -> () seqCo (Refl ty) = seqType ty @@ -2858,54 +2855,23 @@ eqCastCoercionX env = eqTypeX env `on` castCoercionRKind -- have discarded the original 'Coercion'. castCoToCo :: Type -> CastCoercion -> CoercionR castCoToCo _ (CCoercion co) = co -castCoToCo lhs_ty (ZCoercion rhs_ty cos) = mkUnivCo ZCoercionProv cos Representational lhs_ty rhs_ty - -mkSymCastCo :: Type -> CastCoercion -> Coercion -mkSymCastCo lhs_ty cco = mkSymCo (castCoToCo lhs_ty cco) +castCoToCo lhs_ty (ZCoercion rhs_ty cos) = mkUnivCo ZCoercionProv (map CoVarCo (nonDetEltsUniqSet cos)) Representational lhs_ty rhs_ty -- | Compose two 'CastCoercion's transitively, like 'mkTransCo'. If either is -- zapped the whole result will be zapped. mkTransCastCo :: HasDebugCallStack => CastCoercion -> CastCoercion -> CastCoercion mkTransCastCo cco (CCoercion co) = mkTransCastCoCo cco co -mkTransCastCo cco (ZCoercion ty cos) = ZCoercion ty (zapCastCo cco ++ cos) +mkTransCastCo cco (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCastCo cco `unionVarSet` cos) -- | Transitively compose a 'CastCoercion' followed by a 'Coercion'. mkTransCastCoCo :: HasDebugCallStack => CastCoercion -> Coercion -> CastCoercion mkTransCastCoCo (CCoercion co1) co2 = CCoercion (mkTransCo co1 co2) -mkTransCastCoCo (ZCoercion _ cos) co2 = ZCoercion (coercionRKind co2) (zapCo co2 ++ cos) +mkTransCastCoCo (ZCoercion _ cos) co2 = ZCoercion (coercionRKind co2) (shallowCoVarsOfCo co2 `unionVarSet` cos) -- | Transitively compose a 'Coercion' followed by a 'CastCoercion'. mkTransCoCastCo :: HasDebugCallStack => Coercion -> CastCoercion -> CastCoercion mkTransCoCastCo co1 (CCoercion co2) = CCoercion (mkTransCo co1 co2) -mkTransCoCastCo co1 (ZCoercion ty cos) = ZCoercion ty (zapCo co1 ++ cos) - --- TODO: Adapt this or rebuildLam to work for ZCoercion -mkPisCastCo :: Role -> [Var] -> Type -> CastCoercion -> CastCoercion -mkPisCastCo r vs expr_ty = CCoercion . mkPiCos r vs . castCoToCo expr_ty - - -zapCo :: Coercion -> [Coercion] -zapCo co = zapCos [co] - --- | Throw away the structure of coercions, retaining only the set of variables --- on which they depend. --- --- It is important we use only the *shallow* free CoVars here, because those are --- the ones on which the original coercions necessarily depended and which may --- be substituted away later. If we use the deep CoVars here, we can end up --- retaining references to CoVars that are no longer in scope (see Note [Shallow --- and deep free variables] in GHC.Core.TyCo.FVs). -zapCos :: [Coercion] -> [Coercion] -zapCos cos = map mkCoVarCo $ nonDetEltsUniqSet (shallowCoVarsOfCos cos) -- TODO nonDetEltsUniqSet justified? - -zapCastCo :: CastCoercion -> [Coercion] -zapCastCo (CCoercion co) = zapCo co -zapCastCo (ZCoercion _ cos) = cos - - -isReflCastCo :: CastCoercion -> Bool -isReflCastCo (CCoercion co) = isReflCo co -isReflCastCo (ZCoercion _ _) = False -- TODO: track this? +mkTransCoCastCo co1 (ZCoercion ty cos) = ZCoercion ty (shallowCoVarsOfCo co1 `unionVarSet` cos) -- | Slowly checks if the coercion is reflexive. Don't call this in a loop, -- as it walks over the entire coercion. ===================================== compiler/GHC/Core/FVs.hs ===================================== @@ -279,7 +279,7 @@ expr_fvs (Let (Rec pairs) body) fv_cand in_scope acc cast_co_fvs :: CastCoercion -> FV cast_co_fvs (CCoercion co) fv_cand in_scope acc = (tyCoFVsOfCo co) fv_cand in_scope acc -cast_co_fvs (ZCoercion ty cos) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` mapUnionFV tyCoFVsOfCo cos) fv_cand in_scope acc +cast_co_fvs (ZCoercion ty cos) fv_cand in_scope acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCoVarSet cos) fv_cand in_scope acc --------- rhs_fvs :: (Id, CoreExpr) -> FV ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -2221,9 +2221,10 @@ etaInfoApp in_scope expr eis go subst (Tick t e) eis = Tick (substTickish subst t) (go subst e eis) - go subst (Cast e (CCoercion co)) (EI bs mco) -- TODO: etaInfoApp ZCoercion + go subst (Cast e cco) (EI bs mco) = go subst e (EI bs mco') where + co = castCoToCo (exprType e) cco -- TODO: can we avoid this? mco' = checkReflexiveMCo (Core.substCo subst co `mkTransMCoR` mco) -- See Note [Check for reflexive casts in eta expansion] @@ -2701,13 +2702,13 @@ same fix. tryEtaReduce :: UnVarSet -> [Var] -> CoreExpr -> SubDemand -> Maybe CoreExpr -- Return an expression equal to (\bndrs. body) tryEtaReduce rec_ids bndrs body eval_sd - = go (reverse bndrs) body (CCoercion (mkRepReflCo (exprType body))) + = go (reverse bndrs) body (mkRepReflCo (exprType body)) where incoming_arity = count isId bndrs -- See Note [Eta reduction makes sense], point (2) go :: [Var] -- Binders, innermost first, types [a3,a2,a1] -> CoreExpr -- Of type tr - -> CastCoercion -- Of type tr ~ ts + -> Coercion -- Of type tr ~ ts -> Maybe CoreExpr -- Of type a1 -> a2 -> a3 -> ts -- See Note [Eta reduction with casted arguments] -- for why we have an accumulating coercion @@ -2717,7 +2718,7 @@ tryEtaReduce rec_ids bndrs body eval_sd -- See Note [Eta reduction with casted function] go bs (Cast e co1) co2 - = go bs e (co1 `mkTransCastCo` co2) + = go bs e (castCoToCo (exprType e) co1 `mkTransCo` co2) go bs (Tick t e) co | tickishFloatable t @@ -2740,7 +2741,7 @@ tryEtaReduce rec_ids bndrs body eval_sd , remaining_bndrs `ltLength` bndrs -- Only reply Just if /something/ has happened , ok_fun fun - , let used_vars = exprFreeVars fun `unionVarSet` tyCoVarsOfCastCo co + , let used_vars = exprFreeVars fun `unionVarSet` tyCoVarsOfCo co reduced_bndrs = mkVarSet (dropList remaining_bndrs bndrs) -- reduced_bndrs are the ones we are eta-reducing away , used_vars `disjointVarSet` reduced_bndrs @@ -2749,7 +2750,7 @@ tryEtaReduce rec_ids bndrs body eval_sd -- See Note [Eta reduction makes sense], intro and point (1) -- NB: don't compute used_vars from exprFreeVars (mkCast fun co) -- because the latter may be ill formed if the guard fails (#21801) - = Just (mkLams (reverse remaining_bndrs) (mkCastCo fun co)) + = Just (mkLams (reverse remaining_bndrs) (mkCast fun co)) go _remaining_bndrs _fun _ = -- pprTrace "tER fail" (ppr _fun $$ ppr _remaining_bndrs) $ Nothing @@ -2797,17 +2798,17 @@ tryEtaReduce rec_ids bndrs body eval_sd --------------- ok_arg :: Var -- Of type bndr_t -> CoreExpr -- Of type arg_t - -> CastCoercion -- Of kind (t1~t2) + -> Coercion -- Of kind (t1~t2) -> Type -- Type (arg_t -> t1) of the function -- to which the argument is supplied - -> Maybe (CastCoercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) - -- (and similarly for tyvars, coercion args) + -> Maybe (Coercion -- Of type (arg_t -> t1 ~ bndr_t -> t2) + -- (and similarly for tyvars, coercion args) , [CoreTickish]) -- See Note [Eta reduction with casted arguments] - ok_arg bndr (Type arg_ty) (CCoercion co) fun_ty + ok_arg bndr (Type arg_ty) co fun_ty | Just tv <- getTyVar_maybe arg_ty , bndr == tv = case splitForAllForAllTyBinder_maybe fun_ty of - Just (Bndr _ vis, _) -> Just (CCoercion fco, []) + Just (Bndr _ vis, _) -> Just (fco, []) where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag kco co -- The lambda we are eta-reducing always has visibility -- 'coreTyLamForAllTyFlag' which may or may not match @@ -2817,24 +2818,23 @@ tryEtaReduce rec_ids bndrs body eval_sd (text "fun:" <+> ppr bndr $$ text "arg:" <+> ppr arg_ty $$ text "fun_ty:" <+> ppr fun_ty) - ok_arg bndr (Var v) (CCoercion co) fun_ty + ok_arg bndr (Var v) co fun_ty | bndr == v , let mult = idMult bndr , Just (_af, fun_mult, _, _) <- splitFunTy_maybe fun_ty , mult `eqType` fun_mult -- There is no change in multiplicity, otherwise we must abort - = Just (CCoercion $ mkFunResCo Representational bndr co, []) - ok_arg bndr (Cast e co_arg) (CCoercion co) fun_ty + = Just (mkFunResCo Representational bndr co, []) + ok_arg bndr (Cast e co_arg) co fun_ty | (ticks, Var v) <- stripTicksTop tickishFloatable e , Just (_, fun_mult, _, _) <- splitFunTy_maybe fun_ty , bndr == v , fun_mult `eqType` idMult bndr - = Just (CCoercion $ mkFunCoNoFTF Representational (multToCo fun_mult) (mkSymCastCo (exprType e) co_arg) co, ticks) + = Just (mkFunCoNoFTF Representational (multToCo fun_mult) (mkSymCo (castCoToCo (exprType e) co_arg)) co, ticks) -- The simplifier combines multiple casts into one, -- so we can have a simple-minded pattern match here ok_arg bndr (Tick t arg) co fun_ty | tickishFloatable t, Just (co', ticks) <- ok_arg bndr arg co fun_ty = Just (co', t:ticks) - -- TODO ok_arg for ZCoercion? ok_arg _ _ _ _ = Nothing -- | Can we eta-reduce the given function @@ -3107,13 +3107,13 @@ collectBindersPushingCo e go :: [Var] -> CoreExpr -> ([Var], CoreExpr) -- The accumulator is in reverse order go bs (Lam b e) = go (b:bs) e - go bs (Cast e (CCoercion co)) = go_c bs e co -- TODO: ought to have ZCoercion case or go_c generalised + go bs (Cast e co) = go_c bs e (castCoToCo (exprType e) co) -- TODO: can we do better? go bs e = (reverse bs, e) -- We are in a cast; peel off casts until we hit a lambda. go_c :: [Var] -> CoreExpr -> Coercion -> ([Var], CoreExpr) -- (go_c bs e c) is same as (go bs e (e |> c)) - go_c bs (Cast e (CCoercion co1)) co2 = go_c bs e (co1 `mkTransCo` co2) -- TODO ditto + go_c bs (Cast e co1) co2 = go_c bs e (castCoToCo (exprType e) co1 `mkTransCo` co2) -- TODO: can we do better? go_c bs (Lam b e) co = go_lam bs b e co go_c bs e co = (reverse bs, mkCast e co) ===================================== compiler/GHC/Core/Opt/DmdAnal.hs ===================================== @@ -2405,13 +2405,17 @@ coercionDmdEnv co = coercionsDmdEnv [co] castCoercionDmdEnv :: CastCoercion -> DmdEnv castCoercionDmdEnv (CCoercion co) = coercionDmdEnv co -castCoercionDmdEnv (ZCoercion _ cos) = coercionsDmdEnv cos +castCoercionDmdEnv (ZCoercion _ cos) = coVarSetDmdEnv cos coercionsDmdEnv :: [Coercion] -> DmdEnv coercionsDmdEnv cos = mkTermDmdEnv $ mapVarEnv (const topDmd) $ getUniqSet $ coVarsOfCos cos -- The VarSet from coVarsOfCos is really a VarEnv Var +coVarSetDmdEnv :: CoVarSet -> DmdEnv +coVarSetDmdEnv cos + = mkTermDmdEnv $ mapVarEnv (const topDmd) $ getUniqSet cos -- TODO shallow/deep confusion? + addVarDmd :: DmdType -> Var -> Demand -> DmdType addVarDmd (DmdType fv ds) var dmd = DmdType (addVarDmdEnv fv var dmd) ds ===================================== compiler/GHC/Core/Opt/OccurAnal.hs ===================================== @@ -3435,8 +3435,8 @@ scrutOkForBinderSwap :: OutExpr -> BinderSwapDecision -- We use this same function in SpecConstr, and Simplify.Iteration, -- when something binder-swap-like is happening scrutOkForBinderSwap (Var v) = DoBinderSwap v MRefl -scrutOkForBinderSwap (Cast (Var v) (CCoercion co)) -- TODO scrutOkForBinderSwap for ZCoercion - | not (isDictId v) = DoBinderSwap v (MCo (mkSymCo co)) +scrutOkForBinderSwap (Cast (Var v) co) + | not (isDictId v) = DoBinderSwap v (MCo (mkSymCo (castCoToCo (idType v) co))) -- TODO: can we do better? -- Cast: see Note [Case of cast] -- isDictId: see Note [Care with binder-swap on dictionaries] -- The isDictId rejects a Constraint/Constraint binder-swap, perhaps ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -644,7 +644,7 @@ tryCastWorkerWrapper env bind_cxt old_bndr bndr (Cast rhs co) mk_worker_unfolding top_lvl work_id work_rhs = case realUnfoldingInfo info of -- NB: the real one, even for loop-breakers unf@(CoreUnfolding { uf_tmpl = unf_rhs, uf_src = src }) - | isStableSource src -> return (unf { uf_tmpl = mkCast unf_rhs (mkSymCastCo (exprType rhs) co) }) + | isStableSource src -> return (unf { uf_tmpl = mkCast unf_rhs (mkSymCo (castCoToCo (exprType rhs) co)) }) _ -> mkLetUnfolding env top_lvl VanillaSrc work_id False work_rhs tryCastWorkerWrapper env _ _ bndr rhs -- All other bindings ===================================== compiler/GHC/Core/Opt/Simplify/Utils.hs ===================================== @@ -1836,7 +1836,7 @@ rebuildLam env bndrs@(bndr:_) body cont | -- Note [Casts and lambdas] seCastSwizzle env , not (any bad bndrs) - = mkCastCo (mk_lams bndrs body) (mkPisCastCo Representational bndrs (exprType body) co) + = mkCast (mk_lams bndrs body) (mkPiCos Representational bndrs (castCoToCo (exprType body) co)) where co_vars = tyCoVarsOfCastCo co bad bndr = isCoVar bndr && bndr `elemVarSet` co_vars ===================================== compiler/GHC/Core/Ppr.hs ===================================== @@ -35,6 +35,7 @@ import GHC.Types.Fixity (LexicalFixity(..)) import GHC.Types.Literal( pprLiteral ) import GHC.Types.Name( pprInfixName, pprPrefixName ) import GHC.Types.Var +import GHC.Types.Var.Set import GHC.Types.Id import GHC.Types.Id.Info import GHC.Types.Demand @@ -171,10 +172,12 @@ noParens pp = pp pprOptCastCoercion :: CastCoercion -> SDoc pprOptCastCoercion (CCoercion co) = pprOptCo co -pprOptCastCoercion (ZCoercion ty cos) = -- TODO review ppr format - sdocOption sdocSuppressCoercions $ \case - True -> angleBrackets (text "ZapCo:" <> int (sum (map coercionSize cos))) <+> dcolon <+> co_type - False -> parens $ sep [text "Zap", ppr cos, dcolon <+> co_type] +pprOptCastCoercion (ZCoercion ty cos) = pprOptZappedCo ty cos + +pprOptZappedCo :: Type -> CoVarSet -> SDoc +pprOptZappedCo ty cos = sdocOption sdocSuppressCoercions $ \case + True -> angleBrackets (text "ZapCo:" <> int (sizeVarSet cos)) <+> dcolon <+> co_type + False -> parens $ sep [text "ZapCo", ppr cos, dcolon <+> co_type] where co_type = sdocOption sdocSuppressCoercionTypes $ \case True -> int (typeSize ty) <+> text "..." ===================================== compiler/GHC/Core/Rules.hs ===================================== @@ -1108,15 +1108,13 @@ match renv subst (Coercion co1) (Coercion co2) MRefl -- Note [Casts in the target] -- Note [Cancel reflexive casts] -match renv subst e1 (Cast e2 (CCoercion co2)) mco - = match renv subst e1 e2 (checkReflexiveMCo (mkTransMCoR co2 mco)) +match renv subst e1 (Cast e2 co2) mco + = match renv subst e1 e2 (checkReflexiveMCo (mkTransMCoR (castCoToCo (exprType e2) co2) mco)) -- checkReflexiveMCo: cancel casts if possible -- This is important: see Note [Cancel reflexive casts] -match renv subst (Cast e1 (CCoercion co1)) e2 mco - = matchTemplateCast renv subst e1 co1 e2 mco - --- TODO: rule matching for ZCoercion +match renv subst (Cast e1 co1) e2 mco + = matchTemplateCast renv subst e1 (castCoToCo (exprType e1) co1) e2 mco ------------------------ Literals --------------------- match _ subst (Lit lit1) (Lit lit2) mco ===================================== compiler/GHC/Core/SimpleOpt.hs ===================================== @@ -33,6 +33,7 @@ import GHC.Core.DataCon import GHC.Core.Coercion.Opt ( optCoercion, OptCoercionOpts (..) ) import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList , isInScope, substTyVarBndr, cloneTyVarBndr ) +import GHC.Core.TyCo.Subst import GHC.Core.Predicate( isCoVarType ) import GHC.Core.Coercion hiding ( substCo, substCoVarBndr ) @@ -324,7 +325,7 @@ simple_opt_expr env expr ---------------------- go_cast_co (CCoercion co) = CCoercion (go_co co) - go_cast_co (ZCoercion ty cos) = ZCoercion (substTyUnchecked subst ty) (substCos subst cos) + go_cast_co (ZCoercion ty cos) = ZCoercion (substTyUnchecked subst ty) (substCoVarSet subst cos) go_co co = optCoercion (so_co_opts (soe_opts env)) subst co @@ -439,14 +440,13 @@ simple_app env e as finish_app :: HasDebugCallStack => SimpleOptEnv -> OutExpr -> [SimpleClo] -> OutExpr -- See Note [Eliminate casts in function position] -finish_app env (Cast (Lam x e) (CCoercion co)) as@(_:_) +finish_app env (Cast (Lam x e) cco) as@(_:_) | not (isTyVar x) && not (isCoVar x) + , let co = castCoToCo (exprType (Lam x e)) cco , assert (not $ x `elemVarSet` tyCoVarsOfCo co) True , Just (x',e') <- pushCoercionIntoLambda (soeInScope env) x e co = simple_app (soeZapSubst env) (Lam x' e') as --- TODO: ZCoercion version of the finish_app - finish_app env fun args = foldl mk_app fun args where @@ -1297,13 +1297,11 @@ exprIsConApp_maybe ise@(ISE in_scope id_unf) expr go subst floats (Tick t expr) cont | not (tickishIsCode t) = go subst floats expr cont - go subst floats (Cast expr (CCoercion co1)) (CC args m_co2) - | Just (args', m_co1') <- pushCoArgs (subst_co subst co1) args + go subst floats (Cast expr co1) (CC args m_co2) + | Just (args', m_co1') <- pushCoArgs (subst_co subst (castCoToCo (exprType expr) co1)) args -- See Note [Push coercions in exprIsConApp_maybe] = go subst floats expr (CC args' (m_co1' `mkTransMCo` m_co2)) - -- TODO: ZCoercion in exprIsConApp_maybe - go subst floats (App fun arg) (CC args mco) | let arg_type = exprType arg , not (isTypeArg arg) && needsCaseBinding arg_type arg @@ -1590,19 +1588,18 @@ exprIsLambda_maybe ise (Tick t e) = Just (x, e, t:ts) -- Also possible: A casted lambda. Push the coercion inside -exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e (CCoercion co)) +exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e cco) | Just (x, e,ts) <- exprIsLambda_maybe ise casted_e -- Only do value lambdas. -- this implies that x is not in scope in gamma (makes this code simpler) , not (isTyVar x) && not (isCoVar x) + , let co = castCoToCo (exprType casted_e) cco , assert (not $ x `elemVarSet` tyCoVarsOfCo co) True , Just (x',e') <- pushCoercionIntoLambda in_scope_set x e co , let res = Just (x',e',ts) = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)]) res --- TODO: exprIsLambda_maybe for ZCoercion - -- Another attempt: See if we find a partial unfolding exprIsLambda_maybe ise@(ISE in_scope_set id_unf) e | (Var f, as, ts) <- collectArgsTicks tickishFloatable e ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -18,10 +18,10 @@ module GHC.Core.TyCo.FVs coVarsOfType, coVarsOfTypes, coVarsOfCo, coVarsOfCos, coVarsOfCastCo, - shallowCoVarsOfCos, + shallowCoVarsOfCo, shallowCoVarsOfCos, shallowCoVarsOfCastCo, tyCoVarsOfCastCoercionDSet, tyCoVarsOfCoDSet, - tyCoFVsOfCo, tyCoFVsOfCos, + tyCoFVsOfCo, tyCoFVsOfCos, tyCoFVsOfCoVarSet, tyCoVarsOfCoList, coVarsOfCoDSet, coVarsOfCosDSet, @@ -303,7 +303,7 @@ runTyCoVars f = appEndo f emptyVarSet tyCoVarsOfCastCo :: CastCoercion -> TyCoVarSet tyCoVarsOfCastCo (CCoercion co) = coVarsOfCo co -tyCoVarsOfCastCo (ZCoercion ty cos) = tyCoVarsOfType ty `unionVarSet` tyCoVarsOfCos cos -- TODO: more efficient? +tyCoVarsOfCastCo (ZCoercion ty cos) = tyCoVarsOfType ty `unionVarSet` cos tyCoVarsOfType :: Type -> TyCoVarSet -- The "deep" TyCoVars of the the type @@ -412,6 +412,16 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and sy shallowCoVarsOfCos :: [Coercion] -> CoVarSet shallowCoVarsOfCos cos = filterVarSet isCoVar $ shallowTyCoVarsOfCos cos +shallowCoVarsOfCo :: Coercion -> CoVarSet +shallowCoVarsOfCo co = filterVarSet isCoVar $ shallowTyCoVarsOfCo co + +shallowCoVarsOfType :: Type -> CoVarSet +shallowCoVarsOfType ty = filterVarSet isCoVar $ shallowTyCoVarsOfType ty + +shallowCoVarsOfCastCo :: CastCoercion -> CoVarSet +shallowCoVarsOfCastCo (CCoercion co) = shallowCoVarsOfCo co +shallowCoVarsOfCastCo (ZCoercion ty cos) = shallowCoVarsOfType ty `unionVarSet` cos + {- ********************************************************************* * * @@ -432,7 +442,7 @@ See #14880. coVarsOfCastCo :: CastCoercion -> CoVarSet coVarsOfCastCo (CCoercion co) = coVarsOfCo co -coVarsOfCastCo (ZCoercion ty cos) = coVarsOfType ty `unionVarSet` coVarsOfCos cos -- TODO: more efficient? +coVarsOfCastCo (ZCoercion ty cos) = coVarsOfType ty `unionVarSet` cos -- TODO cos doesn't include deep, this isn't enough? -- See Note [Finding free coercion variables] coVarsOfType :: Type -> CoVarSet @@ -666,7 +676,10 @@ tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co tyCoFVsOfCastCoercion :: CastCoercion -> FV tyCoFVsOfCastCoercion (CCoercion co) = tyCoFVsOfCo co -tyCoFVsOfCastCoercion (ZCoercion ty cos) = unionsFV (tyCoFVsOfType ty : map tyCoFVsOfCo cos) +tyCoFVsOfCastCoercion (ZCoercion ty cos) = tyCoFVsOfType ty `unionFV` tyCoFVsOfCoVarSet cos + +tyCoFVsOfCoVarSet :: CoVarSet -> FV +tyCoFVsOfCoVarSet = nonDetStrictFoldVarSet (unionFV . tyCoFVsOfCoVar) emptyFV -- TODO better way? Nondeterminism? tyCoFVsOfCo :: Coercion -> FV -- Extracts type and coercion variables from a coercion ===================================== compiler/GHC/Core/TyCo/Ppr.hs ===================================== @@ -48,6 +48,7 @@ import GHC.Types.Var import GHC.Iface.Type +import GHC.Types.Unique.Set import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -138,7 +139,7 @@ pprCastCo co = getPprStyle $ \ sty -> pprIfaceCastCoercion (tidyToIfaceCastCoSty tidyToIfaceCastCoSty :: CastCoercion -> PprStyle -> IfaceCastCoercion tidyToIfaceCastCoSty (CCoercion co) sty = IfaceCCoercion (tidyToIfaceCoSty co sty) -tidyToIfaceCastCoSty (ZCoercion ty cos) sty = IfaceZCoercion (tidyToIfaceType ty) (map (flip tidyToIfaceCoSty sty) cos) -- TODO +tidyToIfaceCastCoSty (ZCoercion ty cos) sty = IfaceZCoercion (tidyToIfaceType ty) (map (flip tidyToIfaceCoSty sty . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO tidyToIfaceCoSty :: Coercion -> PprStyle -> IfaceCoercion tidyToIfaceCoSty co sty ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -77,7 +77,7 @@ import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstr -- friends: import GHC.Types.Var -import GHC.Types.Var.Set( elemVarSet ) +import GHC.Types.Var.Set import GHC.Core.TyCon import GHC.Core.Coercion.Axiom @@ -847,16 +847,17 @@ Note [Zapped casts] ~~~~~~~~~~~~~~~~~~~ A "zapped cast" is a Cast that does not store the full Coercion being used to cast, but instead stores the type resulting from the cast and a set of CoVars -used in the original coercion. This reduces the effectiveness of Core Lint, -because it cannot check the original coercion. +used in the original coercion. The CastCoercion type is used to represent +the coercion argument to a cast; it may be either a full coercion (CCoercion) +or zapped (ZCoercion). Zapping casts is motivated by performance (see #8095 and related tickets). Sometimes the structure of the coercion can be very large, for example when using type families that take many reduction steps, and when Core Lint is not being used, the full structure of the coercion is not needed. We merely need the result type (to support exprType) and the set of coercion variables -(to avoid floating a coercion out of the scope in which it is valid). -TODO: reference another note about this. +(to avoid floating a coercion out of the scope in which it is valid, see +Note [The importance of tracking UnivCo dependencies]). Zapped casts are introduced in exactly one place: finish_rewrite in GHC.Tc.Solver.Solve. This uses a heuristic (isSmallCo) to determine whether @@ -870,15 +871,32 @@ which is much smaller than: This arises in practice with the Rep type family from GHC Generics. +We can convert a ZCoercion back into a normal Coercion using castCoToCo to +produce a UnivCo; such coercions can be identified for debugging with the +ZCoercionProv provenance. This is sometimes necessary in the optimizer, when a +Cast needs to be moved elsewhere. Since a UnivCo must store both the left and +right hand side types, it is less compact than a ZCoercion, so it is best to +avoid castCoToCo where possible. + The `-fzap-casts` and `-fno-zap-casts` flags can be used to enable or disable cast zapping, for comparative performance testing or to ensure casts are not -zapped when debugging the compiler. In addition, using `-dcore-lint` will -automatically imply `-fno-zap-casts`. +zapped when debugging the compiler. + +Zapping reduces the effectiveness of Core Lint, because it cannot check that +the original coercion was well-typed. Thus `-dcore-lint` will automatically +imply `-fno-zap-casts` for the same module. However, imported modules may still +include zapped casts. TODO: probably the boot libraries ought to be distributed with `-fno-zap-casts`, so users can get full checks from `-dcore-lint`. -TODO: for simplicity ZCoercion currently stores a list of Coercions, but in -principle we need only the CoVars. +ZCoercion discards the structure of the coercion, retaining only the set of variables +on which it depends. It is important we store only the "shallow" free CoVars in the +set, because those are the ones on which the original coercions necessarily depended +and which may be substituted away later. If we use the deep CoVars, we can end up +retaining references to CoVars that are no longer in scope. See also +Note [Shallow and deep free variables] in GHC.Core.TyCo.FVs. + +TODO: review determinism; are our uses of nonDetEltsUniqSet and similar safe? -} @@ -887,7 +905,7 @@ principle we need only the CoVars. -- and free CoVars. See Note [Zapped casts]. data CastCoercion = CCoercion CoercionR -- Not zapped; the Coercion has Representational role - | ZCoercion Type [Coercion] -- Zapped; the Coercions are just variables (TODO: use CoVarSet instead?) + | ZCoercion Type CoVarSet -- Zapped; stores only the RHS type and free CoVars deriving Data.Data -- | A 'Coercion' is concrete evidence of the equality/convertibility @@ -2069,7 +2087,7 @@ typesSize tys = foldr ((+) . typeSize) 0 tys castCoercionSize :: CastCoercion -> Int castCoercionSize (CCoercion co) = coercionSize co -castCoercionSize (ZCoercion ty cos) = typeSize ty + sum (map coercionSize cos) +castCoercionSize (ZCoercion ty cos) = typeSize ty + sizeVarSet cos coercionSize :: Coercion -> Int coercionSize (Refl ty) = typeSize ty ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -34,7 +34,7 @@ module GHC.Core.TyCo.Subst substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked, substTyWithUnchecked, substScaledTyUnchecked, substCoUnchecked, substCoWithUnchecked, - substCastCo, substCastCoUnchecked, + substCastCo, substCoVarSet, substTyWithInScope, substTys, substScaledTys, substTheta, lookupTyVar, @@ -846,12 +846,12 @@ lookupTyVar (Subst _ _ tenv _) tv lookupVarEnv tenv tv substCastCo :: HasDebugCallStack => Subst -> CastCoercion -> CastCoercion -substCastCo subst (CCoercion co) = CCoercion (substCo subst co) -substCastCo subst (ZCoercion ty cos) = ZCoercion (substTy subst ty) (map (substCo subst) cos) -- TODO: zap? +substCastCo subst (CCoercion co) = CCoercion (substCo subst co) +substCastCo subst (ZCoercion ty cos) = ZCoercion (substTy subst ty) (substCoVarSet subst cos) + +substCoVarSet :: HasDebugCallStack => Subst -> CoVarSet -> CoVarSet +substCoVarSet subst = nonDetStrictFoldVarSet (unionVarSet . shallowCoVarsOfCo . substCoVar subst) emptyVarSet -- TODO better impl; determinism? -substCastCoUnchecked :: Subst -> CastCoercion -> CastCoercion -substCastCoUnchecked subst (CCoercion co) = CCoercion (substCoUnchecked subst co) -substCastCoUnchecked subst (ZCoercion ty cos) = ZCoercion (substTyUnchecked subst ty) (map (substCoUnchecked subst) cos) -- TODO: zap? -- | Substitute within a 'Coercion' -- The substitution has to satisfy the invariants described in ===================================== compiler/GHC/Core/TyCo/Tidy.hs ===================================== @@ -26,6 +26,7 @@ import GHC.Core.TyCo.FVs import GHC.Types.Name hiding (varName) import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Utils.Misc (strictMap) import Data.List (mapAccumL) @@ -366,4 +367,4 @@ tidyCos env = strictMap (tidyCo env) tidyCastCo :: TidyEnv -> CastCoercion -> CastCoercion tidyCastCo env (CCoercion co) = CCoercion (tidyCo env co) -tidyCastCo env (ZCoercion ty cos) = ZCoercion (tidyType env ty) (tidyCos env cos) +tidyCastCo env (ZCoercion ty cos) = ZCoercion (tidyType env ty) (mapVarSet (tidyTyCoVarOcc env) cos) ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -77,6 +77,7 @@ import GHC.Core.Type as Type import GHC.Core.Predicate( isCoVarType ) import GHC.Core.FamInstEnv import GHC.Core.TyCo.Compare( eqType, eqTypeX ) +import GHC.Core.TyCo.FVs import GHC.Core.Coercion import GHC.Core.Reduction import GHC.Core.TyCon @@ -297,13 +298,13 @@ mkCast expr co -- | Wrap the given expression in a zapped cast (see Note [Zapped casts] in -- GHC.Core.TyCo.Rep). -mkCastZ :: HasDebugCallStack => CoreExpr -> Type -> [Coercion] -> CoreExpr +mkCastZ :: HasDebugCallStack => CoreExpr -> Type -> CoVarSet -> CoreExpr mkCastZ expr ty cos = case expr of - Cast expr co -> mkCastZ expr ty (zapCastCo co ++ cos) + Cast expr co -> mkCastZ expr ty (shallowCoVarsOfCastCo co `unionVarSet` cos) Tick t expr -> Tick t (mkCastZ expr ty cos) - -- TODO: do we need other cases from mkCast? - _ -> Cast expr (ZCoercion ty (zapCos cos)) + Coercion e_co | isCoVarType ty -> Coercion (mkCoCastCo e_co (ZCoercion ty cos)) + _ -> Cast expr (ZCoercion ty cos) ===================================== compiler/GHC/CoreToIface.hs ===================================== @@ -85,6 +85,7 @@ import GHC.Types.Tickish import GHC.Types.Demand ( isNopSig ) import GHC.Types.Cpr ( topCprSig ) import GHC.Types.SrcLoc (unLoc) +import GHC.Types.Unique.Set import GHC.Utils.Outputable import GHC.Utils.Panic @@ -275,7 +276,7 @@ toIfaceTyLit (CharTyLit x) = IfaceCharTyLit x ---------------- toIfaceCastCoercion :: CastCoercion -> IfaceCastCoercion toIfaceCastCoercion (CCoercion co) = IfaceCCoercion (toIfaceCoercion co) -toIfaceCastCoercion (ZCoercion ty cos) = IfaceZCoercion (toIfaceType ty) (map toIfaceCoercion cos) +toIfaceCastCoercion (ZCoercion ty cos) = IfaceZCoercion (toIfaceType ty) (map (toIfaceCoercion . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO determinism toIfaceCoercion :: Coercion -> IfaceCoercion toIfaceCoercion = toIfaceCoercionX emptyVarSet ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -63,6 +63,7 @@ import GHC.Core.Type import GHC.Core.Coercion import GHC.Core.Coercion.Axiom import GHC.Core.FVs +import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Rep -- needs to build types & coercions in a knot import GHC.Core.TyCo.Subst ( substTyCoVars ) import GHC.Core.InstEnv @@ -1566,7 +1567,7 @@ tcIfaceTyLit (IfaceCharTyLit n) = return (CharTyLit n) tcIfaceCastCoercion :: IfaceCastCoercion -> IfL CastCoercion tcIfaceCastCoercion (IfaceCCoercion co) = CCoercion <$> tcIfaceCo co -tcIfaceCastCoercion (IfaceZCoercion ty cos) = ZCoercion <$> tcIfaceType ty <*> mapM tcIfaceCo cos +tcIfaceCastCoercion (IfaceZCoercion ty cos) = ZCoercion <$> tcIfaceType ty <*> (shallowCoVarsOfCos <$> mapM tcIfaceCo cos) tcIfaceCo :: IfaceCoercion -> IfL Coercion tcIfaceCo = go ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -36,6 +36,7 @@ import GHC.Core.Predicate import GHC.Core.Reduction import GHC.Core.Coercion import GHC.Core.Class( classHasSCs ) +import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Rep (Coercion(..)) import GHC.Types.Id( idType ) @@ -1494,7 +1495,7 @@ finish_rewrite mkCastCoercion :: Bool -> Type -> Coercion -> CastCoercion mkCastCoercion zap_casts lhs_ty co | isSmallCo co || not zap_casts = CCoercion co - | otherwise = ZCoercion lhs_ty (zapCo co) + | otherwise = ZCoercion lhs_ty (shallowCoVarsOfCo co) -- | Is this coercion probably smaller than its type? This is a rough heuristic, -- but crucially we treat axioms (perhaps wrapped in Sym/Sub/etc.) as small ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -64,6 +64,7 @@ import GHC.Tc.Zonk.TcType import GHC.Core.Type import GHC.Core.Coercion import GHC.Core.TyCon +import GHC.Core.TyCo.FVs import GHC.Utils.Outputable import GHC.Utils.Misc @@ -78,11 +79,13 @@ import GHC.Types.Name import GHC.Types.Name.Env import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Types.Id import GHC.Types.TypeEnv import GHC.Types.Basic import GHC.Types.SrcLoc import GHC.Types.Unique.FM +import GHC.Types.Unique.Set import GHC.Types.TyThing import GHC.Tc.Types.BasicTypes @@ -532,15 +535,18 @@ zonkScaledTcTypeToTypeX (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX m zonkTcTypeToTypeX :: TcType -> ZonkTcM Type zonkTcTypesToTypesX :: [TcType] -> ZonkTcM [Type] zonkCoToCo :: Coercion -> ZonkTcM Coercion -zonkCosToCos :: [Coercion] -> ZonkTcM [Coercion] -(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo, zonkCosToCos) +_zonkCosToCos :: [Coercion] -> ZonkTcM [Coercion] +(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo, _zonkCosToCos) = case mapTyCoX zonk_tycomapper of (zty, ztys, zco, zcos) -> (ZonkT . flip zty, ZonkT . flip ztys, ZonkT . flip zco, ZonkT. flip zcos) zonkCastCo :: CastCoercion -> ZonkTcM CastCoercion zonkCastCo (CCoercion co) = CCoercion <$> zonkCoToCo co -zonkCastCo (ZCoercion ty cos) = ZCoercion <$> zonkTcTypeToTypeX ty <*> zonkCosToCos cos +zonkCastCo (ZCoercion ty cos) = ZCoercion <$> zonkTcTypeToTypeX ty <*> zonkCoVarSet cos + +zonkCoVarSet :: CoVarSet -> ZonkTcM CoVarSet +zonkCoVarSet = fmap shallowCoVarsOfCos . mapM zonkCoVarOcc . nonDetEltsUniqSet zonkScaledTcTypesToTypesX :: [Scaled TcType] -> ZonkTcM [Scaled Type] zonkScaledTcTypesToTypesX scaled_tys = ===================================== docs/users_guide/debugging.rst ===================================== @@ -1223,14 +1223,16 @@ Other :type: dynamic :since: TODO + :default: enabled Reduce the size of Core terms by discarding coercion proofs that are needed only for debugging the compiler. This usually helps improve compile-time performance for some programs that make heavy use of type families. - When this flag is enabled, Core Lint will be less effective at verifying the - correctness of Core programs involving casts. Hence this is automatically - switched off by :ghc-flag:`-dcore-lint`. + This is enabled by default. When it is enabled, Core Lint will be less + effective at verifying the correctness of Core programs involving casts. + Hence it is automatically switched off by :ghc-flag:`-dcore-lint`, or you + can disable it using ``-fno-zap-casts``. .. ghc-flag:: -dno-typeable-binds :shortdesc: Don't generate bindings for Typeable methods View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/adef6e9ba1968b1ab4d7dc1e46f57ce... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/adef6e9ba1968b1ab4d7dc1e46f57ce... You're receiving this email because of your account on gitlab.haskell.org.