From d1bf25c7d4829ec5823974af2e8ea3821d724f25 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Sun, 30 Jul 2023 20:53:30 +0200
Subject: [PATCH] Term variable capture (#23740)

This patch changes type variable lookup rules (lookupTypeOccRn) and
implicit quantification rules (filterInScope) so that variables bound
in the term namespace can be captured at the type level

  {-# LANGUAGE RequiredTypeArguments #-}
  f1 x = g1 @x                -- `x` used in a type application
  f2 x = g2 (undefined :: x)  -- `x` used in a type annotation
  f3 x = g3 (type x)          -- `x` used in an embedded type
  f4 x = ...
    where g4 :: x -> x        -- `x` used in a type signature
          g4 = ...

This change alone does not allow us to accept examples shown above,
but at least it gets them past the renamer.
---
 compiler/GHC/Rename/Env.hs                    | 129 +++++++++++----
 compiler/GHC/Rename/HsType.hs                 | 150 ++++++++++++++++--
 compiler/GHC/Rename/Module.hs                 |  10 +-
 compiler/GHC/Tc/Errors/Ppr.hs                 |   2 +-
 compiler/GHC/Tc/Errors/Types/PromotionErr.hs  |   2 +-
 compiler/GHC/Tc/Gen/HsType.hs                 |   2 +
 compiler/GHC/Tc/Gen/Splice.hs                 |   2 +-
 compiler/GHC/Tc/Utils/Env.hs                  |  16 +-
 testsuite/tests/diagnostic-codes/codes.stdout |   1 +
 .../rename/should_compile/T22513a.stderr      |   2 +-
 .../rename/should_compile/T22513b.stderr      |   2 +-
 .../rename/should_compile/T22513c.stderr      |   2 +-
 .../rename/should_compile/T22513d.stderr      |   2 +-
 .../rename/should_compile/T22513e.stderr      |   2 +-
 .../rename/should_compile/T22513f.stderr      |   2 +-
 .../tests/rename/should_compile/T22513g.hs    |   2 +-
 .../rename/should_compile/T22513g.stderr      |   4 +-
 .../rename/should_compile/T22513h.stderr      |   2 +-
 .../rename/should_compile/T22513i.stderr      |   5 +-
 .../tests/rename/should_compile/T22513j.hs    |   8 +
 .../rename/should_compile/T22513j.stderr      |   7 +
 testsuite/tests/rename/should_compile/all.T   |   1 +
 testsuite/tests/rename/should_fail/T12686.hs  |  13 --
 .../tests/rename/should_fail/T12686.stderr    |   8 -
 testsuite/tests/rename/should_fail/T12686a.hs |   6 +
 .../tests/rename/should_fail/T12686a.stderr   |   7 +
 testsuite/tests/rename/should_fail/T12686b.hs |   6 +
 .../tests/rename/should_fail/T12686b.stderr   |   7 +
 testsuite/tests/rename/should_fail/T12686c.hs |   9 ++
 .../tests/rename/should_fail/T12686c.stderr   |   7 +
 testsuite/tests/rename/should_fail/T23740a.hs |   8 +
 .../tests/rename/should_fail/T23740a.stderr   |   5 +
 testsuite/tests/rename/should_fail/T23740b.hs |   8 +
 .../tests/rename/should_fail/T23740b.stderr   |   5 +
 testsuite/tests/rename/should_fail/T23740c.hs |   9 ++
 .../tests/rename/should_fail/T23740c.stderr   |  11 ++
 testsuite/tests/rename/should_fail/T23740d.hs |   5 +
 .../tests/rename/should_fail/T23740d.stderr   |   7 +
 testsuite/tests/rename/should_fail/T23740e.hs |   5 +
 .../tests/rename/should_fail/T23740e.stderr   |   6 +
 testsuite/tests/rename/should_fail/T23740f.hs |   8 +
 .../tests/rename/should_fail/T23740f.stderr   |   6 +
 testsuite/tests/rename/should_fail/T23740g.hs |   7 +
 .../tests/rename/should_fail/T23740g.stderr   |   6 +
 testsuite/tests/rename/should_fail/T23740h.hs |  10 ++
 .../tests/rename/should_fail/T23740h.stderr   |   7 +
 testsuite/tests/rename/should_fail/T23740i.hs |  12 ++
 .../tests/rename/should_fail/T23740i.stderr   |   7 +
 testsuite/tests/rename/should_fail/T23740j.hs |  10 ++
 .../tests/rename/should_fail/T23740j.stderr   |  11 ++
 testsuite/tests/rename/should_fail/all.T      |  14 +-
 .../should_fail/T23738_fail_var.stderr        |   5 +-
 52 files changed, 504 insertions(+), 86 deletions(-)
 create mode 100644 testsuite/tests/rename/should_compile/T22513j.hs
 create mode 100644 testsuite/tests/rename/should_compile/T22513j.stderr
 delete mode 100644 testsuite/tests/rename/should_fail/T12686.hs
 delete mode 100644 testsuite/tests/rename/should_fail/T12686.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T12686a.hs
 create mode 100644 testsuite/tests/rename/should_fail/T12686a.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T12686b.hs
 create mode 100644 testsuite/tests/rename/should_fail/T12686b.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T12686c.hs
 create mode 100644 testsuite/tests/rename/should_fail/T12686c.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740a.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740a.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740b.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740b.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740c.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740c.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740d.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740d.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740e.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740e.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740f.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740f.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740g.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740g.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740h.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740h.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740i.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740i.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T23740j.hs
 create mode 100644 testsuite/tests/rename/should_fail/T23740j.stderr

diff --git a/compiler/GHC/Rename/Env.hs b/compiler/GHC/Rename/Env.hs
index b45dc0b63dea..beaac9c857b5 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 e380b86f5ace..ae4273f75ab7 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 99a34b2f4e80..f779285d5970 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 196a1909a422..1fd5c45aed47 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 47e49a5933e4..ab0d8e3b0fe2 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 6c173e2b3936..d50cd70e3ab5 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 ef4009fb0239..f47bcff9af8c 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 8e6e628648bb..ba45a85b87e4 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 63ca86b328d5..38b6a3effe65 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 339b09eef86a..ce0ecc20d0bf 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 1bda00fb0d81..89dd86c6bf69 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 dab473ca7e8f..b084a8561eda 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 076bcb94c5d8..5afaaf4fe864 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 43207a3b4c03..0a5ca150a6b1 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 94454b67f980..d3b75e44a8eb 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 1895b70bc27b..37f3f20d3a21 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 0c0782d8947e..9ffcbb490f13 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 a88fdbd1abd6..f97df3b8b6cd 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 d99b621a47ab..29f052d53a45 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 000000000000..165f6556c161
--- /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 000000000000..c9a101a0797d
--- /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 c8caa1cd34b4..f64846703c5d 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 a9d0da9aa107..000000000000
--- 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 e8fc83056df6..000000000000
--- 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 000000000000..c31dd485df2a
--- /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 000000000000..ae6dc2668bbb
--- /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 000000000000..6fd585df4d44
--- /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 000000000000..e69ab763f29c
--- /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 000000000000..ac08aff5b588
--- /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 000000000000..d13ded589c78
--- /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 000000000000..e95046a3da85
--- /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 000000000000..58ec490c39cc
--- /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 000000000000..ecc77d78200f
--- /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 000000000000..cb6bbcfa27f2
--- /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 000000000000..4fbf8952e2b3
--- /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 000000000000..aa8c1be804d8
--- /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 000000000000..435961e267b7
--- /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 000000000000..76220b28fcd3
--- /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 000000000000..92c63ce1a3de
--- /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 000000000000..7e996474dfc8
--- /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 000000000000..a4f21c09b749
--- /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 000000000000..ec9fef5ab263
--- /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 000000000000..18a0cfdd3626
--- /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 000000000000..247a3c0b79fb
--- /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 000000000000..678b8338b215
--- /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 000000000000..432d835b2f1a
--- /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 000000000000..3ed5d98c969b
--- /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 000000000000..9fde7cf51889
--- /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 000000000000..35fc7029ddf5
--- /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 000000000000..8a6b634e0624
--- /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 2c68cfb484f4..1734daa99f07 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 0eb9f920ab66..3bb94d19aabf 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
-- 
GitLab