diff --git a/compiler/GHC/Rename/Env.hs b/compiler/GHC/Rename/Env.hs
index b45dc0b63dea5bc0312ff809c7691f0bdffc0f16..beaac9c857b503c97853208aee7b0294a80a83d5 100644
--- a/compiler/GHC/Rename/Env.hs
+++ b/compiler/GHC/Rename/Env.hs
@@ -1058,9 +1058,6 @@ lookupLocalOccRn rdr_name
 lookupTypeOccRn :: RdrName -> RnM Name
 -- see Note [Demotion]
 lookupTypeOccRn rdr_name
-  | (isVarOcc <||> isFieldOcc) (rdrNameOcc rdr_name)  -- See Note [Promoted variables in types]
-  = badVarInType rdr_name
-  | otherwise
   = do { mb_gre <- lookupOccRn_maybe rdr_name
        ; case mb_gre of
              Just gre -> return $ greName gre
@@ -1083,6 +1080,7 @@ To ease migration and minimize breakage, we continue to support those usages
 but emit appropriate warnings.
 -}
 
+-- Used when looking up a term name (varName or dataName) in a type
 lookup_demoted :: RdrName -> RnM Name
 lookup_demoted rdr_name
   | Just demoted_rdr <- demoteRdrName rdr_name
@@ -1108,16 +1106,111 @@ lookup_demoted rdr_name
                                      | otherwise
                                      = star_is_type_hints
                     ; unboundNameX looking_for rdr_name suggestion } }
-  | Just demoted_rdr_name <- demoteRdrNameTv rdr_name,
-    isQual rdr_name
+
+  | isQual rdr_name,
+    Just demoted_rdr_name <- demoteRdrNameTv rdr_name
+    -- Definitely an illegal term variable, as type variables are never exported.
+    -- See Note [Demotion of unqualified variables] (W2)
   = report_qualified_term_in_types rdr_name demoted_rdr_name
 
+  | isUnqual rdr_name,
+    Just demoted_rdr_name <- demoteRdrNameTv rdr_name
+    -- See Note [Demotion of unqualified variables]
+  = do { required_type_arguments <- xoptM LangExt.RequiredTypeArguments
+       ; if required_type_arguments
+         then do { mb_demoted_gre <- lookupOccRn_maybe demoted_rdr_name
+                 ; case mb_demoted_gre of
+                     Nothing -> unboundName (LF WL_Anything WL_Anywhere) rdr_name
+                     Just demoted_gre -> return $ greName demoted_gre }
+         else unboundName looking_for rdr_name }
+
   | otherwise
-  = reportUnboundName' (lf_which looking_for) rdr_name
+  = unboundName looking_for rdr_name
 
   where
     looking_for = LF WL_Constructor WL_Anywhere
 
+{- Note [Demotion of unqualified variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Under RequiredTypeArguments, a term-level variable name (i.e. a name whose
+`occNameSpace` is `varName` as opposed to `tvName`) does not necessarily denote
+a term variable. It can actually stand for a type:
+
+  {-# LANGUAGE RequiredTypeArguments #-}
+  idv :: forall a -> a -> a     -- Note the "forall a ->" in the type
+  idv  t  (x :: t) = id @t x    -- #23739
+  --   ^        ^        ^
+  --  varName  tvName  tvName   -- NameSpace (GHC.Types.Name.Occurrence)
+
+The variable `t` is an alias for the type variable `a`, so it's valid to use it
+in type-level contexts. The only problem is that the namespaces do not match.
+Demotion allows us to connect the `tvName` usages to the `varName` binding.
+
+Demotion of an RdrName means that we change its namespace from tvName/tcClsName
+to varName/dataName. Suppose we are looking up an occurence of a variable `a`
+in a type (in `lookupTypeOccRn`). The parser gave `a` a `tvName` occurrence,
+so we try looking that up first.  If that fails, and RequiredTypeArguments is
+on, then "demote" it to the `varName` namespace with `demoteRdrNameTv` and look
+that up instead. If that succeeds, use it.
+
+(W1) Wrinkle 1
+  As a side effect of demotion, the renamer accepts all these examples:
+    t = True         -- Ordinary term-level binding
+    x = Proxy @t     -- (1) Bad usage in a HsExpr
+    type T = t       -- (2) Bad usage in a TyClDecl
+    f :: t -> t      -- (3) Bad usage in a SigDecl
+
+  However, GHC doesn't promote arbitrary terms to types. See the "T2T-Mapping"
+  section of GHC Proposal #281: "In the type checking environment, the variable
+  must stand for a type variable". Even though the renamer accepts these
+  constructs, the type checker has to reject the uses of `t` shown above.
+
+  All three examples are rejected with the `TermVariablePE` promotion error.
+  The error is generated by `tcTyVar` (GHC.Tc.Gen.HsType)
+      tcTyVar :: Name -> TcM (TcType, TcKind)
+  The first thing `tcTyVar` does is call the `tcLookup` helper (GHC.Tc.Utils.Env)
+  to find the variable in the type checking environment
+      tcLookup :: Name -> TcM TcTyThing
+  What happens next depends on the example in question.
+
+  * In the HsExpr example (1), `tcLookup` finds `ATcId` that corresponds to
+    the `t = True` binding. The `ATcId` is then then turned into an error by
+    the following clause in `tcTyVar`:
+       ATcId{} -> promotionErr name TermVariablePE
+
+  * In the TyClDecl example (2) and the SigDecl example (3), we don't have
+    `ATcId` in the environment just yet because type declarations and signatures
+    are type-checked /before/ term-level bindings.
+
+    This means that `tcLookup` fails to find `t` in the local environment and
+    calls `tcLookupGlobal` (GHC.Tc.Utils.Env)
+        tcLookupGlobal :: Name -> TcM TyThing
+
+    The global environment does not contain `t` either, so `tcLookupGlobal`
+    calls `notFound` (GHC.Tc.Utils.Env)
+        notFound :: Name -> TcM TyThing
+
+    At this point GHC would normally generate a panic: if the variable is
+    neither in the local nor in the global environment, then it shouldn't have
+    passed the renamer. Unfortunately, this expectation is tiresome and
+    expensive to maintain, so we add a special case in `notFound` instead.
+    If the namespace of the variable is `varName`, the only explanation other
+    than a bug in GHC is that the user tried to use a term variable in a type
+    context. Hence the following clause in `notFound`:
+      _ | isTermVarOrFieldNameSpace (nameNameSpace name) ->
+          failWithTc $ TcRnUnpromotableThing name TermVariablePE
+
+(W2) Wrinkle 2
+   Only unqualified variable names are demoted, e.g. `f` but not `M.f`.
+   The reason is that type variables are never bound to a qualified name:
+   they can't be bound at the top level of a module, nor can they be
+   exported or imported, so a qualified occurrence `M.f` must refer to a
+   term-level definition and is never legal at the type level.
+   Demotion of qualified names would not allow us to accept any new programs.
+   We use this fact to generate better suggestions in error messages,
+   see `report_qualified_term_in_types`.
+-}
+
 -- Report a qualified variable name in a type signature:
 --   badSig :: Prelude.head
 --             ^^^^^^^^^^^
@@ -1141,28 +1234,8 @@ lookup_promoted rdr_name
   | otherwise
   = return Nothing
 
-badVarInType :: RdrName -> RnM Name
-badVarInType rdr_name
-  = do { addErr (TcRnUnpromotableThing name TermVariablePE)
-       ; return name }
-      where
-        name = mkUnboundNameRdr rdr_name
-
-{- Note [Promoted variables in types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (#12686):
-   x = True
-   data Bad = Bad 'x
-
-The parser treats the quote in 'x as saying "use the term
-namespace", so we'll get (Bad x{v}), with 'x' in the
-VarName namespace.  If we don't test for this, the renamer
-will happily rename it to the x bound at top level, and then
-the typecheck falls over because it doesn't have 'x' in scope
-when kind-checking.
-
-Note [Demotion]
-~~~~~~~~~~~~~~~
+{- Note [Demotion]
+~~~~~~~~~~~~~~~~~~
 When the user writes:
   data Nat = Zero | Succ Nat
   foo :: f Zero -> Int
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index e380b86f5ace24340385a69f1d4cf57281a6aa78..ae4273f75ab785cc81e1204504bebb21d37743c2 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -871,7 +871,7 @@ bindSigTyVarsFV tvs thing_inside
 ---------------
 bindHsQTyVars :: forall a b.
                  HsDocContext
-              -> Maybe a            -- Just _  => an associated type decl
+              -> Maybe (a, [Name])  -- Just _  => an associated type decl
               -> FreeKiTyVars       -- Kind variables from scope
               -> LHsQTyVars GhcPs
               -> (LHsQTyVars GhcRn -> FreeKiTyVars -> RnM (b, FreeVars))
@@ -892,13 +892,19 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside
 
        ; let -- See Note [bindHsQTyVars examples] for what
              -- all these various things are doing
-             bndrs, implicit_kvs :: [LocatedN RdrName]
+             bndrs, all_implicit_kvs :: [LocatedN RdrName]
              bndrs        = map hsLTyVarLocName hs_tv_bndrs
-             implicit_kvs = filterFreeVarsToBind bndrs $
+             all_implicit_kvs = filterFreeVarsToBind bndrs $
                bndr_kv_occs ++ body_kv_occs
              body_remaining = filterFreeVarsToBind bndr_kv_occs $
               filterFreeVarsToBind bndrs body_kv_occs
 
+       ; implicit_kvs <-
+           case mb_assoc of
+             Nothing -> filterInScopeM all_implicit_kvs
+             Just (_, cls_tvs) -> filterInScopeNonClassM cls_tvs all_implicit_kvs
+                 -- See Note [Class variables and filterInScope]
+
        ; traceRn "checkMixedVars3" $
            vcat [ text "bndrs"   <+> ppr hs_tv_bndrs
                 , text "bndr_kv_occs"   <+> ppr bndr_kv_occs
@@ -971,8 +977,13 @@ Then:
   That's one of the rules for a CUSK, so we pass that info on
   as the second argument to thing_inside.
 
-* Order is not important in these lists.  All we are doing is
-  bring Names into scope.
+* Order is important in these lists. Consider
+    data T (a::k1) (b::k2)
+  We want implicit_kvs to be [k1,k2], not [k2,k1], so that the inferred kind for
+  T quantifies over kind variables in the user-specified order
+    T :: forall k1 k2. k1 -> k2 -> Type  -- OK
+    T :: forall k2 k1. k1 -> k2 -> Type  -- Bad
+  This matters with TypeApplications
 
 * bndr_kv_occs, body_kv_occs, and implicit_kvs can contain duplicates. All
   duplicate occurrences are removed when we bind them with rnImplicitTvOccs.
@@ -1221,14 +1232,14 @@ new_tv_name_rn (Just _) cont lrdr@(L _ rdr)
 Section 7.3: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst#73implicit-quantification
 
 Its purpose is to notify users when implicit quantification occurs that would
-stop working under RequiredTypeArguments (a future GHC extension). Example:
+stop working under RequiredTypeArguments. Example:
 
    a = 42
    id :: a -> a
 
 As it stands, the `a` in the signature `id :: a -> a` is considered free and
 leads to implicit quantification, as if the user wrote `id :: forall a. a -> a`.
-Under RequiredTypeArguments it will capture the term-level variable `a` (bound by `a = 42`),
+Under RequiredTypeArguments it captures the term-level variable `a` (bound by `a = 42`),
 leading to a type error.
 
 `warn_term_var_capture` detects this by demoting the namespace of the
@@ -1816,22 +1827,133 @@ type checking. While viable, this would mean we'd end up accepting this:
 -- Note [Ordering of implicit variables].
 type FreeKiTyVars = [LocatedN RdrName]
 
+-- When renaming a type, do we want to capture or ignore term variables?
+-- Suppose we have a variable binding `a` and we are renaming a type signature
+-- that mentions `a`:
+--
+--    f :: forall t -> ...
+--    f a = ...
+--      where g :: a -> Bool
+--
+-- Does the `a` in the signature for `g` refer to the term variable or is it
+-- implicitly quantified, as if the user wrote `g :: forall a. a -> Bool`?
+-- `CaptureTermVars` selects the former behavior, `DontCaptureTermVars` the latter.
+data TermVariableCapture =
+    CaptureTermVars
+  | DontCaptureTermVars
+
+getTermVariableCapture :: RnM TermVariableCapture
+getTermVariableCapture
+  = do { required_type_arguments <- xoptM LangExt.RequiredTypeArguments
+       ; let tvc | required_type_arguments = CaptureTermVars
+                 | otherwise               = DontCaptureTermVars
+       ; return tvc }
+
 -- | Filter out any type and kind variables that are already in scope in the
 -- the supplied LocalRdrEnv. Note that this includes named wildcards, which
 -- look like perfectly ordinary type variables at this point.
-filterInScope :: LocalRdrEnv -> FreeKiTyVars -> FreeKiTyVars
-filterInScope rdr_env = filterOut (inScope rdr_env . unLoc)
+filterInScope :: TermVariableCapture -> (GlobalRdrEnv, LocalRdrEnv) -> FreeKiTyVars -> FreeKiTyVars
+filterInScope tvc envs = filterOut (inScope tvc envs . unLoc)
+
+-- | Like 'filterInScope', but keep parent class variables intact.
+-- Used with associated types. See Note [Class variables and filterInScope]
+filterInScopeNonClass :: [Name] -> TermVariableCapture -> (GlobalRdrEnv, LocalRdrEnv) -> FreeKiTyVars -> FreeKiTyVars
+filterInScopeNonClass cls_tvs tvc envs = filterOut (in_scope_non_class . unLoc)
+  where
+    in_scope_non_class :: RdrName -> Bool
+    in_scope_non_class rdr
+      | occName rdr `elemOccSet` cls_tvs_set = False
+      | otherwise = inScope tvc envs rdr
+
+    cls_tvs_set :: OccSet
+    cls_tvs_set = mkOccSet (map nameOccName cls_tvs)
 
 -- | Filter out any type and kind variables that are already in scope in the
 -- the environment's LocalRdrEnv. Note that this includes named wildcards,
 -- which look like perfectly ordinary type variables at this point.
 filterInScopeM :: FreeKiTyVars -> RnM FreeKiTyVars
 filterInScopeM vars
-  = do { rdr_env <- getLocalRdrEnv
-       ; return (filterInScope rdr_env vars) }
-
-inScope :: LocalRdrEnv -> RdrName -> Bool
-inScope rdr_env rdr = rdr `elemLocalRdrEnv` rdr_env
+  = do { tvc <- getTermVariableCapture
+       ; envs <- getRdrEnvs
+       ; return (filterInScope tvc envs vars) }
+
+-- | Like 'filterInScopeM', but keep parent class variables intact.
+-- Used with associated types. See Note [Class variables and filterInScope]
+filterInScopeNonClassM :: [Name] -> FreeKiTyVars -> RnM FreeKiTyVars
+filterInScopeNonClassM cls_tvs vars
+  = do { tvc <- getTermVariableCapture
+       ; envs <- getRdrEnvs
+       ; return (filterInScopeNonClass cls_tvs tvc envs vars) }
+
+inScope :: TermVariableCapture -> (GlobalRdrEnv, LocalRdrEnv) -> RdrName -> Bool
+inScope tvc (gbl, lcl) rdr =
+  case tvc of
+    DontCaptureTermVars -> rdr_in_scope
+    CaptureTermVars     -> rdr_in_scope || demoted_rdr_in_scope
+  where
+    rdr_in_scope, demoted_rdr_in_scope :: Bool
+    rdr_in_scope         = elem_lcl rdr
+    demoted_rdr_in_scope = maybe False (elem_lcl <||> elem_gbl) (demoteRdrNameTv rdr)
+
+    elem_lcl, elem_gbl :: RdrName -> Bool
+    elem_lcl name = elemLocalRdrEnv name lcl
+    elem_gbl name = (not . null) (lookupGRE gbl (LookupRdrName name (RelevantGREsFOS WantBoth)))
+
+{- Note [Class variables and filterInScope]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In `bindHsQTyVars` free variables are collected and bound implicitly. Example:
+  type ElemKind (a :: Maybe k) = k
+Both occurrences of `k` are usages, so GHC creates an implicit binding for `k`.
+We can also bind it explicitly with the help of TypeAbstractions:
+  type ElemKind @k (a :: Maybe k) = k
+
+This is similar to implicit quantification that happens in type signatures
+  const :: a -> b -> a               -- `a` and `b` bound implicitly
+  const :: forall a b. a -> b -> a   -- `a` and `b` bound explicitly
+
+In both cases we need to compute the list of free variables to implicitly
+quantify over (NB: list, not set, because order matters with TypeApplications)
+  * implicitly bound variables in ElemKind:  [k]
+  * implicitly bound variables in const:     [a, b]
+
+However, variables that are already in scope are captured. Example:
+  {-# LANGUAGE ScopedTypeVariables #-}
+  f (x :: a) = ...
+    where g :: a -> a
+          g _ = x
+When we look at `g` in isolation, `a` is a free variable:
+  g :: a -> a
+But due to ScopedTypeVariables, `a` is actually bound in the surrounding
+context, namely the (x :: a) pattern.
+It is important that we do /not/ insert an implicit forall in the type of `g`
+  g :: forall a. a -> a   -- No! That would mean a different thing
+The solution is to use `filterInScopeM` to remove variables already in scope
+from candidates for implicit quantification.
+
+Using `filterInScopeM` is additionally important when RequiredTypeArguments is
+in effect. Consider
+  import Prelude (id)
+  data T (a :: id) = MkT    -- Test case T23740e
+
+With RequiredTypeArguments, variables in the term namespace can be referred to
+at the type level, so `id` in the `:: id` kind signature ought to refer to `id`
+from Prelude. Of course it is not a valid program, but we want a proper error
+message rather than implicit quantification:
+  T23740e.hs:5:14: error: [GHC-45510]
+      • Term variable ‘id’ cannot be used here
+          (term variables cannot be promoted)
+
+This leads us to use `filterInScopeM` in `bindHsQTyVars`.
+Unfortunately, associated types make matters more complex. Consider
+  class C (a::k1) (b::k2) (c::k3) where
+    type T (a::k1) b
+When renaming `T`, we have to implicitly quantify over the class variable `k1`,
+despite the fact that `k1` is in scope from the class header. The type checker
+expects to find `k1` in `HsQTvsRn` (the `hsq_ext` field of `LHsQTyVars`). But it
+won't find it there if it is filtered out by `filterInScopeM`.
+
+To account for that, we introduce another helper, `filterInScopeNonClassM`,
+which acts much like `filterInScopeM` but leaves class variables intact. -}
 
 extract_tyarg :: LHsTypeArg GhcPs -> FreeKiTyVars -> FreeKiTyVars
 extract_tyarg (HsValArg ty) acc = extract_lty ty acc
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 99a34b2f4e80c7efe5e98f27fee8852c7563223e..f779285d59708cfff0b31c269c869f572e11fd71 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -855,10 +855,11 @@ rnDataFamInstDecl atfi (DataFamInstDecl { dfid_eqn =
 
 -- Rename associated type family decl in class
 rnATDecls :: Name      -- Class
+          -> [Name]    -- Class variables. See Note [Class variables and filterInScope] in GHC.Rename.HsType
           -> [LFamilyDecl GhcPs]
           -> RnM ([LFamilyDecl GhcRn], FreeVars)
-rnATDecls cls at_decls
-  = rnList (rnFamDecl (Just cls)) at_decls
+rnATDecls cls cls_tvs at_decls
+  = rnList (rnFamDecl (Just (cls, cls_tvs))) at_decls
 
 rnATInstDecls :: (AssocTyFamInfo ->           -- The function that renames
                   decl GhcPs ->               -- an instance. rnTyFamInstDecl
@@ -1746,7 +1747,7 @@ rnTyClDecl (ClassDecl { tcdLayout = layout,
              { (context', cxt_fvs) <- rnMaybeContext cls_doc context
              ; fds'  <- rnFds fds
                          -- The fundeps have no free variables
-             ; (ats', fv_ats) <- rnATDecls cls' ats
+             ; (ats', fv_ats) <- rnATDecls cls' (hsAllLTyVarNames tyvars') ats
              ; let fvs = cxt_fvs     `plusFV`
                          fv_ats
              ; return ((tyvars', context', fds', ats'), fvs) }
@@ -2197,7 +2198,8 @@ rnLDerivStrategy doc mds thing_inside
       (thing, fvs) <- thing_inside
       pure (ds, thing, fvs)
 
-rnFamDecl :: Maybe Name -- Just cls => this FamilyDecl is nested
+rnFamDecl :: Maybe (Name, [Name])
+                        -- Just (cls, cls_tvs) => this FamilyDecl is nested
                         --             inside an *class decl* for cls
                         --             used for associated types
           -> FamilyDecl GhcPs
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 196a1909a422eefa4d2486dbe0ea049830076ce3..1fd5c45aed47e1f871fdf4ce06b31486a25481e5 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1279,7 +1279,7 @@ instance Diagnostic TcRnMessage where
           text "is implicitly quantified," $+$
           text "even though another variable of the same name is in scope:" $+$
           nest 2 var_names $+$
-          text "This is not forward-compatible with a planned GHC extension, RequiredTypeArguments."
+          text "This is not compatible with the RequiredTypeArguments extension."
         where
           var_names = case shadowed_term_names of
               Left gbl_names -> vcat (map (\name -> quotes (ppr $ greName name) <+> pprNameProvenance name) gbl_names)
diff --git a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
index 47e49a5933e43b375ecf312ecc77f78afc286290..ab0d8e3b0fe27f43e1e3fcd9f559aedc1b8fbded 100644
--- a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
+++ b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
@@ -25,7 +25,7 @@ data PromotionErr
 
   | RecDataConPE     -- Data constructor in a recursive loop
                      -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
-  | TermVariablePE   -- See Note [Promoted variables in types]
+  | TermVariablePE   -- See Note [Demotion of unqualified variables] in GHC.Rename.Env
   | TypeVariablePE   -- See Note [Type variable scoping errors during typechecking]
   deriving (Generic)
 
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 6c173e2b39367a9288e96951098f53ecaf5d5e04..d50cd70e3ab5aa4fc5c77a5934a56962426a19a4 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2004,6 +2004,8 @@ tcTyVar name         -- Could be a tyvar, a tycon, or a datacon
                    ; let tc = promoteDataCon dc
                    ; return (mkTyConApp tc [], tyConKind tc) }
 
+           AGlobal AnId{}    -> promotionErr name TermVariablePE
+           ATcId{}           -> promotionErr name TermVariablePE
            APromotionErr err -> promotionErr name err
 
            _  -> wrongThingErr WrongThingType thing name }
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index ef4009fb0239659cd2068b6e687ae1f6dec76ae1..f47bcff9af8c0d081c70757354ff217ba17e0bcc 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -1883,7 +1883,7 @@ reifyInstances' th_nm th_tys
         ; rdr_ty <- cvt th_origin loc (mkThAppTs (TH.ConT th_nm) th_tys)
           -- #9262 says to bring vars into scope, like in HsForAllTy case
           -- of rnHsTyKi
-        ; let tv_rdrs = extractHsTyRdrTyVars rdr_ty
+        ; tv_rdrs <- filterInScopeM $ extractHsTyRdrTyVars rdr_ty
           -- Rename  to HsType Name
         ; ((tv_names, rn_ty), _fvs)
             <- checkNoErrs $ -- If there are out-of-scope Names here, then we
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs
index 8e6e628648bb4bde0f9be188406206d3b9be25a2..ba45a85b87e4557d7e3788e9b41522a438fbe9ac 100644
--- a/compiler/GHC/Tc/Utils/Env.hs
+++ b/compiler/GHC/Tc/Utils/Env.hs
@@ -1075,7 +1075,21 @@ notFound name
              | isUnboundName name -> failM  -- If the name really isn't in scope
                                             -- don't report it again (#11941)
              | otherwise -> failWithTc (TcRnStageRestriction (StageCheckSplice name))
-           _ -> failWithTc $
+
+           _ | isTermVarOrFieldNameSpace (nameNameSpace name) ->
+               -- This code path is only reachable with RequiredTypeArguments enabled
+               -- via the following chain of calls:
+               --   `notFound`       called from
+               --   `tcLookupGlobal` called from
+               --   `tcLookup`       called from
+               --   `tcTyVar`
+               -- It means the user tried to use a term variable at the type level, e.g.
+               --   let { a = 42; f :: a -> a; ... } in ...
+               -- If you are seeing this error for any other reason, it is a bug in GHC.
+               -- See Note [Demotion of unqualified variables] (W1) in GHC.Rename.Env
+               failWithTc $ TcRnUnpromotableThing name TermVariablePE
+
+             | otherwise -> failWithTc $
                 mkTcRnNotInScope (getRdrName name) (NotInScopeTc (getLclEnvTypeEnv lcl_env))
                        -- Take care: printing the whole gbl env can
                        -- cause an infinite loop, in the case where we
diff --git a/testsuite/tests/diagnostic-codes/codes.stdout b/testsuite/tests/diagnostic-codes/codes.stdout
index 63ca86b328d500b716137b1bb190cf00476554a5..38b6a3effe6562e300014fb00e730fa0621e8383 100644
--- a/testsuite/tests/diagnostic-codes/codes.stdout
+++ b/testsuite/tests/diagnostic-codes/codes.stdout
@@ -65,6 +65,7 @@
 [GHC-85337] is untested (constructor = TcRnSpecialiseNotVisible)
 [GHC-91382] is untested (constructor = TcRnIllegalKindSignature)
 [GHC-72520] is untested (constructor = TcRnIgnoreSpecialisePragmaOnDefMethod)
+[GHC-10969] is untested (constructor = TcRnTyThingUsedWrong)
 [GHC-61072] is untested (constructor = TcRnGADTDataContext)
 [GHC-16409] is untested (constructor = TcRnMultipleConForNewtype)
 [GHC-54478] is untested (constructor = TcRnRedundantSourceImport)
diff --git a/testsuite/tests/rename/should_compile/T22513a.stderr b/testsuite/tests/rename/should_compile/T22513a.stderr
index 339b09eef86a6c2ea622316b7e6c1dde10cdd74f..ce0ecc20d0bf3db0b5bd7bac90263d3bef3caf0e 100644
--- a/testsuite/tests/rename/should_compile/T22513a.stderr
+++ b/testsuite/tests/rename/should_compile/T22513a.stderr
@@ -3,5 +3,5 @@ T22513a.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘a’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘a’ defined at T22513a.hs:3:1
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513b.stderr b/testsuite/tests/rename/should_compile/T22513b.stderr
index 1bda00fb0d8131d129e3b0fe1c0869ce8a46dfa8..89dd86c6bf69237b4eac056cd7ce9901f4f91ad8 100644
--- a/testsuite/tests/rename/should_compile/T22513b.stderr
+++ b/testsuite/tests/rename/should_compile/T22513b.stderr
@@ -4,5 +4,5 @@ T22513b.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513b.hs:3:17-18
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513c.stderr b/testsuite/tests/rename/should_compile/T22513c.stderr
index dab473ca7e8f8858d632b46fc31eb1b85c87aa55..b084a8561edafd615256fab97b57907c27721df3 100644
--- a/testsuite/tests/rename/should_compile/T22513c.stderr
+++ b/testsuite/tests/rename/should_compile/T22513c.stderr
@@ -3,5 +3,5 @@ T22513c.hs:6:5: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘a’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘a’ defined at T22513c.hs:4:3
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513d.stderr b/testsuite/tests/rename/should_compile/T22513d.stderr
index 076bcb94c5d8e7bfe7d7d4feca3a2404d3d3c5ae..5afaaf4fe864f17486958752e4bf8cf4dc858fa2 100644
--- a/testsuite/tests/rename/should_compile/T22513d.stderr
+++ b/testsuite/tests/rename/should_compile/T22513d.stderr
@@ -4,5 +4,5 @@ T22513d.hs:3:4: warning: [GHC-54201] [-Wterm-variable-capture]
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513d.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513e.stderr b/testsuite/tests/rename/should_compile/T22513e.stderr
index 43207a3b4c035f63016ae4ea4292d20cc52f5e2c..0a5ca150a6b1376a9931e3b1ae9bbf1e2b13ee99 100644
--- a/testsuite/tests/rename/should_compile/T22513e.stderr
+++ b/testsuite/tests/rename/should_compile/T22513e.stderr
@@ -4,5 +4,5 @@ T22513e.hs:3:1: warning: [GHC-54201] [-Wterm-variable-capture]
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513e.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513f.stderr b/testsuite/tests/rename/should_compile/T22513f.stderr
index 94454b67f980ce0678a8cc66a895f1d582ee0ccb..d3b75e44a8ebe0d68259718eec386a255834b0e6 100644
--- a/testsuite/tests/rename/should_compile/T22513f.stderr
+++ b/testsuite/tests/rename/should_compile/T22513f.stderr
@@ -4,5 +4,5 @@ T22513f.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513f.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513g.hs b/testsuite/tests/rename/should_compile/T22513g.hs
index 1895b70bc27b6f9ae598912fb505cc1e01923350..37f3f20d3a214f13be1774a434e17b37b1ec7143 100644
--- a/testsuite/tests/rename/should_compile/T22513g.hs
+++ b/testsuite/tests/rename/should_compile/T22513g.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE ScopedTypeVariables #-}
 module T22513g where
+
 import Data.Kind
 
 data T k (id::head) (b::k) :: k2 -> head -> Type
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_compile/T22513g.stderr b/testsuite/tests/rename/should_compile/T22513g.stderr
index 0c0782d8947e6d4a27a518c4b8d28afac08fa12c..9ffcbb490f1394c9c7a57a2961ccf2289d33f53f 100644
--- a/testsuite/tests/rename/should_compile/T22513g.stderr
+++ b/testsuite/tests/rename/should_compile/T22513g.stderr
@@ -2,7 +2,7 @@
 T22513g.hs:5:1: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘head’ is implicitly quantified,
     even though another variable of the same name is in scope:
-      ‘head’ imported from ‘Prelude’ at T22513g.hs:2:8-14
+      ‘head’ imported from ‘Prelude’ at T22513g.hs:1:8-14
              (and originally defined in ‘GHC.List’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513h.stderr b/testsuite/tests/rename/should_compile/T22513h.stderr
index a88fdbd1abd6f3cff703ae9fc3ffb034e04d2f31..f97df3b8b6cd1ee44b0acf4436f131d2d9ed570b 100644
--- a/testsuite/tests/rename/should_compile/T22513h.stderr
+++ b/testsuite/tests/rename/should_compile/T22513h.stderr
@@ -4,5 +4,5 @@ T22513h.hs:6:10: warning: [GHC-54201] [-Wterm-variable-capture]
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513h.hs:1:8-14
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
+    This is not compatible with the RequiredTypeArguments extension.
     Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513i.stderr b/testsuite/tests/rename/should_compile/T22513i.stderr
index d99b621a47abc4e6765189964695d3f21cd99615..29f052d53a452093a5089a6ba084df9e1c16920a 100644
--- a/testsuite/tests/rename/should_compile/T22513i.stderr
+++ b/testsuite/tests/rename/should_compile/T22513i.stderr
@@ -1,7 +1,8 @@
+
 T22513i.hs:9:6: warning: [GHC-54201] [-Wterm-variable-capture]
     The type variable ‘id’ is implicitly quantified,
     even though another variable of the same name is in scope:
       ‘id’ imported from ‘Prelude’ at T22513i.hs:3:8-14
            (and originally defined in ‘GHC.Base’)
-    This is not forward-compatible with a planned GHC extension, RequiredTypeArguments.
-    Suggested fix: Consider renaming the type variable.
\ No newline at end of file
+    This is not compatible with the RequiredTypeArguments extension.
+    Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/T22513j.hs b/testsuite/tests/rename/should_compile/T22513j.hs
new file mode 100644
index 0000000000000000000000000000000000000000..165f6556c16111cfdffbe105835bf585271ef1a4
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T22513j.hs
@@ -0,0 +1,8 @@
+module T23740j where
+
+x :: ()
+x = ()
+  where
+    a = a
+    f :: a -> a
+    f = f
diff --git a/testsuite/tests/rename/should_compile/T22513j.stderr b/testsuite/tests/rename/should_compile/T22513j.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..c9a101a0797ddd88c9ea156da62a8bcbaa0b1b23
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T22513j.stderr
@@ -0,0 +1,7 @@
+
+T22513j.hs:7:5: warning: [GHC-54201] [-Wterm-variable-capture]
+    The type variable ‘a’ is implicitly quantified,
+    even though another variable of the same name is in scope:
+      ‘a’ defined at T22513j.hs:6:5
+    This is not compatible with the RequiredTypeArguments extension.
+    Suggested fix: Consider renaming the type variable.
diff --git a/testsuite/tests/rename/should_compile/all.T b/testsuite/tests/rename/should_compile/all.T
index c8caa1cd34b4a02db9bb0a7b05f7147630a53284..f64846703c5dd4f28f3ae3aa45a2e2f24ef53ec1 100644
--- a/testsuite/tests/rename/should_compile/all.T
+++ b/testsuite/tests/rename/should_compile/all.T
@@ -199,6 +199,7 @@ test('T22513f', normal, compile, ['-Wterm-variable-capture'])
 test('T22513g', normal, compile, ['-Wterm-variable-capture'])
 test('T22513h', normal, compile, ['-Wterm-variable-capture'])
 test('T22513i', req_th, compile, ['-Wterm-variable-capture'])
+test('T22513j', normal, compile, ['-Wterm-variable-capture'])
 test('T22913', normal, compile, [''])
 test('NullaryRecordWildcard', normal, compile, [''])
 test('GADTNullaryRecordWildcard', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/T12686.hs b/testsuite/tests/rename/should_fail/T12686.hs
deleted file mode 100644
index a9d0da9aa107ee268927ae15e5766e6b53cd0893..0000000000000000000000000000000000000000
--- a/testsuite/tests/rename/should_fail/T12686.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-module T12686 where
-
-import Data.Proxy
-
-x = True
-
-data Bad = Bad 'x
--- The 'x should be rejected in a civilised way
-
-data AlsoBad = AlsoBad {
-  a :: Int,
-  b :: Either Int 'a }
--- Ditto 'a here
diff --git a/testsuite/tests/rename/should_fail/T12686.stderr b/testsuite/tests/rename/should_fail/T12686.stderr
deleted file mode 100644
index e8fc83056df623318e01d7ed204689b331f154e6..0000000000000000000000000000000000000000
--- a/testsuite/tests/rename/should_fail/T12686.stderr
+++ /dev/null
@@ -1,8 +0,0 @@
-
-T12686.hs:7:16: error: [GHC-45510]
-    Term variable ‘x’ cannot be used here
-      (term variables cannot be promoted)
-
-T12686.hs:12:19: error: [GHC-45510]
-    Term variable ‘a’ cannot be used here
-      (term variables cannot be promoted)
diff --git a/testsuite/tests/rename/should_fail/T12686a.hs b/testsuite/tests/rename/should_fail/T12686a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..c31dd485df2a022a647da07507303748a48d2792
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686a.hs
@@ -0,0 +1,6 @@
+module T12686a where
+
+x = True
+
+data Bad = MkBad 'x
+-- The 'x should be rejected in a civilised way
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T12686a.stderr b/testsuite/tests/rename/should_fail/T12686a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..ae6dc2668bbbfe5427c6376ed5fb5ce0b80934c6
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686a.stderr
@@ -0,0 +1,7 @@
+
+T12686a.hs:5:18: error: [GHC-45510]
+    • Term variable ‘x’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type ‘'x’
+      In the definition of data constructor ‘MkBad’
+      In the data declaration for ‘Bad’
diff --git a/testsuite/tests/rename/should_fail/T12686b.hs b/testsuite/tests/rename/should_fail/T12686b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..6fd585df4d441367920da8967b9c17bec68ca391
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686b.hs
@@ -0,0 +1,6 @@
+module T12686b where
+
+data Bad = MkBad {
+  a :: Int,
+  b :: Either Int 'a }
+-- The 'a should be rejected in a civilised way
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T12686b.stderr b/testsuite/tests/rename/should_fail/T12686b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..e69ab763f29ca4394a2301efe7d2980493a943a5
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686b.stderr
@@ -0,0 +1,7 @@
+
+T12686b.hs:5:19: error: [GHC-45510]
+    • Term variable ‘a’ cannot be used here
+        (term variables cannot be promoted)
+    • In the second argument of ‘Either’, namely ‘'a’
+      In the type ‘Either Int 'a’
+      In the definition of data constructor ‘MkBad’
diff --git a/testsuite/tests/rename/should_fail/T12686c.hs b/testsuite/tests/rename/should_fail/T12686c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ac08aff5b5885a69f34d55bb5fd0ac4fad0f6632
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686c.hs
@@ -0,0 +1,9 @@
+module T12686 where
+
+import Data.Proxy
+
+class C a where
+  x :: a -> Bool
+
+data Bad = MkBad 'x
+-- The 'x should be rejected in a civilised way
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T12686c.stderr b/testsuite/tests/rename/should_fail/T12686c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..d13ded589c78c4b72caabea42f0155c67ac25a35
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T12686c.stderr
@@ -0,0 +1,7 @@
+
+T12686c.hs:8:18: error: [GHC-45510]
+    • Term variable ‘x’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type ‘'x’
+      In the definition of data constructor ‘MkBad’
+      In the data declaration for ‘Bad’
diff --git a/testsuite/tests/rename/should_fail/T23740a.hs b/testsuite/tests/rename/should_fail/T23740a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..e95046a3da85679ebe193fea4dc3cff94d76e394
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740a where
+
+a = 10
+
+f :: a -> a
+f = id
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740a.stderr b/testsuite/tests/rename/should_fail/T23740a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..58ec490c39cc6d258434ed2afa2edd7d7c5de09c
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740a.stderr
@@ -0,0 +1,5 @@
+
+T23740a.hs:7:6: error: [GHC-45510]
+    • Term variable ‘a’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type signature: f :: a -> a
diff --git a/testsuite/tests/rename/should_fail/T23740b.hs b/testsuite/tests/rename/should_fail/T23740b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ecc77d78200fea7ee5cce35026a6c38e87bce5d9
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740b.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740b where
+
+import Prelude (id, Int)
+
+f :: id -> Int
+f _ = 10
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740b.stderr b/testsuite/tests/rename/should_fail/T23740b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..cb6bbcfa27f2901c4125968ee450d2c20c233ba2
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740b.stderr
@@ -0,0 +1,5 @@
+
+T23740b.hs:7:6: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type signature: f :: id -> Int
diff --git a/testsuite/tests/rename/should_fail/T23740c.hs b/testsuite/tests/rename/should_fail/T23740c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4fbf8952e2b3c614658ab5dac338bd7fd951890e
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740c where
+
+f :: Int -> Int
+f a = g a
+  where
+    g :: a -> a
+    g = id
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740c.stderr b/testsuite/tests/rename/should_fail/T23740c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..aa8c1be804d8bbd8cab8d22bd3fe8a3a98589c1e
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740c.stderr
@@ -0,0 +1,11 @@
+
+T23740c.hs:8:10: error: [GHC-45510]
+    • Term variable ‘a’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type signature: g :: a -> a
+      In an equation for ‘f’:
+          f a
+            = g a
+            where
+                g :: a -> a
+                g = id
diff --git a/testsuite/tests/rename/should_fail/T23740d.hs b/testsuite/tests/rename/should_fail/T23740d.hs
new file mode 100644
index 0000000000000000000000000000000000000000..435961e267b7c481cbcaa1669783568d6148e85a
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740d.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T22513d where
+
+f (Just (x :: id) :: Maybe id) = x
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740d.stderr b/testsuite/tests/rename/should_fail/T23740d.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..76220b28fcd38bde3718ddc33827e90872694bf7
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740d.stderr
@@ -0,0 +1,7 @@
+
+T23740d.hs:5:28: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the first argument of ‘Maybe’, namely ‘id’
+      In the type ‘Maybe id’
+      In a pattern type signature: Maybe id
diff --git a/testsuite/tests/rename/should_fail/T23740e.hs b/testsuite/tests/rename/should_fail/T23740e.hs
new file mode 100644
index 0000000000000000000000000000000000000000..92c63ce1a3de09c2abe14bc7ed882be66aa1faff
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740e.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740e where
+
+data T (a :: id) = MkT
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740e.stderr b/testsuite/tests/rename/should_fail/T23740e.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..7e996474dfc8c400f64ef400488ba61ea323b0e1
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740e.stderr
@@ -0,0 +1,6 @@
+
+T23740e.hs:5:14: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the kind ‘id’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/rename/should_fail/T23740f.hs b/testsuite/tests/rename/should_fail/T23740f.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a4f21c09b749d8e5bb32746f5cedae51f76b546b
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740f.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740f where
+
+import Data.Proxy
+
+p :: () -> forall (a :: id). Proxy a
+p () = Proxy
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740f.stderr b/testsuite/tests/rename/should_fail/T23740f.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..ec9fef5ab263f877b058f4306d9ea615b6dff7e1
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740f.stderr
@@ -0,0 +1,6 @@
+
+T23740f.hs:7:25: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the kind ‘id’
+      In the type signature: p :: () -> forall (a :: id). Proxy a
diff --git a/testsuite/tests/rename/should_fail/T23740g.hs b/testsuite/tests/rename/should_fail/T23740g.hs
new file mode 100644
index 0000000000000000000000000000000000000000..18a0cfdd3626614830f078a18f4c9f34ac910557
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740g.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740g where
+
+import Data.Kind
+
+data T k (id::head) (b::k) :: k2 -> head -> Type
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740g.stderr b/testsuite/tests/rename/should_fail/T23740g.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..247a3c0b79fbd92ae087bd68d50c15f75405c739
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740g.stderr
@@ -0,0 +1,6 @@
+
+T23740g.hs:7:15: error: [GHC-45510]
+    • Term variable ‘head’ cannot be used here
+        (term variables cannot be promoted)
+    • In the kind ‘head’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/rename/should_fail/T23740h.hs b/testsuite/tests/rename/should_fail/T23740h.hs
new file mode 100644
index 0000000000000000000000000000000000000000..678b8338b2158985677a551b1181049816c7fd11
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740h.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740h where
+
+class C a where
+    f :: a -> Bool
+
+instance C (Maybe id) where
+    f (Just _) = True
+    f Nothing = False
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740h.stderr b/testsuite/tests/rename/should_fail/T23740h.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..432d835b2f1a6988ea8055e2209d45ff07a51524
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740h.stderr
@@ -0,0 +1,7 @@
+
+T23740h.hs:8:19: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the first argument of ‘Maybe’, namely ‘id’
+      In the first argument of ‘C’, namely ‘(Maybe id)’
+      In the instance declaration for ‘C (Maybe id)’
diff --git a/testsuite/tests/rename/should_fail/T23740i.hs b/testsuite/tests/rename/should_fail/T23740i.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3ed5d98c969b9228133581dad43cdb7cdc05db5b
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740i.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TemplateHaskell, QuasiQuotes #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740i where
+
+import Language.Haskell.TH
+
+sp :: Q ()
+sp =
+    $(do
+        instances <- reifyInstances ''Show [ VarT (mkName "id") ]
+        [e| return () |])
\ No newline at end of file
diff --git a/testsuite/tests/rename/should_fail/T23740i.stderr b/testsuite/tests/rename/should_fail/T23740i.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..9fde7cf518891acfc9b4a788cc096b0e56e369dc
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740i.stderr
@@ -0,0 +1,7 @@
+
+T23740i.hs:10:6: error: [GHC-45510]
+    • Term variable ‘id’ cannot be used here
+        (term variables cannot be promoted)
+    • In the first argument of ‘Show’, namely ‘id’
+      In the type ‘Show id’
+      In the argument of reifyInstances: GHC.Show.Show id
diff --git a/testsuite/tests/rename/should_fail/T23740j.hs b/testsuite/tests/rename/should_fail/T23740j.hs
new file mode 100644
index 0000000000000000000000000000000000000000..35fc7029ddf5153a9011ee6b01c2ab34a41e86b4
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740j.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23740j where
+
+x :: ()
+x = ()
+  where
+    a = a
+    f :: a -> a
+    f = f
diff --git a/testsuite/tests/rename/should_fail/T23740j.stderr b/testsuite/tests/rename/should_fail/T23740j.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..8a6b634e062409562ef823e4079c1fac8192a319
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T23740j.stderr
@@ -0,0 +1,11 @@
+
+T23740j.hs:9:10: error: [GHC-45510]
+    • Term variable ‘a’ cannot be used here
+        (term variables cannot be promoted)
+    • In the type signature: f :: a -> a
+      In an equation for ‘x’:
+          x = ()
+            where
+                a = a
+                f :: a -> a
+                f = f
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 2c68cfb484f4c62cc3ebc9eee951bb2625a92f15..1734daa99f07f8bb75c3b257a230907b395a1e2d 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -129,7 +129,9 @@ test('T11663', normal, compile_fail, [''])
 test('T12146', normal, compile_fail, [''])
 test('T12229', normal, compile, [''])
 test('T12681', normal, multimod_compile_fail, ['T12681','-v0'])
-test('T12686', normal, compile_fail, [''])
+test('T12686a', normal, compile_fail, [''])
+test('T12686b', normal, compile_fail, [''])
+test('T12686c', normal, compile_fail, [''])
 test('T11592', normal, compile_fail, [''])
 test('T12879', normal, compile_fail, [''])
 test('T13644', normal, multimod_compile_fail, ['T13644','-v0'])
@@ -210,5 +212,15 @@ test('T22478b', normal, compile_fail, [''])
 test('T22478d', normal, compile_fail, [''])
 test('T22478e', normal, compile_fail, [''])
 test('T22478f', normal, compile_fail, [''])
+test('T23740a', normal, compile_fail, [''])
+test('T23740b', normal, compile_fail, [''])
+test('T23740c', normal, compile_fail, [''])
+test('T23740d', normal, compile_fail, [''])
+test('T23740e', normal, compile_fail, [''])
+test('T23740f', normal, compile_fail, [''])
+test('T23740g', normal, compile_fail, [''])
+test('T23740h', normal, compile_fail, [''])
+test('T23740i', req_th, compile_fail, [''])
+test('T23740j', normal, compile_fail, [''])
 test('T23570', [extra_files(['T23570_aux.hs'])], multimod_compile_fail, ['T23570', '-v0'])
 test('T23570b', [extra_files(['T23570_aux.hs'])], multimod_compile, ['T23570b', '-v0'])
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr b/testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr
index 0eb9f920ab66fe557b28e28aeff34ecc2d346d4e..3bb94d19aabf79ec5292778ad24f070fd74a52d7 100644
--- a/testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr
+++ b/testsuite/tests/vdq-rta/should_fail/T23738_fail_var.stderr
@@ -1,6 +1,7 @@
 
-T23738_fail_var.hs:11:12: error: [GHC-10969]
-    • Local identifier ‘a’ used as a type
+T23738_fail_var.hs:11:12: error: [GHC-45510]
+    • Term variable ‘a’ cannot be used here
+        (term variables cannot be promoted)
     • In the type ‘a’
       In the expression: vfun a
       In an equation for ‘f’: f a = vfun a