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.

7 files changed, 25 insertions, 32 deletions

diff --git a/compiler/deSugar/Check.hs b/compiler/deSugar/Check.hs
index de53a4af6e..38626a486a 100644
--- a/compiler/deSugar/Check.hs
+++ b/compiler/deSugar/Check.hs
@@ -712,7 +712,7 @@ mkOneConFull x usupply con = (con_abs, constraints)
                  Just (tc, tys) -> ASSERT( tc == data_tc ) tys
                  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
 
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 699fd5d366..d13d38e6ff 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -157,7 +157,7 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
   | null stupid_theta = []      -- The common case
   | otherwise         = filter in_arg_tys stupid_theta
   where
-    tc_subst     = zipTopTCvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
+    tc_subst     = zipOpenTCvSubst (tyConTyVars tycon) (mkTyVarTys univ_tvs)
     stupid_theta = substTheta tc_subst (tyConStupidTheta tycon)
         -- Start by instantiating the master copy of the
         -- stupid theta, taken from the TyCon
@@ -205,8 +205,8 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
     (ex_tvs1, prov_theta1, cont_tau) = tcSplitSigmaTy cont_sigma
     (arg_tys1, _) = tcSplitFunTys cont_tau
     twiddle = char '~'
-    subst = zipTopTCvSubst (univ_tvs1 ++ ex_tvs1)
-                           (mkTyVarTys (univ_tvs ++ ex_tvs))
+    subst = zipOpenTCvSubst (univ_tvs1 ++ ex_tvs1)
+                            (mkTyVarTys (univ_tvs ++ ex_tvs))
 
 ------------------------------------------------------
 type TcMethInfo = (Name, Type, Maybe (DefMethSpec Type))
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 385aa5dc41..35c27bf1d5 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1008,7 +1008,7 @@ inferConstraints main_cls cls_tys inst_ty rep_tc rep_tc_args
     stupid_constraints = mkThetaOrigin DerivOrigin TypeLevel $
                          substTheta tc_subst (tyConStupidTheta rep_tc)
     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
         -- The Data class (only) requires that for
@@ -1889,7 +1889,7 @@ simplifyDeriv pred tvs theta
 
 
        ; let min_theta  = mkMinimalBySCs (bagToList good)
-             subst_skol = zipTopTCvSubst tvs_skols $ mkTyVarTys tvs
+             subst_skol = zipOpenTCvSubst tvs_skols $ mkTyVarTys tvs
                           -- The reverse substitution (sigh)
        ; return (substTheta subst_skol min_theta) }
 
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index d6999f1af2..42581a6c5d 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -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
         ; checkExistentials ex_tvs all_arg_tys penv
         ; (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
 
         ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 62095c7117..4f744680bd 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -142,7 +142,7 @@ module TcType (
   -- Type substitutions
   TCvSubst(..),         -- Representation visible to a few friends
   TvSubstEnv, emptyTCvSubst,
-  mkOpenTCvSubst, zipOpenTCvSubst, zipTopTCvSubst,
+  mkOpenTCvSubst, zipOpenTCvSubst,
   mkTopTCvSubst, notElemTCvSubst, unionTCvSubst,
   getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
   Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
@@ -1740,7 +1740,7 @@ transSuperClasses p
 
 immSuperClasses :: Class -> [Type] -> [PredType]
 immSuperClasses cls tys
-  = substTheta (zipTopTCvSubst tyvars tys) sc_theta
+  = substTheta (zipOpenTCvSubst tyvars tys) sc_theta
   where
     (tyvars,sc_theta,_,_) = classBigSig cls
 
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 04fb02ce41..9d17a0bc41 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -84,7 +84,7 @@ module TyCoRep (
         unionTCvSubst, zipTyEnv, zipCoEnv, mkTyCoInScopeSet,
         mkOpenTCvSubst, zipOpenTCvSubst, zipOpenTCvSubstCoVars,
         zipOpenTCvSubstBinders,
-        mkTopTCvSubst, zipTopTCvSubst,
+        mkTopTCvSubst,
 
         substTelescope,
         substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
@@ -1656,33 +1656,35 @@ mkOpenTCvSubst tenv cenv
 -- | Generates the in-scope set for the 'TCvSubst' from the types in the incoming
 -- environment, hence "open". No CoVars, please!
 zipOpenTCvSubst :: [TyVar] -> [Type] -> TCvSubst
-zipOpenTCvSubst tyvars tys
-  | debugIsOn && (length tyvars /= length tys)
-  = pprTrace "zipOpenTCvSubst" (ppr tyvars $$ ppr tys) emptyTCvSubst
+zipOpenTCvSubst tvs tys
+  | debugIsOn
+  , not (all isTyVar tvs) || length tvs /= length tys
+  = pprTrace "zipOpenTCvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst
   | otherwise
   = 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
--- environment, hence "open".
+-- environment, hence "open".  No TyVars, please!
 zipOpenTCvSubstCoVars :: [CoVar] -> [Coercion] -> TCvSubst
 zipOpenTCvSubstCoVars cvs cos
-  | debugIsOn && (length cvs /= length cos)
+  | debugIsOn
+  , not (all isCoVar cvs) || length cvs /= length cos
   = pprTrace "zipOpenTCvSubstCoVars" (ppr cvs $$ ppr cos) emptyTCvSubst
   | otherwise
   = 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.
--- 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 bndrs tys
   = TCvSubst is tenv emptyCvSubstEnv
   where
     is = mkInScopeSet (tyCoVarsOfTypes tys)
-    (tvs, tys') = unzip [ (tv, ty) | (Named tv _, ty) <- zip bndrs tys ]
-    tenv = zipTyEnv tvs tys'
+    tenv = mkVarEnv [ (tv, ty) | (Named tv _, ty) <- zip bndrs tys ]
 
 -- | Called when doing top-level substitutions. Here we expect that the
 -- free vars of the range of the substitution will be empty.
@@ -1691,15 +1693,6 @@ mkTopTCvSubst prs = TCvSubst emptyInScopeSet tenv cenv
   where (tenv, cenv) = foldl extend (emptyTvSubstEnv, emptyCvSubstEnv) prs
         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 tyvars tys
   = ASSERT( all (not . isCoercionTy) tys )
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 4e67db875a..8b426f131a 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -150,7 +150,7 @@ module Type (
         -- ** Manipulating type substitutions
         emptyTvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
 
-        mkTCvSubst, mkOpenTCvSubst, zipOpenTCvSubst, zipTopTCvSubst, mkTopTCvSubst,
+        mkTCvSubst, mkOpenTCvSubst, zipOpenTCvSubst, mkTopTCvSubst,
         notElemTCvSubst,
         getTvSubstEnv, setTvSubstEnv,
         zapTCvSubst, getTCvInScope,
@@ -1810,7 +1810,7 @@ mkFamilyTyConApp tc tys
   | Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
   , let tvs = tyConTyVars tc
         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)
   | otherwise
   = mkTyConApp tc tys