summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/basicTypes/MkId.hs2
-rw-r--r--compiler/basicTypes/VarEnv.hs4
-rw-r--r--compiler/coreSyn/CoreSubst.hs2
-rw-r--r--compiler/coreSyn/CoreUtils.hs4
-rw-r--r--compiler/iface/BuildTyCl.hs2
-rw-r--r--compiler/typecheck/Inst.hs9
-rw-r--r--compiler/typecheck/TcClassDcl.hs4
-rw-r--r--compiler/typecheck/TcExpr.hs2
-rw-r--r--compiler/typecheck/TcFlatten.hs2
-rw-r--r--compiler/typecheck/TcHsType.hs4
-rw-r--r--compiler/typecheck/TcInteract.hs4
-rw-r--r--compiler/typecheck/TcMType.hs25
-rw-r--r--compiler/typecheck/TcPatSyn.hs2
-rw-r--r--compiler/typecheck/TcSMonad.hs6
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs2
-rw-r--r--compiler/typecheck/TcType.hs1
-rw-r--r--compiler/types/FamInstEnv.hs2
-rw-r--r--compiler/types/TyCoRep.hs96
-rw-r--r--compiler/types/Type.hs3
-rw-r--r--compiler/utils/UniqFM.hs3
20 files changed, 128 insertions, 51 deletions
diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 27e9dc1d17..6876956267 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -730,7 +730,7 @@ dataConArgUnpack arg_ty
[(DataAlt con, rep_ids, body)]
; return (rep_ids, unbox_fn) }
, Boxer $ \ subst ->
- do { rep_ids <- mapM (newLocal . TcType.substTy subst) rep_tys
+ do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
; return (rep_ids, Var (dataConWorkId con)
`mkTyApps` (substTys subst tc_args)
`mkVarApps` rep_ids ) } ) )
diff --git a/compiler/basicTypes/VarEnv.hs b/compiler/basicTypes/VarEnv.hs
index 0fa0f57616..08eabee7cb 100644
--- a/compiler/basicTypes/VarEnv.hs
+++ b/compiler/basicTypes/VarEnv.hs
@@ -40,6 +40,7 @@ module VarEnv (
extendInScopeSet, extendInScopeSetList, extendInScopeSetSet,
getInScopeVars, lookupInScope, lookupInScope_Directly,
unionInScope, elemInScopeSet, uniqAway,
+ varSetInScope,
-- * The RnEnv2 type
RnEnv2,
@@ -140,6 +141,9 @@ unionInScope :: InScopeSet -> InScopeSet -> InScopeSet
unionInScope (InScope s1 _) (InScope s2 n2)
= InScope (s1 `plusVarEnv` s2) n2
+varSetInScope :: VarSet -> InScopeSet -> Bool
+varSetInScope vars (InScope s1 _) = vars `subVarSet` s1
+
-- | @uniqAway in_scope v@ finds a unique that is not used in the
-- in-scope set, and gives that to v.
uniqAway :: InScopeSet -> Var -> Var
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index 8cc609ddf4..a3ab970cc1 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -600,7 +600,7 @@ substCoVarBndr (Subst in_scope id_env tv_env cv_env) cv
-- | See 'Type.substTy'
substTy :: Subst -> Type -> Type
-substTy subst ty = Type.substTy (getTCvSubst subst) ty
+substTy subst ty = Type.substTyUnchecked (getTCvSubst subst) ty
getTCvSubst :: Subst -> TCvSubst
getTCvSubst (Subst in_scope _ tenv cenv) = TCvSubst in_scope tenv cenv
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 9c2f16c127..59f1d4f868 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -1533,12 +1533,12 @@ dataConInstPat fss uniqs con inst_tys
, new_tv)
where
new_tv = mkTyVar (mkSysTvName uniq fs) kind
- kind = Type.substTy subst (tyVarKind tv)
+ kind = Type.substTyUnchecked subst (tyVarKind tv)
-- Make value vars, instantiating types
arg_ids = zipWith4 mk_id_var id_uniqs id_fss arg_tys arg_strs
mk_id_var uniq fs ty str
- = mkLocalIdOrCoVarWithInfo name (Type.substTy full_subst ty) info
+ = mkLocalIdOrCoVarWithInfo name (Type.substTyUnchecked full_subst ty) info
where
name = mkInternalName uniq (mkVarOccFS fs) noSrcSpan
info | isMarkedStrict str = vanillaIdInfo `setUnfoldingInfo` evaldUnfolding
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 0015e01278..75e8875d59 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -184,7 +184,7 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
-- compatible with the pattern synonym
ASSERT2((and [ univ_tvs `equalLength` univ_tvs1
, ex_tvs `equalLength` ex_tvs1
- , pat_ty `eqType` substTy subst pat_ty1
+ , pat_ty `eqType` substTyUnchecked subst pat_ty1
, prov_theta `eqTypes` substTys subst prov_theta1
, req_theta `eqTypes` substTys subst req_theta1
, arg_tys `eqTypes` substTys subst arg_tys1
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 43f7f1eba7..43cbb48e75 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -137,7 +137,8 @@ deeplySkolemise ty
= do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
; (subst, tvs1) <- tcInstSkolTyVars tvs
; ev_vars1 <- newEvVars (substTheta subst theta)
- ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
+ ; (wrap, tvs2, ev_vars2, rho) <-
+ deeplySkolemise (substTyAddInScope subst ty')
; return ( mkWpLams ids1
<.> mkWpTyLams tvs1
<.> mkWpLams ev_vars1
@@ -178,8 +179,8 @@ top_instantiate inst_all orig ty
| otherwise = ([], theta)
; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs)
; let inst_theta' = substTheta subst inst_theta
- sigma' = substTy subst (mkForAllTys leave_bndrs $
- mkFunTys leave_theta rho)
+ sigma' = substTyAddInScope subst (mkForAllTys leave_bndrs $
+ mkFunTys leave_theta rho)
; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta'
; traceTc "Instantiating"
@@ -227,7 +228,7 @@ deeplyInstantiate orig ty
, text "with" <+> ppr tvs'
, text "args:" <+> ppr ids1
, text "theta:" <+> ppr theta' ])
- ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
+ ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)
; return (mkWpLams ids1
<.> wrap2
<.> wrap1
diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index 4fe42b08a3..6ffe902d0f 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -456,7 +456,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
| Just (rhs_ty, _loc) <- defs
= do { let (subst', pat_tys') = mapAccumL subst_tv inst_subst
(tyConTyVars fam_tc)
- rhs' = substTy subst' rhs_ty
+ rhs' = substTyUnchecked subst' rhs_ty
tcv_set' = tyCoVarsOfTypes pat_tys'
(tv_set', cv_set') = partitionVarSet isTyVar tcv_set'
tvs' = varSetElemsWellScoped tv_set'
@@ -486,7 +486,7 @@ tcATDefault emit_warn loc inst_subst defined_ats (ATI fam_tc defs)
| otherwise
= (extendTCvSubst subst tc_tv ty', ty')
where
- ty' = mkTyVarTy (updateTyVarKind (substTy subst) tc_tv)
+ ty' = mkTyVarTy (updateTyVarKind (substTyUnchecked subst) tc_tv)
warnMissingAT :: Name -> TcM ()
warnMissingAT name
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 125d455701..ad49631f31 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -872,7 +872,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
(con1_tvs `zip` result_inst_tys)
; let rec_res_ty = TcType.substTy result_subst con1_res_ty
- scrut_ty = TcType.substTy scrut_subst con1_res_ty
+ scrut_ty = TcType.substTyUnchecked scrut_subst con1_res_ty
con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
; wrap_res <- tcSubTypeHR (exprCtOrigin expr)
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index f87a302d5c..612f8a691b 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -956,7 +956,7 @@ flatten_one (TyConApp tc tys)
-- Expand type synonyms that mention type families
-- on the RHS; see Note [Flattening synonyms]
| Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
- , let expanded_ty = mkAppTys (substTy (mkTopTCvSubst tenv) rhs) tys'
+ , let expanded_ty = mkAppTys (substTyUnchecked (mkTopTCvSubst tenv) rhs) tys'
= do { mode <- getMode
; let used_tcs = tyConsOfType rhs
; case mode of
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index b301149c6a..76c2977e2d 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -760,7 +760,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
; go emptyTCvSubst ki orig_args n0 [] }
where
go subst fun_kind [] n acc
- = return ( substTy subst fun_kind, reverse acc, [], n )
+ = return ( substTyUnchecked subst fun_kind, reverse acc, [], n )
-- when we call this when checking type family patterns, we really
-- do want to instantiate all invisible arguments. During other
-- typechecking, we don't.
@@ -784,7 +784,7 @@ tc_infer_args mode orig_ty ki mb_kind_info orig_args n0
do { let mode' | isNamedBinder bndr = kindLevel mode
| otherwise = mode
; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
- tc_lhs_type mode' arg (substTy subst $ binderType bndr)
+ tc_lhs_type mode' arg (substTyUnchecked subst $ binderType bndr)
; let subst' = case binderVar_maybe bndr of
Just tv -> extendTCvSubst subst tv arg'
Nothing -> subst
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 8582c7298f..1853cb322f 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1257,7 +1257,7 @@ emitFunDepDeriveds fd_eqns
do_one_eq loc subst (Pair ty1 ty2)
= unifyDerived loc Nominal $
- Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
+ Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
{-
**********************************************************************
@@ -1513,7 +1513,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
(theta', _) <- instFlexiTcS (varSetElems unsubstTvs)
let subst = theta `unionTCvSubst` theta'
- return [ Pair arg (substTy subst ax_arg)
+ return [ Pair arg (substTyUnchecked subst ax_arg)
| case cabr of
Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
_ -> True
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 7ab59be38d..bb31005c01 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -294,7 +294,7 @@ tcInstType inst_tyvars ty
return ([], theta, tau)
(tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
- ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
+ ; let (theta, tau) = tcSplitPhiTy (substTyUnchecked subst rho)
; return (tyvars', theta, tau) }
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
@@ -311,9 +311,10 @@ tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTCvSubst [])
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
- = (extendTCvSubst subst tv (mkTyVarTy new_tv), new_tv)
+ = (extendTCvSubst (extendTCvInScope subst new_tv) tv (mkTyVarTy new_tv)
+ , new_tv)
where
- kind = substTy subst (tyVarKind tv)
+ kind = substTyUnchecked subst (tyVarKind tv)
new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
-- Wrappers
@@ -392,10 +393,13 @@ instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
= do { uniq <- newUnique
; let new_tv = mk_tcv uniq old_name kind
- ; return (extendTCvSubst subst tycovar (mk_ty_co new_tv), new_tv) }
+ ; return (extendTCvSubst (extendTCvInScope subst new_tv) tycovar
+ (mk_ty_co new_tv)
+ , new_tv)
+ }
where
old_name = tyVarName tycovar
- kind = substTy subst (tyVarKind tycovar)
+ kind = substTyUnchecked subst (tyVarKind tycovar)
mk_ty_co v
| isTyVar v = mkTyVarTy v
@@ -687,9 +691,12 @@ newMetaTyVarX subst tyvar
; details <- newMetaDetails info
; let name = mkSystemName uniq (getOccName tyvar)
-- See Note [Name of an instantiated type variable]
- kind = substTy subst (tyVarKind tyvar)
+ kind = substTyUnchecked subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
- ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+ ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
+ (mkTyVarTy new_tv)
+ , new_tv)
+ }
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
@@ -699,7 +706,9 @@ newMetaSigTyVarX subst tyvar
; let name = mkSystemName uniq (getOccName tyvar)
kind = substTy subst (tyVarKind tyvar)
new_tv = mkTcTyVar name kind details
- ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
+ ; return (extendTCvSubst (extendTCvInScope subst new_tv) tyvar
+ (mkTyVarTy new_tv)
+ , new_tv) }
{- Note [Name of an instantiated type variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index c12ca6cba1..0c6d713c3a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -278,7 +278,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details
arg_id <- tcLookupId arg_name
; coi <- unifyType (Just arg_id)
(idType arg_id)
- (substTy subst arg_ty)
+ (substTyUnchecked subst arg_ty)
; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
{- Note [Checking against a pattern signature]
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 0214f135da..44e9a03203 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -2857,7 +2857,7 @@ instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTCvSubst tvs)
where
inst_one subst tv
= do { ty' <- instFlexiTcSHelper (tyVarName tv)
- (substTy subst (tyVarKind tv))
+ (substTyUnchecked subst (tyVarKind tv))
; return (extendTCvSubst subst tv ty', ty') }
instFlexiTcSHelper :: Name -> Kind -> TcM TcType
@@ -3065,8 +3065,8 @@ deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
mkCastTy (mkTyVarTys tvs1) kind_cos
body2' = substTyWith tvs2 tvs1' body2
; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
- ; let phi1 = Type.substTy subst body1
- phi2 = Type.substTy subst body2'
+ ; let phi1 = Type.substTyUnchecked subst body1
+ phi2 = Type.substTyUnchecked subst body2'
skol_info = UnifyForAllSkol phi1
; (ctev, hole_co) <- newWantedEq loc role phi1 phi2
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 2d2c5bb8d8..95f773ea0b 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -999,7 +999,7 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
-- See Note [Type-checking default assoc decls]
; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
- Just subst -> return ( Just (substTy subst rhs_ty, loc) )
+ Just subst -> return ( Just (substTyUnchecked subst rhs_ty, loc) )
Nothing -> failWithTc (defaultAssocKindErr fam_tc)
-- We check for well-formedness and validity later,
-- in checkValidClass
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 2f00be2fe8..1b9ae29d55 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -149,6 +149,7 @@ module TcType (
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
extendTCvSubstList, isInScope, mkTCvSubst, zipTyEnv, zipCoEnv,
Type.substTy, substTys, substTyWith, substTyWithCoVars,
+ substTyAddInScope, substTyUnchecked,
substTheta,
isUnLiftedType, -- Source types are always lifted
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 4b4cc5d2f6..1167ac254c 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -1237,7 +1237,7 @@ normalise_tc_app tc tys
; case expandSynTyCon_maybe tc ntys of
{ Just (tenv, rhs, ntys') ->
do { (co2, ninst_rhs)
- <- normalise_type (substTy (mkTopTCvSubst tenv) rhs)
+ <- normalise_type (substTyUnchecked (mkTopTCvSubst tenv) rhs)
; return $
if isReflCo co2
then (args_co, mkTyConApp tc ntys)
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index c0fc5fe240..bd5745ac5f 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -19,6 +19,7 @@ Note [The Type-related module hierarchy]
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
DeriveTraversable, MultiWayIf #-}
+{-# LANGUAGE ImplicitParams #-}
module TyCoRep (
TyThing(..),
@@ -88,7 +89,7 @@ module TyCoRep (
substTelescope,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
substCoWith,
- substTy,
+ substTy, substTyAddInScope, substTyUnchecked,
substTyWithBinders,
substTys, substTheta,
lookupTyVar, substTyVarBndr,
@@ -144,11 +145,13 @@ import Pair
import UniqSupply
import ListSetOps
import Util
+import UniqFM
-- libraries
import qualified Data.Data as Data hiding ( TyCon )
import Data.List
import Data.IORef ( IORef ) -- for CoercionHole
+import GHC.Stack (CallStack)
{-
%************************************************************************
@@ -1383,6 +1386,7 @@ data TCvSubst
-- See Note [Apply Once]
-- and Note [Extending the TvSubstEnv]
-- and Note [Substituting types and coercions]
+ -- and Note [Generating the in-scope set for a substitution]
-- | A substitution of 'Type's for 'TyVar's
-- and 'Kind's for 'KindVar's
@@ -1454,6 +1458,25 @@ Note that the TvSubstEnv should *never* map a CoVar (built with the Id
constructor) and the CvSubstEnv should *never* map a TyVar. Furthermore,
the range of the TvSubstEnv should *never* include a type headed with
CoercionTy.
+
+Note [Generating the in-scope set for a substitution]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When calling substTy subst ty it should be the case that
+the in-scope set in the substitution is a superset of both:
+
+ * The free vars of the range of the substitution
+ * The free vars of ty minus the domain of the substitution
+
+If we want to substitute [a -> ty1, b -> ty2] I used to
+think it was enough to generate an in-scope set that includes
+fv(ty1,ty2). But that's not enough; we really should also take the
+free vars of the type we are substituting into! Example:
+ (forall b. (a,b,x)) [a -> List b]
+Then if we use the in-scope set {b}, there is a danger we will rename
+the forall'd variable to 'x' by mistake, getting this:
+ (forall x. (List b, x, x))
+
+Breaking this invariant caused the bug from #11371.
-}
emptyTvSubstEnv :: TvSubstEnv
@@ -1588,19 +1611,6 @@ unionTCvSubst (TCvSubst in_scope1 tenv1 cenv1) (TCvSubst in_scope2 tenv2 cenv2)
-- the types given; but it's just a thunk so with a bit of luck
-- it'll never be evaluated
--- Note [Generating the in-scope set for a substitution]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- If we want to substitute [a -> ty1, b -> ty2] I used to
--- think it was enough to generate an in-scope set that includes
--- fv(ty1,ty2). But that's not enough; we really should also take the
--- free vars of the type we are substituting into! Example:
--- (forall b. (a,b,x)) [a -> List b]
--- Then if we use the in-scope set {b}, there is a danger we will rename
--- the forall'd variable to 'x' by mistake, getting this:
--- (forall x. (List b, x, x))
--- Urk! This means looking at all the calls to mkOpenTCvSubst....
-
-
-- | Generates an in-scope set from the free variables in a list of types
-- and a list of coercions
mkTyCoInScopeSet :: [Type] -> [Coercion] -> InScopeSet
@@ -1753,7 +1763,7 @@ substTelescope = go_subst emptyTCvSubst
-- is assumed to be open, see 'zipOpenTCvSubst'
substTyWith :: [TyVar] -> [Type] -> Type -> Type
substTyWith tvs tys = ASSERT( length tvs == length tys )
- substTy (zipOpenTCvSubst tvs tys)
+ substTyUnchecked (zipOpenTCvSubst tvs tys)
-- | Coercion substitution making use of an 'TCvSubst' that
-- is assumed to be open, see 'zipOpenTCvSubst'
@@ -1781,11 +1791,59 @@ substTysWithCoVars cvs cos = ASSERT( length cvs == length cos )
-- simply ignore their matching type.
substTyWithBinders :: [TyBinder] -> [Type] -> Type -> Type
substTyWithBinders bndrs tys = ASSERT( length bndrs == length tys )
- substTy (zipOpenTCvSubstBinders bndrs tys)
+ substTyUnchecked (zipOpenTCvSubstBinders bndrs tys)
+
+-- | Substitute within a 'Type' after adding the free variables of the type
+-- to the in-scope set. This is useful for the case when the free variables
+-- aren't already in the in-scope set or easily available.
+-- See also Note [Generating the in-scope set for a substitution].
+substTyAddInScope :: TCvSubst -> Type -> Type
+substTyAddInScope subst ty =
+ substTy (extendTCvInScopeSet subst $ tyCoVarsOfType ty) ty
+
+-- | When calling `substTy` it should be the case that the in-scope set in
+-- the substitution is a superset of the free vars of the range of the
+-- substitution.
+-- See also Note [Generating the in-scope set for a substitution].
+isValidTCvSubst :: TCvSubst -> Bool
+isValidTCvSubst (TCvSubst in_scope tenv cenv) =
+ (tenvFVs `varSetInScope` in_scope) &&
+ (cenvFVs `varSetInScope` in_scope)
+ where
+ tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
+ cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
-- | Substitute within a 'Type'
-substTy :: TCvSubst -> Type -> Type
-substTy subst ty | isEmptyTCvSubst subst = ty
+-- The substitution has to satisfy the invariants described in
+-- Note [Generating the in-scope set for a substitution].
+substTy :: (?callStack :: CallStack) => TCvSubst -> Type -> Type
+substTy subst@(TCvSubst in_scope tenv cenv) ty
+ | isEmptyTCvSubst subst = ty
+ | otherwise = ASSERT2( isValidTCvSubst subst,
+ text "in_scope" <+> ppr in_scope $$
+ text "tenv" <+> ppr tenv $$
+ text "cenv" <+> ppr cenv $$
+ text "ty" <+> ppr ty )
+ ASSERT2( typeFVsInScope,
+ text "in_scope" <+> ppr in_scope $$
+ text "tenv" <+> ppr tenv $$
+ text "cenv" <+> ppr cenv $$
+ text "ty" <+> ppr ty $$
+ text "needInScope" <+> ppr needInScope )
+ subst_ty subst ty
+ where
+ substDomain = varEnvKeys tenv ++ varEnvKeys cenv
+ needInScope = tyCoVarsOfType ty `delListFromUFM_Directly` substDomain
+ typeFVsInScope = needInScope `varSetInScope` in_scope
+
+-- | Substitute within a 'Type' disabling the sanity checks.
+-- The problems that the sanity checks in substTy catch are described in
+-- Note [Generating the in-scope set for a substitution].
+-- 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.
+substTyUnchecked :: TCvSubst -> Type -> Type
+substTyUnchecked subst ty
+ | isEmptyTCvSubst subst = ty
| otherwise = subst_ty subst ty
-- | Substitute within several 'Type's
@@ -1931,7 +1989,7 @@ lookupCoVar :: TCvSubst -> Var -> Maybe Coercion
lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
substTyVarBndr :: TCvSubst -> TyVar -> (TCvSubst, TyVar)
-substTyVarBndr = substTyVarBndrCallback substTy
+substTyVarBndr = substTyVarBndrCallback substTyUnchecked
-- | Substitute a tyvar in a binding position, returning an
-- extended subst and a new tyvar.
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 94da5f1349..4e67db875a 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -161,6 +161,7 @@ module Type (
-- ** Performing substitution on types and kinds
substTy, substTys, substTyWith, substTysWith, substTheta,
+ substTyAddInScope, substTyUnchecked,
substTyVarBndr, substTyVar, substTyVars,
cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, substTelescope,
@@ -293,7 +294,7 @@ coreView :: Type -> Maybe Type
-- By being non-recursive and inlined, this case analysis gets efficiently
-- joined onto the case analysis that the caller is already doing
coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
- = Just (mkAppTys (substTy (mkTopTCvSubst tenv) rhs) tys')
+ = Just (mkAppTys (substTyUnchecked (mkTopTCvSubst tenv) rhs) tys')
-- Its important to use mkAppTys, rather than (foldl AppTy),
-- because the function part might well return a
-- partially-applied type constructor; indeed, usually will!
diff --git a/compiler/utils/UniqFM.hs b/compiler/utils/UniqFM.hs
index 9d8669ba04..969e1dc10a 100644
--- a/compiler/utils/UniqFM.hs
+++ b/compiler/utils/UniqFM.hs
@@ -48,6 +48,7 @@ module UniqFM (
delFromUFM,
delFromUFM_Directly,
delListFromUFM,
+ delListFromUFM_Directly,
plusUFM,
plusUFM_C,
plusUFM_CD,
@@ -138,6 +139,7 @@ adjustUFM_Directly :: (elt -> elt) -> UniqFM elt -> Unique -> UniqFM elt
delFromUFM :: Uniquable key => UniqFM elt -> key -> UniqFM elt
delListFromUFM :: Uniquable key => UniqFM elt -> [key] -> UniqFM elt
+delListFromUFM_Directly :: UniqFM elt -> [Unique] -> UniqFM elt
delFromUFM_Directly :: UniqFM elt -> Unique -> UniqFM elt
-- Bindings in right argument shadow those in the left
@@ -252,6 +254,7 @@ adjustUFM_Directly f (UFM m) u = UFM (M.adjust f (getKey u) m)
delFromUFM (UFM m) k = UFM (M.delete (getKey $ getUnique k) m)
delListFromUFM = foldl delFromUFM
delFromUFM_Directly (UFM m) u = UFM (M.delete (getKey u) m)
+delListFromUFM_Directly = foldl delFromUFM_Directly
-- M.union is left-biased, plusUFM should be right-biased.
plusUFM (UFM x) (UFM y) = UFM (M.union y x)
View Lorry Controller Status