Remove TCvSubst and use Subst for both term and type-level subst

This patch removes the TCvSubst data type and instead uses Subst as
the environment for both term and type level substitution. This
change is partially motivated by the existential type proposal,
which will introduce types that contain expressions and therefore
forces us to carry around an "IdSubstEnv" even when substituting for
types. It also reduces the amount of code because "Subst" and
"TCvSubst" share a lot of common operations. There isn't any
noticeable impact on performance (geo. mean for ghc/alloc is around
0.0% but we have -94 loc and one less data type to worry abount).

Currently, the "TCvSubst" data type for substitution on types is
identical to the "Subst" data type except the former doesn't store
"IdSubstEnv". Using "Subst" for type-level substitution means there
will be a redundant field stored in the data type. However, in cases
where the substitution starts from the expression, using "Subst" for
type-level substitution saves us from having to project "Subst" into a
"TCvSubst". This probably explains why the allocation is mostly even
despite the redundant field.

The patch deletes "TCvSubst" and moves "Subst" and its relevant
functions from "GHC.Core.Subst" into "GHC.Core.TyCo.Subst".
Substitution on expressions is still defined in "GHC.Core.Subst" so we
don't have to expose the definition of "Expr" in the hs-boot file that
"GHC.Core.TyCo.Subst" must import to refer to "IdSubstEnv" (whose
codomain is "CoreExpr"). Most functions named fooTCvSubst are renamed
into fooSubst with a few exceptions (e.g. "isEmptyTCvSubst" is a
distinct function from "isEmptySubst"; the former ignores the
emptiness of "IdSubstEnv"). These exceptions mainly exist for
performance reasons and will go away when "Expr" and "Type" are
mutually recursively defined (we won't be able to take those
shortcuts if we can't make the assumption that expressions don't
appear in types).

18 files changed, 113 insertions, 121 deletions

diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index f191f74d46..7df65bd367 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -645,9 +645,9 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mb_lderiv_strat overlap_mode))
                           DerivErrDerivingViaWrongKind inst_ty_kind via_ty via_kind)
 
                let Just kind_subst = mb_match
-                   ki_subst_range  = getTCvSubstRangeFVs kind_subst
+                   ki_subst_range  = getSubstRangeTyCoFVs kind_subst
                    -- See Note [Unification of two kind variables in deriving]
-                   unmapped_tkvs = filter (\v -> v `notElemTCvSubst` kind_subst
+                   unmapped_tkvs = filter (\v -> v `notElemSubst` kind_subst
                                         && not (v `elemVarSet` ki_subst_range))
                                           tvs
                    (subst, _)    = substTyVarBndrs kind_subst unmapped_tkvs
@@ -769,9 +769,9 @@ deriveTyData tc tc_args mb_deriv_strat deriv_tvs cls cls_tys cls_arg_kind
               propagate_subst kind_subst tkvs' cls_tys' tc_args' mb_deriv_strat'
                 = (final_tkvs, final_cls_tys, final_tc_args, final_mb_deriv_strat)
                 where
-                  ki_subst_range  = getTCvSubstRangeFVs kind_subst
+                  ki_subst_range  = getSubstRangeTyCoFVs kind_subst
                   -- See Note [Unification of two kind variables in deriving]
-                  unmapped_tkvs   = filter (\v -> v `notElemTCvSubst` kind_subst
+                  unmapped_tkvs   = filter (\v -> v `notElemSubst` kind_subst
                                          && not (v `elemVarSet` ki_subst_range))
                                            tkvs'
                   (subst, _)           = substTyVarBndrs kind_subst unmapped_tkvs
@@ -1008,7 +1008,7 @@ the type variable binder for c, since its kind is (k2 -> k2 -> *).
 
 We used to accomplish this by doing the following:
 
-    unmapped_tkvs = filter (`notElemTCvSubst` kind_subst) all_tkvs
+    unmapped_tkvs = filter (`notElemSubst` kind_subst) all_tkvs
     (subst, _)    = substTyVarBndrs kind_subst unmapped_tkvs
 
 Where all_tkvs contains all kind variables in the class and instance types (in
@@ -1024,9 +1024,9 @@ in an ill-kinded instance (this caused #11837).
 
 To prevent this, we need to filter out any variable from all_tkvs which either
 
-1. Appears in the domain of kind_subst. notElemTCvSubst checks this.
+1. Appears in the domain of kind_subst. notElemSubst checks this.
 2. Appears in the range of kind_subst. To do this, we compute the free
-   variable set of the range of kind_subst with getTCvSubstRangeFVs, and check
+   variable set of the range of kind_subst with getSubstRangeTyCoFVs, and check
    if a kind variable appears in that set.
 
 Note [Eta-reducing type synonyms]
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 810c4c7a32..ab0bbd0c11 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -2759,7 +2759,7 @@ buildDataConInstArgEnv rep_tc rep_tc_args =
 -- | Apply a substitution to all of the 'Type's contained in a 'DerivInstTys'.
 -- See @Note [Instantiating field types in stock deriving]@ for why we need to
 -- substitute into a 'DerivInstTys' in the first place.
-substDerivInstTys :: TCvSubst -> DerivInstTys -> DerivInstTys
+substDerivInstTys :: Subst -> DerivInstTys -> DerivInstTys
 substDerivInstTys subst
   dit@(DerivInstTys { dit_cls_tys = cls_tys, dit_tc_args = tc_args
                     , dit_rep_tc = rep_tc, dit_rep_tc_args = rep_tc_args })
diff --git a/compiler/GHC/Tc/Deriv/Infer.hs b/compiler/GHC/Tc/Deriv/Infer.hs
index 94a00ce52b..c17fee9753 100644
--- a/compiler/GHC/Tc/Deriv/Infer.hs
+++ b/compiler/GHC/Tc/Deriv/Infer.hs
@@ -178,7 +178,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
            con_arg_constraints
              :: (CtOrigin -> TypeOrKind
                           -> Type
-                          -> [(ThetaSpec, Maybe TCvSubst)])
+                          -> [(ThetaSpec, Maybe Subst)])
              -> (ThetaSpec, [TyVar], [TcType], DerivInstTys)
            con_arg_constraints get_arg_constraints
              = let -- Constraints from the fields of each data constructor.
@@ -215,8 +215,8 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                    -- kinds with (* -> *).
                    -- See Note [Inferring the instance context]
                    subst        = foldl' composeTCvSubst
-                                         emptyTCvSubst (catMaybes mbSubsts)
-                   unmapped_tvs = filter (\v -> v `notElemTCvSubst` subst
+                                         emptySubst (catMaybes mbSubsts)
+                   unmapped_tvs = filter (\v -> v `notElemSubst` subst
                                              && not (v `isInScope` subst)) tvs
                    (subst', _)  = substTyVarBndrs subst unmapped_tvs
                    stupid_theta_origin = mkDirectThetaSpec
@@ -236,13 +236,13 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
                           || is_generic1
 
            get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
-                                -> [(ThetaSpec, Maybe TCvSubst)]
+                                -> [(ThetaSpec, Maybe Subst)]
            get_gen1_constraints functor_cls orig t_or_k ty
               = mk_functor_like_constraints orig t_or_k functor_cls $
                 get_gen1_constrained_tys last_tv ty
 
            get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
-                                   -> [(ThetaSpec, Maybe TCvSubst)]
+                                   -> [(ThetaSpec, Maybe Subst)]
            get_std_constrained_tys orig t_or_k ty
                | is_functor_like
                = mk_functor_like_constraints orig t_or_k main_cls $
@@ -253,7 +253,7 @@ inferConstraintsStock dit@(DerivInstTys { dit_cls_tys     = cls_tys
 
            mk_functor_like_constraints :: CtOrigin -> TypeOrKind
                                        -> Class -> [Type]
-                                       -> [(ThetaSpec, Maybe TCvSubst)]
+                                       -> [(ThetaSpec, Maybe Subst)]
            -- 'cls' is usually main_cls (Functor or Traversable etc), but if
            -- main_cls = Generic1, then 'cls' can be Functor; see
            -- get_gen1_constraints
diff --git a/compiler/GHC/Tc/Deriv/Utils.hs b/compiler/GHC/Tc/Deriv/Utils.hs
index f28ad0e8f4..b6ad253ec1 100644
--- a/compiler/GHC/Tc/Deriv/Utils.hs
+++ b/compiler/GHC/Tc/Deriv/Utils.hs
@@ -637,7 +637,7 @@ mkDirectThetaSpec origin t_or_k =
                , sps_type_or_kind = t_or_k
                })
 
-substPredSpec :: HasCallStack => TCvSubst -> PredSpec -> PredSpec
+substPredSpec :: HasCallStack => Subst -> PredSpec -> PredSpec
 substPredSpec subst ps =
   case ps of
     SimplePredSpec { sps_pred = pred
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index d045984024..3fed598f4d 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE RankNTypes          #-}
@@ -1572,12 +1571,12 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
            -- Note that in a typical application (F t1 t2 t3),
            -- the 'fun' is just a TyCon, so tcTypeKind is fast
 
-        empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+        empty_subst = mkEmptySubst $ mkInScopeSet $
                       tyCoVarsOfType fun_ki
 
     go :: Int             -- The # of the next argument
        -> TcType          -- Function applied to some args
-       -> TCvSubst        -- Applies to function kind
+       -> Subst        -- Applies to function kind
        -> TcKind          -- Function kind
        -> [LHsTypeArg GhcRn]    -- Un-type-checked args
        -> TcM (TcType, TcKind)  -- Result type and its kind
@@ -1687,7 +1686,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
           | otherwise
           = fallthrough
 
-        zapped_subst   = zapTCvSubst subst
+        zapped_subst   = zapSubst subst
         substed_fun_ki = substTy subst fun_ki
         hs_ty          = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
 
@@ -1700,10 +1699,10 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
     ty_app_err arg ty
       = failWith $ TcRnInvalidVisibleKindArgument arg ty
 
-mkAppTyM :: TCvSubst
+mkAppTyM :: Subst
          -> TcType -> TyCoBinder    -- fun, plus its top-level binder
          -> TcType                  -- arg
-         -> TcM (TCvSubst, TcType)  -- Extended subst, plus (fun arg)
+         -> TcM (Subst, TcType)  -- Extended subst, plus (fun arg)
 -- Precondition: the application (fun arg) is well-kinded after zonking
 --               That is, the application makes sense
 --
@@ -2581,7 +2580,7 @@ kcCheckDeclHeader_sig sig_kind name flav
         -- Why? So that the TyConBinders of the TyCon will lexically scope over the
         -- associated types and methods of a class.
         ; let swizzle_env = mkVarEnv (map swap implicit_prs)
-              (subst, swizzled_tcbs) = mapAccumL (swizzleTcb swizzle_env) emptyTCvSubst all_tcbs
+              (subst, swizzled_tcbs) = mapAccumL (swizzleTcb swizzle_env) emptySubst all_tcbs
               swizzled_kind          = substTy subst tycon_res_kind
               all_tv_prs             = mkTyVarNamePairs (binderVars swizzled_tcbs)
 
@@ -2621,7 +2620,7 @@ matchUpSigWithDecl
 -- Invariant: Length of returned TyConBinders + length of excess TyConBinders
 --            = length of incoming TyConBinders
 matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside
-  = go emptyTCvSubst sig_tcbs hs_bndrs
+  = go emptySubst sig_tcbs hs_bndrs
   where
     go subst tcbs []
       = do { let (subst', tcbs') = substTyConBindersX subst tcbs
@@ -2663,16 +2662,16 @@ matchUpSigWithDecl sig_tcbs sig_res_kind hs_bndrs thing_inside
            ; discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig]
              unifyKind (Just (NameThing hs_nm)) sig_kind expected_kind }
 
-substTyConBinderX :: TCvSubst -> TyConBinder -> (TCvSubst, TyConBinder)
+substTyConBinderX :: Subst -> TyConBinder -> (Subst, TyConBinder)
 substTyConBinderX subst (Bndr tv vis)
   = (subst', Bndr tv' vis)
   where
     (subst', tv') = substTyVarBndr subst tv
 
-substTyConBindersX :: TCvSubst -> [TyConBinder] -> (TCvSubst, [TyConBinder])
+substTyConBindersX :: Subst -> [TyConBinder] -> (Subst, [TyConBinder])
 substTyConBindersX = mapAccumL substTyConBinderX
 
-swizzleTcb :: VarEnv Name -> TCvSubst -> TyConBinder -> (TCvSubst, TyConBinder)
+swizzleTcb :: VarEnv Name -> Subst -> TyConBinder -> (Subst, TyConBinder)
 swizzleTcb swizzle_env subst (Bndr tv vis)
   = (subst', Bndr tv2 vis)
   where
@@ -3698,7 +3697,7 @@ splitTyConKind skol_info in_scope avoid_occs kind
                          -- Note [Avoid name clashes for associated data types]
                          , not (occ `elem` avoid_occs) ]
               new_uniqs = uniqsFromSupply uniqs
-              subst = mkEmptyTCvSubst in_scope
+              subst = mkEmptySubst in_scope
               details = SkolemTv skol_info (pushTcLevel lvl) False
                         -- As always, allocate skolems one level in
 
@@ -3713,7 +3712,7 @@ splitTyConKind skol_info in_scope avoid_occs kind
                         arg'   = substTy subst (scaledThing arg)
                         name   = mkInternalName uniq occ loc
                         tv     = mkTcTyVar name arg' details
-                        subst' = extendTCvInScope subst tv
+                        subst' = extendSubstInScope subst tv
                         (uniq:uniqs') = uniqs
                         (occ:occs')   = occs
 
@@ -3843,7 +3842,7 @@ tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
 tcbVisibilities tc orig_args
   = go (tyConKind tc) init_subst orig_args
   where
-    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes orig_args))
+    init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfTypes orig_args))
     go _ _ []
       = []
 
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 83bb70e35f..b5c6b4c5c5 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE RankNTypes #-}
@@ -1239,7 +1238,7 @@ Wrinkles:
 
 tcConArgs :: ConLike
           -> [Scaled TcSigmaTypeFRR]
-          -> TCvSubst            -- Instantiating substitution for constructor type
+          -> Subst            -- Instantiating substitution for constructor type
           -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
 tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
   PrefixCon type_args arg_pats -> do
diff --git a/compiler/GHC/Tc/Instance/FunDeps.hs b/compiler/GHC/Tc/Instance/FunDeps.hs
index 067c87a50f..b11ed10efc 100644
--- a/compiler/GHC/Tc/Instance/FunDeps.hs
+++ b/compiler/GHC/Tc/Instance/FunDeps.hs
@@ -324,7 +324,7 @@ improveClsFD clas_tvs fd
 
                     meta_tvs = [ setVarType tv (substTy subst (varType tv))
                                | tv <- qtvs
-                               , tv `notElemTCvSubst` subst
+                               , tv `notElemSubst` subst
                                , tv `elemVarSet` rtys1_tvs ]
                         -- meta_tvs are the quantified type variables
                         -- that have not been substituted out
@@ -343,7 +343,7 @@ improveClsFD clas_tvs fd
                         --              whose kind mentions that kind variable! #6015, #6068
                         --          (c) no need to include tyvars not in rtys1
   where
-    init_subst     = mkEmptyTCvSubst $ mkInScopeSet $
+    init_subst     = mkEmptySubst $ mkInScopeSet $
                      mkVarSet qtvs `unionVarSet` tyCoVarsOfTypes ltys2
     (ltys1, rtys1) = instFD fd clas_tvs tys_inst
     (ltys2, rtys2) = instFD fd clas_tvs tys_actual
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 81aa291785..ec8e11b168 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -867,7 +867,7 @@ solveForAll ev@(CtWanted { ctev_dest = dest, ctev_rewriters = rewriters, ctev_lo
     -- TcLclEnv for the implication, and that in turn sets the location
     -- for the Givens when solving the constraint (#21006)
     do { skol_info <- mkSkolemInfo QuantCtxtSkol
-       ; let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+       ; let empty_subst = mkEmptySubst $ mkInScopeSet $
                            tyCoVarsOfTypes (pred:theta) `delVarSetList` tvs
        ; (subst, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst tvs
        ; given_ev_vars <- mapM newEvVar (substTheta subst theta)
@@ -1210,7 +1210,7 @@ can_eq_nc_forall ev eq_rel s1 s2
                 ; canEqHardFailure ev s1 s2 }
         else
    do { traceTcS "Creating implication for polytype equality" $ ppr ev
-      ; let empty_subst1 = mkEmptyTCvSubst $ mkInScopeSet free_tvs
+      ; let empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs
       ; skol_info <- mkSkolemInfo (UnifyForAllSkol phi1)
       ; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $
                               binderVars bndrs1
@@ -1218,7 +1218,7 @@ can_eq_nc_forall ev eq_rel s1 s2
       ; let phi1' = substTy subst1 phi1
 
             -- Unify the kinds, extend the substitution
-            go :: [TcTyVar] -> TCvSubst -> [TyVarBinder]
+            go :: [TcTyVar] -> Subst -> [TyVarBinder]
                -> TcS (TcCoercion, Cts)
             go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
               = do { let tv2 = binderVar bndr2
@@ -1239,7 +1239,7 @@ can_eq_nc_forall ev eq_rel s1 s2
 
             go _ _ _ = panic "cna_eq_nc_forall"  -- case (s:ss) []
 
-            empty_subst2 = mkEmptyTCvSubst (getTCvInScope subst1)
+            empty_subst2 = mkEmptySubst (getSubstInScope subst1)
 
       ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
                                     go skol_tvs empty_subst2 bndrs2
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index e60e6993cc..ac29f55505 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1,4 +1,3 @@
-
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
 
@@ -1859,19 +1858,19 @@ emitFunDepWanteds work_rewriters fd_eqns
 
      | otherwise
      = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs)
-          ; subst <- instFlexiX emptyTCvSubst tvs  -- Takes account of kind substitution
+          ; subst <- instFlexiX emptySubst tvs  -- Takes account of kind substitution
           ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) }
                -- See Note [Reverse order of fundep equations]
      where
        all_rewriters = work_rewriters S.<> rewriters
 
     do_one_eq loc rewriters subst (Pair ty1 ty2)
-       = unifyWanted rewriters loc Nominal (Type.substTy subst' ty1) ty2
+       = unifyWanted rewriters loc Nominal (substTyUnchecked subst' ty1) ty2
          -- ty2 does not mention fd_qtvs, so no need to subst it.
          -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
          --     Wrinkle (1)
       where
-         subst' = extendTCvInScopeSet subst (tyCoVarsOfType ty1)
+         subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
          -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
          -- of matching with the [W] constraint. So we add its free
          -- vars to InScopeSet, to satisfy substTy's invariants, even
@@ -2082,7 +2081,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
           -> (a -> [Type])           -- get LHS of an axiom
           -> (a -> Type)             -- get RHS of an axiom
           -> (a -> Maybe CoAxBranch) -- Just => apartness check required
-          -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
+          -> [( [Type], Subst, [TyVar], Maybe CoAxBranch )]
              -- Result:
              -- ( [arguments of a matching axiom]
              -- , RHS-unifying substitution
@@ -2102,7 +2101,7 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
                    -- in telescope order e.g. (k:*) (a:k)
 
       injImproveEqns :: [Bool]
-                     -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
+                     -> ([Type], Subst, [TyCoVar], Maybe CoAxBranch)
                      -> TcS [TypeEqn]
       injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
         = do { subst <- instFlexiX subst unsubstTvs
@@ -2577,4 +2576,3 @@ information as described in Note [Replacement vs keeping], 2a.
 Test case: typecheck/should_compile/T20582.
 
 -}
-
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 6621f54317..f41e1991ce 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1614,11 +1614,11 @@ newFlexiTcSTy knd = wrapTcS (TcM.newFlexiTyVarTy knd)
 cloneMetaTyVar :: TcTyVar -> TcS TcTyVar
 cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv)
 
-instFlexiX :: TCvSubst -> [TKVar] -> TcS TCvSubst
+instFlexiX :: Subst -> [TKVar] -> TcS Subst
 instFlexiX subst tvs
   = wrapTcS (foldlM instFlexiHelper subst tvs)
 
-instFlexiHelper :: TCvSubst -> TKVar -> TcM TCvSubst
+instFlexiHelper :: Subst -> TKVar -> TcM Subst
 -- Makes fresh tyvar, extends the substitution, and the in-scope set
 instFlexiHelper subst tv
   = do { uniq <- TcM.newUnique
@@ -1637,7 +1637,7 @@ matchGlobalInst :: DynFlags
 matchGlobalInst dflags short_cut cls tys
   = wrapTcS (TcM.matchGlobalInst dflags short_cut cls tys)
 
-tcInstSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcS (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])
 tcInstSkolTyVarsX skol_info subst tvs = wrapTcS $ TcM.tcInstSkolTyVarsX skol_info subst tvs
 
 -- Creating and setting evidence variables and CtFlavors
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 87580c1865..03e7d45148 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -2585,7 +2585,7 @@ tcDefaultAssocDecl fam_tc
            ])
        ; let subst = case traverse getTyVar_maybe pats of
                        Just cpt_tvs -> zipTvSubst cpt_tvs (mkTyVarTys fam_tvs)
-                       Nothing      -> emptyTCvSubst
+                       Nothing      -> emptySubst
                        -- The Nothing case can only be reached in invalid
                        -- associated type family defaults. In such cases, we
                        -- simply create an empty substitution and let GHC fall
@@ -3798,7 +3798,7 @@ rejigConRes :: [KnotTied TyConBinder]  -- Template for result type; e.g.
                 [InvisTVBinder],  -- The constructor's rejigged, user-written
                                   -- type variables
                 [EqSpec],         -- Equality predicates
-                TCvSubst)         -- Substitution to apply to argument types
+                Subst)            -- Substitution to apply to argument types
         -- We don't check that the TyCon given in the ResTy is
         -- the same as the parent tycon, because checkValidDataCon will do it
 -- NB: All arguments may potentially be knot-tied
@@ -3847,7 +3847,7 @@ rejigConRes tc_tvbndrs res_tmpl dc_tvbndrs res_ty
         -- albeit bogus, relying on checkValidDataCon to check the
         --  bad-result-type error before seeing that the other fields look odd
         -- See Note [rejigConRes]
-  = (tc_tvs, dc_tvs `minusList` tc_tvs, dc_tvbndrs, [], emptyTCvSubst)
+  = (tc_tvs, dc_tvs `minusList` tc_tvs, dc_tvbndrs, [], emptySubst)
   where
     dc_tvs = binderVars dc_tvbndrs
     tc_tvs = binderVars tc_tvbndrs
@@ -3995,28 +3995,28 @@ certainly degrade error messages a bit, though.
 -- See Note [mkGADTVars].
 mkGADTVars :: [TyVar]    -- ^ The tycon vars
            -> [TyVar]    -- ^ The datacon vars
-           -> TCvSubst   -- ^ The matching between the template result type
+           -> Subst   -- ^ The matching between the template result type
                          -- and the actual result type
            -> ( [TyVar]
               , [EqSpec]
-              , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
+              , Subst ) -- ^ The univ. variables, the GADT equalities,
                            -- and a subst to apply to the GADT equalities
                            -- and existentials.
 mkGADTVars tmpl_tvs dc_tvs subst
   = choose [] [] empty_subst empty_subst tmpl_tvs
   where
     in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
-               `unionInScope` getTCvInScope subst
-    empty_subst = mkEmptyTCvSubst in_scope
+               `unionInScope` getSubstInScope subst
+    empty_subst = mkEmptySubst in_scope
 
     choose :: [TyVar]           -- accumulator of univ tvs, reversed
            -> [EqSpec]          -- accumulator of GADT equalities, reversed
-           -> TCvSubst          -- template substitution
-           -> TCvSubst          -- res. substitution
+           -> Subst          -- template substitution
+           -> Subst          -- res. substitution
            -> [TyVar]           -- template tvs (the univ tvs passed in)
            -> ( [TyVar]         -- the univ_tvs
               , [EqSpec]        -- GADT equalities
-              , TCvSubst )       -- a substitution to fix kinds in ex_tvs
+              , Subst )       -- a substitution to fix kinds in ex_tvs
 
     choose univs eqs _t_sub r_sub []
       = (reverse univs, reverse eqs, r_sub)
diff --git a/compiler/GHC/Tc/TyCl/Class.hs b/compiler/GHC/Tc/TyCl/Class.hs
index dee46e9189..a57f6df973 100644
--- a/compiler/GHC/Tc/TyCl/Class.hs
+++ b/compiler/GHC/Tc/TyCl/Class.hs
@@ -505,7 +505,7 @@ inst_decl_ctxt doc = hang (text "In the instance declaration for")
                         2 (quotes doc)
 
 tcATDefault :: SrcSpan
-            -> TCvSubst
+            -> Subst
             -> NameSet
             -> ClassATItem
             -> TcM [FamInst]
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index dad820674e..814e5640a2 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -436,7 +436,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
          -- expected type. Even though the tyvars in the type are
          -- already skolems, this step changes their TcLevels,
          -- avoiding level-check errors when unifying.
-       ; (skol_subst0, skol_univ_bndrs) <- skolemiseTvBndrsX skol_info emptyTCvSubst univ_bndrs
+       ; (skol_subst0, skol_univ_bndrs) <- skolemiseTvBndrsX skol_info emptySubst univ_bndrs
        ; (skol_subst, skol_ex_bndrs)    <- skolemiseTvBndrsX skol_info skol_subst0   ex_bndrs
        ; let skol_univ_tvs   = binderVars skol_univ_bndrs
              skol_ex_tvs     = binderVars skol_ex_bndrs
@@ -457,7 +457,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
            tcExtendNameTyVarEnv univ_tv_prs $
            tcCheckPat PatSyn lpat (unrestricted skol_pat_ty)   $
            do { let in_scope    = mkInScopeSetList skol_univ_tvs
-                    empty_subst = mkEmptyTCvSubst in_scope
+                    empty_subst = mkEmptySubst in_scope
               ; (inst_subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst skol_ex_tvs
                     -- newMetaTyVarX: see the "Existential type variables"
                     -- part of Note [Checking against a pattern signature]
@@ -494,7 +494,7 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
                           (args', skol_arg_tys)
                           skol_pat_ty rec_fields }
   where
-    tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTc)
+    tc_arg :: Subst -> Name -> Type -> TcM (LHsExpr GhcTc)
      -- Look up the variable actually bound by lpat
      -- and check that it has the expected type
     tc_arg subst arg_name arg_ty
@@ -515,8 +515,8 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
                 -- See Note [Pattern synonyms and higher rank types]
            ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
 
-skolemiseTvBndrsX :: SkolemInfo -> TCvSubst -> [VarBndr TyVar flag]
-                  -> TcM (TCvSubst, [VarBndr TcTyVar flag])
+skolemiseTvBndrsX :: SkolemInfo -> Subst -> [VarBndr TyVar flag]
+                  -> TcM (Subst, [VarBndr TcTyVar flag])
 -- Make new TcTyVars, all skolems with levels, but do not clone
 -- The level is one level deeper than the current level
 -- See Note [Skolemising when checking a pattern synonym]
@@ -525,8 +525,8 @@ skolemiseTvBndrsX skol_info orig_subst tvs
        ; let pushed_lvl = pushTcLevel tc_lvl
              details    = SkolemTv skol_info pushed_lvl False
 
-             mk_skol_tv_x :: TCvSubst -> VarBndr TyVar flag
-                          -> (TCvSubst, VarBndr TcTyVar flag)
+             mk_skol_tv_x :: Subst -> VarBndr TyVar flag
+                          -> (Subst, VarBndr TcTyVar flag)
              mk_skol_tv_x subst (Bndr tv flag)
                = (subst', Bndr new_tv flag)
                where
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index cbe8f03be9..4497fe4d4b 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE DisambiguateRecordFields #-}
 
@@ -179,7 +178,7 @@ topSkolemise :: SkolemInfo
 topSkolemise skolem_info ty
   = go init_subst idHsWrapper [] [] ty
   where
-    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+    init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     -- Why recursive?  See Note [Skolemisation]
     go subst wrap tv_prs ev_vars ty
@@ -241,16 +240,16 @@ instantiateSigma orig tvs theta body_ty
   where
     free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta
     in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs)
-    empty_subst = mkEmptyTCvSubst in_scope
+    empty_subst = mkEmptySubst in_scope
 
-instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
+instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM Subst
 -- Use this when you want to instantiate (forall a b c. ty) with
 -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
 -- not yet match (perhaps because there are unsolved constraints; #14154)
 -- If they don't match, emit a kind-equality to promise that they will
 -- eventually do so, and thus make a kind-homongeneous substitution.
 instTyVarsWith orig tvs tys
-  = go emptyTCvSubst tvs tys
+  = go emptySubst tvs tys
   where
     go subst [] []
       = return subst
@@ -335,11 +334,11 @@ instDFunType dfun_id dfun_inst_tys
   where
     dfun_ty = idType dfun_id
     (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
-    empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
+    empty_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
                   -- With quantified constraints, the
                   -- type of a dfun may not be closed
 
-    go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
+    go :: Subst -> [TyVar] -> [DFunInstType] -> TcM (Subst, [TcType])
     go subst [] [] = return (subst, [])
     go subst (tv:tvs) (Just ty : mb_tys)
       = do { (subst', tys) <- go (extendTvSubstAndInScope subst tv ty)
@@ -382,7 +381,7 @@ tcInstInvisibleTyBindersN 0 kind
 tcInstInvisibleTyBindersN n ty
   = go n empty_subst ty
   where
-    empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+    empty_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     go n subst kind
       | n > 0
@@ -395,7 +394,7 @@ tcInstInvisibleTyBindersN n ty
       = return ([], substTy subst kind)
 
 -- | Used only in *types*
-tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
+tcInstInvisibleTyBinder :: Subst -> TyBinder -> TcM (Subst, TcType)
 tcInstInvisibleTyBinder subst (Named (Bndr tv _))
   = do { (subst', tv') <- newMetaTyVarX subst tv
        ; return (subst', mkTyVarTy tv') }
@@ -458,7 +457,7 @@ mkEqBoxTy co ty1 ty2
 *                                                                      *
 ********************************************************************* -}
 
-tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
+tcInstType :: ([TyVar] -> TcM (Subst, [TcTyVar]))
                    -- ^ How to instantiate the type variables
            -> Id                                           -- ^ Type to instantiate
            -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
@@ -470,7 +469,7 @@ tcInstType inst_tyvars id
   | otherwise
   = do { (subst, tyvars') <- inst_tyvars tyvars
        ; let tv_prs  = map tyVarName tyvars `zip` tyvars'
-             subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+             subst'  = extendSubstInScopeSet subst (tyCoVarsOfType rho)
        ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
   where
     (tyvars, rho) = tcSplitForAllInvisTyVars (idType id)
@@ -484,16 +483,16 @@ tcInstTypeBndrs poly_ty
                   --      (?x :: Int) => Int -> Int
   = return ([], theta, tau)
   | otherwise
-  = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars
+  = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptySubst tyvars
        ; let tv_prs  = map (tyVarName . binderVar) tyvars `zip` tyvars'
-             subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
+             subst'  = extendSubstInScopeSet subst (tyCoVarsOfType rho)
        ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
   where
     (tyvars, rho) = splitForAllInvisTVBinders poly_ty
     (theta, tau)  = tcSplitPhiTy rho
 
-    inst_invis_bndr :: TCvSubst -> InvisTVBinder
-                    -> TcM (TCvSubst, InvisTVBinder)
+    inst_invis_bndr :: Subst -> InvisTVBinder
+                    -> TcM (Subst, InvisTVBinder)
     inst_invis_bndr subst (Bndr tv spec)
       = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
            ; return (subst', Bndr tv' spec) }
@@ -506,14 +505,14 @@ tcSkolDFunType skol_info dfun
   = do { (tv_prs, theta, tau) <- tcInstType (tcInstSuperSkolTyVars skol_info) dfun
        ; return (map snd tv_prs, theta, tau) }
 
-tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (TCvSubst, [TcTyVar])
+tcSuperSkolTyVars :: TcLevel -> SkolemInfo -> [TyVar] -> (Subst, [TcTyVar])
 -- Make skolem constants, but do *not* give them new names, as above
 -- As always, allocate them one level in
 -- Moreover, make them "super skolems"; see GHC.Core.InstEnv
 --    Note [Binding when looking up instances]
 -- See Note [Kind substitution when instantiating]
 -- Precondition: tyvars should be ordered by scoping
-tcSuperSkolTyVars tc_lvl skol_info = mapAccumL do_one emptyTCvSubst
+tcSuperSkolTyVars tc_lvl skol_info = mapAccumL do_one emptySubst
   where
     details = SkolemTv skol_info (pushTcLevel tc_lvl)
                        True   -- The "super" bit
@@ -525,29 +524,29 @@ tcSuperSkolTyVars tc_lvl skol_info = mapAccumL do_one emptyTCvSubst
 -- | Given a list of @['TyVar']@, skolemize the type variables,
 -- returning a substitution mapping the original tyvars to the
 -- skolems, and the list of newly bound skolems.
-tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
 -- See Note [Skolemising type variables]
-tcInstSkolTyVars skol_info = tcInstSkolTyVarsX skol_info emptyTCvSubst
+tcInstSkolTyVars skol_info = tcInstSkolTyVarsX skol_info emptySubst
 
-tcInstSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
 -- See Note [Skolemising type variables]
 tcInstSkolTyVarsX skol_info = tcInstSkolTyVarsPushLevel skol_info False
 
-tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
 -- See Note [Skolemising type variables]
 -- This version freshens the names and creates "super skolems";
 -- see comments around superSkolemTv.
-tcInstSuperSkolTyVars skol_info = tcInstSuperSkolTyVarsX skol_info emptyTCvSubst
+tcInstSuperSkolTyVars skol_info = tcInstSuperSkolTyVarsX skol_info emptySubst
 
-tcInstSuperSkolTyVarsX :: SkolemInfo -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+tcInstSuperSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
 -- See Note [Skolemising type variables]
 -- This version freshens the names and creates "super skolems";
 -- see comments around superSkolemTv.
 tcInstSuperSkolTyVarsX skol_info subst = tcInstSkolTyVarsPushLevel skol_info True subst
 
 tcInstSkolTyVarsPushLevel :: SkolemInfo -> Bool  -- True <=> make "super skolem"
-                          -> TCvSubst -> [TyVar]
-                          -> TcM (TCvSubst, [TcTyVar])
+                          -> Subst -> [TyVar]
+                          -> TcM (Subst, [TcTyVar])
 -- Skolemise one level deeper, hence pushTcLevel
 -- See Note [Skolemising type variables]
 tcInstSkolTyVarsPushLevel skol_info overlappable subst tvs
@@ -557,8 +556,8 @@ tcInstSkolTyVarsPushLevel skol_info overlappable subst tvs
        ; tcInstSkolTyVarsAt skol_info pushed_lvl overlappable subst tvs }
 
 tcInstSkolTyVarsAt :: SkolemInfo -> TcLevel -> Bool
-                   -> TCvSubst -> [TyVar]
-                   -> TcM (TCvSubst, [TcTyVar])
+                   -> Subst -> [TyVar]
+                   -> TcM (Subst, [TcTyVar])
 tcInstSkolTyVarsAt skol_info lvl overlappable subst tvs
   = freshenTyCoVarsX new_skol_tv subst tvs
   where
@@ -575,12 +574,12 @@ tcSkolemiseInvisibleBndrs skol_info ty
        ; skol_info     <- mkSkolemInfo skol_info
        ; let details = SkolemTv skol_info lvl False
              mk_skol_tv name kind = return (mkTcTyVar name kind details)  -- No freshening
-       ; (subst, tvs') <- instantiateTyVarsX mk_skol_tv emptyTCvSubst tvs
+       ; (subst, tvs') <- instantiateTyVarsX mk_skol_tv emptySubst tvs
        ; return (tvs', substTy subst body_ty) }
 
 instantiateTyVarsX :: (Name -> Kind -> TcM TcTyVar)
-                   -> TCvSubst -> [TyVar]
-                   -> TcM (TCvSubst, [TcTyVar])
+                   -> Subst -> [TyVar]
+                   -> TcM (Subst, [TcTyVar])
 -- Instantiate each type variable in turn with the specified function
 instantiateTyVarsX mk_tv subst tvs
   = case tvs of
@@ -592,25 +591,25 @@ instantiateTyVarsX mk_tv subst tvs
                      ; return (subst', tv':tvs') }
 
 ------------------
-freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
+freshenTyVarBndrs :: [TyVar] -> TcM (Subst, [TyVar])
 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
 --   as TyVars, rather than becoming TcTyVars
 -- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
 freshenTyVarBndrs = freshenTyCoVars mkTyVar
 
-freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
+freshenCoVarBndrsX :: Subst -> [CoVar] -> TcM (Subst, [CoVar])
 -- ^ Give fresh uniques to a bunch of CoVars
 -- Used in "GHC.Tc.Instance.Family.newFamInst"
 freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
 
 ------------------
 freshenTyCoVars :: (Name -> Kind -> TyCoVar)
-                -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
-freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
+                -> [TyVar] -> TcM (Subst, [TyCoVar])
+freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptySubst
 
 freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
-                 -> TCvSubst -> [TyCoVar]
-                 -> TcM (TCvSubst, [TyCoVar])
+                 -> Subst -> [TyCoVar]
+                 -> TcM (Subst, [TyCoVar])
 -- This a complete freshening operation:
 -- the skolems have a fresh unique, and a location from the monad
 -- See Note [Skolemising type variables]
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index c44ceba426..eed03d9323 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE MultiWayIf      #-}
 {-# LANGUAGE TupleSections   #-}
 
@@ -1072,35 +1071,35 @@ newOpenBoxedTypeKind
        ; let rr = mkTyConApp boxedRepDataConTyCon [lev]
        ; return (mkTYPEapp rr) }
 
-newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaTyVars :: [TyVar] -> TcM (Subst, [TcTyVar])
 -- Instantiate with META type variables
 -- Note that this works for a sequence of kind, type, and coercion variables
 -- variables.  Eg    [ (k:*), (a:k->k) ]
 --             Gives [ (k7:*), (a8:k7->k7) ]
-newMetaTyVars = newMetaTyVarsX emptyTCvSubst
-    -- emptyTCvSubst has an empty in-scope set, but that's fine here
+newMetaTyVars = newMetaTyVarsX emptySubst
+    -- emptySubst has an empty in-scope set, but that's fine here
     -- Since the tyvars are freshly made, they cannot possibly be
     -- captured by any existing for-alls.
 
-newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaTyVarsX :: Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
 -- Just like newMetaTyVars, but start with an existing substitution.
 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
 
-newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newMetaTyVarX :: Subst -> TyVar -> TcM (Subst, TcTyVar)
 -- Make a new unification variable tyvar whose Name and Kind come from
 -- an existing TyVar. We substitute kind variables in the kind.
 newMetaTyVarX = new_meta_tv_x TauTv
 
-newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newMetaTyVarTyVarX :: Subst -> TyVar -> TcM (Subst, TcTyVar)
 -- Just like newMetaTyVarX, but make a TyVarTv
 newMetaTyVarTyVarX = new_meta_tv_x TyVarTv
 
-newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+newWildCardX :: Subst -> TyVar -> TcM (Subst, TcTyVar)
 newWildCardX subst tv
   = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
        ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }
 
-new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+new_meta_tv_x :: MetaInfo -> Subst -> TyVar -> TcM (Subst, TcTyVar)
 new_meta_tv_x info subst tv
   = do  { new_tv <- cloneAnonMetaTyVar info tv substd_kind
         ; let subst1 = extendTvSubstWithClone subst tv new_tv
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 82924e9115..805e58fc39 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections       #-}
@@ -158,15 +157,15 @@ module GHC.Tc.Utils.TcType (
   isVisibleBinder, isInvisibleBinder,
 
   -- Type substitutions
-  TCvSubst(..),         -- Representation visible to a few friends
-  TvSubstEnv, emptyTCvSubst, mkEmptyTCvSubst,
+  Subst(..),         -- Representation visible to a few friends
+  TvSubstEnv, emptySubst, mkEmptySubst,
   zipTvSubst,
-  mkTvSubstPrs, notElemTCvSubst, unionTCvSubst,
-  getTvSubstEnv, setTvSubstEnv, getTCvInScope, extendTCvInScope,
-  extendTCvInScopeList, extendTCvInScopeSet, extendTvSubstAndInScope,
+  mkTvSubstPrs, notElemSubst, unionSubst,
+  getTvSubstEnv, getSubstInScope, extendSubstInScope,
+  extendSubstInScopeList, extendSubstInScopeSet, extendTvSubstAndInScope,
   Type.lookupTyVar, Type.extendTCvSubst, Type.substTyVarBndr,
   Type.extendTvSubst,
-  isInScope, mkTCvSubst, mkTvSubst, zipTyEnv, zipCoEnv,
+  isInScope, mkSubst, mkTvSubst, zipTyEnv, zipCoEnv,
   Type.substTy, substTys, substScaledTys, substTyWith, substTyWithCoVars,
   substTyAddInScope,
   substTyUnchecked, substTysUnchecked, substScaledTyUnchecked,
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 91b0d5015e..1eb81d8191 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1370,7 +1370,7 @@ deeplySkolemise :: SkolemInfo -> TcSigmaType
 deeplySkolemise skol_info ty
   = go init_subst ty
   where
-    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+    init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     go subst ty
       | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
@@ -1397,7 +1397,7 @@ deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
 deeplyInstantiate orig ty
   = go init_subst ty
   where
-    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
+    init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     go subst ty
       | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index cd628b5622..d6a5b15dbb 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1,4 +1,3 @@
-
 {-# LANGUAGE DerivingStrategies #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -2272,7 +2271,7 @@ checkConsistentFamInst (InClsInst { ai_class = clas
     -- For check_match, bind_me, see
     -- Note [Matching in the consistent-instantiation check]
     check_match :: [(Type,Type,ArgFlag)] -> TcM ()
-    check_match triples = go emptyTCvSubst emptyTCvSubst triples
+    check_match triples = go emptySubst emptySubst triples
 
     go _ _ [] = return ()
     go lr_subst rl_subst ((ty1,ty2,vis):triples)