Commit bb956eb8 authored by niteria's avatar niteria

Add asserts to other substitution functions

This adds asserts to `substTys`, `substCo` and `substCos` in
the same spirit as already existing asserts on `substTy`, protecting
every possible entry point to `subst_ty` and `subst_co`.

I've replaced the violators with unchecked versions.

Test Plan: ./validate --slow

Reviewers: simonpj, goldfire, austin, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1862

GHC Trac Issues: #11371
parent bc83c733
...@@ -732,7 +732,7 @@ dataConArgUnpack arg_ty ...@@ -732,7 +732,7 @@ dataConArgUnpack arg_ty
, Boxer $ \ subst -> , Boxer $ \ subst ->
do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
; return (rep_ids, Var (dataConWorkId con) ; return (rep_ids, Var (dataConWorkId con)
`mkTyApps` (substTys subst tc_args) `mkTyApps` (substTysUnchecked subst tc_args)
`mkVarApps` rep_ids ) } ) ) `mkVarApps` rep_ids ) } ) )
| otherwise | otherwise
= pprPanic "dataConArgUnpack" (ppr arg_ty) = pprPanic "dataConArgUnpack" (ppr arg_ty)
......
...@@ -1284,7 +1284,7 @@ lintCoercion (ForAllCo tv1 kind_co co) ...@@ -1284,7 +1284,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co ; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co
; let tyl = mkNamedForAllTy tv1 Invisible t1 ; let tyl = mkNamedForAllTy tv1 Invisible t1
tyr = mkNamedForAllTy tv2 Invisible $ tyr = mkNamedForAllTy tv2 Invisible $
substTyWith [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo kind_co] t2 substTyWithUnchecked [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo kind_co] t2
; return (k3, k4, tyl, tyr, r) } ; return (k3, k4, tyl, tyr, r) }
lintCoercion (CoVarCo cv) lintCoercion (CoVarCo cv)
......
...@@ -97,7 +97,7 @@ exprType (Lit lit) = literalType lit ...@@ -97,7 +97,7 @@ exprType (Lit lit) = literalType lit
exprType (Coercion co) = coercionType co exprType (Coercion co) = coercionType co
exprType (Let bind body) exprType (Let bind body)
| NonRec tv rhs <- bind -- See Note [Type bindings] | NonRec tv rhs <- bind -- See Note [Type bindings]
, Type ty <- rhs = substTyWith [tv] [ty] (exprType body) , Type ty <- rhs = substTyWithUnchecked [tv] [ty] (exprType body)
| otherwise = exprType body | otherwise = exprType body
exprType (Case _ _ ty _) = ty exprType (Case _ _ ty _) = ty
exprType (Cast _ co) = pSnd (coercionKind co) exprType (Cast _ co) = pSnd (coercionKind co)
......
...@@ -628,7 +628,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields ...@@ -628,7 +628,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
-- I'm not bothering to clone the ex_tvs -- I'm not bothering to clone the ex_tvs
; eqs_vars <- mapM newPredVarDs (substTheta subst (eqSpecPreds eq_spec)) ; eqs_vars <- mapM newPredVarDs (substTheta subst (eqSpecPreds eq_spec))
; theta_vars <- mapM newPredVarDs (substTheta subst prov_theta) ; theta_vars <- mapM newPredVarDs (substTheta subst prov_theta)
; arg_ids <- newSysLocalsDs (substTys subst arg_tys) ; arg_ids <- newSysLocalsDs (substTysUnchecked subst arg_tys)
; let field_labels = conLikeFieldLabels con ; let field_labels = conLikeFieldLabels con
val_args = zipWithEqual "dsExpr:RecordUpd" mk_val_arg val_args = zipWithEqual "dsExpr:RecordUpd" mk_val_arg
field_labels arg_ids field_labels arg_ids
......
...@@ -597,7 +597,7 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls ...@@ -597,7 +597,7 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
Just subst Just subst
-> isNothing $ -- Bogus legacy test (Trac #10675) -> isNothing $ -- Bogus legacy test (Trac #10675)
-- See Note [Bogus consistency check] -- See Note [Bogus consistency check]
tcUnifyTys bind_fn (substTys subst rtys1) (substTys subst rtys2) tcUnifyTys bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
where where
trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1 trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs1
......
...@@ -136,7 +136,7 @@ deeplySkolemise ty ...@@ -136,7 +136,7 @@ deeplySkolemise ty
| Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
= do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
; (subst, tvs1) <- tcInstSkolTyVars tvs ; (subst, tvs1) <- tcInstSkolTyVars tvs
; ev_vars1 <- newEvVars (substTheta subst theta) ; ev_vars1 <- newEvVars (substThetaUnchecked subst theta)
; (wrap, tvs2, ev_vars2, rho) <- ; (wrap, tvs2, ev_vars2, rho) <-
deeplySkolemise (substTyAddInScope subst ty') deeplySkolemise (substTyAddInScope subst ty')
; return ( mkWpLams ids1 ; return ( mkWpLams ids1
...@@ -178,7 +178,7 @@ top_instantiate inst_all orig ty ...@@ -178,7 +178,7 @@ top_instantiate inst_all orig ty
| null leave_bndrs = (theta, []) | null leave_bndrs = (theta, [])
| otherwise = ([], theta) | otherwise = ([], theta)
; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs) ; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs)
; let inst_theta' = substTheta subst inst_theta ; let inst_theta' = substThetaUnchecked subst inst_theta
sigma' = substTyAddInScope subst (mkForAllTys leave_bndrs $ sigma' = substTyAddInScope subst (mkForAllTys leave_bndrs $
mkFunTys leave_theta rho) mkFunTys leave_theta rho)
...@@ -221,8 +221,8 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) ...@@ -221,8 +221,8 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
deeplyInstantiate orig ty deeplyInstantiate orig ty
| Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
= do { (subst, tvs') <- newMetaTyVars tvs = do { (subst, tvs') <- newMetaTyVars tvs
; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys) ; ids1 <- newSysLocalIds (fsLit "di") (substTysUnchecked subst arg_tys)
; let theta' = substTheta subst theta ; let theta' = substThetaUnchecked subst theta
; wrap1 <- instCall orig (mkTyVarTys tvs') theta' ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
, text "type" <+> ppr ty , text "type" <+> ppr ty
...@@ -302,7 +302,7 @@ instDFunType :: DFunId -> [DFunInstType] ...@@ -302,7 +302,7 @@ instDFunType :: DFunId -> [DFunInstType]
-- See Note [DFunInstType: instantiating types] in InstEnv -- See Note [DFunInstType: instantiating types] in InstEnv
instDFunType dfun_id dfun_inst_tys instDFunType dfun_id dfun_inst_tys
= do { (subst, inst_tys) <- go emptyTCvSubst dfun_tvs dfun_inst_tys = do { (subst, inst_tys) <- go emptyTCvSubst dfun_tvs dfun_inst_tys
; return (inst_tys, substTheta subst dfun_theta) } ; return (inst_tys, substThetaUnchecked subst dfun_theta) }
where where
(dfun_tvs, dfun_theta, _) = tcSplitSigmaTy (idType dfun_id) (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy (idType dfun_id)
......
...@@ -887,7 +887,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ...@@ -887,7 +887,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
; rbinds' <- tcRecordUpd con1 con1_arg_tys' rbinds ; rbinds' <- tcRecordUpd con1 con1_arg_tys' rbinds
-- STEP 6: Deal with the stupid theta -- STEP 6: Deal with the stupid theta
; let theta' = substTheta scrut_subst (conLikeStupidTheta con1) ; let theta' = substThetaUnchecked scrut_subst (conLikeStupidTheta con1)
; instStupidTheta RecordUpdOrigin theta' ; instStupidTheta RecordUpdOrigin theta'
-- Step 7: make a cast for the scrutinee, in the -- Step 7: make a cast for the scrutinee, in the
...@@ -902,7 +902,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ...@@ -902,7 +902,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
-- Step 8: Check that the req constraints are satisfied -- Step 8: Check that the req constraints are satisfied
-- For normal data constructors req_theta is empty but we must do -- For normal data constructors req_theta is empty but we must do
-- this check for pattern synonyms. -- this check for pattern synonyms.
; let req_theta' = substTheta scrut_subst req_theta ; let req_theta' = substThetaUnchecked scrut_subst req_theta
; req_wrap <- instCallConstraints RecordUpdOrigin req_theta' ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta'
-- Phew! -- Phew!
...@@ -1160,7 +1160,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald ...@@ -1160,7 +1160,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
ASSERT( binderVisibility binder == Specified ) ASSERT( binderVisibility binder == Specified )
do { let kind = tyVarKind tv do { let kind = tyVarKind tv
; ty_arg <- tcHsTypeApp hs_ty_arg kind ; ty_arg <- tcHsTypeApp hs_ty_arg kind
; let insted_ty = substTyWith [tv] [ty_arg] inner_ty ; let insted_ty = substTyWithUnchecked [tv] [ty_arg] inner_ty
; (inner_wrap, args', res_ty) ; (inner_wrap, args', res_ty)
<- go acc_args (n+1) insted_ty args <- go acc_args (n+1) insted_ty args
-- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
......
...@@ -3060,7 +3060,7 @@ deferTcSForAllEq :: Role -- Nominal or Representational ...@@ -3060,7 +3060,7 @@ deferTcSForAllEq :: Role -- Nominal or Representational
deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2) deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
= do { let tvs1' = zipWithEqual "deferTcSForAllEq" = do { let tvs1' = zipWithEqual "deferTcSForAllEq"
mkCastTy (mkTyVarTys tvs1) kind_cos mkCastTy (mkTyVarTys tvs1) kind_cos
body2' = substTyWith tvs2 tvs1' body2 body2' = substTyWithUnchecked tvs2 tvs1' body2
; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1 ; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
; let phi1 = Type.substTyUnchecked subst body1 ; let phi1 = Type.substTyUnchecked subst body1
phi2 = Type.substTyUnchecked subst body2' phi2 = Type.substTyUnchecked subst body2'
......
...@@ -153,7 +153,10 @@ module TcType ( ...@@ -153,7 +153,10 @@ module TcType (
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr, Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
extendTCvSubstList, isInScope, mkTCvSubst, zipTyEnv, zipCoEnv, extendTCvSubstList, isInScope, mkTCvSubst, zipTyEnv, zipCoEnv,
Type.substTy, substTys, substTyWith, substTyWithCoVars, Type.substTy, substTys, substTyWith, substTyWithCoVars,
substTyAddInScope, substTyUnchecked, substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithBindersUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTheta, substTheta,
isUnliftedType, -- Source types are always lifted isUnliftedType, -- Source types are always lifted
......
...@@ -892,7 +892,7 @@ mkLRCo lr co = LRCo lr co ...@@ -892,7 +892,7 @@ mkLRCo lr co = LRCo lr co
-- | Instantiates a 'Coercion'. -- | Instantiates a 'Coercion'.
mkInstCo :: Coercion -> Coercion -> Coercion mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg) mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg)
= substCoWith [tv] [arg] body_co = substCoWithUnchecked [tv] [arg] body_co
mkInstCo co arg = InstCo co arg mkInstCo co arg = InstCo co arg
-- This could work harder to produce Refl coercions, but that would be -- This could work harder to produce Refl coercions, but that would be
...@@ -1721,7 +1721,7 @@ coercionKind co = go co ...@@ -1721,7 +1721,7 @@ coercionKind co = go co
= let Pair _ k2 = go k_co = let Pair _ k2 = go k_co
tv2 = setTyVarKind tv1 k2 tv2 = setTyVarKind tv1 k2
Pair ty1 ty2 = go co Pair ty1 ty2 = go co
ty2' = substTyWith [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co] ty2 in ty2' = substTyWithUnchecked [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co] ty2 in
mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2' mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2'
go (CoVarCo cv) = toPair $ coVarTypes cv go (CoVarCo cv) = toPair $ coVarTypes cv
go (AxiomInstCo ax ind cos) go (AxiomInstCo ax ind cos)
...@@ -1796,7 +1796,7 @@ coercionKindRole = go ...@@ -1796,7 +1796,7 @@ coercionKindRole = go
= let Pair _ k2 = coercionKind k_co = let Pair _ k2 = coercionKind k_co
tv2 = setTyVarKind tv1 k2 tv2 = setTyVarKind tv1 k2
(Pair ty1 ty2, r) = go co (Pair ty1 ty2, r) = go co
ty2' = substTyWith [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co] ty2 in ty2' = substTyWithUnchecked [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co] ty2 in
(mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2', r) (mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2', r)
go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv) go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax) go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
......
...@@ -570,7 +570,7 @@ opt_trans_rule is co1 co2 ...@@ -570,7 +570,7 @@ opt_trans_rule is co1 co2
mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where where
is' = is `extendInScopeSet` tv1 is' = is `extendInScopeSet` tv1
r2' = substCoWith [tv2] [TyVarTy tv1] r2 r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2
-- Push transitivity inside axioms -- Push transitivity inside axioms
opt_trans_rule is co1 co2 opt_trans_rule is co1 co2
......
...@@ -89,7 +89,10 @@ module TyCoRep ( ...@@ -89,7 +89,10 @@ module TyCoRep (
substTelescope, substTelescope,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith, substCoWith,
substTy, substTyAddInScope, substTyUnchecked, substTy, substTyAddInScope,
substTyUnchecked, substTysUnchecked, substThetaUnchecked,
substTyWithBindersUnchecked, substTyWithUnchecked,
substCoUnchecked, substCoWithUnchecked,
substTyWithBinders, substTyWithInScope, substTyWithBinders, substTyWithInScope,
substTys, substTheta, substTys, substTheta,
lookupTyVar, substTyVarBndr, lookupTyVar, substTyVarBndr,
...@@ -1782,8 +1785,23 @@ substTelescope = go_subst emptyTCvSubst ...@@ -1782,8 +1785,23 @@ substTelescope = go_subst emptyTCvSubst
-- | Type substitution, see 'zipTvSubst' -- | Type substitution, see 'zipTvSubst'
substTyWith :: [TyVar] -> [Type] -> Type -> Type substTyWith ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
[TyVar] -> [Type] -> Type -> Type
substTyWith tvs tys = ASSERT( length tvs == length tys ) substTyWith tvs tys = ASSERT( length tvs == length tys )
substTy (zipTvSubst tvs tys)
-- | Type substitution, see 'zipTvSubst'. Disables sanity checks.
-- The problems that the sanity checks in substTy catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substTyUnchecked to
-- substTy and remove this function. Please don't use in new code.
substTyWithUnchecked :: [TyVar] -> [Type] -> Type -> Type
substTyWithUnchecked tvs tys
= ASSERT( length tvs == length tys )
substTyUnchecked (zipTvSubst tvs tys) substTyUnchecked (zipTvSubst tvs tys)
-- | Substitute tyvars within a type using a known 'InScopeSet'. -- | Substitute tyvars within a type using a known 'InScopeSet'.
...@@ -1797,10 +1815,27 @@ substTyWithInScope in_scope tvs tys ty = ...@@ -1797,10 +1815,27 @@ substTyWithInScope in_scope tvs tys ty =
where tenv = zipTyEnv tvs tys where tenv = zipTyEnv tvs tys
-- | Coercion substitution, see 'zipTvSubst' -- | Coercion substitution, see 'zipTvSubst'
substCoWith :: [TyVar] -> [Type] -> Coercion -> Coercion substCoWith ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
[TyVar] -> [Type] -> Coercion -> Coercion
substCoWith tvs tys = ASSERT( length tvs == length tys ) substCoWith tvs tys = ASSERT( length tvs == length tys )
substCo (zipTvSubst tvs tys) substCo (zipTvSubst tvs tys)
-- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
-- The problems that the sanity checks in substCo catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substCoUnchecked to
-- substCo and remove this function. Please don't use in new code.
substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
substCoWithUnchecked tvs tys
= ASSERT( length tvs == length tys )
substCoUnchecked (zipTvSubst tvs tys)
-- | Substitute covars within a type -- | Substitute covars within a type
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos) substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
...@@ -1817,8 +1852,24 @@ substTysWithCoVars cvs cos = ASSERT( length cvs == length cos ) ...@@ -1817,8 +1852,24 @@ substTysWithCoVars cvs cos = ASSERT( length cvs == length cos )
-- | Type substitution using 'Binder's. Anonymous binders -- | Type substitution using 'Binder's. Anonymous binders
-- simply ignore their matching type. -- simply ignore their matching type.
substTyWithBinders :: [TyBinder] -> [Type] -> Type -> Type substTyWithBinders ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
[TyBinder] -> [Type] -> Type -> Type
substTyWithBinders bndrs tys = ASSERT( length bndrs == length tys ) substTyWithBinders bndrs tys = ASSERT( length bndrs == length tys )
substTy (zipTyBinderSubst bndrs tys)
-- | Type substitution using 'Binder's disabling the sanity checks.
-- Anonymous binders simply ignore their matching type.
-- The problems that the sanity checks in substTy catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substTyUnchecked to
-- substTy and remove this function. Please don't use in new code.
substTyWithBindersUnchecked :: [TyBinder] -> [Type] -> Type -> Type
substTyWithBindersUnchecked bndrs tys
= ASSERT( length bndrs == length tys )
substTyUnchecked (zipTyBinderSubst bndrs tys) substTyUnchecked (zipTyBinderSubst bndrs tys)
-- | Substitute within a 'Type' after adding the free variables of the type -- | Substitute within a 'Type' after adding the free variables of the type
...@@ -1841,19 +1892,15 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) = ...@@ -1841,19 +1892,15 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
cenvFVs = tyCoVarsOfCos $ varEnvElts cenv cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
-- | Substitute within a 'Type' -- | This checks if the substitution satisfies the invariant from
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant]. -- Note [The substitution invariant].
checkValidSubst ::
substTy ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0) #if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) => (?callStack :: CallStack) =>
#endif #endif
TCvSubst -> Type -> Type TCvSubst -> [Type] -> [Coercion] -> a -> a
substTy subst@(TCvSubst in_scope tenv cenv) ty checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
| isEmptyTCvSubst subst = ty = ASSERT2( isValidTCvSubst subst,
| otherwise = ASSERT2( isValidTCvSubst subst,
text "in_scope" <+> ppr in_scope $$ text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$ text "tenv" <+> ppr tenv $$
text "tenvFVs" text "tenvFVs"
...@@ -1861,18 +1908,35 @@ substTy subst@(TCvSubst in_scope tenv cenv) ty ...@@ -1861,18 +1908,35 @@ substTy subst@(TCvSubst in_scope tenv cenv) ty
text "cenv" <+> ppr cenv $$ text "cenv" <+> ppr cenv $$
text "cenvFVs" text "cenvFVs"
<+> ppr (tyCoVarsOfCos $ varEnvElts cenv) $$ <+> ppr (tyCoVarsOfCos $ varEnvElts cenv) $$
text "ty" <+> ppr ty ) text "tys" <+> ppr tys $$
ASSERT2( typeFVsInScope, text "cos" <+> ppr cos )
ASSERT2( tysCosFVsInScope,
text "in_scope" <+> ppr in_scope $$ text "in_scope" <+> ppr in_scope $$
text "tenv" <+> ppr tenv $$ text "tenv" <+> ppr tenv $$
text "cenv" <+> ppr cenv $$ text "cenv" <+> ppr cenv $$
text "ty" <+> ppr ty $$ text "tys" <+> ppr tys $$
text "cos" <+> ppr cos $$
text "needInScope" <+> ppr needInScope ) text "needInScope" <+> ppr needInScope )
subst_ty subst ty a
where where
substDomain = varEnvKeys tenv ++ varEnvKeys cenv substDomain = varEnvKeys tenv ++ varEnvKeys cenv
needInScope = tyCoVarsOfType ty `delListFromUFM_Directly` substDomain needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
typeFVsInScope = needInScope `varSetInScope` in_scope `delListFromUFM_Directly` substDomain
tysCosFVsInScope = needInScope `varSetInScope` in_scope
-- | Substitute within a 'Type'
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substTy ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
TCvSubst -> Type -> Type
substTy subst ty
| isEmptyTCvSubst subst = ty
| otherwise = checkValidSubst subst [ty] [] $ subst_ty subst ty
-- | Substitute within a 'Type' disabling the sanity checks. -- | Substitute within a 'Type' disabling the sanity checks.
-- The problems that the sanity checks in substTy catch are described in -- The problems that the sanity checks in substTy catch are described in
...@@ -1885,14 +1949,48 @@ substTyUnchecked subst ty ...@@ -1885,14 +1949,48 @@ substTyUnchecked subst ty
| otherwise = subst_ty subst ty | otherwise = subst_ty subst ty
-- | Substitute within several 'Type's -- | Substitute within several 'Type's
substTys :: TCvSubst -> [Type] -> [Type] -- The substitution has to satisfy the invariants described in
substTys subst tys | isEmptyTCvSubst subst = tys -- Note [The substitution invariant].
substTys ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
TCvSubst -> [Type] -> [Type]
substTys subst tys
| isEmptyTCvSubst subst = tys
| otherwise = checkValidSubst subst tys [] $ map (subst_ty subst) tys
-- | Substitute within several 'Type's disabling the sanity checks.
-- The problems that the sanity checks in substTys catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substTysUnchecked to
-- substTys and remove this function. Please don't use in new code.
substTysUnchecked :: TCvSubst -> [Type] -> [Type]
substTysUnchecked subst tys
| isEmptyTCvSubst subst = tys
| otherwise = map (subst_ty subst) tys | otherwise = map (subst_ty subst) tys
-- | Substitute within a 'ThetaType' -- | Substitute within a 'ThetaType'
substTheta :: TCvSubst -> ThetaType -> ThetaType -- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
substTheta ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
TCvSubst -> ThetaType -> ThetaType
substTheta = substTys substTheta = substTys
-- | Substitute within a 'ThetaType' disabling the sanity checks.
-- The problems that the sanity checks in substTys catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substThetaUnchecked to
-- substTheta and remove this function. Please don't use in new code.
substThetaUnchecked :: TCvSubst -> ThetaType -> ThetaType
substThetaUnchecked = substTysUnchecked
subst_ty :: TCvSubst -> Type -> Type subst_ty :: TCvSubst -> Type -> Type
-- subst_ty is the main workhorse for type substitution -- subst_ty is the main workhorse for type substitution
-- --
...@@ -1911,7 +2009,7 @@ subst_ty subst ty ...@@ -1911,7 +2009,7 @@ subst_ty subst ty
go (ForAllTy (Anon arg) res) go (ForAllTy (Anon arg) res)
= (ForAllTy $! (Anon $! go arg)) $! go res = (ForAllTy $! (Anon $! go arg)) $! go res
go (ForAllTy (Named tv vis) ty) go (ForAllTy (Named tv vis) ty)
= case substTyVarBndr subst tv of = case substTyVarBndrUnchecked subst tv of
(subst', tv') -> (subst', tv') ->
(ForAllTy $! ((Named $! tv') vis)) $! (ForAllTy $! ((Named $! tv') vis)) $!
(subst_ty subst' ty) (subst_ty subst' ty)
...@@ -1936,14 +2034,40 @@ lookupTyVar (TCvSubst _ tenv _) tv ...@@ -1936,14 +2034,40 @@ lookupTyVar (TCvSubst _ tenv _) tv
lookupVarEnv tenv tv lookupVarEnv tenv tv
-- | Substitute within a 'Coercion' -- | Substitute within a 'Coercion'
substCo :: TCvSubst -> Coercion -> Coercion -- The substitution has to satisfy the invariants described in
substCo subst co | isEmptyTCvSubst subst = co -- Note [The substitution invariant].
substCo ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
TCvSubst -> Coercion -> Coercion
substCo subst co
| isEmptyTCvSubst subst = co
| otherwise = checkValidSubst subst [] [co] $ subst_co subst co
-- | Substitute within a 'Coercion' disabling sanity checks.
-- The problems that the sanity checks in substCo catch are described in
-- Note [The substitution invariant].
-- The goal of #11371 is to migrate all the calls of substCoUnchecked to
-- substCo and remove this function. Please don't use in new code.
substCoUnchecked :: TCvSubst -> Coercion -> Coercion
substCoUnchecked subst co
| isEmptyTCvSubst subst = co
| otherwise = subst_co subst co | otherwise = subst_co subst co
-- | Substitute within several 'Coercion's -- | Substitute within several 'Coercion's
substCos :: TCvSubst -> [Coercion] -> [Coercion] -- The substitution has to satisfy the invariants described in
substCos subst cos | isEmptyTCvSubst subst = cos -- Note [The substitution invariant].
| otherwise = map (substCo subst) cos substCos ::
-- CallStack wasn't present in GHC 7.10.1, disable callstacks in stage 1
#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
(?callStack :: CallStack) =>
#endif
TCvSubst -> [Coercion] -> [Coercion]
substCos subst cos
| isEmptyTCvSubst subst = cos
| otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
subst_co :: TCvSubst -> Coercion -> Coercion subst_co :: TCvSubst -> Coercion -> Coercion
subst_co subst co subst_co subst co
...@@ -1958,7 +2082,7 @@ subst_co subst co ...@@ -1958,7 +2082,7 @@ subst_co subst co
in args' `seqList` mkTyConAppCo r tc args' in args' `seqList` mkTyConAppCo r tc args'
go (AppCo co arg) = (mkAppCo $! go co) $! go arg go (AppCo co arg) = (mkAppCo $! go co) $! go arg
go (ForAllCo tv kind_co co) go (ForAllCo tv kind_co co)
= case substForAllCoBndr subst tv kind_co of { (subst', tv', kind_co') -> = case substForAllCoBndrUnchecked subst tv kind_co of { (subst', tv', kind_co') ->
((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co } ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co }
go (CoVarCo cv) = substCoVar subst cv go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
...@@ -1989,6 +2113,15 @@ substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion ...@@ -1989,6 +2113,15 @@ substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion