Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC Commits: 29d1d7b2 by Adam Gundry at 2026-06-12T15:36:55+01:00 Minor fixes - - - - - 9 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Opt/Simplify/Iteration.hs - compiler/GHC/Core/Rules.hs - compiler/GHC/Core/SimpleOpt.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -63,6 +63,10 @@ module GHC.Core.Coercion ( applyForAllTy, decomposeFunCastCo, + mkSymTypedCastCo, + mkTransTypedCastCo, + typedCastCoercionKind, + -- ** Decomposition instNewTyCon_maybe, @@ -97,7 +101,8 @@ module GHC.Core.Coercion ( -- ** Free variables tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo, tyCoVarsOfCastCo, - coercionSize, castCoercionSize, anyFreeVarsOfCo, + coercionSize, castCoercionSize, + anyFreeVarsOfCo, anyFreeVarsOfCastCo, -- ** Substitution CvSubstEnv, emptyCvSubstEnv, @@ -123,7 +128,7 @@ module GHC.Core.Coercion ( eqCoercion, eqCoercionX, eqCastCoercion, eqCastCoercionX, -- ** Forcing evaluation of coercions - seqCo, seqCos, seqCastCoercion, + seqCo, seqCos, seqCastCoercion, seqTypedCastCoercion, -- * Pretty-printing pprCo, pprParendCo, @@ -852,15 +857,16 @@ mkFunCoNoFTF r w arg_co res_co Pair argl_ty argr_ty = coercionKind arg_co Pair resl_ty resr_ty = coercionKind res_co --- AMG TODO: more cases here, or maybe better to have a FunCo constructor of CastCoercion? -mkFunCastCoNoFTF :: HasDebugCallStack => Role -> Mult -> Type -> CastCoercion -> Type -> CastCoercion -> CastCoercion -mkFunCastCoNoFTF _ mult _ (ZCoercion arg_ty arg_cos) _ (ZCoercion res_ty res_cos) = ZCoercion (mkFunctionType mult arg_ty res_ty) (arg_cos `unionDVarSet` res_cos) -mkFunCastCoNoFTF _ mult _ (ZCoercion arg_ty arg_cos) res_ty res_co = ZCoercion (mkFunctionType mult arg_ty (castCoercionRKind res_ty res_co)) (arg_cos `unionDVarSet` coVarsOfCastCoDSet res_co) -mkFunCastCoNoFTF _ mult arg_ty arg_co _ (ZCoercion res_ty res_cos) = ZCoercion (mkFunctionType mult (castCoercionRKind arg_ty arg_co) res_ty) (res_cos `unionDVarSet` coVarsOfCastCoDSet arg_co) -mkFunCastCoNoFTF r mult _ (CCoercion arg_co) _ (CCoercion res_co) = CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co res_co) -mkFunCastCoNoFTF _ _ _ ReflCastCo _ ReflCastCo = ReflCastCo -mkFunCastCoNoFTF r mult _ (CCoercion arg_co) res_ty ReflCastCo = CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co (mkReflCo r res_ty)) -mkFunCastCoNoFTF r mult arg_ty ReflCastCo _ (CCoercion res_co) = CCoercion (mkFunCoNoFTF r (multToCo mult) (mkReflCo r arg_ty) res_co) +-- AMG TODO: maybe better to have a FunCo constructor of CastCoercion? +mkFunCastCoNoFTF :: HasDebugCallStack => Role -> Mult -> TypedCastCoercion -> TypedCastCoercion -> CastCoercion +mkFunCastCoNoFTF r mult (TCC arg_ty0 arg_co) (TCC res_ty0 res_co) = + case (arg_co, res_co) of + (ReflCastCo, ReflCastCo) -> ReflCastCo + (ZCoercion arg_ty1 arg_cos, _) -> ZCoercion (mkFunctionType mult arg_ty1 (castCoercionRKind res_ty0 res_co)) (arg_cos `unionDVarSet` coVarsOfCastCoDSet res_co) + (_, ZCoercion res_ty1 res_cos) -> ZCoercion (mkFunctionType mult (castCoercionRKind arg_ty0 arg_co) res_ty1) (res_cos `unionDVarSet` coVarsOfCastCoDSet arg_co) + (CCoercion arg_co, CCoercion res_co) -> CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co res_co) + (CCoercion arg_co, ReflCastCo) -> CCoercion (mkFunCoNoFTF r (multToCo mult) arg_co (mkReflCo r res_ty0)) + (ReflCastCo, CCoercion res_co) -> CCoercion (mkFunCoNoFTF r (multToCo mult) (mkReflCo r arg_ty0) res_co) -- | Build a function 'Coercion' from two other 'Coercion's. That is, @@ -990,8 +996,8 @@ mkForAllCo v visL visR kind_co co = mk_forall_co v visL visR kind_co co mkForAllCastCo :: HasDebugCallStack => Role -> TyCoVar -> ForAllTyFlag -> ForAllTyFlag - -> Type -> CastCoercion -> CastCoercion -mkForAllCastCo r v visL visR ty cco = case cco of + -> TypedCastCoercion -> CastCoercion +mkForAllCastCo r v visL visR (TCC ty cco) = case cco of CCoercion co -> CCoercion (mkForAllCo v visL visR MRefl co) ZCoercion ty cos -> ZCoercion (mkTyCoForAllTy v visR ty) cos ReflCastCo | visL `eqForAllVis` visR -> ReflCastCo @@ -1224,6 +1230,9 @@ mkSymCastCo _ (CCoercion co) = CCoercion (mkSymCo co) mkSymCastCo ty (ZCoercion _ cos) = ZCoercion ty cos mkSymCastCo _ ReflCastCo = ReflCastCo +mkSymTypedCastCo :: TypedCastCoercion -> TypedCastCoercion +mkSymTypedCastCo (TCC ty co) = TCC (castCoercionRKind ty co) (mkSymCastCo ty co) + -- | mkTransCo creates a new 'Coercion' by composing the two -- given 'Coercion's transitively: (co1 ; co2) mkTransCo :: HasDebugCallStack => Coercion -> Coercion -> Coercion @@ -2529,6 +2538,9 @@ seqCastCoercion (CCoercion co) = seqCo co seqCastCoercion (ZCoercion ty cos) = seqType ty `seq` seqDVarSet cos seqCastCoercion ReflCastCo = () +seqTypedCastCoercion :: TypedCastCoercion -> () +seqTypedCastCoercion (TCC ty co) = seqType ty `seq` seqCastCoercion co + seqCo :: Coercion -> () seqCo (Refl ty) = seqType ty seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco @@ -3022,3 +3034,10 @@ coToCastCo :: Coercion -> CastCoercion -- See #19815 for a bit of data and discussion on this point coToCastCo co | isReflCo co = ReflCastCo | otherwise = CCoercion co + + +typedCastCoercionKind :: TypedCastCoercion -> Pair Type +typedCastCoercionKind (TCC tyL co) = Pair (castCoercionLKind tyL co) (castCoercionRKind tyL co) + +mkTransTypedCastCo :: TypedCastCoercion -> TypedCastCoercion -> TypedCastCoercion +mkTransTypedCastCo (TCC ty1 co1) (TCC _ co2) = TCC ty1 (mkTransCastCo co1 co2) ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -4,7 +4,7 @@ module GHC.Core.Coercion.Opt ( optCoercion, optTransCo - , optCastCoercion + , optCastCoercion, optTransCastCo , OptCoercionOpts (..) ) where @@ -178,6 +178,18 @@ optTransCo opts in_scope co1 co2 | otherwise = co1 `mkTransCo` co2 +optTransCastCo :: HasDebugCallStack => OptCoercionOpts -> InScopeSet + -> TypedCastCoercion -> TypedCastCoercion -> TypedCastCoercion +optTransCastCo opts in_scope co1 co2 + | optCoercionEnabled opts + = case (co1, co2) of + (TCC ty (CCoercion co1'), TCC _ (CCoercion co2')) -> TCC ty (CCoercion (opt_trans in_scope co1' co2')) + (co1, TCC _ ReflCastCo) -> co1 + (TCC _ ReflCastCo, co2) -> co2 + _ -> co1 `mkTransTypedCastCo` co2 + | otherwise + = co1 `mkTransTypedCastCo` co2 + -- AMG TODO: not clear if coercionLKind or substTy is better choice here optCastCoercion :: OptCoercionOpts -> Subst -> TypedCastCoercion -> TypedCastCoercion optCastCoercion _ env (TCC tyL ReflCastCo) = TCC (substTy env tyL) ReflCastCo ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -2702,7 +2702,6 @@ tryEtaReduce rec_ids bndrs body eval_sd where incoming_arity = count isId bndrs -- See Note [Eta reduction makes sense], point (2) - -- AMG TOOD: make this pass TypedCastCoercion so we can call ok_arg more easily? go :: [Var] -- Binders, innermost first, types [a3,a2,a1] -> CoreExpr -- Of type tr -> CastCoercion -- Of type tr ~ ts @@ -2723,7 +2722,7 @@ tryEtaReduce rec_ids bndrs body eval_sd -- Float app ticks: \x -> Tick t (e x) ==> Tick t e go (b : bs) (App fun arg) co - | Just (co', ticks) <- ok_arg b arg co (exprType fun) (exprType (App fun arg)) + | Just (co', ticks) <- ok_arg b arg (TCC (exprType (App fun arg)) co) (exprType fun) = fmap (flip (foldr mkTick) ticks) $ go bs fun co' -- Float arg ticks: \x -> e (Tick t x) ==> Tick t e @@ -2795,19 +2794,18 @@ tryEtaReduce rec_ids bndrs body eval_sd --------------- ok_arg :: Var -- Of type bndr_t -> CoreExpr -- Of type arg_t - -> CastCoercion -- Of kind (t1~t2) + -> TypedCastCoercion-- Of kind (t1~t2) -> Type -- Type (arg_t -> t1) of the function -- to which the argument is supplied - -> Type -- Type t1 of the result (AMG TODO: use TypedCastCoercion or avoid needing to pass this?) -> Maybe (CastCoercion -- 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) co fun_ty res_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 (fco, []) - where !fco = mkForAllCastCo Representational tv vis coreTyLamForAllTyFlag res_ty co + where !fco = mkForAllCastCo Representational tv vis coreTyLamForAllTyFlag co -- The lambda we are eta-reducing always has visibility -- 'coreTyLamForAllTyFlag' which may or may not match -- the visibility on the inner function (#24014) @@ -2815,24 +2813,25 @@ 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) co fun_ty _ + ok_arg bndr (Var v) (TCC _ 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 (mkFunResCastCo Representational bndr co, []) - ok_arg bndr (Cast e co_arg) co fun_ty _ + ok_arg bndr (Cast e co_arg) co fun_ty | (ticks, Var v) <- stripTicksTop tickishFloatable e - , Just (_, fun_mult, _, res_ty) <- splitFunTy_maybe fun_ty + , Just (_, fun_mult, _, _) <- splitFunTy_maybe fun_ty , bndr == v , fun_mult `eqType` idMult bndr - = Just (mkFunCastCoNoFTF Representational fun_mult (castCoercionRKind (exprType e) co_arg) (mkSymCastCo (exprType e) co_arg) res_ty co, ticks) + , let co_arg' = TCC (exprType e) co_arg + = Just (mkFunCastCoNoFTF Representational fun_mult (mkSymTypedCastCo 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 res_ty - | tickishFloatable t, Just (co', ticks) <- ok_arg bndr arg co fun_ty res_ty + 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) - ok_arg _ _ _ _ _ = Nothing + ok_arg _ _ _ _ = Nothing {- ********************************************************************* @@ -3003,18 +3002,17 @@ pushCoValArg co old_arg_ty = funArgTy tyR pushCoercionIntoLambda - :: HasDebugCallStack => InScopeSet -> Var -> CoreExpr -> Type -> CastCoercion -> Maybe (Var, CoreExpr) + :: HasDebugCallStack => InScopeSet -> Var -> CoreExpr -> TypedCastCoercion -> Maybe (Var, CoreExpr) -- This implements the Push rule from the paper on coercions -- (\x. e) |> co -- ===> -- (\x'. e |> co') -pushCoercionIntoLambda in_scope x e ty co +pushCoercionIntoLambda in_scope x e co | assert (not (isTyVar x) && not (isCoVar x)) True - , let s1s2 = castCoercionLKind ty co - , let t1t2 = castCoercionRKind ty co + , Pair s1s2 t1t2 <- typedCastCoercionKind co , Just (_, _, s1, _) <- splitFunTy_maybe s1s2 , Just (_, w1, t1,_t2) <- splitFunTy_maybe t1t2 - , (co1, co2) <- decomposeFunCastCo co + , (co1, co2) <- decomposeFunCastCo (tccCastCoercion co) , typeHasFixedRuntimeRep t1 -- We can't push the coercion into the lambda if it would create -- a representation-polymorphic binder. ===================================== compiler/GHC/Core/Opt/Simplify/Iteration.hs ===================================== @@ -1412,6 +1412,19 @@ simplCoercion env co opts = seOptCoercionOpts env subst_only = isEmptyTvSubst subst || reSimplifying env +simplCastCoercion :: SimplEnv -> InTypedCastCoercion -> SimplM OutTypedCastCoercion +simplCastCoercion env co + = seqTypedCastCoercion opt_co `seq` return opt_co + where + -- See Note [Optimising coercions] + -- NB: substCo has a short-cut when both type and coercion substs are empty + opt_co | subst_only = substTypedCastCo subst co + | otherwise = optCastCoercion opts subst co + + subst = getTCvSubst env + opts = seOptCoercionOpts env + subst_only = isEmptyTvSubst subst || reSimplifying env + {- Note [Optimising coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Some programs have very big coercions and we'd like to avoid repeatedly @@ -1440,19 +1453,6 @@ re-optimising them: -} -simplCastCoercion :: SimplEnv -> InTypedCastCoercion -> SimplM OutTypedCastCoercion -simplCastCoercion env co - = do { let opt_co | reSimplifying env = substTypedCastCo subst co - | otherwise = optCastCoercion opts subst co - -- If (reSimplifying env) is True we have already simplified - -- this coercion once, and we don't want do so again; doing - -- so repeatedly risks non-linear behaviour - -- See Note [Inline depth] in GHC.Core.Opt.Simplify.Env - ; seqCastCoercion (tccCastCoercion opt_co) `seq` return opt_co } - where - subst = getTCvSubst env - opts = seOptCoercionOpts env - ----------------------------------- -- | Push a TickIt context outwards past applications and cases, as @@ -1861,7 +1861,7 @@ simplArg :: SimplEnvIS -- ^ Used only for its InScopeSet -- continuation passed to 'simplExprC' -> OutType -- ^ Type of the function applied to this arg -> StaticEnv -> CoreExpr -- ^ Expression with its static envt - -> OutCastCoercion -- Wrap this around the result + -> OutCastCoercion -- ^ Wrap this around the result -> SimplM OutExpr simplArg _ _ _ (Simplified {}) arg co = return $ mkCastCo arg co -- See Note [Avoid repeated simplification] ===================================== compiler/GHC/Core/Rules.hs ===================================== @@ -57,7 +57,6 @@ import GHC.Core.Unify as Unify ( ruleMatchTyKiX ) import GHC.Core.Type as Type ( Type, extendTvSubst, extendCvSubst , substTy, getTyVar_maybe ) -import GHC.Core.TyCo.FVs ( anyFreeVarsOfCastCo ) import GHC.Core.TyCo.Ppr( pprParendType ) import GHC.Core.Coercion as Coercion import GHC.Core.Tidy ( tidyRules ) ===================================== compiler/GHC/Core/SimpleOpt.hs ===================================== @@ -29,7 +29,7 @@ import GHC.Core.Unfold.Make import GHC.Core.Make import GHC.Core.Opt.OccurAnal( occurAnalyseExpr, occurAnalysePgm, zapLambdaBndrs ) import GHC.Core.DataCon -import GHC.Core.Coercion.Opt ( optCoercion, optCastCoercion, OptCoercionOpts (..) ) +import GHC.Core.Coercion.Opt ( optCoercion, optCastCoercion, OptCoercionOpts (..), optTransCastCo ) import GHC.Core.Type hiding ( substTy, extendTvSubst, extendCvSubst, extendTvSubstList , isInScope, substTyVarBndr, cloneTyVarBndr ) import GHC.Core.Predicate( isCoVarType ) @@ -303,11 +303,11 @@ simpleOptPgm opts this_mod binds rules = ---------------------- type SimpleClo = (SimpleOptEnv, InExpr) -data SimpleContItem = ApplyToArg SimpleClo | CastIt OutType OutCastCoercion +data SimpleContItem = ApplyToArg SimpleClo | CastIt OutTypedCastCoercion instance Outputable SimpleContItem where ppr (ApplyToArg (_, arg)) = text "ARG" <+> ppr arg - ppr (CastIt _ co) = text "CAST" <+> ppr co + ppr (CastIt co) = text "CAST" <+> ppr co data SimpleOptEnv = SOE { soe_opts :: {-# UNPACK #-} !SimpleOpts @@ -473,7 +473,7 @@ simple_app env e0@(Lam {}) as0@(_:_) where (env', b') = subst_opt_bndr env b -- See Note [Eliminate casts in function position] - do_beta env e@(Lam b _) as@(CastIt ty out_co:rest) + do_beta env e@(Lam b _) as@(CastIt out_co:rest) | isNonCoVarId b -- Optimise the inner lambda to make it an 'OutExpr', which makes it -- possible to call 'pushCoercionIntoLambda' with the 'OutCoercion' 'co'. @@ -482,7 +482,7 @@ simple_app env e0@(Lam {}) as0@(_:_) -- we need to do this to avoid mixing 'InExpr' and 'OutExpr', or two -- 'InExpr' with different environments (getting this wrong caused #26588 & #26589.) , Lam out_b out_body <- simple_app env e [] - , Just (b', body') <- pushCoercionIntoLambda (soeInScope env) out_b out_body ty out_co + , Just (b', body') <- pushCoercionIntoLambda (soeInScope env) out_b out_body out_co = do_beta (soeZapSubst env) (Lam b' body') rest -- soeZapSubst: we've already optimised everything (the lambda and 'rest') by now. | otherwise @@ -542,19 +542,18 @@ simple_app env (Cast e co) as simple_app env e as = rebuild_app env (simple_opt_expr env e) as --- FIXME (cast-zapping rebase): HEAD added optTransCo to further optimise the --- combined coercion when stacking. There is no optTransCastCo yet, so for now --- we use mkTransCastCo and leave the deeper optimisation as a TODO. add_cast :: SimpleOptEnv -> InTypedCastCoercion -> [SimpleContItem] -> [SimpleContItem] -add_cast env (TCC tyL co1) as - | isReflCastCo co1' +add_cast env co1 as + | isReflCastCo (tccCastCoercion co1) = as | otherwise = case as of - CastIt _ co2:rest -> CastIt ty (co1' `mkTransCastCo` co2):rest - _ -> CastIt ty co1':as + CastIt co2:rest -> CastIt (optTransCastCo opts in_scope opt_co1 co2):rest + _ -> CastIt opt_co1:as where - TCC ty co1' = optCastCoercion (so_co_opts (soe_opts env)) (soe_subst env) (TCC tyL co1) + opts = so_co_opts (soe_opts env) + in_scope = soeInScope env + opt_co1 = optCastCoercion opts (soe_subst env) co1 rebuild_app :: HasDebugCallStack => SimpleOptEnv -> OutExpr -> [SimpleContItem] -> OutExpr @@ -563,19 +562,19 @@ rebuild_app env fun args = foldl mk_app fun args in_scope = soeInScope env mk_app out_fun = \case ApplyToArg arg -> App out_fun (simple_opt_clo in_scope arg) - CastIt _ co -> mk_cast out_fun co + CastIt co -> mk_cast out_fun co -mk_cast :: CoreExpr -> CastCoercion -> CoreExpr +mk_cast :: CoreExpr -> TypedCastCoercion -> CoreExpr -- Like GHC.Core.Utils.mkCast, but does a full reflexivity check. -- mkCast doesn't do that because the Simplifier does (in simplCast) -- But in SimpleOpt it's nice to kill those nested casts (#18112) -mk_cast (Cast e co1) co2 = mk_cast e (co1 `mkTransCastCo` co2) -mk_cast (Tick t e) co = Tick t (mk_cast e co) +mk_cast (Cast e co1) (TCC _ co2) = mk_cast e (TCC (exprType e) (co1 `mkTransCastCo` co2)) +mk_cast (Tick t e) co = Tick t (mk_cast e co) mk_cast e co - | isReflexiveCastCo (TCC (exprType e) co) + | isReflexiveCastCo co = e | otherwise - = Cast e co + = Cast e (tccCastCoercion co) {- Note [Desugaring unlifted newtypes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1853,7 +1852,7 @@ exprIsLambda_maybe ise@(ISE in_scope_set _) (Cast casted_e co) -- this implies that x is not in scope in gamma (makes this code simpler) , not (isTyVar x) && not (isCoVar x) , assert (not $ x `elemVarSet` tyCoVarsOfCastCo co) True - , Just (x',e') <- pushCoercionIntoLambda in_scope_set x e (exprType casted_e) co + , Just (x',e') <- pushCoercionIntoLambda in_scope_set x e (TCC (exprType casted_e) co) , let res = Just (x',e',ts) = --pprTrace "exprIsLambda_maybe:Cast" (vcat [ppr casted_e,ppr co,ppr res)]) res ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -205,11 +205,6 @@ in GHC.Tc.Solver. Yuk. This is not pretty. * * ********************************************************************* -} -tyCoVarsOfCastCo :: CastCoercion -> TyCoVarSet -tyCoVarsOfCastCo (CCoercion co) = coVarsOfCo co -tyCoVarsOfCastCo (ZCoercion ty cos) = tyCoVarsOfType ty `unionVarSet` dVarSetToVarSet cos -tyCoVarsOfCastCo ReflCastCo = emptyVarSet - tyCoVarsOfType :: Type -> TyCoVarSet -- The "deep" TyCoVars of the the type tyCoVarsOfType ty = runTyCoVars (deepTypeFV ty) @@ -227,6 +222,9 @@ tyCoVarsOfCo :: Coercion -> TyCoVarSet -- See Note [Computing deep free variables] tyCoVarsOfCo co = runTyCoVars (deepCoFV co) +tyCoVarsOfCastCo :: CastCoercion -> TyCoVarSet +tyCoVarsOfCastCo co = runTyCoVars (deepCastCoFV co) + tyCoVarsOfMCo :: MCoercion -> TyCoVarSet tyCoVarsOfMCo MRefl = emptyVarSet tyCoVarsOfMCo (MCo co) = tyCoVarsOfCo co @@ -264,7 +262,8 @@ deepTypeFV :: Type -> TyCoFV deepTypesFV :: [Type] -> TyCoFV deepCoFV :: Coercion -> TyCoFV deepCosFV :: [Coercion] -> TyCoFV -(deepTypeFV, deepTypesFV, deepCoFV, deepCosFV, _) = foldTyCo deepTcvFolder +deepCastCoFV :: CastCoercion -> TyCoFV +(deepTypeFV, deepTypesFV, deepCoFV, deepCosFV, deepCastCoFV) = foldTyCo deepTcvFolder deepTcvFolder :: TyCoFolder TyCoFV -- It's important that we use a one-shot EndoOS, to ensure that all @@ -908,10 +907,8 @@ anyFreeVarsOfCo check_fv co = DM.getAny (runFVTop (f co)) where (_, _, f, _, _) = foldTyCo (afvFolder check_fv) anyFreeVarsOfCastCo :: (TyCoVar -> Bool) -> CastCoercion -> Bool -anyFreeVarsOfCastCo check_fv (CCoercion co) = anyFreeVarsOfCo check_fv co -anyFreeVarsOfCastCo check_fv (ZCoercion ty cvs) = - anyFreeVarsOfType check_fv ty || anyDVarSet check_fv cvs -anyFreeVarsOfCastCo _ ReflCastCo = False +anyFreeVarsOfCastCo check_fv co = DM.getAny (runFVTop (f co)) + where (_, _, _, _, f) = foldTyCo (afvFolder check_fv) noFreeVarsOfType :: Type -> Bool noFreeVarsOfType ty = not $ DM.getAny (runFVTop (f ty)) ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1058,6 +1058,9 @@ instance Outputable Coercion where instance Outputable CastCoercion where ppr = pprCastCo +instance Outputable TypedCastCoercion where + ppr (TCC ty co) = text "TCC" <> parens (ppr ty <> text "," <+> ppr co) + instance Outputable CoSel where ppr (SelTyCon n r) = text "Tc" <> parens (int n <> comma <> pprOneCharRole r) ppr SelForAll = text "All" ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -636,7 +636,7 @@ optSubTypeHsWrapper wrap not_in v (WpCompose w1 w2) = not_in v w1 && not_in v w2 not_in v (WpEvApp (EvExpr e)) = not (v `elemVarSet` exprFreeVars e) not_in v (WpEvApp (EvCastExpr e co ty)) = not (v `elemVarSet` exprFreeVars e) - && not_in_cast_co v co + && not (anyFreeVarsOfCastCo (== v) co) && not (anyFreeVarsOfType (== v) ty) not_in _ (WpEvApp (EvTypeable {})) = False -- Giving up; conservative not_in _ (WpEvApp (EvFun {})) = False -- Giving up; conservative @@ -644,13 +644,6 @@ optSubTypeHsWrapper wrap not_in _ (WpEvLam {}) = False -- Ditto not_in _ (WpLet {}) = False -- Ditto - not_in_cast_co :: TyVar -> CastCoercion -> Bool - not_in_cast_co v = \case - CCoercion co -> not (anyFreeVarsOfCo (== v) co) - ZCoercion ty cvs -> not (anyFreeVarsOfType (== v) ty) - && not (v `elemDVarSet` cvs) - ReflCastCo -> True - not_in_submult :: TyVar -> SubMultCo -> Bool not_in_submult v = \case EqMultCo co -> not (anyFreeVarsOfCo (== v) co) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29d1d7b24d49795cb561066c4954255f... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/29d1d7b24d49795cb561066c4954255f... You're receiving this email because of your account on gitlab.haskell.org.