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

13 files changed, 222 insertions, 70 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index c7ef602081..fd6c2ce74f 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -732,7 +732,7 @@ dataConArgUnpack arg_ty
      , Boxer $ \ subst ->
        do { rep_ids <- mapM (newLocal . TcType.substTyUnchecked subst) rep_tys
           ; return (rep_ids, Var (dataConWorkId con)
-                             `mkTyApps` (substTys subst tc_args)
+                             `mkTyApps` (substTysUnchecked subst tc_args)
                              `mkVarApps` rep_ids ) } ) )
   | otherwise
   = pprPanic "dataConArgUnpack" (ppr arg_ty)
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 26e7257c7e..f094415a8f 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -1284,7 +1284,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
        ; (k3, k4, t1, t2, r) <- addInScopeVar tv1 $ lintCoercion co
        ; let tyl = mkNamedForAllTy tv1 Invisible t1
              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) }
 
 lintCoercion (CoVarCo cv)
diff --git a/compiler/coreSyn/CoreUtils.hs b/compiler/coreSyn/CoreUtils.hs
index 8bea570383..be9f463eb7 100644
--- a/compiler/coreSyn/CoreUtils.hs
+++ b/compiler/coreSyn/CoreUtils.hs
@@ -97,7 +97,7 @@ exprType (Lit lit)           = literalType lit
 exprType (Coercion co)       = coercionType co
 exprType (Let bind body)
   | 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
 exprType (Case _ _ ty _)     = ty
 exprType (Cast _ co)         = pSnd (coercionKind co)
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index 27cb4b8c3b..6d4b0d9f66 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -628,7 +628,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                 -- I'm not bothering to clone the ex_tvs
            ; eqs_vars   <- mapM newPredVarDs (substTheta subst (eqSpecPreds eq_spec))
            ; 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
                  val_args = zipWithEqual "dsExpr:RecordUpd" mk_val_arg
                                          field_labels arg_ids
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index 72d8345736..5a9b57ace9 100644
--- a/compiler/typecheck/FunDeps.hs
+++ b/compiler/typecheck/FunDeps.hs
@@ -597,7 +597,7 @@ checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
           Just subst
             -> isNothing $   -- Bogus legacy test (Trac #10675)
                              -- See Note [Bogus consistency check]
-               tcUnifyTys bind_fn (substTys subst rtys1) (substTys subst rtys2)
+               tcUnifyTys bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
 
       where
         trimmed_tcs    = trimRoughMatchTcs cls_tvs fd rough_tcs1
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index fe17d52d7a..f142dcaa75 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -136,7 +136,7 @@ deeplySkolemise ty
   | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
        ; (subst, tvs1) <- tcInstSkolTyVars tvs
-       ; ev_vars1 <- newEvVars (substTheta subst theta)
+       ; ev_vars1 <- newEvVars (substThetaUnchecked subst theta)
        ; (wrap, tvs2, ev_vars2, rho) <-
            deeplySkolemise (substTyAddInScope subst ty')
        ; return ( mkWpLams ids1
@@ -178,7 +178,7 @@ top_instantiate inst_all orig ty
                | null leave_bndrs = (theta, [])
                | otherwise        = ([], theta)
        ; (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 $
                                                     mkFunTys leave_theta rho)
 
@@ -221,8 +221,8 @@ deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 deeplyInstantiate orig ty
   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
   = do { (subst, tvs') <- newMetaTyVars tvs
-       ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
-       ; let theta' = substTheta subst theta
+       ; ids1  <- newSysLocalIds (fsLit "di") (substTysUnchecked subst arg_tys)
+       ; let theta' = substThetaUnchecked subst theta
        ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
        ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
                                                 , text "type" <+> ppr ty
@@ -302,7 +302,7 @@ instDFunType :: DFunId -> [DFunInstType]
 -- See Note [DFunInstType: instantiating types] in InstEnv
 instDFunType dfun_id 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
     (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy (idType dfun_id)
 
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 8d7ac41b12..1911b063b1 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -887,7 +887,7 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
         ; rbinds'      <- tcRecordUpd con1 con1_arg_tys' rbinds
 
         -- STEP 6: Deal with the stupid theta
-        ; let theta' = substTheta scrut_subst (conLikeStupidTheta con1)
+        ; let theta' = substThetaUnchecked scrut_subst (conLikeStupidTheta con1)
         ; instStupidTheta RecordUpdOrigin theta'
 
         -- 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
         -- Step 8: Check that the req constraints are satisfied
         -- For normal data constructors req_theta is empty but we must do
         -- 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'
 
         -- Phew!
@@ -1160,7 +1160,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                  ASSERT( binderVisibility binder == Specified )
                  do { let kind = tyVarKind tv
                     ; 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)
                         <- go acc_args (n+1) insted_ty args
                    -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 2cf7d792c8..a6cf0198e7 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -3060,7 +3060,7 @@ deferTcSForAllEq :: Role -- Nominal or Representational
 deferTcSForAllEq role loc kind_cos (bndrs1,body1) (bndrs2,body2)
  = do { let tvs1'  = zipWithEqual "deferTcSForAllEq"
                        mkCastTy (mkTyVarTys tvs1) kind_cos
-            body2' = substTyWith tvs2 tvs1' body2
+            body2' = substTyWithUnchecked tvs2 tvs1' body2
       ; (subst, skol_tvs) <- wrapTcS $ TcM.tcInstSkolTyVars tvs1
       ; let phi1  = Type.substTyUnchecked subst body1
             phi2  = Type.substTyUnchecked subst body2'
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 29e7a6b869..63c06afdde 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -153,7 +153,10 @@ module TcType (
   Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
   extendTCvSubstList, isInScope, mkTCvSubst, zipTyEnv, zipCoEnv,
   Type.substTy, substTys, substTyWith, substTyWithCoVars,
-  substTyAddInScope, substTyUnchecked,
+  substTyAddInScope,
+  substTyUnchecked, substTysUnchecked, substThetaUnchecked,
+  substTyWithBindersUnchecked, substTyWithUnchecked,
+  substCoUnchecked, substCoWithUnchecked,
   substTheta,
 
   isUnliftedType,       -- Source types are always lifted
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index c6a7845585..5b2fb4fbbb 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -892,7 +892,7 @@ mkLRCo lr co           = LRCo lr co
 -- | Instantiates a 'Coercion'.
 mkInstCo :: Coercion -> Coercion -> Coercion
 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
 
 -- This could work harder to produce Refl coercions, but that would be
@@ -1721,7 +1721,7 @@ coercionKind co = go co
       = let Pair _ k2          = go k_co
             tv2                = setTyVarKind tv1 k2
             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'
     go (CoVarCo cv)         = toPair $ coVarTypes cv
     go (AxiomInstCo ax ind cos)
@@ -1796,7 +1796,7 @@ coercionKindRole = go
       = let Pair _ k2          = coercionKind k_co
             tv2                = setTyVarKind tv1 k2
             (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)
     go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
     go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index c9db4b3e67..2af66f6391 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -570,7 +570,7 @@ opt_trans_rule is co1 co2
       mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
     where
       is' = is `extendInScopeSet` tv1
-      r2' = substCoWith [tv2] [TyVarTy tv1] r2
+      r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2
 
 -- Push transitivity inside axioms
 opt_trans_rule is co1 co2
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 4bc9f59053..758ac257a6 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -89,7 +89,10 @@ module TyCoRep (
         substTelescope,
         substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
         substCoWith,
-        substTy, substTyAddInScope, substTyUnchecked,
+        substTy, substTyAddInScope,
+        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
+        substTyWithBindersUnchecked, substTyWithUnchecked,
+        substCoUnchecked, substCoWithUnchecked,
         substTyWithBinders, substTyWithInScope,
         substTys, substTheta,
         lookupTyVar, substTyVarBndr,
@@ -1782,9 +1785,24 @@ substTelescope = go_subst emptyTCvSubst
 
 
 -- | 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 )
-                      substTyUnchecked (zipTvSubst tvs 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)
 
 -- | Substitute tyvars within a type using a known 'InScopeSet'.
 -- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
@@ -1797,10 +1815,27 @@ substTyWithInScope in_scope tvs tys ty =
   where tenv = zipTyEnv tvs tys
 
 -- | 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 )
                       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
 substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
 substTyWithCoVars cvs cos = substTy (zipCvSubst cvs cos)
@@ -1817,9 +1852,25 @@ substTysWithCoVars cvs cos = ASSERT( length cvs == length cos )
 
 -- | Type substitution using 'Binder's. Anonymous binders
 -- 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 )
-                               substTyUnchecked (zipTyBinderSubst bndrs 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)
 
 -- | 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
@@ -1841,58 +1892,105 @@ isValidTCvSubst (TCvSubst in_scope tenv cenv) =
   tenvFVs = tyCoVarsOfTypes $ varEnvElts tenv
   cenvFVs = tyCoVarsOfCos $ varEnvElts cenv
 
+-- | This checks if the substitution satisfies the invariant from
+-- Note [The substitution invariant].
+checkValidSubst ::
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,2,0)
+    (?callStack :: CallStack) =>
+#endif
+    TCvSubst -> [Type] -> [Coercion] -> a -> a
+checkValidSubst subst@(TCvSubst in_scope tenv cenv) tys cos a
+  = ASSERT2( isValidTCvSubst subst,
+             text "in_scope" <+> ppr in_scope $$
+             text "tenv" <+> ppr tenv $$
+             text "tenvFVs"
+               <+> ppr (tyCoVarsOfTypes $ varEnvElts tenv) $$
+             text "cenv" <+> ppr cenv $$
+             text "cenvFVs"
+               <+> ppr (tyCoVarsOfCos $ varEnvElts cenv) $$
+             text "tys" <+> ppr tys $$
+             text "cos" <+> ppr cos )
+    ASSERT2( tysCosFVsInScope,
+             text "in_scope" <+> ppr in_scope $$
+             text "tenv" <+> ppr tenv $$
+             text "cenv" <+> ppr cenv $$
+             text "tys" <+> ppr tys $$
+             text "cos" <+> ppr cos $$
+             text "needInScope" <+> ppr needInScope )
+    a
+  where
+  substDomain = varEnvKeys tenv ++ varEnvKeys cenv
+  needInScope = (tyCoVarsOfTypes tys `unionVarSet` tyCoVarsOfCos cos)
+                  `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@(TCvSubst in_scope tenv cenv) ty
+substTy subst ty
   | isEmptyTCvSubst subst = ty
-  | otherwise = ASSERT2( isValidTCvSubst subst,
-                         text "in_scope" <+> ppr in_scope $$
-                         text "tenv" <+> ppr tenv $$
-                         text "tenvFVs"
-                           <+> ppr (tyCoVarsOfTypes $ varEnvElts tenv) $$
-                         text "cenv" <+> ppr cenv $$
-                         text "cenvFVs"
-                           <+> ppr (tyCoVarsOfCos $ varEnvElts 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
+  | otherwise = checkValidSubst subst [ty] [] $ subst_ty subst ty
 
 -- | Substitute within a 'Type' disabling the 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.
-substTyUnchecked :: TCvSubst -> Type  -> Type
+substTyUnchecked :: TCvSubst -> Type -> Type
 substTyUnchecked subst ty
                  | isEmptyTCvSubst subst = ty
                  | otherwise             = subst_ty subst ty
 
 -- | Substitute within several 'Type's
-substTys :: TCvSubst -> [Type] -> [Type]
-substTys subst tys | isEmptyTCvSubst subst = tys
-                   | otherwise             = map (subst_ty subst) tys
+-- The substitution has to satisfy the invariants described in
+-- 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
 
 -- | 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
 
+-- | 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 is the main workhorse for type substitution
 --
@@ -1911,7 +2009,7 @@ subst_ty subst ty
     go (ForAllTy (Anon arg) res)
                          = (ForAllTy $! (Anon $! go arg)) $! go res
     go (ForAllTy (Named tv vis) ty)
-                         = case substTyVarBndr subst tv of
+                         = case substTyVarBndrUnchecked subst tv of
                              (subst', tv') ->
                                (ForAllTy $! ((Named $! tv') vis)) $!
                                             (subst_ty subst' ty)
@@ -1936,14 +2034,40 @@ lookupTyVar (TCvSubst _ tenv _) tv
     lookupVarEnv tenv tv
 
 -- | Substitute within a 'Coercion'
-substCo :: TCvSubst -> Coercion -> Coercion
-substCo subst co | isEmptyTCvSubst subst = co
-                 | otherwise             = subst_co subst co
+-- The substitution has to satisfy the invariants described in
+-- 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
 
 -- | Substitute within several 'Coercion's
-substCos :: TCvSubst -> [Coercion] -> [Coercion]
-substCos subst cos | isEmptyTCvSubst subst = cos
-                   | otherwise             = map (substCo subst) cos
+-- The substitution has to satisfy the invariants described in
+-- Note [The substitution invariant].
+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 subst co
@@ -1958,7 +2082,7 @@ subst_co subst co
                                in  args' `seqList` mkTyConAppCo r tc args'
     go (AppCo co arg)        = (mkAppCo $! go co) $! go arg
     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 }
     go (CoVarCo cv)          = substCoVar subst cv
     go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
@@ -1989,6 +2113,15 @@ substForAllCoBndr :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion
 substForAllCoBndr subst
   = substForAllCoBndrCallback False (substCo subst) subst
 
+-- | Like 'substForAllCoBndr', but 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.
+substForAllCoBndrUnchecked :: TCvSubst -> TyVar -> Coercion -> (TCvSubst, TyVar, Coercion)
+substForAllCoBndrUnchecked subst
+  = substForAllCoBndrCallback False (substCoUnchecked subst) subst
+
 -- See Note [Sym and ForAllCo]
 substForAllCoBndrCallback :: Bool  -- apply sym to binder?
                           -> (Coercion -> Coercion)  -- transformation to kind co
@@ -2026,8 +2159,21 @@ substCoVars subst cvs = map (substCoVar subst) cvs
 lookupCoVar :: TCvSubst -> Var  -> Maybe Coercion
 lookupCoVar (TCvSubst _ _ cenv) v = lookupVarEnv cenv v
 
-substTyVarBndr :: TCvSubst -> TyVar -> (TCvSubst, TyVar)
-substTyVarBndr = substTyVarBndrCallback substTyUnchecked
+substTyVarBndr ::
+-- 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 -> TyVar -> (TCvSubst, TyVar)
+substTyVarBndr = substTyVarBndrCallback substTy
+
+-- | Like 'substTyVarBndr' but 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.
+substTyVarBndrUnchecked :: TCvSubst -> TyVar -> (TCvSubst, TyVar)
+substTyVarBndrUnchecked = 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 74763dae94..43aad5b069 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -161,7 +161,10 @@ module Type (
 
         -- ** Performing substitution on types and kinds
         substTy, substTys, substTyWith, substTysWith, substTheta,
-        substTyAddInScope, substTyUnchecked,
+        substTyAddInScope,
+        substTyUnchecked, substTysUnchecked, substThetaUnchecked,
+        substTyWithBindersUnchecked, substTyWithUnchecked,
+        substCoUnchecked, substCoWithUnchecked,
         substTyVarBndr, substTyVar, substTyVars,
         cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar, substTelescope,
 
@@ -798,7 +801,7 @@ funResultTy ty = piResultTy ty (pprPanic "funResultTy" (ppr ty))
 piResultTy :: Type -> Type -> Type
 piResultTy ty arg | Just ty' <- coreView ty = piResultTy ty' arg
 piResultTy (ForAllTy (Anon _) res)     _   = res
-piResultTy (ForAllTy (Named tv _) res) arg = substTyWith [tv] [arg] res
+piResultTy (ForAllTy (Named tv _) res) arg = substTyWithUnchecked [tv] [arg] res
 piResultTy ty arg                          = pprPanic "piResultTy"
                                                  (ppr ty $$ ppr arg)
 
@@ -1404,11 +1407,11 @@ applyTysD :: SDoc -> Type -> [Type] -> Type     -- Debug version
 applyTysD _   orig_fun_ty []      = orig_fun_ty
 applyTysD doc orig_fun_ty arg_tys
   | n_bndrs == n_args     -- The vastly common case
-  = substTyWithBinders bndrs arg_tys rho_ty
+  = substTyWithBindersUnchecked bndrs arg_tys rho_ty
   | n_bndrs > n_args      -- Too many for-alls
-  = substTyWithBinders (take n_args bndrs) arg_tys
-                       (mkForAllTys (drop n_args bndrs) rho_ty)
-  | otherwise           -- Too many type args
+  = substTyWithBindersUnchecked (take n_args bndrs) arg_tys
+                                (mkForAllTys (drop n_args bndrs) rho_ty)
+  | otherwise             -- Too many type args
   = ASSERT2( n_bndrs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys )       -- Zero case gives infinite loop!
     applyTysD doc (substTyWithBinders bndrs (take n_bndrs arg_tys) rho_ty)
                   (drop n_bndrs arg_tys)
@@ -1421,7 +1424,7 @@ applyTysX :: [TyVar] -> Type -> [Type] -> Type
 -- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys
 applyTysX tvs body_ty arg_tys
   = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys )
-    mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty)
+    mkAppTys (substTyWithUnchecked tvs (take n_tvs arg_tys) body_ty)
              (drop n_tvs arg_tys)
   where
     n_tvs = length tvs
@@ -1537,7 +1540,7 @@ isPredTy ty = go ty []
     -- True <=> kind is k1 -> .. -> kn -> Constraint
     go_k k [] = isConstraintKind k
     go_k (ForAllTy bndr k1) (arg:args)
-      = go_k (substTyWithBinders [bndr] [arg] k1) args
+      = go_k (substTyWithBindersUnchecked [bndr] [arg] k1) args
     go_k _ _ = False                  -- Typeable * Int :: Constraint
 
 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool