Rename SigTv to TyVarTv (#15480)

because since #15050, these are no longer used in pattern SIGnatures,
but still in other places where meta-variables should only be unified
with TYpe VARiables.

I also found mentions of `SigTv` in parts of the renamer and desugarer
that do not seem to directly relate to `SigTv` as used in the type
checker, but rather to uses of `forall a.` in type signatures. I renamed
these to `ScopedTv`.

Differential Revision: https://phabricator.haskell.org/D5074

22 files changed, 165 insertions, 173 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 5b74487..ed2c612 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -122,7 +122,7 @@ repTopDs group@(HsGroup { hs_valds   = valds
                         , hs_annds   = annds
                         , hs_ruleds  = ruleds
                         , hs_docs    = docs })
- = do { let { bndrs  = hsSigTvBinders valds
+ = do { let { bndrs  = hsScopedTvBinders valds
                        ++ hsGroupBinders group
                        ++ hsPatSynSelectors valds
             ; instds = tyclds >>= group_instds } ;
@@ -180,9 +180,9 @@ repTopDs group@(HsGroup { hs_valds   = valds
       = notHandledL loc "Haddock documentation" empty
 repTopDs (XHsGroup _) = panic "repTopDs"
 
-hsSigTvBinders :: HsValBinds GhcRn -> [Name]
+hsScopedTvBinders :: HsValBinds GhcRn -> [Name]
 -- See Note [Scoped type variables in bindings]
-hsSigTvBinders binds
+hsScopedTvBinders binds
   = concatMap get_scoped_tvs sigs
   where
     sigs = case binds of
@@ -222,7 +222,7 @@ Here the 'forall a' brings 'a' into scope over the binding group.
 To achieve this we
 
   a) Gensym a binding for 'a' at the same time as we do one for 'f'
-     collecting the relevant binders with hsSigTvBinders
+     collecting the relevant binders with hsScopedTvBinders
 
   b) When processing the 'forall', don't gensym
 
@@ -1484,12 +1484,12 @@ repBinds (EmptyLocalBinds _)
 repBinds b@(HsIPBinds {}) = notHandled "Implicit parameters" (ppr b)
 
 repBinds (HsValBinds _ decs)
- = do   { let { bndrs = hsSigTvBinders decs ++ collectHsValBinders decs }
+ = do   { let { bndrs = hsScopedTvBinders decs ++ collectHsValBinders decs }
                 -- No need to worry about detailed scopes within
                 -- the binding group, because we are talking Names
                 -- here, so we can safely treat it as a mutually
                 -- recursive group
-                -- For hsSigTvBinders see Note [Scoped type variables in bindings]
+                -- For hsScopedTvBinders see Note [Scoped type variables in bindings]
         ; ss        <- mkGenSyms bndrs
         ; prs       <- addBinds ss (rep_val_binds decs)
         ; core_list <- coreList decQTyConName
diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs
index a2218e4..7cd5c55 100644
--- a/compiler/rename/RnBinds.hs
+++ b/compiler/rename/RnBinds.hs
@@ -296,7 +296,7 @@ rnValBindsRHS :: HsSigCtxt
 
 rnValBindsRHS ctxt (ValBinds _ mbinds sigs)
   = do { (sigs', sig_fvs) <- renameSigs ctxt sigs
-       ; binds_w_dus <- mapBagM (rnLBind (mkSigTvFn sigs')) mbinds
+       ; binds_w_dus <- mapBagM (rnLBind (mkScopedTvFn sigs')) mbinds
        ; let !(anal_binds, anal_dus) = depAnalBinds binds_w_dus
 
        ; let patsyn_fvs = foldr (unionNameSet . psb_ext) emptyNameSet $
@@ -581,21 +581,21 @@ depAnalBinds binds_w_dus
 
 ---------------------
 -- Bind the top-level forall'd type variables in the sigs.
--- E.g  f :: a -> a
+-- E.g  f :: forall a. a -> a
 --      f = rhs
 --      The 'a' scopes over the rhs
 --
 -- NB: there'll usually be just one (for a function binding)
 --     but if there are many, one may shadow the rest; too bad!
---      e.g  x :: [a] -> [a]
---           y :: [(a,a)] -> a
+--      e.g  x :: forall a. [a] -> [a]
+--           y :: forall a. [(a,a)] -> a
 --           (x,y) = e
 --      In e, 'a' will be in scope, and it'll be the one from 'y'!
 
-mkSigTvFn :: [LSig GhcRn] -> (Name -> [Name])
+mkScopedTvFn :: [LSig GhcRn] -> (Name -> [Name])
 -- Return a lookup function that maps an Id Name to the names
 -- of the type variables that should scope over its body.
-mkSigTvFn sigs = \n -> lookupNameEnv env n `orElse` []
+mkScopedTvFn sigs = \n -> lookupNameEnv env n `orElse` []
   where
     env = mkHsSigEnv get_scoped_tvs sigs
 
@@ -663,9 +663,9 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
        -- invariant: no free vars here when it's a FunBind
   = do  { pattern_synonym_ok <- xoptM LangExt.PatternSynonyms
         ; unless pattern_synonym_ok (addErr patternSynonymErr)
-        ; let sig_tvs = sig_fn name
+        ; let scoped_tvs = sig_fn name
 
-        ; ((pat', details'), fvs1) <- bindSigTyVarsFV sig_tvs $
+        ; ((pat', details'), fvs1) <- bindSigTyVarsFV scoped_tvs $
                                       rnPat PatSyn pat $ \pat' ->
          -- We check the 'RdrName's instead of the 'Name's
          -- so that the binding locations are reported
@@ -700,7 +700,7 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
             Unidirectional -> return (Unidirectional, emptyFVs)
             ImplicitBidirectional -> return (ImplicitBidirectional, emptyFVs)
             ExplicitBidirectional mg ->
-                do { (mg', fvs) <- bindSigTyVarsFV sig_tvs $
+                do { (mg', fvs) <- bindSigTyVarsFV scoped_tvs $
                                    rnMatchGroup (mkPrefixFunRhs (L l name))
                                                 rnLExpr mg
                    ; return (ExplicitBidirectional mg', fvs) }
@@ -867,7 +867,7 @@ rnMethodBinds is_cls_decl cls ktv_names binds sigs
        -- Answer no in Haskell 2010, but yes if you have -XScopedTypeVariables
        ; scoped_tvs  <- xoptM LangExt.ScopedTypeVariables
        ; (binds'', bind_fvs) <- maybe_extend_tyvar_env scoped_tvs $
-              do { binds_w_dus <- mapBagM (rnLBind (mkSigTvFn other_sigs')) binds'
+              do { binds_w_dus <- mapBagM (rnLBind (mkScopedTvFn other_sigs')) binds'
                  ; let bind_fvs = foldrBag (\(_,_,fv1) fv2 -> fv1 `plusFV` fv2)
                                            emptyFVs binds_w_dus
                  ; return (mapBag fstOf3 binds_w_dus, bind_fvs) }
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 4bd91d8..b549856 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -941,12 +941,12 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                                       , sig_inst_theta = annotated_theta
                                       , sig_inst_skols = annotated_tvs }))
   = -- Choose quantifiers for a partial type signature
-    do { psig_qtv_prs <- zonkSigTyVarPairs annotated_tvs
+    do { psig_qtv_prs <- zonkTyVarTyVarPairs annotated_tvs
 
             -- Check whether the quantified variables of the
             -- partial signature have been unified together
             -- See Note [Quantified variables in partial type signatures]
-       ; mapM_ report_dup_sig_tv_err  (findDupSigTvs psig_qtv_prs)
+       ; mapM_ report_dup_tyvar_tv_err  (findDupTyVarTvs psig_qtv_prs)
 
             -- Check whether a quantified variable of the partial type
             -- signature is not actually quantified.  How can that happen?
@@ -969,7 +969,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
 
        ; return (final_qtvs, my_theta) }
   where
-    report_dup_sig_tv_err (n1,n2)
+    report_dup_tyvar_tv_err (n1,n2)
       | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
       = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
                         <+> text "with" <+> quotes (ppr n2))
@@ -977,7 +977,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                            2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
 
       | otherwise -- Can't happen; by now we know it's a partial sig
-      = pprPanic "report_sig_tv_err" (ppr sig)
+      = pprPanic "report_tyvar_tv_err" (ppr sig)
 
     report_mono_sig_tv_err n
       | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
@@ -985,7 +985,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                      2 (hang (text "bound by the partial type signature:")
                            2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
       | otherwise -- Can't happen; by now we know it's a partial sig
-      = pprPanic "report_sig_tv_err" (ppr sig)
+      = pprPanic "report_mono_sig_tv_err" (ppr sig)
 
     choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
                         -> TcM (VarSet, TcThetaType)
@@ -1136,7 +1136,7 @@ Consider
   g x y = [x, y]
 
 Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
-together, which is fine.  So we bind 'a' and 'b' to SigTvs, which can then
+together, which is fine.  So we bind 'a' and 'b' to TyVarTvs, which can then
 unify with each other.
 
 But now consider:
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index c45afd2..d6aed31 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1993,10 +1993,10 @@ canEqTyVarTyVar, are these
    number) on the left, so there is the best chance of unifying it
         alpha[3] ~ beta[2]
 
- * If both are meta-tyvars and both at the same level, put a SigTv
+ * If both are meta-tyvars and both at the same level, put a TyVarTv
    on the right if possible
         alpha[2] ~ beta[2](sig-tv)
-   That way, when we unify alpha := beta, we don't lose the SigTv flag.
+   That way, when we unify alpha := beta, we don't lose the TyVarTv flag.
 
  * Put a meta-tv with a System Name on the left if possible so it
    gets eliminated (improves error messages)
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index c044cde..bc5b061 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -635,8 +635,8 @@ isSkolemTy :: TcLevel -> Type -> Bool
 isSkolemTy tc_lvl ty
   | Just tv <- getTyVar_maybe ty
   =  isSkolemTyVar tv
-  || (isSigTyVar tv && isTouchableMetaTyVar tc_lvl tv)
-     -- The last case is for touchable SigTvs
+  || (isTyVarTyVar tv && isTouchableMetaTyVar tc_lvl tv)
+     -- The last case is for touchable TyVarTvs
      -- we postpone untouchables to a latter test (too obscure)
 
   | otherwise
@@ -1606,7 +1606,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
   , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
-    || isSigTyVar tv1 && not (isTyVarTy ty2)
+    || isTyVarTyVar tv1 && not (isTyVarTy ty2)
     || ctEqRel ct == ReprEq
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
@@ -1669,7 +1669,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
 
   -- If the immediately-enclosing implication has 'tv' a skolem, and
   -- we know by now its an InferSkol kind of skolem, then presumably
-  -- it started life as a SigTv, else it'd have been unified, given
+  -- it started life as a TyVarTv, else it'd have been unified, given
   -- that there's no occurs-check or forall problem
   | (implic:_) <- cec_encl ctxt
   , Implic { ic_skols = skols } <- implic
@@ -1707,7 +1707,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
   -- Nastiest case: attempt to unify an untouchable variable
   -- So tv is a meta tyvar (or started that way before we
   -- generalised it).  So presumably it is an *untouchable*
-  -- meta tyvar or a SigTv, else it'd have been unified
+  -- meta tyvar or a TyVarTv, else it'd have been unified
   -- See Note [Error messages for untouchables]
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 529fbaf..79ffc4d 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -2075,9 +2075,9 @@ unflattenWanteds tv_eqs funeqs
       | Just (rhs_tv, co) <- getCastedTyVar_maybe rhs
                              -- co :: kind(rhs_tv) ~ kind(lhs_tv)
       , isFmvTyVar rhs_tv || (isTouchableMetaTyVar tclvl rhs_tv
-                              && not (isSigTyVar rhs_tv))
+                              && not (isTyVarTyVar rhs_tv))
                               -- LHS is a filled fmv, and so is a type
-                              -- family application, which a SigTv should
+                              -- family application, which a TyVarTv should
                               -- not unify with
       = do { is_filled <- isFilledMetaTyVar rhs_tv
            ; if is_filled then return False
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 007b970..6048caa 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1367,7 +1367,7 @@ Sidenote: It's quite possible that later, we'll consider (t -> s)
 as a degenerate case of some (pi (x :: t) -> s) and then this will
 all get more permissive.
 
-Note [Kind generalisation and SigTvs]
+Note [Kind generalisation and TyVarTvs]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
   data T (a :: k1) x = MkT (S a ())
@@ -1375,14 +1375,14 @@ Consider
 
 While we are doing kind inference for the mutually-recursive S,T,
 we will end up unifying k1 and k2 together. So they can't be skolems.
-We therefore make them SigTvs, which can unify with type variables,
+We therefore make them TyVarTvs, which can unify with type variables,
 but not with general types.  All this is very similar at the level
 of terms: see Note [Quantified variables in partial type signatures]
 in TcBinds.
 
 There are some wrinkles
 
-* We always want to kind-generalise over SigTvs, and /not/ default
+* We always want to kind-generalise over TyVarTvs, and /not/ default
   them to Type.  Another way to say this is: a SigTV should /never/
   stand for a type, even via defaulting. Hence the check in
   TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar.  Here's
@@ -1398,7 +1398,7 @@ There are some wrinkles
   Here we will unify k1 with k2, but this time doing so is an error,
   because k1 and k2 are bound in the same delcaration.
 
-  We sort this out using findDupSigTvs, in TcTyClTyVars; very much
+  We sort this out using findDupTyVarTvs, in TcTyClTyVars; very much
   as we do with partial type signatures in mk_psig_qtvs in
   TcBinds.chooseInferredQuantifiers
 
@@ -1571,8 +1571,8 @@ kcLHsQTyVars name flav cusk
 
   | otherwise
   = do { (scoped_kvs, (tc_tvs, res_kind))
-           -- Why kcImplicitTKBndrs which uses newSigTyVar?
-           -- See Note [Kind generalisation and SigTvs]
+           -- Why kcImplicitTKBndrs which uses newTyVarTyVar?
+           -- See Note [Kind generalisation and TyVarTvs]
            <- kcImplicitTKBndrs kv_ns $
               kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside
 
@@ -1691,14 +1691,14 @@ Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
 --------------------------------------
 
 -- | Bring implicitly quantified type/kind variables into scope during
--- kind checking. Uses SigTvs, as per Note [Use SigTvs in kind-checking pass]
+-- kind checking. Uses TyVarTvs, as per Note [Use TyVarTvs in kind-checking pass]
 -- in TcTyClsDecls.
 kcImplicitTKBndrs :: [Name]     -- of the vars
                   -> TcM a
                   -> TcM ([TcTyVar], a)  -- returns the tyvars created
                                          -- these are *not* dependency ordered
 kcImplicitTKBndrs var_ns thing_inside
-  = do { tkvs <- mapM newFlexiKindedSigTyVar var_ns
+  = do { tkvs <- mapM newFlexiKindedTyVarTyVar var_ns
        ; result <- tcExtendTyVarEnv tkvs thing_inside
        ; return (tkvs, result) }
 
@@ -1709,7 +1709,7 @@ tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs
   -> TcM a
   -> TcM ([TcTyVar], a)
 tcImplicitTKBndrs    = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar
-tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedSigTyVar
+tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedTyVarTyVar
 tcImplicitQTKBndrs   = tcImplicitTKBndrsX newFlexiKindedQTyVar
 
 tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function
@@ -1741,7 +1741,7 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
                  ; return (tkvs, result) }
 
        ; skol_tvs <- mapM zonkTcTyCoVarBndr skol_tvs
-          -- use zonkTcTyCoVarBndr because a skol_tv might be a SigTv
+          -- use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
 
           -- do a stable topological sort, following
           -- Note [Ordering of implicit variables] in HsTypes
@@ -1767,8 +1767,8 @@ newFlexiKindedTyVar new_tv name
 newFlexiKindedSkolemTyVar :: Name -> TcM TyVar
 newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar
 
-newFlexiKindedSigTyVar :: Name -> TcM TyVar
-newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
+newFlexiKindedTyVarTyVar :: Name -> TcM TyVar
+newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar
 
 --------------------------------------
 -- Explicit binders
@@ -1776,13 +1776,13 @@ newFlexiKindedSigTyVar = newFlexiKindedTyVar newSigTyVar
 
 -- | Used during the "kind-checking" pass in TcTyClsDecls only,
 -- and even then only for data-con declarations.
--- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
+-- See Note [Use TyVarTvs in kind-checking pass] in TcTyClsDecls
 kcExplicitTKBndrs :: [LHsTyVarBndr GhcRn]
                   -> TcM a
                   -> TcM a
 kcExplicitTKBndrs [] thing_inside = thing_inside
 kcExplicitTKBndrs (L _ hs_tv : hs_tvs) thing_inside
-  = do { tv <- tcHsTyVarBndr newSigTyVar hs_tv
+  = do { tv <- tcHsTyVarBndr newTyVarTyVar hs_tv
        ; tcExtendTyVarEnv [tv] $
          kcExplicitTKBndrs hs_tvs thing_inside }
 
@@ -2067,7 +2067,7 @@ kcLookupTcTyCon nm
 -- Never emits constraints, though the thing_inside might.
 kcTyClTyVars :: Name -> TcM a -> TcM a
 kcTyClTyVars tycon_name thing_inside
-  -- See Note [Use SigTvs in kind-checking pass] in TcTyClsDecls
+  -- See Note [Use TyVarTvs in kind-checking pass] in TcTyClsDecls
   = do { tycon <- kcLookupTcTyCon tycon_name
        ; tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
 
@@ -2097,9 +2097,9 @@ tcTyClTyVars tycon_name thing_inside
        ; let flav = tyConFlavour tycon
              scoped_prs = tcTyConScopedTyVars tycon
              scoped_tvs = map snd scoped_prs
-             still_sig_tvs = filter isSigTyVar scoped_tvs
+             still_sig_tvs = filter isTyVarTyVar scoped_tvs
 
-       ; mapM_ report_sig_tv_err (findDupSigTvs scoped_prs)
+       ; mapM_ report_sig_tv_err (findDupTyVarTvs scoped_prs)
 
        ; checkNoErrs $ reportFloatingKvs tycon_name flav
                                          scoped_tvs still_sig_tvs
@@ -2284,7 +2284,7 @@ tcHsPartialSigType ctxt sig_ty
                   ; return (wcs, wcx, theta, tau) }
 
          -- We must return these separately, because all the zonking below
-         -- might change the name of a SigTv. This, in turn, causes trouble
+         -- might change the name of a TyVarTv. This, in turn, causes trouble
          -- in partial type signatures that bind scoped type variables, as
          -- we bring the wrong name into scope in the function body.
          -- Test case: partial-sigs/should_compile/LocalDefinitionBug
@@ -2295,17 +2295,17 @@ tcHsPartialSigType ctxt sig_ty
        -- See Note [Extra-constraint holes in partial type signatures]
        ; emitWildCardHoleConstraints wcs
 
-         -- The SigTvs created above will sometimes have too high a TcLevel
+         -- The TyVarTvs created above will sometimes have too high a TcLevel
          -- (note that they are generated *after* bumping the level in
          -- the tc{Im,Ex}plicitTKBndrsSig functions. Bumping the level
          -- is still important here, because the kinds of these variables
          -- do indeed need to have the higher level, so they can unify
          -- with other local type variables. But, now that we've type-checked
          -- everything (and solved equalities in the tcImplicit call)
-         -- we need to promote the SigTvs so we don't violate the TcLevel
+         -- we need to promote the TyVarTvs so we don't violate the TcLevel
          -- invariant
        ; all_tvs <- mapM zonkPromoteTyCoVarBndr (implicit_tvs ++ explicit_tvs)
-            -- zonkPromoteTyCoVarBndr deals well with SigTvs
+            -- zonkPromoteTyCoVarBndr deals well with TyVarTvs
 
        ; theta   <- mapM zonkPromoteType theta
        ; tau     <- zonkPromoteType tau
@@ -2427,7 +2427,7 @@ tcHsPatSigType ctxt sig_ty
     mk_tv_pair tv = do { tv' <- zonkTcTyVarToTyVar tv
                        ; return (tyVarName tv, tv') }
          -- The Name is one of sig_vars, the lexically scoped name
-         -- But if it's a SigTyVar, it might have been unified
+         -- But if it's a TyVarTv, it might have been unified
          -- with an existing in-scope skolem, so we must zonk
          -- here.  See Note [Pattern signature binders]
 tcHsPatSigType _ (HsWC _ (XHsImplicitBndrs _)) = panic "tcHsPatSigType"
@@ -2470,7 +2470,7 @@ tcPatSig in_pat_bind sig res_ty
                 -- Here 'a' doesn't get a binding.  Sigh
         ; let bad_tvs = [ tv | (_,tv) <- sig_tvs
                              , not (tv `elemVarSet` exactTyCoVarsOfType sig_ty) ]
-        ; checkTc (null bad_tvs) (badPatSigTvs sig_ty bad_tvs)
+        ; checkTc (null bad_tvs) (badPatTyVarTvs sig_ty bad_tvs)
 
         -- Now do a subsumption check of the pattern signature against res_ty
         ; wrap <- addErrCtxtM (mk_msg sig_ty) $
@@ -2625,8 +2625,8 @@ zonkPromoteTyCoVarKind = updateTyVarKindM zonkPromoteType
 
 zonkPromoteTyCoVarBndr :: TyCoVar -> TcM TyCoVar
 zonkPromoteTyCoVarBndr tv
-  | isSigTyVar tv
-  = tcGetTyVar "zonkPromoteTyCoVarBndr SigTv" <$> zonkPromoteTcTyVar tv
+  | isTyVarTyVar tv
+  = tcGetTyVar "zonkPromoteTyCoVarBndr TyVarTv" <$> zonkPromoteTcTyVar tv
 
   | isTcTyVar tv && isSkolemTyVar tv
   = do { tc_lvl <- getTcLevel
@@ -2699,8 +2699,8 @@ promotionErr name err
 ************************************************************************
 -}
 
-badPatSigTvs :: TcType -> [TyVar] -> SDoc
-badPatSigTvs sig_ty bad_tvs
+badPatTyVarTvs :: TcType -> [TyVar] -> SDoc
+badPatTyVarTvs sig_ty bad_tvs
   = vcat [ fsep [text "The type variable" <> plural bad_tvs,
                  quotes (pprWithCommas ppr bad_tvs),
                  text "should be bound by the pattern signature" <+> quotes (ppr sig_ty),
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index a44b5e0..3beef4d 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -50,8 +50,8 @@ module TcMType (
   --------------------------------
   -- Instantiation
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
-  newMetaSigTyVars, newMetaSigTyVarX,
-  newSigTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
+  newMetaTyVarTyVars, newMetaTyVarTyVarX,
+  newTyVarTyVar, newTauTyVar, newSkolemTyVar, newWildCardX,
   tcInstType,
   tcInstSkolTyVars,tcInstSkolTyVarsX,
   tcInstSuperSkolTyVarsX,
@@ -65,7 +65,7 @@ module TcMType (
   tidyEvVar, tidyCt, tidySkolemInfo,
   skolemiseRuntimeUnk,
   zonkTcTyVar, zonkTcTyVars,
-  zonkTcTyVarToTyVar, zonkSigTyVarPairs,
+  zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
   zonkTyCoVarsAndFV, zonkTcTypeAndFV,
   zonkTyCoVarsAndFVList,
   zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
@@ -621,32 +621,32 @@ instead of the buggous
 -}
 
 {-
-Note [SigTv]
+Note [TyVarTv]
 ~~~~~~~~~~~~
 
-A SigTv can unify with type *variables* only, including other SigTvs and
+A TyVarTv can unify with type *variables* only, including other TyVarTvs and
 skolems. Sometimes, they can unify with type variables that the user would
 rather keep distinct; see #11203 for an example.  So, any client of this
-function needs to either allow the SigTvs to unify with each other or check
-that they don't (say, with a call to findDubSigTvs).
+function needs to either allow the TyVarTvs to unify with each other or check
+that they don't (say, with a call to findDubTyVarTvs).
 
-Before #15050 this was used for ScopedTypeVariables in patterns, to make sure
-these type variables only refer to other type variables, but this restriction
-was dropped, and ScopedTypeVariables can now refer to full types (GHC Proposal
-29).
+Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in
+patterns, to make sure these type variables only refer to other type variables,
+but this restriction was dropped, and ScopedTypeVariables can now refer to full
+types (GHC Proposal 29).
 
-The remaining uses of newSigTyVars are
-* in kind signatures, see Note [Kind generalisation and SigTvs]
-  and Note [Use SigTvs in kind-checking pass]
+The remaining uses of newTyVarTyVars are
+* in kind signatures, see Note [Kind generalisation and TyVarTvs]
+  and Note [Use TyVarTvs in kind-checking pass]
 * in partial type signatures, see Note [Quantified variables in partial type signatures]
 -}
 
--- see Note [SigTv]
-newSigTyVar :: Name -> Kind -> TcM TcTyVar
-newSigTyVar name kind
-  = do { details <- newMetaDetails SigTv
+-- see Note [TyVarTv]
+newTyVarTyVar :: Name -> Kind -> TcM TcTyVar
+newTyVarTyVar name kind
+  = do { details <- newMetaDetails TyVarTv
        ; let tyvar = mkTcTyVar name kind details
-       ; traceTc "newSigTyVar" (ppr tyvar)
+       ; traceTc "newTyVarTyVar" (ppr tyvar)
        ; return tyvar }
 
 
@@ -846,7 +846,7 @@ newAnonMetaTyVar meta_info kind
                         TauTv       -> fsLit "t"
                         FlatMetaTv  -> fsLit "fmv"
                         FlatSkolTv  -> fsLit "fsk"
-                        SigTv       -> fsLit "a"
+                        TyVarTv      -> fsLit "a"
         ; details <- newMetaDetails meta_info
         ; let tyvar = mkTcTyVar name kind details
         ; traceTc "newAnonMetaTyVar" (ppr tyvar)
@@ -892,8 +892,8 @@ newOpenFlexiTyVarTy
   = do { kind <- newOpenTypeKind
        ; newFlexiTyVarTy kind }
 
-newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
-newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst
+newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
+newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst
 
 newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Instantiate with META type variables
@@ -914,9 +914,9 @@ newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
 -- Just like newMetaTyVars, but start with an existing substitution.
 newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
 
-newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
--- Just like newMetaTyVarX, but make a SigTv
-newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar
+newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
+-- Just like newMetaTyVarX, but make a TyVarTv
+newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar
 
 newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
 newWildCardX subst tv
@@ -1102,16 +1102,16 @@ defaultTyVar default_kind tv
   | not (isMetaTyVar tv)
   = return False
 
-  | isSigTyVar tv
-    -- Do not default SigTvs. Doing so would violate the invariants
-    -- on SigTvs; see Note [Signature skolems] in TcType.
+  | isTyVarTyVar tv
+    -- Do not default TyVarTvs. Doing so would violate the invariants
+    -- on TyVarTvs; see Note [Signature skolems] in TcType.
     -- Trac #13343 is an example; #14555 is another
-    -- See Note [Kind generalisation and SigTvs]
+    -- See Note [Kind generalisation and TyVarTvs]
   = return False
 
 
   | isRuntimeRepVar tv  -- Do not quantify over a RuntimeRep var
-                        -- unless it is a SigTv, handled earlier
+                        -- unless it is a TyVarTv, handled earlier
   = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
@@ -1575,14 +1575,14 @@ zonkCo = mapCoercion zonkTcTypeMapper ()
 
 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
 -- A tyvar binder is never a unification variable (TauTv),
--- rather it is always a skolem. It *might* be a SigTv.
--- (Because non-CUSK type declarations use SigTvs.)
+-- rather it is always a skolem. It *might* be a TyVarTv.
+-- (Because non-CUSK type declarations use TyVarTvs.)
 -- Regardless, it may have a kind
 -- that has not yet been zonked, and may include kind
 -- unification variables.
 zonkTcTyCoVarBndr tyvar
-  | isSigTyVar tyvar
-  = tcGetTyVar "zonkTcTyCoVarBndr SigTv" <$> zonkTcTyVar tyvar
+  | isTyVarTyVar tyvar
+  = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" <$> zonkTcTyVar tyvar
 
   | otherwise
     -- can't use isCoVar, because it looks at a TyCon. Argh.
@@ -1614,7 +1614,7 @@ zonkTcTyVar tv
                               ; return (mkTyVarTy z_tv) }
 
 -- Variant that assumes that any result of zonking is still a TyVar.
--- Should be used only on skolems and SigTvs
+-- Should be used only on skolems and TyVarTvs
 zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar
 zonkTcTyVarToTyVar tv
   = do { ty <- zonkTcTyVar tv
@@ -1624,8 +1624,8 @@ zonkTcTyVarToTyVar tv
                                           (ppr tv $$ ppr ty)
        ; return tv' }
 
-zonkSigTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
-zonkSigTyVarPairs prs
+zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)]
+zonkTyVarTyVarPairs prs
   = mapM do_one prs
   where
     do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index ed7a445..fabe16a 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -550,10 +550,10 @@ a pattern synonym.  What about the /building/ side?
   tcPatSynBuilderBind, by converting the pattern to an expression and
   typechecking it.
 
-  At one point, for ImplicitBidirectional I used SigTvs (instead of
+  At one point, for ImplicitBidirectional I used TyVarTvs (instead of
   TauTvs) in tcCheckPatSynDecl.  But (a) strengthening the check here
   is redundant since tcPatSynBuilderBind does the job, (b) it was
-  still incomplete (SigTvs can unify with each other), and (c) it
+  still incomplete (TyVarTvs can unify with each other), and (c) it
   didn't even work (Trac #13441 was accepted with
   ExplicitBidirectional, but rejected if expressed in
   ImplicitBidirectional form.  Conclusion: trying to be too clever is
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 6627c25..ca5639b 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1500,7 +1500,7 @@ data TcIdSigInst
   = TISI { sig_inst_sig :: TcIdSigInfo
 
          , sig_inst_skols :: [(Name, TcTyVar)]
-               -- Instantiated type and kind variables, SigTvs
+               -- Instantiated type and kind variables, TyVarTvs
                -- The Name is the Name that the renamer chose;
                --   but the TcTyVar may come from instantiating
                --   the type and hence have a different unique.
diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs
index 4f4d9b0..f3fa882 100644
--- a/compiler/typecheck/TcSigs.hs
+++ b/compiler/typecheck/TcSigs.hs
@@ -401,7 +401,7 @@ tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
 -- Instantiate a type signature; only used with plan InferGen
 tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
   = setSrcSpan loc $  -- Set the binding site of the tyvars
-    do { (tv_prs, theta, tau) <- tcInstType newMetaSigTyVars poly_id
+    do { (tv_prs, theta, tau) <- tcInstType newMetaTyVarTyVars poly_id
               -- See Note [Pattern bindings and complete signatures]
 
        ; return (TISI { sig_inst_sig   = sig
@@ -446,8 +446,8 @@ tcInstSig sig@(PartialSig { psig_hs_ty = hs_ty
   where
     mk_sig_tv old_name kind
       = do { uniq <- newUnique
-           ; newSigTyVar (setNameUnique old_name uniq) kind }
-      -- Why newSigTyVar?  See TcBinds
+           ; newTyVarTyVar (setNameUnique old_name uniq) kind }
+      -- Why newTyVarTyVar?  See TcBinds
       -- Note [Quantified variables in partial type signatures]
 
 
@@ -461,8 +461,8 @@ Consider
 Here we'll infer a type from the pattern of 'T a', but if we feed in
 the signature types for f and g, we'll end up unifying 'a' and 'b'
 
-So we instantiate f and g's signature with SigTv skolems
-(newMetaSigTyVars) that can unify with each other.  If too much
+So we instantiate f and g's signature with TyVarTv skolems
+(newMetaTyVarTyVars) that can unify with each other.  If too much
 unification takes place, we'll find out when we do the final
 impedance-matching check in TcBinds.mkExport
 
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 7ea19b4..c2d7eb0 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -932,7 +932,7 @@ decideMonoTyVars infer_mode name_taus psigs candidates
   = do { (no_quant, maybe_quant) <- pick infer_mode candidates
 
        -- If possible, we quantify over partial-sig qtvs, so they are
-       -- not mono. Need to zonk them because they are meta-tyvar SigTvs
+       -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
        ; psig_qtvs <- mapM zonkTcTyVarToTyVar $
                       concatMap (map snd . sig_inst_skols) psigs
 
@@ -1165,7 +1165,7 @@ However, in the case of a partial type signature, be doing inference
 or
    g :: (Eq _a) => _b -> _b
 In both cases we use plan InferGen, and hence call simplifyInfer.  But
-those 'a' variables are skolems (actually SigTvs), and we should be
+those 'a' variables are skolems (actually TyVarTvs), and we should be
 sure to quantify over them.  This leads to several wrinkles:
 
 * Wrinkle 1.  In the case of a type error
@@ -1953,9 +1953,9 @@ promoteTyVarTcS tv
 defaultTyVarTcS :: TcTyVar -> TcS Bool
 defaultTyVarTcS the_tv
   | isRuntimeRepVar the_tv
-  , not (isSigTyVar the_tv)  -- SigTvs should only be unified with a tyvar
+  , not (isTyVarTyVar the_tv)  -- TyVarTvs should only be unified with a tyvar
                              -- never with a type; c.f. TcMType.defaultTyVar
-                             -- See Note [Kind generalisation and SigTvs]
+                             -- See Note [Kind generalisation and TyVarTvs]
   = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
        ; unifyTyVar the_tv liftedRepTy
        ; return True }
@@ -2286,7 +2286,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
 
     float_tv_eq_candidate tv1 ty2  -- See Note [Which equalities to float]
       =  isMetaTyVar tv1
-      && (not (isSigTyVar tv1) || isTyVarTy ty2)
+      && (not (isTyVarTyVar tv1) || isTyVarTy ty2)
 
 
 {- Note [Float equalities from under a skolem binding]
@@ -2320,7 +2320,7 @@ happen.  In particular, float out equalities that are:
 
 * Of form (alpha ~# ty) or (ty ~# alpha), where
    * alpha is a meta-tyvar.
-   * And 'alpha' is not a SigTv with 'ty' being a non-tyvar.  In that
+   * And 'alpha' is not a TyVarTv with 'ty' being a non-tyvar.  In that
      case, floating out won't help either, and it may affect grouping
      of error messages.
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index cd80be6..97f794d 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -554,7 +554,7 @@ kcTyClGroup decls
 
            ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
            ; tc_res_kind'        <- zonkTcTypeToType env tc_res_kind
-           ; scoped_tvs'         <- zonkSigTyVarPairs scoped_tvs
+           ; scoped_tvs'         <- zonkTyVarTyVarPairs scoped_tvs
 
              -- See Note [Check telescope again during generalisation]
            ; let extra = text "NB: Implicitly declared variables come before others."
@@ -775,7 +775,7 @@ kcConDecl :: ConDecl GhcRn -> TcM ()
 kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
                       , con_mb_cxt = ex_ctxt, con_args = args })
   = addErrCtxt (dataConCtxtName [name]) $
-      -- See Note [Use SigTvs in kind-checking pass]
+      -- See Note [Use TyVarTvs in kind-checking pass]
     kcExplicitTKBndrs ex_tvs $
     do { _ <- tcHsMbContext ex_ctxt
        ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
@@ -822,8 +822,8 @@ mappings:
 APromotionErr is only used for DataCons, and only used during type checking
 in tcTyClGroup.
 
-Note [Use SigTvs in kind-checking pass]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Use TyVarTvs in kind-checking pass]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
 
   data Proxy a where
@@ -833,7 +833,7 @@ Consider
 It seems reasonable that this should be accepted. But something very strange
 is going on here: when we're kind-checking this declaration, we need to unify
 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
-MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
+MkProxy{1,2}. The best approach we've come up with is to use TyVarTvs during
 the kind-checking pass. First off, note that it's OK if the kind-checking pass
 is too permissive: we'll snag the problems in the type-checking pass later.
 (This extra permissiveness might happen with something like
@@ -842,20 +842,20 @@ is too permissive: we'll snag the problems in the type-checking pass later.
   data Bad a where
     MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
 
-which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
-in the second pass, though. Test case: polykinds/SigTvKinds3)
+which would be accepted if k1 and k2 were TyVarTvs. This is correctly rejected
+in the second pass, though. Test case: polykinds/TyVarTvKinds3)
 Recall that the kind-checking pass exists solely to collect constraints
 on the kinds and to power unification.
 
-To achieve the use of SigTvs, we must be careful to use specialized functions
-that produce SigTvs, not ordinary skolems. This is why we need
+To achieve the use of TyVarTvs, we must be careful to use specialized functions
+that produce TyVarTvs, not ordinary skolems. This is why we need
 kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
 tc... variants.
 
 The drawback of this approach is sometimes it will accept a definition that
 a (hypothetical) declarative specification would likely reject. As a general
 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
-the whole point of CUSKs is to allow polymorphic recursion. Yet, the SigTvs
+the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs
 approach allows a limited form of polymorphic recursion *without* a CUSK.
 
 To wit:
@@ -865,7 +865,7 @@ To wit:
 Note that this is polymorphically recursive, with the recursive occurrence
 of T used at a kind other than a's kind. The approach outlined here accepts
 this definition, because this kind is still a kind variable (and so the
-SigTvs unify). Stepping back, I (Richard) have a hard time envisioning a
+TyVarTvs unify). Stepping back, I (Richard) have a hard time envisioning a
 way to describe exactly what declarations will be accepted and which will
 be rejected (without a CUSK). However, the accepted definitions are indeed
 well-kinded and any rejected definitions would be accepted with a CUSK,
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4beae38..898a0f2 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -40,14 +40,14 @@ module TcType (
   TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv,
   MetaDetails(Flexi, Indirect), MetaInfo(..),
   isImmutableTyVar, isSkolemTyVar, isMetaTyVar,  isMetaTyVarTy, isTyVarTy,
-  isSigTyVar, isOverlappableTyVar,  isTyConableTyVar,
+  isTyVarTyVar, isOverlappableTyVar,  isTyConableTyVar,
   isFskTyVar, isFmvTyVar, isFlattenTyVar,
   isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
   isFlexi, isIndirect, isRuntimeUnkSkol,
   metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
   isTouchableMetaTyVar,
   isFloatedTouchableMetaTyVar,
-  findDupSigTvs, mkTyVarNamePairs,
+  findDupTyVarTvs, mkTyVarNamePairs,
 
   --------------------------------
   -- Builders
@@ -453,31 +453,23 @@ why Var.hs shouldn't actually have the definition, but it "belongs" here.
 
 Note [Signature skolems]
 ~~~~~~~~~~~~~~~~~~~~~~~~
-A SigTv is a specialised variant of TauTv, with the following invarints:
+A TyVarTv is a specialised variant of TauTv, with the following invarints:
 
-    * A SigTv can be unified only with a TyVar,
+    * A TyVarTv can be unified only with a TyVar,
       not with any other type
 
-    * Its MetaDetails, if filled in, will always be another SigTv
+    * Its MetaDetails, if filled in, will always be another TyVarTv
       or a SkolemTv
 
-SigTvs are only distinguished to improve error messages.
+TyVarTvs are only distinguished to improve error messages.
 Consider this
 
-  f :: forall a. [a] -> Int
-  f (x::b : xs) = 3
-
-Here 'b' is a lexically scoped type variable, but it turns out to be
-the same as the skolem 'a'.  So we make them both SigTvs, which can unify
-with each other.
-
-Similarly consider
   data T (a:k1) = MkT (S a)
   data S (b:k2) = MkS (T b)
+
 When doing kind inference on {S,T} we don't want *skolems* for k1,k2,
-because they end up unifying; we want those SigTvs again.
+because they end up unifying; we want those TyVarTvs again.
 
-SigTvs are used *only* for pattern type signatures.
 
 Note [TyVars and TcTyVars during type checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -536,7 +528,7 @@ data MetaInfo
                    -- A TauTv is always filled in with a tau-type, which
                    -- never contains any ForAlls.
 
-   | SigTv         -- A variant of TauTv, except that it should not be
+   | TyVarTv       -- A variant of TauTv, except that it should not be
                    --   unified with a type, only with a type variable
                    -- See Note [Signature skolems]
 
@@ -564,7 +556,7 @@ pprTcTyVarDetails (MetaTv { mtv_info = info, mtv_tclvl = tclvl })
   where
     pp_info = case info of
                 TauTv      -> text "tau"
-                SigTv      -> text "sig"
+                TyVarTv    -> text "tyv"
                 FlatMetaTv -> text "fmv"
                 FlatSkolTv -> text "fsk"
 
@@ -716,7 +708,7 @@ Note [TcLevel and untouchable type variables]
 
 * A unification variable is *touchable* if its level number
   is EQUAL TO that of its immediate parent implication,
-  and it is a TauTv or SigTv (but /not/ FlatMetaTv or FlatSkolTv
+  and it is a TauTv or TyVarTv (but /not/ FlatMetaTv or FlatSkolTv
 
 Note [WantedInv]
 ~~~~~~~~~~~~~~~~
@@ -1216,12 +1208,12 @@ isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
 isTyConableTyVar tv
         -- True of a meta-type variable that can be filled in
         -- with a type constructor application; in particular,
-        -- not a SigTv
+        -- not a TyVarTv
   | isTyVar tv -- See Note [Coercion variables in free variable lists]
   = ASSERT2( tcIsTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-        MetaTv { mtv_info = SigTv } -> False
-        _                           -> True
+        MetaTv { mtv_info = TyVarTv } -> False
+        _                             -> True
   | otherwise = True
 
 isFmvTyVar tv
@@ -1317,11 +1309,11 @@ setMetaTyVarTcLevel tv tclvl
       details@(MetaTv {}) -> setTcTyVarDetails tv (details { mtv_tclvl = tclvl })
       _ -> pprPanic "metaTyVarTcLevel" (ppr tv)
 
-isSigTyVar :: Var -> Bool
-isSigTyVar tv
+isTyVarTyVar :: Var -> Bool
+isTyVarTyVar tv
   = case tcTyVarDetails tv of
-        MetaTv { mtv_info = SigTv } -> True
-        _                           -> False
+        MetaTv { mtv_info = TyVarTv } -> True
+        _                             -> False
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
@@ -1340,10 +1332,10 @@ mkTyVarNamePairs :: [TyVar] -> [(Name,TyVar)]
 -- Just pair each TyVar with its own name
 mkTyVarNamePairs tvs = [(tyVarName tv, tv) | tv <- tvs]
 
-findDupSigTvs :: [(Name,TcTyVar)] -> [(Name,Name)]
+findDupTyVarTvs :: [(Name,TcTyVar)] -> [(Name,Name)]
 -- If we have [...(x1,tv)...(x2,tv)...]
 -- return (x1,x2) in the result list
-findDupSigTvs prs
+findDupTyVarTvs prs
   = concatMap mk_result_prs $
     findDupsEq eq_snd prs
   where
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 2ed861c..045132e 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -1231,11 +1231,11 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
   = return (emptyBag, emptyTcEvBinds)
 
   | otherwise
-  = ASSERT2( all (isSkolemTyVar <||> isSigTyVar) skol_tvs, ppr skol_tvs )
-      -- Why allow SigTvs? Because implicitly declared kind variables in
-      -- non-CUSK type declarations are SigTvs, and we need to bring them
+  = ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs )
+      -- Why allow TyVarTvs? Because implicitly declared kind variables in
+      -- non-CUSK type declarations are TyVarTvs, and we need to bring them
       -- into scope as a skolem in an implication. This is OK, though,
-      -- because SigTvs will always remain tyvars, even after unification.
+      -- because TyVarTvs will always remain tyvars, even after unification.
     do { ev_binds_var <- newTcEvBinds
        ; implic <- newImplication
        ; let implic' = implic { ic_tclvl  = tclvl
@@ -1692,7 +1692,7 @@ lhsPriority tv
       SkolemTv {} -> 0
       MetaTv { mtv_info = info } -> case info of
                                      FlatSkolTv -> 1
-                                     SigTv      -> 2
+                                     TyVarTv    -> 2
                                      TauTv      -> 3
                                      FlatMetaTv -> 4
 {- Note [TyVar/TyVar orientation]
@@ -1717,11 +1717,11 @@ So we look for a positive reason to swap, using a three-step test:
         outer one.  So nothing can be deeper than a FlatMetaTv
 
 
-  - SigTv/TauTv:  if we have  sig_tv ~ tau_tv, put tau_tv
-                  on the left because there are fewer
-                  restrictions on updating TauTvs
+  - TyVarTv/TauTv: if we have  tyv_tv ~ tau_tv, put tau_tv
+                   on the left because there are fewer
+                   restrictions on updating TauTvs
 
-  - SigTv/TauTv:  put on the left either
+  - TyVarTv/TauTv:  put on the left either
      a) Because it's touchable and can be unified, or
      b) Even if it's not touchable, TcSimplify.floatEqualities
         looks for meta tyvars on the left
@@ -1862,8 +1862,8 @@ canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
 canSolveByUnification tclvl tv xi
   | isTouchableMetaTyVar tclvl tv
   = case metaTyVarInfo tv of
-      SigTv -> is_tyvar xi
-      _     -> True
+      TyVarTv -> is_tyvar xi
+      _       -> True
 
   | otherwise    -- Untouchable
   = False
@@ -1874,8 +1874,8 @@ canSolveByUnification tclvl tv xi
           Just tv -> case tcTyVarDetails tv of
                        MetaTv { mtv_info = info }
                                    -> case info of
-                                        SigTv -> True
-                                        _     -> False
+                                        TyVarTv -> True
+                                        _       -> False
                        SkolemTv {} -> True
                        RuntimeUnk  -> True
 
@@ -2225,7 +2225,7 @@ preCheck dflags ty_fam_ok tv ty
 canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
 canUnifyWithPolyType dflags details
   = case details of
-      MetaTv { mtv_info = SigTv }    -> False
-      MetaTv { mtv_info = TauTv }    -> xopt LangExt.ImpredicativeTypes dflags
-      _other                         -> True
+      MetaTv { mtv_info = TyVarTv }    -> False
+      MetaTv { mtv_info = TauTv }      -> xopt LangExt.ImpredicativeTypes dflags
+      _other                           -> True
           -- We can have non-meta tyvars in given constraints
diff --git a/testsuite/tests/dependent/should_compile/T14066a.hs b/testsuite/tests/dependent/should_compile/T14066a.hs
index 30b203d..1d6b724 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.hs
+++ b/testsuite/tests/dependent/should_compile/T14066a.hs
@@ -10,7 +10,7 @@ import Data.Type.Bool
 
 type family Bar x y where
   Bar (x :: a) (y :: b) = Int
-  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be SigTvs and unify appropriately
+  Bar (x :: c) (y :: d) = Bool   -- a,b,c,d should be TyVarTvs and unify appropriately
 
 
   -- the two k's, even though they have different scopes, should unify in the
diff --git a/testsuite/tests/polykinds/SigTvKinds.hs b/testsuite/tests/polykinds/TyVarTvKinds.hs
index 782a7b3..a3a0de3 100644
--- a/testsuite/tests/polykinds/SigTvKinds.hs
+++ b/testsuite/tests/polykinds/TyVarTvKinds.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE PolyKinds #-}
 
-module SigTvKinds where
+module TyVarTvKinds where
 
 data T (a :: k1) x = MkT (S a ())
 data S (b :: k2) y = MkS (T b ())
diff --git a/testsuite/tests/polykinds/SigTvKinds2.hs b/testsuite/tests/polykinds/TyVarTvKinds2.hs
index 1ec1ebb..49817d7 100644
--- a/testsuite/tests/polykinds/SigTvKinds2.hs
+++ b/testsuite/tests/polykinds/TyVarTvKinds2.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE PolyKinds #-}
 
-module SigTvKinds2 where
+module TyVarTvKinds2 where
 
 data SameKind :: k -> k -> *
 
diff --git a/testsuite/tests/polykinds/SigTvKinds2.stderr b/testsuite/tests/polykinds/TyVarTvKinds2.stderr
index 9f52370..1a55288 100644
--- a/testsuite/tests/polykinds/SigTvKinds2.stderr
+++ b/testsuite/tests/polykinds/TyVarTvKinds2.stderr
@@ -1,5 +1,5 @@
 
-SigTvKinds2.hs:7:48: error:
+TyVarTvKinds2.hs:7:48: error:
     • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the type ‘SameKind a b’
diff --git a/testsuite/tests/polykinds/SigTvKinds3.hs b/testsuite/tests/polykinds/TyVarTvKinds3.hs
index 7c9dace..570078c 100644
--- a/testsuite/tests/polykinds/SigTvKinds3.hs
+++ b/testsuite/tests/polykinds/TyVarTvKinds3.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE GADTs, ExplicitForAll, PolyKinds #-}
 
-module SigTvKinds3 where
+module TyVarTvKinds3 where
 
 import Data.Kind
 
diff --git a/testsuite/tests/polykinds/SigTvKinds3.stderr b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
index b498c03..67da965 100644
--- a/testsuite/tests/polykinds/SigTvKinds3.stderr
+++ b/testsuite/tests/polykinds/TyVarTvKinds3.stderr
@@ -1,5 +1,5 @@
 
-SigTvKinds3.hs:9:62: error:
+TyVarTvKinds3.hs:9:62: error:
     • Expected kind ‘k1’, but ‘b’ has kind ‘k2’
     • In the second argument of ‘SameKind’, namely ‘b’
       In the first argument of ‘Bad’, namely ‘(SameKind a b)’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index de46acf..3e37205 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -122,8 +122,8 @@ test('T10134', normal, multimod_compile, ['T10134.hs','-v0'])
 test('T10742', normal, compile, [''])
 test('T10934', normal, compile, [''])
 test('T11142', normal, compile_fail, [''])
-test('SigTvKinds', normal, compile, [''])
-test('SigTvKinds2', expect_broken(11203), compile_fail, [''])
+test('TyVarTvKinds', normal, compile, [''])
+test('TyVarTvKinds2', expect_broken(11203), compile_fail, [''])
 test('T9017', normal, compile_fail, [''])
 test('TidyClassKinds', normal, compile_fail, ['-fprint-explicit-kinds'])
 test('T11249', normal, compile, [''])
@@ -187,7 +187,7 @@ test('T14710', normal, compile_fail, [''])
 test('T14723', normal, compile, [''])
 test('T14846', normal, compile_fail, [''])
 test('T14873', normal, compile, [''])
-test('SigTvKinds3', normal, compile_fail, [''])
+test('TyVarTvKinds3', normal, compile_fail, [''])
 test('T15116', normal, compile_fail, [''])
 test('T15116a', normal, compile_fail, [''])
 test('T15170', normal, compile, [''])