Commit 1c6d70c2 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Kill off zipTopTCvSubst in favour of zipOpenTCvSubst

As Bartosz has discovered, the invariants for substitutions were
wrong, and in particular the "mkTop...Subst" and "zipTop..Subst"
functions were building substitutions that didn't obey even the
old invariants.

This patch kills of the bogus zipTopTCvSubst in favour of the
more robust zipOpenTCvSubst.

I tripped over this because my upcoming patch (concerning SetLevels,
Trac #11330) triggered an ASSERT failure in the substitution
well-formedness assertion in TyCoRep.
parent 47b3f588
...@@ -712,7 +712,7 @@ mkOneConFull x usupply con = (con_abs, constraints) ...@@ -712,7 +712,7 @@ mkOneConFull x usupply con = (con_abs, constraints)
Just (tc, tys) -> ASSERT( tc == data_tc ) tys Just (tc, tys) -> ASSERT( tc == data_tc ) tys
Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty) Nothing -> pprPanic "mkOneConFull: Not TyConApp:" (ppr res_ty)
subst1 = zipTopTCvSubst univ_tvs tc_args subst1 = zipOpenTCvSubst univ_tvs tc_args
(subst, ex_tvs') = cloneTyVarBndrs subst1 ex_tvs usupply1 (subst, ex_tvs') = cloneTyVarBndrs subst1 ex_tvs usupply1
......
...@@ -157,7 +157,7 @@ mkDataConStupidTheta tycon arg_tys univ_tvs ...@@ -157,7 +157,7 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
| null stupid_theta = [] -- The common case | null stupid_theta = [] -- The common case
| otherwise = filter in_arg_tys stupid_theta | otherwise = filter in_arg_tys stupid_theta
where where
tc_subst = zipTopTCvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs) tc_subst = zipOpenTCvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
stupid_theta = substTheta tc_subst (tyConStupidTheta tycon) stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
-- Start by instantiating the master copy of the -- Start by instantiating the master copy of the
-- stupid theta, taken from the TyCon -- stupid theta, taken from the TyCon
...@@ -205,8 +205,8 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder ...@@ -205,8 +205,8 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
(ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy cont_sigma (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy cont_sigma
(arg_tys1, _) = tcSplitFunTys cont_tau (arg_tys1, _) = tcSplitFunTys cont_tau
twiddle = char '~' twiddle = char '~'
subst = zipTopTCvSubst (univ_tvs1 ++ ex_tvs1) subst = zipOpenTCvSubst (univ_tvs1 ++ ex_tvs1)
(mkTyVarTys (univ_tvs ++ ex_tvs)) (mkTyVarTys (univ_tvs ++ ex_tvs))
------------------------------------------------------ ------------------------------------------------------
type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type)) type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type))
......
...@@ -1008,7 +1008,7 @@ inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args ...@@ -1008,7 +1008,7 @@ inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args
stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $ stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $
substTheta tc_subst (tyConStupidTheta rep_tc) substTheta tc_subst (tyConStupidTheta rep_tc)
tc_subst = ASSERT( equalLength rep_tc_tvs all_rep_tc_args ) tc_subst = ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
zipTopTCvSubst rep_tc_tvs all_rep_tc_args zipOpenTCvSubst rep_tc_tvs all_rep_tc_args
-- Extra Data constraints -- Extra Data constraints
-- The Data class (only) requires that for -- The Data class (only) requires that for
...@@ -1889,7 +1889,7 @@ simplifyDeriv pred tvs theta ...@@ -1889,7 +1889,7 @@ simplifyDeriv pred tvs theta
; let min_theta = mkMinimalBySCs (bagToList good) ; let min_theta = mkMinimalBySCs (bagToList good)
subst_skol = zipTopTCvSubst tvs_skols $ mkTyVarTys tvs subst_skol = zipOpenTCvSubst tvs_skols $ mkTyVarTys tvs
-- The reverse substitution (sigh) -- The reverse substitution (sigh)
; return (substTheta subst_skol min_theta) } ; return (substTheta subst_skol min_theta) }
......
...@@ -647,7 +647,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside ...@@ -647,7 +647,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
; checkExistentials ex_tvs all_arg_tys penv ; checkExistentials ex_tvs all_arg_tys penv
; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
(zipTopTCvSubst univ_tvs ctxt_res_tys) ex_tvs (zipOpenTCvSubst univ_tvs ctxt_res_tys) ex_tvs
-- Get location from monad, not from ex_tvs -- Get location from monad, not from ex_tvs
; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
......
...@@ -142,7 +142,7 @@ module TcType ( ...@@ -142,7 +142,7 @@ module TcType (
-- Type substitutions -- Type substitutions
TCvSubst(..), -- Representation visible to a few friends TCvSubst(..), -- Representation visible to a few friends
TvSubstEnv, emptyTCvSubst, TvSubstEnv, emptyTCvSubst,
mkOpenTCvSubst, zipOpenTCvSubst, zipTopTCvSubst, mkOpenTCvSubst, zipOpenTCvSubst,
mkTopTCvSubst, notElemTCvSubst, unionTCvSubst, mkTopTCvSubst, notElemTCvSubst, unionTCvSubst,
getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope, getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr, Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
...@@ -1740,7 +1740,7 @@ transSuperClasses p ...@@ -1740,7 +1740,7 @@ transSuperClasses p
immSuperClasses :: Class -> [Type] -> [PredType] immSuperClasses :: Class -> [Type] -> [PredType]
immSuperClasses cls tys immSuperClasses cls tys
= substTheta (zipTopTCvSubst tyvars tys) sc_theta = substTheta (zipOpenTCvSubst tyvars tys) sc_theta
where where
(tyvars,sc_theta,_,_) = classBigSig cls (tyvars,sc_theta,_,_) = classBigSig cls
......
...@@ -84,7 +84,7 @@ module TyCoRep ( ...@@ -84,7 +84,7 @@ module TyCoRep (
unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet, unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
mkOpenTCvSubst, zipOpenTCvSubst, zipOpenTCvSubstCoVars, mkOpenTCvSubst, zipOpenTCvSubst, zipOpenTCvSubstCoVars,
zipOpenTCvSubstBinders, zipOpenTCvSubstBinders,
mkTopTCvSubst, zipTopTCvSubst, mkTopTCvSubst,
substTelescope, substTelescope,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars, substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
...@@ -1656,33 +1656,35 @@ mkOpenTCvSubst tenv cenv ...@@ -1656,33 +1656,35 @@ mkOpenTCvSubst tenv cenv
-- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
-- environment, hence "open". No CoVars, please! -- environment, hence "open". No CoVars, please!
zipOpenTCvSubst :: [TyVar] -> [Type] -> TCvSubst zipOpenTCvSubst :: [TyVar] -> [Type] -> TCvSubst
zipOpenTCvSubst tyvars tys zipOpenTCvSubst tvs tys
| debugIsOn && (length tyvars /= length tys) | debugIsOn
= pprTrace "zipOpenTCvSubst" (ppr tyvars $$ ppr tys) emptyTCvSubst , not (all isTyVar tvs) || length tvs /= length tys
= pprTrace "zipOpenTCvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst
| otherwise | otherwise
= TCvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv emptyCvSubstEnv = TCvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv emptyCvSubstEnv
where tenv = zipTyEnv tyvars tys where
tenv = zipTyEnv tvs tys
-- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
-- environment, hence "open". -- environment, hence "open". No TyVars, please!
zipOpenTCvSubstCoVars :: [CoVar] -> [Coercion] -> TCvSubst zipOpenTCvSubstCoVars :: [CoVar] -> [Coercion] -> TCvSubst
zipOpenTCvSubstCoVars cvs cos zipOpenTCvSubstCoVars cvs cos
| debugIsOn && (length cvs /= length cos) | debugIsOn
, not (all isCoVar cvs) || length cvs /= length cos
= pprTrace "zipOpenTCvSubstCoVars" (ppr cvs $$ ppr cos) emptyTCvSubst = pprTrace "zipOpenTCvSubstCoVars" (ppr cvs $$ ppr cos) emptyTCvSubst
| otherwise | otherwise
= TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv = TCvSubst (mkInScopeSet (tyCoVarsOfCos cos)) emptyTvSubstEnv cenv
where cenv = zipCoEnv cvs cos where
cenv = zipCoEnv cvs cos
-- | Create an open TCvSubst combining the binders and types provided. -- | Create an open TCvSubst combining the binders and types provided.
-- NB: It is OK if the lists are of different lengths. -- NB: It is specifically OK if the lists are of different lengths.
zipOpenTCvSubstBinders :: [TyBinder] -> [Type] -> TCvSubst zipOpenTCvSubstBinders :: [TyBinder] -> [Type] -> TCvSubst
zipOpenTCvSubstBinders bndrs tys zipOpenTCvSubstBinders bndrs tys
= TCvSubst is tenv emptyCvSubstEnv = TCvSubst is tenv emptyCvSubstEnv
where where
is = mkInScopeSet (tyCoVarsOfTypes tys) is = mkInScopeSet (tyCoVarsOfTypes tys)
(tvs, tys') = unzip [ (tv, ty) | (Named tv _, ty) <- zip bndrs tys ] tenv = mkVarEnv [ (tv, ty) | (Named tv _, ty) <- zip bndrs tys ]
tenv = zipTyEnv tvs tys'
-- | Called when doing top-level substitutions. Here we expect that the -- | Called when doing top-level substitutions. Here we expect that the
-- free vars of the range of the substitution will be empty. -- free vars of the range of the substitution will be empty.
...@@ -1691,15 +1693,6 @@ mkTopTCvSubst prs = TCvSubst emptyInScopeSet tenv cenv ...@@ -1691,15 +1693,6 @@ mkTopTCvSubst prs = TCvSubst emptyInScopeSet tenv cenv
where (tenv, cenv) = foldl extend (emptyTvSubstEnv, emptyCvSubstEnv) prs where (tenv, cenv) = foldl extend (emptyTvSubstEnv, emptyCvSubstEnv) prs
extend envs (v, ty) = extendSubstEnvs envs v ty extend envs (v, ty) = extendSubstEnvs envs v ty
-- | Makes a subst with an empty in-scope-set. No CoVars, please!
zipTopTCvSubst :: [TyVar] -> [Type] -> TCvSubst
zipTopTCvSubst tyvars tys
| debugIsOn && (length tyvars /= length tys)
= pprTrace "zipTopTCvSubst" (ppr tyvars $$ ppr tys) emptyTCvSubst
| otherwise
= TCvSubst emptyInScopeSet tenv emptyCvSubstEnv
where tenv = zipTyEnv tyvars tys
zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv zipTyEnv :: [TyVar] -> [Type] -> TvSubstEnv
zipTyEnv tyvars tys zipTyEnv tyvars tys
= ASSERT( all (not . isCoercionTy) tys ) = ASSERT( all (not . isCoercionTy) tys )
......
...@@ -150,7 +150,7 @@ module Type ( ...@@ -150,7 +150,7 @@ module Type (
-- ** Manipulating type substitutions -- ** Manipulating type substitutions
emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst, emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
mkTCvSubst, mkOpenTCvSubst, zipOpenTCvSubst, zipTopTCvSubst, mkTopTCvSubst, mkTCvSubst, mkOpenTCvSubst, zipOpenTCvSubst, mkTopTCvSubst,
notElemTCvSubst, notElemTCvSubst,
getTvSubstEnv, setTvSubstEnv, getTvSubstEnv, setTvSubstEnv,
zapTCvSubst, getTCvInScope, zapTCvSubst, getTCvInScope,
...@@ -1810,7 +1810,7 @@ mkFamilyTyConApp tc tys ...@@ -1810,7 +1810,7 @@ mkFamilyTyConApp tc tys
| Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
, let tvs = tyConTyVars tc , let tvs = tyConTyVars tc
fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys ) fam_subst = ASSERT2( length tvs == length tys, ppr tc <+> ppr tys )
zipTopTCvSubst tvs tys zipOpenTCvSubst tvs tys
= mkTyConApp fam_tc (substTys fam_subst fam_tys) = mkTyConApp fam_tc (substTys fam_subst fam_tys)
| otherwise | otherwise
= mkTyConApp tc tys = mkTyConApp tc tys
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment