Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC Commits: 85e0e01f by Adam Gundry at 2025-12-02T21:57:22+00:00 WIP: use CCoercion for CastTy - - - - - 29 changed files: - compiler/GHC/Core/Coercion.hs - compiler/GHC/Core/Coercion.hs-boot - compiler/GHC/Core/Coercion/Opt.hs - compiler/GHC/Core/FamInstEnv.hs - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Opt/Arity.hs - compiler/GHC/Core/Reduction.hs - compiler/GHC/Core/TyCo/FVs.hs - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/TyCo/Tidy.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Type.hs-boot - compiler/GHC/Core/Unify.hs - compiler/GHC/CoreToIface.hs - compiler/GHC/HsToCore.hs - compiler/GHC/Iface/Rename.hs - compiler/GHC/Iface/Syntax.hs - compiler/GHC/Iface/Type.hs - compiler/GHC/IfaceToCore.hs - compiler/GHC/Tc/Gen/App.hs - compiler/GHC/Tc/Gen/Bind.hs - compiler/GHC/Tc/Gen/HsType.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Rewrite.hs - compiler/GHC/Tc/TyCl/Utils.hs - compiler/GHC/Tc/Utils/Instantiate.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/Unify.hs Changes: ===================================== compiler/GHC/Core/Coercion.hs ===================================== @@ -64,6 +64,8 @@ module GHC.Core.Coercion ( mkForAllCastCo, mkFunResCastCo, mkFunCastCoNoFTF, + mkGReflLeftCastCo, + mkGReflRightCastCo, applyForAllTy, decomposeFunCastCo, @@ -397,7 +399,7 @@ mkSymMCo (MCo co) = MCo (mkSymCo co) -- | Cast a type by an 'MCoercion' mkCastTyMCo :: Type -> MCoercion -> Type mkCastTyMCo ty MRefl = ty -mkCastTyMCo ty (MCo co) = ty `mkCastTy` co +mkCastTyMCo ty (MCo co) = ty `mkCastTy` CCoercion co mkFunResMCo :: Id -> CastCoercion -> CastCoercion mkFunResMCo _ ReflCastCo = ReflCastCo @@ -412,6 +414,17 @@ mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion mkGReflRightMCo r ty MRefl = mkReflCo r ty mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co +mkGReflLeftCastCo :: Role -> Type -> CastCoercion -> Coercion +mkGReflLeftCastCo r ty ReflCastCo = mkReflCo r ty +mkGReflLeftCastCo r ty (CCoercion co) = mkGReflLeftCo r ty co +mkGReflLeftCastCo _r _ty (ZCoercion _ki _cos) = error "AMG TODO mkGReflLeftCastCo" + +mkGReflRightCastCo :: Role -> Type -> CastCoercion -> Coercion +mkGReflRightCastCo r ty ReflCastCo = mkReflCo r ty +mkGReflRightCastCo r ty (CCoercion co) = mkGReflRightCo r ty co +mkGReflRightCastCo _r _ty (ZCoercion _ki _cos) = error "AMG TODO mkGReflRightCastCo" + + -- | Like 'mkCoherenceRightCo', but with an 'MCoercion' mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion mkCoherenceRightMCo _ _ MRefl co2 = co2 @@ -526,7 +539,7 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] = let arg_co = mkSelCo SelForAll (mkSymCo co) res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co) - subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co) + subst1' = extendTCvSubst subst1 a (ty `CastTy` CCoercion arg_co) subst2' = extendTCvSubst subst2 b ty in go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys @@ -1797,10 +1810,10 @@ castCoercionKind1 :: Coercion -> Role -> Type -> Type castCoercionKind1 g r t1 t2 h = case g of Refl {} -> assert (r == Nominal) $ -- Refl is always Nominal - mkNomReflCo (mkCastTy t2 h) + mkNomReflCo (mkCastTy t2 (CCoercion h)) GRefl _ _ mco -> case mco of - MRefl -> mkReflCo r (mkCastTy t2 h) - MCo kind_co -> mkGReflMCo r (mkCastTy t1 h) + MRefl -> mkReflCo r (mkCastTy t2 (CCoercion h)) + MCo kind_co -> mkGReflMCo r (mkCastTy t1 (CCoercion h)) (mkSymCo h `mkTransCo` kind_co `mkTransCo` h) _ -> castCoercionKind2 g r t1 t2 h h @@ -2293,8 +2306,10 @@ ty_co_subst !lc role ty else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t) go r ty@(LitTy {}) = assert (r == Nominal) $ mkNomReflCo ty - go r (CastTy ty co) = castCoercionKind (go r ty) (substLeftCo lc co) + go r (CastTy ty cco) = castCoercionKind (go r ty) (substLeftCo lc co) (substRightCo lc co) + where + co = castCoToCo (typeKind ty) cco go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co) (substRightCo lc co) where kco = go Nominal (coercionType co) @@ -2617,7 +2632,7 @@ coercion_lr_kind which orig_co where go (Refl ty) = ty go (GRefl _ ty MRefl) = ty - go (GRefl _ ty (MCo co1)) = pickLR which (ty, mkCastTy ty co1) + go (GRefl _ ty (MCo co1)) = pickLR which (ty, mkCastTy ty (CCoercion co1)) go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos) go (AppCo co1 co2) = mkAppTy (go co1) (go co2) go (CoVarCo cv) = go_covar cv @@ -2710,7 +2725,7 @@ coercion_lr_kind which orig_co k2 = coercionRKind k_co tv2 = setTyVarKind tv1 (substTy subst k2) subst' = extendTvSubst (extendSubstInScope subst tv2) tv1 $ - TyVarTy tv2 `mkCastTy` mkSymCo k_co + TyVarTy tv2 `mkCastTy` CCoercion (mkSymCo k_co) go_forall_right subst (ForAllCo { fco_tcv = cv1, fco_visR = visR , fco_kind = k_mco, fco_body = co }) @@ -2815,13 +2830,15 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' - go (CastTy ty1 co) ty2 - = let co' = go ty1 ty2 + go (CastTy ty1 cco) ty2 + = let co = castCoToCo (typeKind ty1) cco + co' = go ty1 ty2 r = coercionRole co' in mkCoherenceLeftCo r ty1 co co' - go ty1 (CastTy ty2 co) - = let co' = go ty1 ty2 + go ty1 (CastTy ty2 cco) + = let co = castCoToCo (typeKind ty2) cco + co' = go ty1 ty2 r = coercionRole co' in mkCoherenceRightCo r ty2 co co' @@ -2858,7 +2875,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 where kind_co = go (tyVarKind tv1) (tyVarKind tv2) in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co ty2' = substTyWithInScope in_scope [tv2] - [mkTyVarTy tv1 `mkCastTy` kind_co] + [mkTyVarTy tv1 `mkCastTy` CCoercion kind_co] ty2 go (ForAllTy (Bndr cv1 flag1) ty1) (ForAllTy (Bndr cv2 flag2) ty2) @@ -2972,7 +2989,7 @@ eqCastCoercionX env ty1 co1 ty2 co2 = eqTypeX env ty1 ty2 -- | Convert a 'CastCoercion' back into a 'Coercion', using a 'UnivCo' if we -- have discarded the original 'Coercion'. -castCoToCo :: Type -> CastCoercion -> CoercionR +castCoToCo :: Type -> CastCoercion -> Coercion castCoToCo _ (CCoercion co) = co castCoToCo lhs_ty (ZCoercion rhs_ty cos) = mkUnivCo ZCoercionProv (map CoVarCo (nonDetEltsUniqSet cos)) Representational lhs_ty rhs_ty castCoToCo lhs_ty ReflCastCo = mkRepReflCo lhs_ty ===================================== compiler/GHC/Core/Coercion.hs-boot ===================================== @@ -55,3 +55,9 @@ coercionType :: Coercion -> Type topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type) -- used to look through newtypes to the right of -- function arrows, in 'GHC.Core.Type.getRuntimeArgTys' + +castCoToCo :: Type -> CastCoercion -> Coercion +isReflexiveCastCo :: Type -> CastCoercion -> Bool +mkTransCastCo :: HasDebugCallStack => CastCoercion -> CastCoercion -> CastCoercion +seqCastCoercion :: CastCoercion -> () +castCoercionRKind :: HasDebugCallStack => Type -> CastCoercion -> Type ===================================== compiler/GHC/Core/Coercion/Opt.hs ===================================== @@ -884,7 +884,7 @@ opt_trans_rule is co1 co2 (opt_trans is' r1 r2') where is' = is `extendInScopeSet` tv1 - r2' = substCoWithInScope is' [tv2] [mkCastTy (TyVarTy tv1) kco1] r2 + r2' = substCoWithInScope is' [tv2] [mkCastTyCo (TyVarTy tv1) kco1] r2 -- Push transitivity inside forall -- forall over coercions. @@ -1481,7 +1481,7 @@ optForAllCoBndr env sym tcv k_mco -- override the substitution for the original variable to the -- re-kinded one, suitably casted tv2 = tv1 `setTyVarKind` coercionLKind k_co' - subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` k_co')) + subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` CCoercion k_co')) `extendSubstInScope` tv2 _ -> (subst1, tv1) ===================================== compiler/GHC/Core/FamInstEnv.hs ===================================== @@ -1485,9 +1485,10 @@ normalise_type ty ; redn <- withLC lc' $ normalise_type ty ; return $ mkForAllRedn vis tv' k_redn redn } go (TyVarTy tv) = normalise_tyvar tv - go (CastTy ty co) + go (CastTy ty cco) = do { redn <- go ty ; lc <- getLC + ; let co = castCoToCo (typeKind ty) cco ; let co' = substRightCo lc co ; return $ mkCastRedn2 Nominal ty co redn co' -- ^^^^^^^^^^^ uses castCoercionKind2 ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -1990,9 +1990,10 @@ lintType ty@(ForAllTy {}) = do { lintType body_ty ; lintForAllBody tcvs body_ty } -lintType (CastTy ty co) +lintType (CastTy ty cco) = do { lintType ty ; ty_kind <- substTyM (typeKind ty) + ; let co = castCoToCo (typeKind ty) cco -- TODO: maybe show the actual cco in mkCastTyErr/mkCastErr? ; co_lk <- lintStarCoercion co ; ensureEqTys ty_kind co_lk (mkCastTyErr ty co ty_kind co_lk) } ===================================== compiler/GHC/Core/Opt/Arity.hs ===================================== @@ -2925,7 +2925,7 @@ pushCoTyArg co ty | isForAllTy_ty tyL = assertPpr (isForAllTy_ty tyR) (ppr co $$ ppr ty) $ - Just (ty `mkCastTy` co1, coercionLKind co2, CCoercion co2) + Just (ty `mkCastTyCo` co1, coercionLKind co2, CCoercion co2) | otherwise = Nothing ===================================== compiler/GHC/Core/Reduction.hs ===================================== @@ -227,7 +227,7 @@ mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction mkGReflRightRedn role ty co = mkReduction (mkGReflRightCo role ty co) - (mkCastTy ty co) + (mkCastTyCo ty co) {-# INLINE mkGReflRightRedn #-} -- | Create a 'Reduction' from a kind cast, in which @@ -236,11 +236,11 @@ mkGReflRightRedn role ty co -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@ -- at the given 'Role'. -mkGReflRightMRedn :: Role -> Type -> MCoercionN -> Reduction +mkGReflRightMRedn :: Role -> Type -> CastCoercion -> Reduction mkGReflRightMRedn role ty mco = mkReduction - (mkGReflRightMCo role ty mco) - (mkCastTyMCo ty mco) + (mkGReflRightCastCo role ty mco) + (mkCastTy ty mco) {-# INLINE mkGReflRightMRedn #-} -- | Create a 'Reduction' from a kind cast, in which @@ -262,10 +262,10 @@ mkGReflLeftRedn role ty co -- Given @ty :: k1@, @mco :: k1 ~ k2@, -- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@ -- at the given 'Role'. -mkGReflLeftMRedn :: Role -> Type -> MCoercionN -> Reduction +mkGReflLeftMRedn :: Role -> Type -> CastCoercion -> Reduction mkGReflLeftMRedn role ty mco = mkReduction - (mkGReflLeftMCo role ty mco) + (mkGReflLeftCastCo role ty mco) ty {-# INLINE mkGReflLeftMRedn #-} @@ -279,7 +279,7 @@ mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction mkCoherenceRightRedn r (Reduction co1 ty2) kco = mkReduction (mkCoherenceRightCo r ty2 kco co1) - (mkCastTy ty2 kco) + (mkCastTyCo ty2 kco) {-# INLINE mkCoherenceRightRedn #-} -- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'. @@ -314,7 +314,7 @@ mkCastRedn1 r ty cast_co (Reduction co xi) -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co) = mkReduction (castCoercionKind1 co r ty xi cast_co) - (mkCastTy xi cast_co) + (mkCastTyCo xi cast_co) {-# INLINE mkCastRedn1 #-} -- | Apply casts on both sides of a 'Reduction' (of the given 'Role'). @@ -333,7 +333,7 @@ mkCastRedn2 :: Role mkCastRedn2 r ty cast_co (Reduction nco nty) cast_co' = mkReduction (castCoercionKind2 nco r ty nty cast_co cast_co') - (mkCastTy nty cast_co') + (mkCastTyCo nty cast_co') {-# INLINE mkCastRedn2 #-} -- | Apply one 'Reduction' to another. ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -76,6 +76,7 @@ import GHC.Utils.EndoOS import GHC.Data.Pair +import Data.Maybe import Data.Semigroup {- @@ -667,7 +668,7 @@ tyCoFVsOfType (LitTy {}) f bound_vars acc = emptyFV f bound_vars acc tyCoFVsOfType (AppTy fun arg) f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc tyCoFVsOfType (FunTy _ w arg res) f bound_vars acc = (tyCoFVsOfType w `unionFV` tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc tyCoFVsOfType (ForAllTy bndr ty) f bound_vars acc = tyCoFVsBndr bndr (tyCoFVsOfType ty) f bound_vars acc -tyCoFVsOfType (CastTy ty co) f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCo co) f bound_vars acc +tyCoFVsOfType (CastTy ty co) f bound_vars acc = (tyCoFVsOfType ty `unionFV` tyCoFVsOfCastCoercion co) f bound_vars acc tyCoFVsOfType (CoercionTy co) f bound_vars acc = tyCoFVsOfCo co f bound_vars acc tyCoFVsBndr :: ForAllTyBinder -> FV -> FV @@ -765,6 +766,11 @@ almost_devoid_co_var_of_mco :: MCoercion -> CoVar -> Bool almost_devoid_co_var_of_mco MRefl _ = True almost_devoid_co_var_of_mco (MCo co) cv = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_cast_co :: CastCoercion -> CoVar -> Bool +almost_devoid_co_var_of_cast_co ReflCastCo _ = True +almost_devoid_co_var_of_cast_co (CCoercion co) cv = almost_devoid_co_var_of_co co cv +almost_devoid_co_var_of_cast_co (ZCoercion ty cos) cv = almost_devoid_co_var_of_type ty cv && not (elemVarSet cv cos) + almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into @@ -829,7 +835,7 @@ almost_devoid_co_var_of_type (ForAllTy (Bndr v _) ty) cv && (v == cv || almost_devoid_co_var_of_type ty cv) almost_devoid_co_var_of_type (CastTy ty co) cv = almost_devoid_co_var_of_type ty cv - && almost_devoid_co_var_of_co co cv + && almost_devoid_co_var_of_cast_co co cv almost_devoid_co_var_of_type (CoercionTy co) cv = almost_devoid_co_var_of_co co cv @@ -866,7 +872,7 @@ visVarsOfType orig_ty = Pair invis_vars vis_vars = ((`delVarSet` tv) <$> go ty) `mappend` (invisible (tyCoVarsOfType $ varType tv)) go (LitTy {}) = mempty - go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCo co) + go (CastTy ty co) = go ty `mappend` invisible (tyCoVarsOfCastCo co) go (CoercionTy co) = invisible $ tyCoVarsOfCo co invisible vs = Pair vs emptyVarSet @@ -1005,7 +1011,7 @@ invisibleVarsOfType = go where (invisibles, visibles) = partitionInvisibleTypes tc tys go (ForAllTy tvb ty) = tyCoFVsBndr tvb $ go ty go LitTy{} = emptyFV - go (CastTy ty co) = tyCoFVsOfCo co `unionFV` go ty + go (CastTy ty co) = tyCoFVsOfCastCoercion co `unionFV` go ty go (CoercionTy co) = tyCoFVsOfCo co -- | Like 'invisibleVarsOfType', but for many types. @@ -1096,7 +1102,7 @@ tyConsOfType ty go a `unionUniqSets` go b `unionUniqSets` go_tc (funTyFlagTyCon af) go (ForAllTy (Bndr tv _) ty) = go ty `unionUniqSets` go (varType tv) - go (CastTy ty co) = go ty `unionUniqSets` go_co co + go (CastTy ty co) = go ty `unionUniqSets` go_cast_co co go (CoercionTy co) = go_co co go_co (Refl ty) = go ty @@ -1123,6 +1129,10 @@ tyConsOfType ty go_mco MRefl = emptyUniqSet go_mco (MCo co) = go_co co + go_cast_co ReflCastCo = emptyUniqSet + go_cast_co (CCoercion co) = go_co co + go_cast_co (ZCoercion ty _cos) = go ty + go_cos cos = foldr (unionUniqSets . go_co) emptyUniqSet cos go_tc tc = unitUniqSet tc @@ -1256,7 +1266,7 @@ occCheckExpand vs_to_avoid ty -- Failing that, try to expand a synonym go cxt (CastTy ty co) = do { ty' <- go cxt ty - ; co' <- go_co cxt co + ; co' <- go_cast_co cxt co ; return (CastTy ty' co') } go cxt (CoercionTy co) = do { co' <- go_co cxt co ; return (CoercionTy co') } @@ -1273,6 +1283,14 @@ occCheckExpand vs_to_avoid ty go_mco _ MRefl = return MRefl go_mco ctx (MCo co) = MCo <$> go_co ctx co + go_cast_co _ ReflCastCo = return ReflCastCo + go_cast_co ctx (CCoercion co) = CCoercion <$> go_co ctx co + go_cast_co ctx (ZCoercion ty cos) = ZCoercion <$> go ctx ty <*> go_covars ctx cos + + go_covars (as, env) cos + | anyVarSet (bad_var_occ as) cos = Nothing + | otherwise = return $ mapVarSet (\cv -> fromMaybe cv (lookupVarEnv env cv)) cos + ------------------ go_co cxt (Refl ty) = do { ty' <- go cxt ty ; return (Refl ty') } ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -186,7 +186,7 @@ data Type | CastTy Type - KindCoercion -- ^ A kind cast. The coercion is always nominal. + CastCoercion -- ^ A kind cast. The coercion is always nominal. -- INVARIANT: The cast is never reflexive \(EQ2) -- INVARIANT: The Type is not a CastTy (use TransCo instead) \(EQ3) -- INVARIANT: The Type is not a ForAllTy over a tyvar \(EQ4) @@ -2055,7 +2055,7 @@ foldTyCo (TyCoFolder { tcf_view = view go_ty env (TyVarTy tv) = tyvar env tv go_ty env (AppTy t1 t2) = go_ty env t1 `mappend` go_ty env t2 go_ty _ (LitTy {}) = mempty - go_ty env (CastTy ty co) = go_ty env ty `mappend` go_co env co + go_ty env (CastTy ty co) = go_ty env ty `mappend` go_cast_co env co go_ty env (CoercionTy co) = go_co env co go_ty env (FunTy _ w arg res) = go_ty env w `mappend` go_ty env arg `mappend` go_ty env res go_ty env (TyConApp _ tys) = go_tys env tys @@ -2071,6 +2071,10 @@ foldTyCo (TyCoFolder { tcf_view = view go_cos _ [] = mempty go_cos env (c:cs) = go_co env c `mappend` go_cos env cs + go_cast_co _ ReflCastCo = mempty + go_cast_co env (CCoercion co) = go_co env co + go_cast_co env (ZCoercion ty cos) = go_ty env ty `mappend` nonDetStrictFoldVarSet (mappend . covar env) mempty cos + go_co env (Refl ty) = go_ty env ty go_co env (GRefl _ ty MRefl) = go_ty env ty go_co env (GRefl _ ty (MCo co)) = go_ty env ty `mappend` go_co env co @@ -2134,7 +2138,7 @@ typeSize (AppTy t1 t2) = typeSize t1 + typeSize t2 typeSize (FunTy _ _ t1 t2) = typeSize t1 + typeSize t2 typeSize (ForAllTy (Bndr tv _) t) = typeSize (varType tv) + typeSize t typeSize (TyConApp _ ts) = 1 + typesSize ts -typeSize (CastTy ty co) = typeSize ty + coercionSize co +typeSize (CastTy ty co) = typeSize ty + castCoercionSize co typeSize (CoercionTy co) = coercionSize co typesSize :: [Type] -> Int ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -797,7 +797,7 @@ subst_ty subst ty !(subst',tv') = substVarBndrUnchecked subst tv -- Unchecked because subst_ty is used from substTyUnchecked go (LitTy n) = LitTy $! n - go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co) + go (CastTy ty co) = (mkCastTy $! (go ty)) $! (substCastCo subst co) go (CoercionTy co) = CoercionTy $! (subst_co subst co) substTyVar :: Subst -> TyVar -> Type ===================================== compiler/GHC/Core/TyCo/Tidy.hs ===================================== @@ -235,7 +235,7 @@ tidyType env (TyVarTy tv) = TyVarTy $! tidyTyCoVarOcc env tv tidyType _ t@(TyConApp _ []) = t -- Preserve sharing if possible tidyType env (TyConApp tycon tys) = TyConApp tycon $! tidyTypes env tys tidyType env (AppTy fun arg) = (AppTy $! (tidyType env fun)) $! (tidyType env arg) -tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCo env co) +tidyType env (CastTy ty co) = (CastTy $! tidyType env ty) $! (tidyCastCo env co) tidyType env (CoercionTy co) = CoercionTy $! (tidyCo env co) tidyType env ty@(FunTy _ w arg res) = let { !w' = tidyType env w ; !arg' = tidyType env arg ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -73,6 +73,7 @@ module GHC.Core.Type ( getLevity, levityType_maybe, mkCastTy, mkCoercionTy, splitCastTy_maybe, + mkCastTyCo, ErrorMsgType, pprUserTypeErrorTy, @@ -236,6 +237,7 @@ import GHC.Core.TyCo.FVs import GHC.Types.Var import GHC.Types.Var.Env import GHC.Types.Var.Set +import GHC.Types.Unique.Set import GHC.Core.TyCon import GHC.Builtin.Types.Prim @@ -258,9 +260,12 @@ import {-# SOURCE #-} GHC.Core.Coercion , mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo , mkKindCo, mkSubCo, mkFunCo, funRole , decomposePiCos, coercionKind - , coercionRKind, coercionType - , isReflexiveCo, seqCo + , coercionType + , isReflexiveCastCo, seqCo , topNormaliseNewType_maybe + , mkTransCastCo + , seqCastCoercion, castCoercionRKind + , castCoToCo ) import {-# SOURCE #-} GHC.Tc.Utils.TcType ( isConcreteTyVar ) @@ -514,12 +519,16 @@ expandTypeSynonyms ty go subst (ForAllTy (Bndr tv vis) t) = let (subst', tv') = substVarBndrUsing go subst tv in ForAllTy (Bndr tv' vis) (go subst' t) - go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co) + go subst (CastTy ty co) = mkCastTy (go subst ty) (go_cast_co subst co) go subst (CoercionTy co) = mkCoercionTy (go_co subst co) go_mco _ MRefl = MRefl go_mco subst (MCo co) = MCo (go_co subst co) + go_cast_co _ ReflCastCo = ReflCastCo + go_cast_co subst (CCoercion co) = CCoercion (go_co subst co) + go_cast_co subst (ZCoercion ty cos) = ZCoercion (go subst ty) (substCoVarSet subst cos) + go_co subst (Refl ty) = mkNomReflCo (go subst ty) go_co subst (GRefl r ty mco) @@ -905,7 +914,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar go_ty !env (TyVarTy tv) = tyvar env tv go_ty !env (AppTy t1 t2) = mkAppTy <$> go_ty env t1 <*> go_ty env t2 go_ty !_ ty@(LitTy {}) = return ty - go_ty !env (CastTy ty co) = mkCastTy <$> go_ty env ty <*> go_co env co + go_ty !env (CastTy ty co) = mkCastTy <$> go_ty env ty <*> go_cast_co env co go_ty !env (CoercionTy co) = CoercionTy <$> go_co env co go_ty !env ty@(FunTy _ w arg res) @@ -936,6 +945,10 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar go_mco !_ MRefl = return MRefl go_mco !env (MCo co) = MCo <$> (go_co env co) + go_cast_co !_ ReflCastCo = return ReflCastCo + go_cast_co !env (CCoercion co) = CCoercion <$> (go_co env co) + go_cast_co !env (ZCoercion ty cos) = ZCoercion <$> go_ty env ty <*> (coVarsOfCos <$> mapM (covar env) (nonDetEltsUniqSet cos)) -- TODO + go_co :: env -> Coercion -> m Coercion go_co !env (Refl ty) = Refl <$> go_ty env ty go_co !env (GRefl r ty mco) = mkGReflCo r <$> go_ty env ty <*> go_mco env mco @@ -1020,10 +1033,10 @@ isTyVarTy ty = isJust (getTyVar_maybe ty) -- | If the type is a tyvar, possibly under a cast, returns it, along -- with the coercion. Thus, the co is :: kind tv ~N kind ty -getCastedTyVar_maybe :: Type -> Maybe (TyVar, CoercionN) +getCastedTyVar_maybe :: Type -> Maybe (TyVar, CastCoercion) getCastedTyVar_maybe ty = case coreFullView ty of CastTy (TyVarTy tv) co -> Just (tv, co) - TyVarTy tv -> Just (tv, mkReflCo Nominal (tyVarKind tv)) + TyVarTy tv -> Just (tv, ReflCastCo) _ -> Nothing @@ -1063,9 +1076,10 @@ type checker (e.g. when matching type-function equations). -- | Applies a type to another, as in e.g. @k a@ mkAppTy :: Type -> Type -> Type -- See Note [Respecting definitional equality], invariant (EQ1). -mkAppTy (CastTy fun_ty co) arg_ty - | ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty] - = (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co +mkAppTy (CastTy fun_ty cco) arg_ty + | let co = castCoToCo (typeKind fun_ty) cco -- TOOD: can we get rid of this? + , ([arg_co], res_co) <- decomposePiCos co (coercionKind co) [arg_ty] + = (fun_ty `mkAppTy` (arg_ty `mkCastTy` CCoercion arg_co)) `mkCastTy` CCoercion res_co mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2]) mkAppTy ty1 ty2 = AppTy ty1 ty2 @@ -1084,15 +1098,16 @@ mkAppTy ty1 ty2 = AppTy ty1 ty2 mkAppTys :: Type -> [Type] -> Type mkAppTys ty1 [] = ty1 -mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy +mkAppTys (CastTy fun_ty cco) arg_tys -- much more efficient then nested mkAppTy -- Why do this? See (EQ1) of -- Note [Respecting definitional equality] -- in GHC.Core.TyCo.Rep - = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers + = foldl' AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` CCoercion res_co) leftovers where + co = castCoToCo (typeKind fun_ty) cco (arg_cos, res_co) = decomposePiCos co (coercionKind co) arg_tys (args_to_cast, leftovers) = splitAtList arg_cos arg_tys - casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos + casted_arg_tys = zipWith (\ ty co -> mkCastTy ty (CCoercion co)) args_to_cast arg_cos mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2) mkAppTys ty1 tys2 = foldl' AppTy ty1 tys2 @@ -1647,16 +1662,19 @@ newTyConInstRhs tycon tys * * ********************************************************************* -} -splitCastTy_maybe :: Type -> Maybe (Type, Coercion) +splitCastTy_maybe :: Type -> Maybe (Type, CastCoercion) splitCastTy_maybe ty | CastTy ty' co <- coreFullView ty = Just (ty', co) | otherwise = Nothing +mkCastTyCo :: Type -> Coercion -> Type +mkCastTyCo ty co = mkCastTy ty (CCoercion co) + -- | Make a 'CastTy'. The Coercion must be nominal. Checks the -- Coercion for reflexivity, dropping it if it's reflexive. -- See @Note [Respecting definitional equality]@ in "GHC.Core.TyCo.Rep" -mkCastTy :: Type -> Coercion -> Type -mkCastTy orig_ty co | isReflexiveCo co = orig_ty -- (EQ2) from the Note +mkCastTy :: Type -> CastCoercion -> Type +mkCastTy orig_ty co | isReflexiveCastCo (typeKind orig_ty) co = orig_ty -- (EQ2) from the Note -- NB: Do the slow check here. This is important to keep the splitXXX -- functions working properly. Otherwise, we may end up with something -- like (((->) |> something_reflexive_but_not_obviously_so) biz baz) @@ -1666,7 +1684,7 @@ mkCastTy orig_ty co = mk_cast_ty orig_ty co -- | Like 'mkCastTy', but avoids checking the coercion for reflexivity, -- as that can be expensive. -mk_cast_ty :: Type -> Coercion -> Type +mk_cast_ty :: Type -> CastCoercion -> Type mk_cast_ty orig_ty co = go orig_ty where go :: Type -> Type @@ -1675,14 +1693,14 @@ mk_cast_ty orig_ty co = go orig_ty go (CastTy ty co1) -- (EQ3) from the Note - = mkCastTy ty (co1 `mkTransCo` co) + = mkCastTy ty (co1 `mkTransCastCo` co) -- call mkCastTy again for the reflexivity check go (ForAllTy (Bndr tv vis) inner_ty) -- (EQ4) from the Note -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep. | isTyVar tv - , let fvs = tyCoVarsOfCo co + , let fvs = tyCoVarsOfCastCo co = -- have to make sure that pushing the co in doesn't capture the bound var! if tv `elemVarSet` fvs then let empty_subst = mkEmptySubst (mkInScopeSet fvs) @@ -2546,7 +2564,7 @@ seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2 seqType (FunTy _ w t1 t2) = seqType w `seq` seqType t1 `seq` seqType t2 seqType (TyConApp tc tys) = tc `seq` seqTypes tys seqType (ForAllTy (Bndr tv _) ty) = seqType (varType tv) `seq` seqType ty -seqType (CastTy ty co) = seqType ty `seq` seqCo co +seqType (CastTy ty co) = seqType ty `seq` seqCastCoercion co seqType (CoercionTy co) = seqCo co seqTypes :: [Type] -> () @@ -2640,7 +2658,7 @@ typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys typeKind (LitTy l) = typeLiteralKind l typeKind (FunTy { ft_af = af }) = liftedTypeOrConstraintKind (funTyFlagResultTypeOrConstraint af) typeKind (TyVarTy tyvar) = tyVarKind tyvar -typeKind (CastTy _ty co) = coercionRKind co +typeKind (CastTy ty co) = castCoercionRKind (typeKind ty) co typeKind (CoercionTy co) = coercionType co typeKind (AppTy fun arg) ===================================== compiler/GHC/Core/Type.hs-boot ===================================== @@ -4,7 +4,7 @@ module GHC.Core.Type where import GHC.Prelude import {-# SOURCE #-} GHC.Core.TyCon -import {-# SOURCE #-} GHC.Core.TyCo.Rep( Type, Coercion ) +import {-# SOURCE #-} GHC.Core.TyCo.Rep( Type, CastCoercion ) import GHC.Utils.Misc import GHC.Types.Var( FunTyFlag, TyVar ) import GHC.Types.Basic( TypeOrConstraint ) @@ -16,7 +16,7 @@ chooseFunTyFlag :: HasDebugCallStack => Type -> Type -> FunTyFlag typeKind :: HasDebugCallStack => Type -> Type isCoercionTy :: Type -> Bool mkAppTy :: Type -> Type -> Type -mkCastTy :: Type -> Coercion -> Type +mkCastTy :: Type -> CastCoercion -> Type mkTyConApp :: TyCon -> [Type] -> Type getLevity :: HasDebugCallStack => Type -> Type getTyVar_maybe :: Type -> Maybe TyVar ===================================== compiler/GHC/Core/Unify.hs ===================================== @@ -1582,12 +1582,13 @@ type AmIUnifying = Bool -- True <=> Unifying -- False <=> Matching type InType = Type -- Before applying the RnEnv2 -type OutCoercion = Coercion -- After applying the RnEnv2 +type OutCastCoercion = CastCoercion -- After applying the RnEnv2 + unify_ty :: UMEnv -> InType -> InType -- Types to be unified - -> OutCoercion -- A nominal coercion between their kinds + -> OutCastCoercion -- A nominal coercion between their kinds -- OutCoercion: the RnEnv has already been applied -- When matching, the coercion is in "target space", -- not "template space" @@ -1609,28 +1610,28 @@ unify_ty env ty1 ty2 kco | Just ty2' <- coreView ty2 = unify_ty env ty1 ty2' kco unify_ty env (CastTy ty1 co1) ty2 kco - | mentionsForAllBoundTyVarsL env (tyCoVarsOfCo co1) + | mentionsForAllBoundTyVarsL env (tyCoVarsOfCastCo co1) -- See (KCU1) in Note [Kind coercions in Unify] = maybeApart MARCast -- See (KCU2) | um_unif env - = unify_ty env ty1 ty2 (co1 `mkTransCo` kco) + = unify_ty env ty1 ty2 (co1 `mkTransCastCo` kco) | otherwise -- We are matching, not unifying = do { subst <- getSubst env - ; let co' = substCo subst co1 + ; let co' = substCastCo subst co1 -- We match left-to-right, so the free template vars of the -- coercion should already have been matched. -- See Note [Matching in the presence of casts (1)] -- NB: co1 does not mention forall-bound vars, so no need to rename - ; unify_ty env ty1 ty2 (co' `mkTransCo` kco) } + ; unify_ty env ty1 ty2 (co' `mkTransCastCo` kco) } unify_ty env ty1 (CastTy ty2 co2) kco - | mentionsForAllBoundTyVarsR env (tyCoVarsOfCo co2) + | mentionsForAllBoundTyVarsR env (tyCoVarsOfCastCo co2) -- See (KCU1) in Note [Kind coercions in Unify] = maybeApart MARCast -- See (KCU2) | otherwise - = unify_ty env ty1 ty2 (kco `mkTransCo` mkSymCo co2) + = unify_ty env ty1 ty2 (kco `mkTransCastCo` mkSymCastCo (typeKind ty2) co2) -- NB: co2 does not mention forall-bound variables -- Applications need a bit of care! @@ -1647,7 +1648,7 @@ unify_ty _ (LitTy x) (LitTy y) _kco | x == y = return () unify_ty env (ForAllTy (Bndr tv1 _) ty1) (ForAllTy (Bndr tv2 _) ty2) kco -- ToDo: See Note [Unifying coercion-foralls] - = do { unify_ty env (varType tv1) (varType tv2) (mkNomReflCo liftedTypeKind) + = do { unify_ty env (varType tv1) (varType tv2) ReflCastCo ; let env' = umRnBndr2 env tv1 tv2 ; unify_ty env' ty1 ty2 kco } @@ -1658,7 +1659,7 @@ unify_ty env (CoercionTy co1) (CoercionTy co2) kco CoVarCo cv | not (um_unif env) , not (cv `elemVarEnv` c_subst) -- Not forall-bound - , let (_mult_co, co_l, co_r) = decomposeFunCo kco + , let (_mult_co, co_l, co_r) = decomposeFunCo (castCoToCo (typeKind (CoercionTy co1)) kco) -- Because the coercion is used in a type, it should be safe to -- ignore the multiplicity coercion, _mult_co -- cv :: t1 ~ t2 @@ -1678,7 +1679,7 @@ unify_ty env (TyVarTy tv1) ty2 kco unify_ty env ty1 (TyVarTy tv2) kco | um_unif env -- If unifying, can swap args; but not when matching - = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCo kco) + = uVarOrFam (umSwapRn env) (TyVarLHS tv2) ty1 (mkSymCastCo (typeKind ty1) kco) -- Deal with TyConApps unify_ty env ty1 ty2 kco @@ -1689,7 +1690,7 @@ unify_ty env ty1 ty2 kco | um_unif env , Just (tc,tys) <- mb_sat_fam_app2 - = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCo kco) + = uVarOrFam (umSwapRn env) (TyFamLHS tc tys) ty1 (mkSymCastCo (typeKind ty1) kco) -- Handle oversaturated type families. Suppose we have -- (F a b) ~ (c d) where F has arity 1 @@ -1760,8 +1761,8 @@ unify_ty_app env ty1 ty1args ty2 ty2args = do { let ki1 = typeKind ty1 ki2 = typeKind ty2 -- See Note [Kind coercions in Unify] - ; unify_ty env ki1 ki2 (mkNomReflCo liftedTypeKind) - ; unify_ty env ty1 ty2 (mkNomReflCo ki2) + ; unify_ty env ki1 ki2 ReflCastCo + ; unify_ty env ty1 ty2 ReflCastCo -- TODO: simplify following comment? -- Very important: 'ki2' not 'ki1' -- See Note [Matching in the presence of casts (2)] ; unify_tys env ty1args ty2args } @@ -1775,7 +1776,7 @@ unify_tys env orig_xs orig_ys go [] [] = return () go (x:xs) (y:ys) -- See Note [Kind coercions in Unify] - = do { unify_ty env x y (mkNomReflCo $ typeKind y) + = do { unify_ty env x y ReflCastCo -- TODO: simplify following comment? -- Very important: 'y' not 'x' -- See Note [Matching in the presence of casts (2)] ; go xs ys } @@ -1784,7 +1785,7 @@ unify_tys env orig_xs orig_ys -- See Note [Polykinded tycon applications] --------------------------------- -uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCoercion -> UM () +uVarOrFam :: UMEnv -> CanEqLHS -> InType -> OutCastCoercion -> UM () -- Invariants: (a) If ty1 is a TyFamLHS, then ty2 is NOT a TyVarTy -- (b) both args have had coreView already applied -- Why saturated? See (ATF4) in Note [Apartness and type families] @@ -1811,7 +1812,7 @@ uVarOrFam env ty1 ty2 kco ----------------------------- -- LHS is a type variable -- The sequence of tests is very similar to go_tv - go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCoercion -> UM () + go :: SwapFlag -> UMState -> CanEqLHS -> InType -> OutCastCoercion -> UM () go swapped substs lhs@(TyVarLHS tv1) ty2 kco | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1' = -- We already have a substitution for tv1 @@ -1856,7 +1857,7 @@ uVarOrFam env ty1 ty2 kco | um_unif env , NotSwapped <- swapped -- If we have swapped already, don't do so again , Just lhs2 <- canEqLHS_maybe ty2 - = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCo kco) + = go IsSwapped substs lhs2 (mkTyVarTy tv1) (mkSymCastCo (varType tv1) kco) | occurs_check = maybeApart MARInfinite -- Occurs check | otherwise = surelyApart @@ -1864,7 +1865,7 @@ uVarOrFam env ty1 ty2 kco where tv1' = umRnOccL env tv1 ty2_fvs = tyCoVarsOfType ty2 - rhs = ty2 `mkCastTy` mkSymCo kco + rhs = ty2 `mkCastTy` mkSymCastCo (varType tv1') kco tv1_is_bindable | not (tv1' `elemVarSet` foralld_tvs) -- tv1' is not forall-bound, but tv1 can still differ -- from tv1; see Note [Cloning the template binders] @@ -1928,13 +1929,14 @@ uVarOrFam env ty1 ty2 kco | um_unif env , NotSwapped <- swapped , Just lhs2 <- canEqLHS_maybe ty2 - = go IsSwapped substs lhs2 (mkTyConApp tc1 tys1) (mkSymCo kco) + , let ty1' = mkTyConApp tc1 tys1 + = go IsSwapped substs lhs2 ty1' (mkSymCastCo (typeKind ty1') kco) | otherwise -- See (ATF5) in Note [Apartness and type families] = surelyApart where - rhs = ty2 `mkCastTy` mkSymCo kco + rhs = ty2 `mkCastTy` mkSymCastCo (typeKind (mkTyConApp tc1 tys1)) kco ----------------------------- -- go_fam_fam: LHS and RHS are both saturated type-family applications, @@ -1971,7 +1973,7 @@ uVarOrFam env ty1 ty2 kco | otherwise = return () - rhs1 = mkTyConApp tc tys2 `mkCastTy` mkSymCo kco + rhs1 = mkTyConApp tc tys2 `mkCastTy` mkSymCastCo (typeKind (mkTyConApp tc tys1)) kco -- TODO: correct? rhs2 = mkTyConApp tc tys1 `mkCastTy` kco @@ -2335,9 +2337,10 @@ ty_co_match menv subst ty co lkco rkco noneSet f = allVarSet (not . f) ty_co_match menv subst ty co lkco rkco - | CastTy ty' co' <- ty + | CastTy ty' cco' <- ty -- See Note [Matching in the presence of casts (1)] = let empty_subst = mkEmptySubst (rnInScopeSet (me_env menv)) + co' = castCoToCo (typeKind ty') cco' substed_co_l = substCo (liftEnvSubstLeft empty_subst subst) co' substed_co_r = substCo (liftEnvSubstRight empty_subst subst) co' in @@ -2448,7 +2451,7 @@ ty_co_match menv subst ty co1 lkco rkco -- But transitive coercions are not helpful. Therefore we deal -- with it here: we do recursion on the smaller reflexive coercion, -- while propagating the correct kind coercions. - = let kco' = mkSymCo co + = let kco' = mkSymCo (castCoToCo (typeKind t) co) in ty_co_match menv subst ty (mkReflCo r t) (lkco `mkTransCo` kco') (rkco `mkTransCo` kco') ===================================== compiler/GHC/CoreToIface.hs ===================================== @@ -192,7 +192,7 @@ toIfaceTypeX fr (ForAllTy b t) = IfaceForAllTy (toIfaceForAllBndrX fr b) (toIfaceTypeX (fr `delVarSet` binderVar b) t) toIfaceTypeX fr (FunTy { ft_arg = t1, ft_mult = w, ft_res = t2, ft_af = af }) = IfaceFunTy af (toIfaceTypeX fr w) (toIfaceTypeX fr t1) (toIfaceTypeX fr t2) -toIfaceTypeX fr (CastTy ty co) = IfaceCastTy (toIfaceTypeX fr ty) (toIfaceCoercionX fr co) +toIfaceTypeX fr (CastTy ty co) = IfaceCastTy (toIfaceTypeX fr ty) (toIfaceCastCoercionX fr co) toIfaceTypeX fr (CoercionTy co) = IfaceCoercionTy (toIfaceCoercionX fr co) toIfaceTypeX fr (TyConApp tc tys) @@ -271,9 +271,12 @@ toIfaceTyLit (CharTyLit x) = IfaceCharTyLit x ---------------- toIfaceCastCoercion :: CastCoercion -> IfaceCastCoercion -toIfaceCastCoercion (CCoercion co) = IfaceCCoercion (toIfaceCoercion co) -toIfaceCastCoercion (ZCoercion ty cos) = IfaceZCoercion (toIfaceType ty) (map (toIfaceCoercion . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO determinism -toIfaceCastCoercion ReflCastCo = IfaceReflCastCo +toIfaceCastCoercion = toIfaceCastCoercionX emptyVarSet + +toIfaceCastCoercionX :: VarSet -> CastCoercion -> IfaceCastCoercion +toIfaceCastCoercionX fr (CCoercion co) = IfaceCCoercion (toIfaceCoercionX fr co) +toIfaceCastCoercionX fr (ZCoercion ty cos) = IfaceZCoercion (toIfaceTypeX fr ty) (map (toIfaceCoercionX fr . CoVarCo) (nonDetEltsUniqSet cos)) -- TODO determinism +toIfaceCastCoercionX _ ReflCastCo = IfaceReflCastCo toIfaceCoercion :: Coercion -> IfaceCoercion toIfaceCoercion = toIfaceCoercionX emptyVarSet ===================================== compiler/GHC/HsToCore.hs ===================================== @@ -748,7 +748,7 @@ mkUnsafeCoercePrimPair _old_id old_expr runtimeRep1Ty runtimeRep2Ty (scrut2, scrut2_ty, ab_cv_ty) = unsafe_equality (mkTYPEapp runtimeRep2Ty) - (openAlphaTy `mkCastTy` alpha_co) + (openAlphaTy `mkCastTyCo` alpha_co) openBetaTy -- alpha_co :: TYPE r1 ~# TYPE r2 ===================================== compiler/GHC/Iface/Rename.hs ===================================== @@ -947,7 +947,7 @@ rnIfaceType (IfaceForAllTy tv t) rnIfaceType (IfaceCoercionTy co) = IfaceCoercionTy <$> rnIfaceCo co rnIfaceType (IfaceCastTy ty co) - = IfaceCastTy <$> rnIfaceType ty <*> rnIfaceCo co + = IfaceCastTy <$> rnIfaceType ty <*> rnIfaceCastCo co rnIfaceScaledType :: Rename (IfaceMult, IfaceType) rnIfaceScaledType (m, t) = (,) <$> rnIfaceType m <*> rnIfaceType t ===================================== compiler/GHC/Iface/Syntax.hs ===================================== @@ -2067,7 +2067,7 @@ freeNamesIfType (IfaceTupleTy _ _ ts) = freeNamesIfAppArgs ts freeNamesIfType (IfaceLitTy _) = emptyNameSet freeNamesIfType (IfaceForAllTy tv t) = freeNamesIfVarBndr tv &&& freeNamesIfType t freeNamesIfType (IfaceFunTy _ w s t) = freeNamesIfType s &&& freeNamesIfType t &&& freeNamesIfType w -freeNamesIfType (IfaceCastTy t c) = freeNamesIfType t &&& freeNamesIfCoercion c +freeNamesIfType (IfaceCastTy t c) = freeNamesIfType t &&& freeNamesIfCastCoercion c freeNamesIfType (IfaceCoercionTy c) = freeNamesIfCoercion c freeNamesIfMCoercion :: IfaceMCoercion -> NameSet ===================================== compiler/GHC/Iface/Type.hs ===================================== @@ -190,7 +190,7 @@ data IfaceType | IfaceForAllTy IfaceForAllBndr IfaceType | IfaceTyConApp IfaceTyCon IfaceAppArgs -- Not necessarily saturated -- Includes newtypes, synonyms, tuples - | IfaceCastTy IfaceType IfaceCoercion + | IfaceCastTy IfaceType IfaceCastCoercion | IfaceCoercionTy IfaceCoercion | IfaceTupleTy -- Saturated tuples (unsaturated ones use IfaceTyConApp) @@ -776,12 +776,16 @@ substIfaceType env ty go (IfaceTyConApp tc tys) = IfaceTyConApp tc (substIfaceAppArgs env tys) go (IfaceTupleTy s i tys) = IfaceTupleTy s i (substIfaceAppArgs env tys) go (IfaceForAllTy {}) = pprPanic "substIfaceType" (ppr ty) - go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_co co) + go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_cast_co co) go (IfaceCoercionTy co) = IfaceCoercionTy (go_co co) go_mco IfaceMRefl = IfaceMRefl go_mco (IfaceMCo co) = IfaceMCo $ go_co co + go_cast_co IfaceReflCastCo = IfaceReflCastCo + go_cast_co (IfaceCCoercion co) = IfaceCCoercion (go_co co) + go_cast_co (IfaceZCoercion ty cos) = IfaceZCoercion (go ty) (map go_co cos) + go_co (IfaceReflCo ty) = IfaceReflCo (go ty) go_co (IfaceGReflCo r ty mco) = IfaceGReflCo r (go ty) (go_mco mco) go_co (IfaceFunCo r w c1 c2) = IfaceFunCo r (go_co w) (go_co c1) (go_co c2) @@ -2191,6 +2195,9 @@ pprPromotionQuoteI IsPromoted = char '\'' instance Outputable IfaceCoercion where ppr = pprIfaceCoercion +instance Outputable IfaceCastCoercion where + ppr = pprIfaceCastCoercion + instance Binary IfaceTyCon where put_ bh (IfaceTyCon n i) = put_ bh n >> put_ bh i ===================================== compiler/GHC/IfaceToCore.hs ===================================== @@ -1527,7 +1527,7 @@ tcIfaceType = go go (IfaceForAllTy bndr t) = bindIfaceForAllBndr bndr $ \ tv' vis -> ForAllTy (Bndr tv' vis) <$> go t - go (IfaceCastTy ty co) = CastTy <$> go ty <*> tcIfaceCo co + go (IfaceCastTy ty co) = CastTy <$> go ty <*> tcIfaceCastCoercion co go (IfaceCoercionTy co) = CoercionTy <$> tcIfaceCo co tcIfaceTupleTy :: TupleSort -> PromotionFlag -> IfaceAppArgs -> IfL Type ===================================== compiler/GHC/Tc/Gen/App.hs ===================================== @@ -813,7 +813,7 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args -- NB: kappa is uninstantiated ('go' already checked that) ; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa) -- unifyKind: see (UQL3) in Note [QuickLook unification] - ; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co)) + ; liftZonkM (writeMetaTyVar kappa (mkCastTyCo fun_ty' kind_co)) ; let co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co) acc' = addArgWrap co_wrap acc @@ -2225,7 +2225,7 @@ qlUnify ty1 ty2 do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind -- unifyKind: see (UQL2) in Note [QuickLook unification] -- and (MIV2) in Note [Monomorphise instantiation variables] - ; let ty2' = mkCastTy ty2 co + ; let ty2' = mkCastTyCo ty2 co ; traceTc "qlUnify:update" $ ppr kappa <+> text ":=" <+> ppr ty2 ; liftZonkM $ writeMetaTyVar kappa ty2' } ===================================== compiler/GHC/Tc/Gen/Bind.hs ===================================== @@ -58,7 +58,7 @@ import GHC.Core.Reduction ( Reduction(..) ) import GHC.Core.Multiplicity import GHC.Core.FamInstEnv( normaliseType ) import GHC.Core.Class ( Class ) -import GHC.Core.Coercion( mkSymCo ) +import GHC.Core.Coercion( mkSymCastCo ) import GHC.Core.Type (mkStrLitTy, mkCastTy) import GHC.Core.TyCo.Ppr( pprTyVars ) import GHC.Core.TyCo.Tidy( tidyOpenTypeX ) @@ -1093,7 +1093,7 @@ chooseInferredQuantifiers residual inferred_theta tau_tvs qtvs -- So, to make the kinds work out, we reverse the cast here. Just (wc_var, wc_co) -> liftZonkM $ writeMetaTyVar wc_var (mkConstraintTupleTy diff_theta - `mkCastTy` mkSymCo wc_co) + `mkCastTy` mkSymCastCo (varType wc_var) wc_co) Nothing -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty) ; traceTc "completeTheta" $ ===================================== compiler/GHC/Tc/Gen/HsType.hs ===================================== @@ -1696,7 +1696,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args do { let arrows_needed = n_initial_val_args all_args ; co <- matchExpectedFunKind (HsTypeRnThing $ unLoc hs_ty) arrows_needed substed_fun_ki - ; fun' <- liftZonkM $ zonkTcType (fun `mkCastTy` co) + ; fun' <- liftZonkM $ zonkTcType (fun `mkCastTyCo` co) -- This zonk is essential, to expose the fruits -- of matchExpectedFunKind to the 'go' loop @@ -1963,7 +1963,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind ; traceTc "checkExpectedKind" (vcat [ ppr act_kind , ppr exp_kind , ppr co_k ]) - ; return (res_ty `mkCastTy` co_k) } } + ; return (res_ty `mkCastTyCo` co_k) } } where -- We need to make sure that both kinds have the same number of implicit -- foralls and constraints out front. If the actual kind has more, instantiate @@ -1986,7 +1986,7 @@ checkExpKind _rn_ty ty ki (Infer cell) = do -- NB: do not instantiate. -- See Note [Do not always instantiate eagerly in types] co <- fillInferResultNoInst ki cell - pure (ty `mkCastTy` co) + pure (ty `mkCastTyCo` co) --------------------------- ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -359,11 +359,11 @@ can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 can_eq_nc rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 | isNothing (canEqLHS_maybe ty2) = -- See (EIK3) in Note [Equalities with heterogeneous kinds] - canEqCast rewritten rdr_env envs ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2 + canEqCast rewritten rdr_env envs ev eq_rel NotSwapped ty1 (castCoToCo (typeKind ty1) co1) ty2 ps_ty2 can_eq_nc rewritten rdr_env envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ | isNothing (canEqLHS_maybe ty1) = -- See (EIK3) in Note [Equalities with heterogeneous kinds] - canEqCast rewritten rdr_env envs ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1 + canEqCast rewritten rdr_env envs ev eq_rel IsSwapped ty2 (castCoToCo (typeKind ty2) co2) ty1 ps_ty1 ---------------------- -- Otherwise try to decompose @@ -522,7 +522,7 @@ can_eq_nc_forall ev eq_rel s1 s2 (substTy subst2 (tyVarKind tv2)) ; let subst2' = extendTvSubstAndInScope subst2 tv2 - (mkCastTy (mkTyVarTy skol_tv) kind_co) + (mkCastTyCo (mkTyVarTy skol_tv) kind_co) -- skol_tv is already in the in-scope set, but the -- free vars of kind_co are not; hence "...AndInScope" ; co <- go uenv skol_tvs subst2' bndrs1 bndrs2 @@ -1741,7 +1741,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -- kind_co :: ki2 ~N ki1 lhs_redn = mkReflRedn role ps_xi1 rhs_redn = mkGReflRightRedn role xi2 kind_co - new_xi2 = mkCastTy ps_xi2 kind_co + new_xi2 = mkCastTyCo ps_xi2 kind_co canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs -- or, if swapped: rhs ~ lhs @@ -1753,14 +1753,14 @@ canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 | (xi2', mco) <- split_cast_ty xi2 , Just lhs2 <- canEqLHS_maybe xi2' - = canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 (ps_xi2 `mkCastTyMCo` mkSymMCo mco) mco + = canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 (ps_xi2 `mkCastTy` mkSymCastCo (typeKind xi2') mco) mco | otherwise = canEqCanLHSFinish ev eq_rel swapped lhs1 ps_xi2 where - split_cast_ty (CastTy ty co) = (ty, MCo co) - split_cast_ty other = (other, MRefl) + split_cast_ty (CastTy ty co) = (ty, co) + split_cast_ty other = (other, ReflCastCo) -- This function deals with the case that both LHS and RHS are potential -- CanEqLHSs. @@ -1771,7 +1771,7 @@ canEqCanLHS2 :: CtEvidence -- lhs ~ (rhs |> mco) -> TcType -- pretty lhs -> CanEqLHS -- rhs -> TcType -- pretty rhs - -> MCoercion -- :: kind(rhs) ~N kind(lhs) + -> CastCoercion -- :: kind(rhs) ~N kind(lhs) -> TcS (StopOrContinue (Either IrredCt EqCt)) canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco | lhs1 `eqCanEqLHS` lhs2 @@ -1823,13 +1823,13 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco then finish_with_swapping else finish_without_swapping } where - sym_mco = mkSymMCo mco + sym_mco = mkSymCastCo (canEqLHSKind lhs2) mco role = eqRelRole eq_rel lhs1_ty = canEqLHSType lhs1 lhs2_ty = canEqLHSType lhs2 finish_without_swapping - = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTyMCo` mco) + = canEqCanLHSFinish ev eq_rel swapped lhs1 (ps_xi2 `mkCastTy` mco) -- Swapping. We have ev : lhs1 ~ lhs2 |> co -- We swap to new_ev : lhs2 ~ lhs1 |> sym co @@ -1840,7 +1840,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco = do { let lhs1_redn = mkGReflRightMRedn role lhs1_ty sym_mco lhs2_redn = mkGReflLeftMRedn role lhs2_ty mco ; new_ev <-rewriteEqEvidence ev swapped lhs1_redn lhs2_redn emptyCoHoleSet - ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTyMCo` sym_mco) } + ; canEqCanLHSFinish new_ev eq_rel IsSwapped lhs2 (ps_xi1 `mkCastTy` sym_mco) } put_tyvar_on_lhs = isWanted ev && eq_rel == NomEq -- See Note [Orienting TyVarLHS/TyFamLHS] ===================================== compiler/GHC/Tc/Solver/Rewrite.hs ===================================== @@ -561,8 +561,9 @@ rewrite_one ty@(ForAllTy {}) ; redn <- rewrite_one rho ; return $ mkHomoForAllRedn bndrs redn } -rewrite_one (CastTy ty g) +rewrite_one (CastTy ty cco) = do { redn <- rewrite_one ty + ; let g = castCoToCo (typeKind ty) cco ; g' <- rewrite_co g ; role <- getRole ; return $ mkCastRedn1 role ty g' redn } ===================================== compiler/GHC/Tc/TyCl/Utils.hs ===================================== @@ -37,7 +37,7 @@ import GHC.Builtin.Uniques ( mkBuiltinUnique ) import GHC.Hs -import GHC.Core.TyCo.Rep( Type(..), Coercion(..), MCoercion(..) ) +import GHC.Core.TyCo.Rep( Type(..), Coercion(..), MCoercion(..), CastCoercion(..) ) import GHC.Core.Multiplicity import GHC.Core.Predicate import GHC.Core.Make( rEC_SEL_ERROR_ID ) @@ -101,7 +101,7 @@ synonymTyConsOfType ty go (AppTy a b) = go a `plusNameEnv` go b go (FunTy _ w a b) = go w `plusNameEnv` go a `plusNameEnv` go b go (ForAllTy _ ty) = go ty - go (CastTy ty co) = go ty `plusNameEnv` go_co co + go (CastTy ty co) = go ty `plusNameEnv` go_cast_co co go (CoercionTy co) = go_co co -- Note [TyCon cycles through coercions?!] @@ -128,6 +128,10 @@ synonymTyConsOfType ty go_mco MRefl = emptyNameEnv go_mco (MCo co) = go_co co + go_cast_co ReflCastCo = emptyNameEnv + go_cast_co (CCoercion co) = go_co co + go_cast_co (ZCoercion ty _) = go ty + go_co (Refl ty) = go ty go_co (GRefl _ ty mco) = go ty `plusNameEnv` go_mco mco go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs ===================================== compiler/GHC/Tc/Utils/Instantiate.hs ===================================== @@ -331,7 +331,7 @@ instTyVarsWith orig tvs tys = go (extendTvSubstAndInScope subst tv ty) tvs tys | otherwise = do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind - ; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys } + ; go (extendTvSubstAndInScope subst tv (ty `mkCastTyCo` co)) tvs tys } where tv_kind = substTy subst (tyVarKind tv) ty_kind = typeKind ty ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -1435,7 +1435,7 @@ collect_cand_qtvs orig_ty is_dep cur_lvl bound dvs ty go dv (FunTy _ w arg res) = foldlM go dv [w, arg, res] go dv (LitTy {}) = return dv go dv (CastTy ty co) = do { dv1 <- go dv ty - ; collect_cand_qtvs_co orig_ty cur_lvl bound dv1 co } + ; collect_cand_qtvs_cast_co orig_ty cur_lvl bound dv1 co } go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty cur_lvl bound dv co go dv (TyVarTy tv) @@ -1516,6 +1516,18 @@ collect_cand_qtvs orig_ty is_dep cur_lvl bound dvs ty -- See Note [Recurring into kinds for candidateQTyVars] ; collect_cand_qtvs orig_ty True cur_lvl bound dv' tv_kind } } +collect_cand_qtvs_cast_co :: TcType -- original type at top of recursion; for errors + -> TcLevel + -> VarSet -- bound variables + -> CandidatesQTvs -> CastCoercion + -> TcM CandidatesQTvs +collect_cand_qtvs_cast_co orig_ty cur_lvl bound dv cco = case cco of + ReflCastCo -> return dv + CCoercion co -> collect_cand_qtvs_co orig_ty cur_lvl bound dv co + ZCoercion ty cos -> do { dv1 <- collect_cand_qtvs orig_ty True cur_lvl bound dv ty + ; foldM (\dv cv -> collect_cand_qtvs_co orig_ty cur_lvl bound dv (CoVarCo cv)) dv1 (nonDetEltsUniqSet cos) -- TODO + } + collect_cand_qtvs_co :: TcType -- original type at top of recursion; for errors -> TcLevel -> VarSet -- bound variables ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -2696,11 +2696,11 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2 -- didn't do it this way, and then the unification above was deferred. go (CastTy t1 co1) t2 = do { co_tys <- uType env t1 t2 - ; return (mkCoherenceLeftCo role t1 co1 co_tys) } + ; return (mkCoherenceLeftCo role t1 (castCoToCo (typeKind t1) co1) co_tys) } go t1 (CastTy t2 co2) = do { co_tys <- uType env t1 t2 - ; return (mkCoherenceRightCo role t2 co2 co_tys) } + ; return (mkCoherenceRightCo role t2 (castCoToCo (typeKind t2) co2) co_tys) } -- Variables; go for uUnfilledVar -- Note that we pass in *original* (before synonym expansion), @@ -3484,7 +3484,7 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs where lhs_info = metaTyVarInfo lhs_tv - !(occ_in_ty, occ_in_co) = mkOccFolders (tyVarName lhs_tv) + !(occ_in_ty, occ_in_co, occ_in_cast_co) = mkOccFolders (tyVarName lhs_tv) lhs_tv_lvl = tcTyVarLevel lhs_tv lhs_tv_is_concrete = isConcreteTyVar lhs_tv @@ -3525,17 +3525,17 @@ simpleUnifyCheck caller given_eq_lvl lhs_tv rhs | otherwise = False rhs_is_ok (AppTy t1 t2) = rhs_is_ok t1 && rhs_is_ok t2 - rhs_is_ok (CastTy ty co) = not (occ_in_co co) && rhs_is_ok ty + rhs_is_ok (CastTy ty co) = not (occ_in_cast_co co) && rhs_is_ok ty rhs_is_ok (CoercionTy co) = not (occ_in_co co) rhs_is_ok (LitTy {}) = True -mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool) +mkOccFolders :: Name -> (TcType -> Bool, TcCoercion -> Bool, TcCastCoercion -> Bool) -- These functions return True -- * if lhs_tv occurs (incl deeply, in the kind of variable) -- * if there is a coercion hole -- No expansion of type synonyms -mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co) +mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co, getAny . check_cast_co) where !(check_ty, _, check_co, _) = foldTyCo occ_folder emptyVarSet occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms @@ -3549,6 +3549,11 @@ mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co) do_bndr is tcv _faf = extendVarSet is tcv do_hole _is _hole = DM.Any True -- Reject coercion holes + check_cast_co ReflCastCo = Any False + check_cast_co (CCoercion co) = check_co co + check_cast_co (ZCoercion _ty _cos) = error "AMG TODO check_cast_co" + + {- ********************************************************************* * * Equality invariant checking @@ -4144,7 +4149,7 @@ check_ty_eq_rhs flags ty ; return (mkAppRedn <$> fun_res <*> arg_res) } CastTy ty co -> do { ty_res <- check_ty_eq_rhs flags ty - ; co_res <- checkCo flags co + ; co_res <- checkCo flags (castCoToCo (typeKind ty) co) ; return (mkCastRedn1 Nominal ty <$> co_res <*> ty_res) } CoercionTy co -> do { co_res <- checkCo flags co @@ -4540,7 +4545,7 @@ simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv | otherwise = TyVarCheck_Success where - (check_kind, _) = mkOccFolders lhs_tv + (check_kind, _, _) = mkOccFolders lhs_tv ------------------------- tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/85e0e01f31532219cb8f4a808b84d5a2... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/85e0e01f31532219cb8f4a808b84d5a2... You're receiving this email because of your account on gitlab.haskell.org.