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

5 files changed, 14 insertions, 11 deletions

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