diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index d81f735f648c5beb34747e30dc05df82d49cc24a..5a01b10479f239a816a6ba365a77a50b618ac9b8 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1386,15 +1386,17 @@ repTy (HsTyVar _ _ (L _ n))
   | n `hasKey` constraintKindTyConKey  = repTConstraint
   | n `hasKey` unrestrictedFunTyConKey = repArrowTyCon
   | n `hasKey` fUNTyConKey             = repMulArrowTyCon
-  | isTvOcc occ   = do tv1 <- lookupOcc n
-                       repTvar tv1
-  | isDataOcc occ = do tc1 <- lookupOcc n
-                       repPromotedDataCon tc1
-  | n == eqTyConName = repTequality
-  | otherwise     = do tc1 <- lookupOcc n
-                       repNamedTyCon tc1
+  | n `hasKey` eqTyConKey              = repTequality
+  | isVarNameSpace     ns = do tv1 <- lookupOcc n
+                               repTvar tv1
+  | isDataConNameSpace ns = do dc1 <- lookupOcc n
+                               repPromotedDataCon dc1
+  | isTcClsNameSpace   ns = do tc1 <- lookupOcc n
+                               repNamedTyCon tc1
+  | otherwise = panic "repTy: HsTyVar: unknown namespace"
   where
     occ = nameOccName n
+    ns  = occNameSpace occ
 
 repTy (HsAppTy _ f a)       = do
                                 f1 <- repLTy f
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index a27cc513cd3e7d786be58598f3d894bd7aec5394..f57fe07a6bae5ef81e81e106bbcd5872f43902b7 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -819,18 +819,12 @@ instance Diagnostic TcRnMessage where
             fsep [ text "Pattern matching on GADTs without MonoLocalBinds"
                  , text "is fragile." ]
     TcRnIncorrectNameSpace name _
-      -> mkSimpleDecorated $ msg
+      -> mkSimpleDecorated $
+           text "The" <+> what <+> text "does not live in" <+> other_ns
         where
-          msg
-            -- We are in a type-level namespace,
-            -- and the name is incorrectly at the term-level.
-            | isValNameSpace ns
-            = text "The" <+> what <+> text "does not live in the type-level namespace"
-
-            -- We are in a term-level namespace,
-            -- and the name is incorrectly at the type-level.
-            | otherwise
-            = text "Illegal term-level use of the" <+> what
+          -- the other (opposite) namespace
+          other_ns | isValNameSpace ns = text "the type-level namespace"
+                   | otherwise         = text "the term-level namespace"
           ns = nameNameSpace name
           what = pprNameSpace ns <+> quotes (ppr name)
     TcRnNotInScope err name imp_errs _
@@ -1046,6 +1040,10 @@ instance Diagnostic TcRnMessage where
                      TermVariablePE -> text "term variables cannot be promoted"
                      TypeVariablePE -> text "type variables bound in a kind signature cannot be used in the type"
           same_rec_group_msg = text "it is defined and used in the same recursive group"
+    TcRnIllegalTermLevelUse name err
+      -> mkSimpleDecorated $
+           text "Illegal term-level use of the" <+>
+             text (teCategory err) <+> quotes (ppr name)
     TcRnMatchesHaveDiffNumArgs argsContext (MatchArgMatches match1 bad_matches)
       -> mkSimpleDecorated $
            (vcat [ pprMatchContextNouns argsContext <+>
@@ -1258,9 +1256,7 @@ instance Diagnostic TcRnMessage where
 
     TcRnIllformedTypePattern p
       -> mkSimpleDecorated $
-          hang (text "Ill-formed type pattern:") 2 (ppr p) $$
-          text "Expected a type pattern introduced with the"
-            <+> quotes (text "type") <+> text "keyword."
+          hang (text "Ill-formed type pattern:") 2 (ppr p)
     TcRnIllegalTypePattern
       -> mkSimpleDecorated $
           text "Illegal type pattern." $$
@@ -2203,6 +2199,8 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnUnpromotableThing{}
       -> ErrorWithoutFlag
+    TcRnIllegalTermLevelUse{}
+      -> ErrorWithoutFlag
     TcRnMatchesHaveDiffNumArgs{}
       -> ErrorWithoutFlag
     TcRnCannotBindScopedTyVarInPatSig{}
@@ -2847,6 +2845,8 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnUnpromotableThing{}
       -> noHints
+    TcRnIllegalTermLevelUse{}
+      -> noHints
     TcRnMatchesHaveDiffNumArgs{}
       -> noHints
     TcRnCannotBindScopedTyVarInPatSig{}
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index be15f54a8ad0b77bc42b014704323a91371c8787..95de0016e5f8063f408f7c7656cdffec541ecc59 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -75,6 +75,7 @@ module GHC.Tc.Errors.Types (
   , HoleFitDispConfig(..)
   , RelevantBindings(..), pprRelevantBindings
   , PromotionErr(..), pprPECategory, peCategory
+  , TermLevelUseErr(..), teCategory
   , NotInScopeError(..), mkTcRnNotInScope
   , ImportError(..)
   , HoleError(..)
@@ -2054,9 +2055,11 @@ data TcRnMessage where
 
       Example:
 
-        f x = Int
+        list2 = $( conE ''(:) `appE` litE (IntegerL 5) `appE` conE '[] )
+        --              ^^^^^
+        --              should use a single quotation tick, i.e. '(:)
 
-      Test cases: T18740a, T20884.
+      Test cases: T20884.
   -}
   TcRnIncorrectNameSpace :: Name
                          -> Bool -- ^ whether the error is happening
@@ -2379,6 +2382,27 @@ data TcRnMessage where
   -}
   TcRnUnpromotableThing :: !Name -> !PromotionErr -> TcRnMessage
 
+  {- | TcRnIllegalTermLevelUse is an error that occurs when the user attempts to
+       use a type-level entity at the term-level.
+
+       Examples:
+          f x = Int                 -- illegal use of a type constructor
+          g (Proxy :: Proxy a) = a  -- illegal use of a type variable
+
+       Note that the namespace cannot be used to determine if a name refers to a
+       type-level entity:
+
+          {-# LANGUAGE RequiredTypeArguments #-}
+          bad :: forall (a :: k) -> k
+          bad t = t
+
+      The name `t` is assigned the `varName` namespace but stands for a type
+      variable that cannot be used at the term level.
+
+      Test cases: T18740a, T18740b, T23739_fail_ret, T23739_fail_case
+  -}
+  TcRnIllegalTermLevelUse :: !Name -> !TermLevelUseErr -> TcRnMessage
+
   {-| TcRnMatchesHaveDiffNumArgs is an error occurring when something has matches
      that have different numbers of arguments
 
diff --git a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
index ab0d8e3b0fe27f43e1e3fcd9f559aedc1b8fbded..b05d122432f490c35826823978ca2e24bfedf8f6 100644
--- a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
+++ b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
@@ -2,6 +2,8 @@
 module GHC.Tc.Errors.Types.PromotionErr ( PromotionErr(..)
                                         , pprPECategory
                                         , peCategory
+                                        , TermLevelUseErr(..)
+                                        , teCategory
                                         ) where
 
 import GHC.Prelude
@@ -52,6 +54,17 @@ peCategory RecDataConPE         = "data constructor"
 peCategory TermVariablePE       = "term variable"
 peCategory TypeVariablePE       = "type variable"
 
+-- The opposite of a promotion error (a demotion error, in a sense).
+data TermLevelUseErr
+  = TyConTE   -- Type constructor used at the term level, e.g. x = Int
+  | ClassTE   -- Class used at the term level,            e.g. x = Functor
+  | TyVarTE   -- Type variable used at the term level,    e.g. f (Proxy :: Proxy a) = a
+  deriving (Generic)
+
+teCategory :: TermLevelUseErr -> String
+teCategory ClassTE = "class"
+teCategory TyConTE = "type constructor"
+teCategory TyVarTE = "type variable"
 
 {- Note [Type variable scoping errors during typechecking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 2aaaed941f4f187ecaf00dc9b32ef6af917c7f45..a9bf54b254180625e3efe71454637d8481a77d2f 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -1100,13 +1100,13 @@ At definition sites we may have type /patterns/ to abstract over type variables
    fs           x       = rhs   -- Specified: type pattern omitted
    fs @a       (x :: a) = rhs   -- Specified: type pattern supplied (NB: not implemented)
    fr (type a) (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier used
-   fr a        (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
+   fr a        (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
 
 Type patterns in lambdas work the same way as they do in a function LHS
    fs = \           x       -> rhs   -- Specified: type pattern omitted
    fs = \ @a       (x :: a) -> rhs   -- Specified: type pattern supplied (NB: not implemented)
    fr = \ (type a) (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier used
-   fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted (NB: not implemented)
+   fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
 
 Type patterns may also occur in a constructor pattern. Consider the following data declaration
    data T where
@@ -1177,7 +1177,7 @@ Syntax of abstractions in Pat
 * Examples:
       \ (MkT @a  (x :: a)) -> rhs    -- ConPat (c.o. Pat) and HsConPatTyArg (c.o. HsConPatTyArg)
       \ (type a) (x :: a)  -> rhs    -- EmbTyPat (c.o. Pat)
-      \ a        (x :: a)  -> rhs    -- VarPat (c.o. Pat)   (NB. not implemented)
+      \ a        (x :: a)  -> rhs    -- VarPat (c.o. Pat)
       \ @a       (x :: a)  -> rhs    -- to be decided       (NB. not implemented)
 
 * A HsTyPat is not necessarily a plain variable. At the very least,
@@ -1230,7 +1230,7 @@ variable.  Only later (in the type checker) will we find out that it stands for
 the forall-bound type variable `a`.  So when RequiredTypeArguments is in effect,
 we change implicit quantification to take term variables into account; that is,
 we do not implicitly quantify the signature of `g` to `g :: forall t. t->t`
-because of the term-level `t` that is in scope. (NB. not implemented)
+because of the term-level `t` that is in scope.
 See Note [Term variable capture and implicit quantification].
 
 Typechecking type applications
@@ -1294,9 +1294,9 @@ and ordinary patterns:
   * tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
 
 tc_forall_pat unwraps the EmbTyPat and uses the type pattern contained
-within it. This is another spot where the "T2T-Mapping" can take place.
-This would allow us to support
-  f a (x :: a) = rhs    -- no EmbTyPat    (NB. not implemented)
+within it. This is another spot where the "T2T-Mapping" can take place,
+allowing us to support
+  f a (x :: a) = rhs    -- no EmbTyPat
 
 Type patterns in constructor patterns are handled in with tcConTyArg.
 Both tc_forall_pat and tcConTyArg delegate most of the work to tcHsTyPat.
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index 99645fcec1bf1bd6d73e746ac6d943262d63ab2a..4c8e4c9d92cde740aa71934f4df6bd4f918e3cd4 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -83,6 +83,7 @@ import GHC.Driver.DynFlags
 import GHC.Utils.Misc
 import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic.Plain
+import qualified GHC.LanguageExtensions as LangExt
 
 import GHC.Data.Maybe
 import Control.Monad
@@ -1161,13 +1162,15 @@ tc_infer_id id_name
           pprov = case lookupGRE_Name gre nm of
                       Just gre -> nest 2 (pprNameProvenance gre)
                       Nothing  -> empty
-      fail_with_msg dataName nm pprov
+          err | isClassTyCon tc = ClassTE
+              | otherwise       = TyConTE
+      fail_with_msg dataName nm pprov err
 
     fail_tyvar nm =
       let pprov = nest 2 (text "bound at" <+> ppr (getSrcLoc nm))
-      in fail_with_msg varName nm pprov
+      in fail_with_msg varName nm pprov TyVarTE
 
-    fail_with_msg whatName nm pprov = do
+    fail_with_msg whatName nm pprov err = do
       (import_errs, hints) <- get_suggestions whatName
       unit_state <- hsc_units <$> getTopEnv
       let
@@ -1177,15 +1180,64 @@ tc_infer_id id_name
         import_err_msg = vcat $ map ppr import_errs
         info = ErrInfo { errInfoContext = pprov, errInfoSupplementary = import_err_msg $$ hint_msg }
       failWithTc $ TcRnMessageWithInfo unit_state (
-              mkDetailedMessage info (TcRnIncorrectNameSpace nm False))
+              mkDetailedMessage info (TcRnIllegalTermLevelUse nm err))
 
     get_suggestions ns = do
-       let occ = mkOccNameFS ns (occNameFS (occName id_name))
-       lcl_env <- getLocalRdrEnv
-       unknownNameSuggestions lcl_env WL_Anything (mkRdrUnqual occ)
+      required_type_arguments <- xoptM LangExt.RequiredTypeArguments
+      if required_type_arguments && isVarNameSpace ns
+      then return ([], [])  -- See Note [Suppress hints with RequiredTypeArguments]
+      else do
+        let occ = mkOccNameFS ns (occNameFS (occName id_name))
+        lcl_env <- getLocalRdrEnv
+        unknownNameSuggestions lcl_env WL_Anything (mkRdrUnqual occ)
 
     return_id id = return (HsVar noExtField (noLocA id), idType id)
 
+{- Note [Suppress hints with RequiredTypeArguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When a type variable is used at the term level, GHC assumes the user might
+have made a typo and suggests a term variable with a similar name.
+
+For example, if the user writes
+  f (Proxy :: Proxy nap) (Proxy :: Proxy gap) = nap (+1) [1,2,3]
+then GHC will helpfully suggest `map` instead of `nap`
+  • Illegal term-level use of the type variable ‘nap’
+  • Perhaps use ‘map’ (imported from Prelude)
+
+Importantly, GHC does /not/ suggest `gap`, which is in scope.
+Question: How does GHC know not to suggest `gap`?  After all, the edit distance
+          between `map`, `nap`, and `gap` is equally short.
+Answer: GHC takes the namespace into consideration. `gap` is a `tvName`, and GHC
+        would only suggest a `varName` at the term level.
+
+In other words, the current hint infrastructure assumes that the namespace of an
+entity is a reliable indicator of its level
+   term-level name <=> term-level entity
+   type-level name <=> type-level entity
+
+With RequiredTypeArguments, this assumption does not hold. Consider
+  bad :: forall a b -> ...
+  bad nap gap = nap
+
+This use of `nap` on the RHS is illegal because `nap` stands for a type
+variable. It cannot be returned as the result of a function. At the same time,
+it is bound as a `varName`, i.e. in the term-level namespace.
+
+Unless we suppress hints, GHC gets awfully confused
+    • Illegal term-level use of the variable ‘nap’
+    • Perhaps use one of these:
+        ‘nap’ (line 2), ‘gap’ (line 2), ‘map’ (imported from Prelude)
+
+GHC shouldn't suggest `gap`, which is also a type variable; using it would
+result in the same error. And it especially shouldn't suggest using `nap`
+instead of `nap`, which is absurd.
+
+The proper solution is to overhaul the hint system to consider what a name
+stands for instead of looking at its namespace alone. This is tracked in #24231.
+As a temporary measure, we avoid those potentially misleading hints by
+suppressing them entirely if RequiredTypeArguments is in effect.
+-}
+
 check_local_id :: Id -> TcM ()
 check_local_id id
   = do { checkThLocalId id
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 7734625bb713803ef80e46458c41e2b4c04420d1..037db0fa3a334b997e77dd9b935311c024ecc97a 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -390,13 +390,78 @@ tc_tt_pat (ExpForAllPatTy tv)  penv pat thing_inside = tc_forall_pat penv (pat,
 
 tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
 tc_forall_pat _ (EmbTyPat _ toktype tp, tv) thing_inside
+  -- The entire type pattern is guarded with the `type` herald:
+  --    f (type t) (x :: t) = ...
+  -- This special case is not necessary for correctness but avoids
+  -- a redundant `ExpansionPat` node.
+  = do { (arg_ty, result) <- tc_ty_pat tp tv thing_inside
+       ; return (EmbTyPat arg_ty toktype tp, result) }
+tc_forall_pat _ (pat, tv) thing_inside
+  -- The type pattern is not guarded with the `type` herald, or perhaps
+  -- only parts of it are, e.g.
+  --    f (t :: Type)        (x :: t) = ...    -- no `type` herald
+  --    f ((type t) :: Type) (x :: t) = ...    -- nested `type` herald
+  -- Apply a recursive T2T transformation.
+  = do { tp <- pat_to_type_pat pat
+       ; (arg_ty, result) <- tc_ty_pat tp tv thing_inside
+       ; let pat' = XPat $ ExpansionPat pat (EmbTyPat arg_ty noHsTok tp)
+       ; return (pat', result) }
+
+-- Convert a Pat into the equivalent HsTyPat.
+-- See `expr_to_type` (GHC.Tc.Gen.App) for the HsExpr counterpart.
+-- The `TcM` monad is only used to fail on ill-formed type patterns.
+pat_to_type_pat :: Pat GhcRn -> TcM (HsTyPat GhcRn)
+pat_to_type_pat (EmbTyPat _ _ tp) = return tp
+pat_to_type_pat (VarPat _ lname)  = return (HsTP x b)
+  where b = noLocA (HsTyVar noAnn NotPromoted lname)
+        x = HsTPRn { hstp_nwcs    = []
+                   , hstp_imp_tvs = []
+                   , hstp_exp_tvs = [unLoc lname] }
+pat_to_type_pat (WildPat _) = return (HsTP x b)
+  where b = noLocA (HsWildCardTy noExtField)
+        x = HsTPRn { hstp_nwcs    = []
+                   , hstp_imp_tvs = []
+                   , hstp_exp_tvs = [] }
+pat_to_type_pat (SigPat _ pat sig_ty)
+  = do { HsTP x_hstp t <- pat_to_type_pat (unLoc pat)
+       ; let { !(HsPS x_hsps k) = sig_ty
+             ; x = append_hstp_hsps x_hstp x_hsps
+             ; b = noLocA (HsKindSig noAnn t k) }
+       ; return (HsTP x b) }
+  where
+    -- Quadratic for nested signatures ((p :: t1) :: t2)
+    -- but those are unlikely to occur in practice.
+    append_hstp_hsps :: HsTyPatRn -> HsPSRn -> HsTyPatRn
+    append_hstp_hsps t p
+      = HsTPRn { hstp_nwcs     = hstp_nwcs    t ++ hsps_nwcs    p
+               , hstp_imp_tvs  = hstp_imp_tvs t ++ hsps_imp_tvs p
+               , hstp_exp_tvs  = hstp_exp_tvs t }
+pat_to_type_pat (ParPat _ _ pat _)
+  = do { HsTP x t <- pat_to_type_pat (unLoc pat)
+       ; return (HsTP x (noLocA (HsParTy noAnn t))) }
+pat_to_type_pat pat =
+  -- There are other cases to handle (ConPat, ListPat, TuplePat, etc), but these
+  -- would always be rejected by the unification in `tcHsTyPat`, so it's fine to
+  -- skip them here. This won't continue to be the case when visible forall is
+  -- permitted in data constructors:
+  --
+  --   data T a where { Typed :: forall a -> a -> T a }
+  --   g :: T Int -> Int
+  --   g (Typed Int x) = x   -- Note the `Int` type pattern
+  --
+  -- See ticket #18389. When this feature lands, it would be best to extend
+  -- `pat_to_type_pat` to handle as many pattern forms as possible.
+  failWith $ TcRnIllformedTypePattern pat
+  -- This failure is the only use of the TcM monad in `pat_to_type_pat`
+
+tc_ty_pat :: HsTyPat GhcRn -> TcTyVar -> TcM r -> TcM (TcType, r)
+tc_ty_pat tp tv thing_inside
   = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsTyPat tp (varType tv)
        ; _ <- unifyType Nothing arg_ty (mkTyVarTy tv)
        ; result <- tcExtendNameTyVarEnv sig_wcs $
                    tcExtendNameTyVarEnv sig_ibs $
                    thing_inside
-       ; return (EmbTyPat arg_ty toktype tp, result) }
-tc_forall_pat _ (pat, _) _ = failWith $ TcRnIllformedTypePattern pat
+       ; return (arg_ty, result) }
 
 tc_pat  :: Scaled ExpSigmaTypeFRR
         -- ^ Fully refined result type
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 2acd145599ab066199973540b6b63e70bf0264b0..d6a5441141018bec046c39221d87a06b59fe451f 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -600,6 +600,7 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnPatersonCondFailure"                       = 22979
   GhcDiagnosticCode "TcRnDeprecatedInvisTyArgInConPat"              = 69797
   GhcDiagnosticCode "TcRnInvalidDefaultedTyVar"                     = 45625
+  GhcDiagnosticCode "TcRnIllegalTermLevelUse"                       = 01928
 
   -- TcRnTypeApplicationsDisabled
   GhcDiagnosticCode "TypeApplication"                               = 23482
diff --git a/testsuite/tests/module/mod132.stderr b/testsuite/tests/module/mod132.stderr
index 917d4904401f3d8133fa00d6b232cd3ede5be6d9..ff1df1c6e3d1416544456ad456f3819fcccf5d6c 100644
--- a/testsuite/tests/module/mod132.stderr
+++ b/testsuite/tests/module/mod132.stderr
@@ -1,6 +1,6 @@
 
-mod132.hs:6:7: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘Foo’
+mod132.hs:6:7: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘Foo’
     • imported from ‘Mod132_B’ at mod132.hs:4:1-15
       (and originally defined in ‘Mod132_A’ at Mod132_A.hs:3:1-14)
     • Perhaps use variable ‘foo’ (line 6)
diff --git a/testsuite/tests/module/mod147.stderr b/testsuite/tests/module/mod147.stderr
index a4ca6980f5d021eb63a83d8520804c857aa306d0..61bcf6c8f559271c60f15f04815c2a6a322a8556 100644
--- a/testsuite/tests/module/mod147.stderr
+++ b/testsuite/tests/module/mod147.stderr
@@ -1,6 +1,6 @@
 
-mod147.hs:6:5: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘D’
+mod147.hs:6:5: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘D’
     • imported from ‘Mod147_A’ at mod147.hs:4:1-15
       (and originally defined at Mod147_A.hs:3:1-14)
     • In the expression: D 4
diff --git a/testsuite/tests/rename/should_fail/RnStaticPointersFail02.stderr b/testsuite/tests/rename/should_fail/RnStaticPointersFail02.stderr
index 07405667dfbedd54032eb8a53aaccd7eb1638ca4..4efb66f5620ab2ddfa0eb7947ff16145a43520cb 100644
--- a/testsuite/tests/rename/should_fail/RnStaticPointersFail02.stderr
+++ b/testsuite/tests/rename/should_fail/RnStaticPointersFail02.stderr
@@ -1,6 +1,6 @@
 
-RnStaticPointersFail02.hs:5:12: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘T’
+RnStaticPointersFail02.hs:5:12: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘T’
     • defined at RnStaticPointersFail02.hs:7:1
     • In the body of a static form: T
       In the expression: static T
diff --git a/testsuite/tests/rename/should_fail/T18740a.stderr b/testsuite/tests/rename/should_fail/T18740a.stderr
index 5b36171a388981fc57ada4f7ccc0203100ffc943..5ac0b947d38802d9d71e8836f6cd4ba87789fd91 100644
--- a/testsuite/tests/rename/should_fail/T18740a.stderr
+++ b/testsuite/tests/rename/should_fail/T18740a.stderr
@@ -1,6 +1,6 @@
 
-T18740a.hs:3:5: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘Int’
+T18740a.hs:3:5: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘Int’
     • imported from ‘Prelude’ at T18740a.hs:1:8-14
       (and originally defined in ‘GHC.Types’)
     • In the expression: Int
diff --git a/testsuite/tests/rename/should_fail/T18740b.stderr b/testsuite/tests/rename/should_fail/T18740b.stderr
index 1e13c3a9743afbab32d1dd5126b3d79b9dd1aafe..17267c5928569989f7344df96d8f4b674e26a034 100644
--- a/testsuite/tests/rename/should_fail/T18740b.stderr
+++ b/testsuite/tests/rename/should_fail/T18740b.stderr
@@ -1,5 +1,5 @@
 
-T18740b.hs:6:24: error: [GHC-31891]
+T18740b.hs:6:24: error: [GHC-01928]
     • Illegal term-level use of the type variable ‘a’
     • bound at T18740b.hs:6:4
     • In the expression: a
diff --git a/testsuite/tests/th/T14627.stderr b/testsuite/tests/th/T14627.stderr
index 373d59dee8285a7f170632b0944b936b7e575d78..c8f5359cea912157a3664cd7f3d732107af2061b 100644
--- a/testsuite/tests/th/T14627.stderr
+++ b/testsuite/tests/th/T14627.stderr
@@ -1,6 +1,6 @@
 
-T14627.hs:4:1: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘Bool’
+T14627.hs:4:1: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘Bool’
     • imported from ‘Prelude’ at T14627.hs:1:1
       (and originally defined in ‘GHC.Types’)
     • In the expression: Bool
diff --git a/testsuite/tests/th/T18740c.stderr b/testsuite/tests/th/T18740c.stderr
index 23631f31c4a00e403e360ca11efc47f5853fdeee..efc37f248b5a944dd9c9397dcdf697f0776835e5 100644
--- a/testsuite/tests/th/T18740c.stderr
+++ b/testsuite/tests/th/T18740c.stderr
@@ -1,5 +1,5 @@
 
-T18740c.hs:9:1: error: [GHC-31891]
+T18740c.hs:9:1: error: [GHC-01928]
     • Illegal term-level use of the type variable ‘a’
     • bound at T18740c.hs:9:1
     • In the expression: a
diff --git a/testsuite/tests/type-data/should_fail/TDExpression.stderr b/testsuite/tests/type-data/should_fail/TDExpression.stderr
index 354dac183fb299f7844eba4e263b91587fbb9145..08e1408d52b218dd21087ebae705871db1bde33e 100644
--- a/testsuite/tests/type-data/should_fail/TDExpression.stderr
+++ b/testsuite/tests/type-data/should_fail/TDExpression.stderr
@@ -1,6 +1,6 @@
 
-TDExpression.hs:7:5: [GHC-31891]
-     Illegal term-level use of the type constructor or class ‘Zero’
-     defined at TDExpression.hs:4:17
-     In the expression: Zero
+TDExpression.hs:7:5: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘Zero’
+    • defined at TDExpression.hs:4:17
+    • In the expression: Zero
       In an equation for ‘z’: z = Zero
diff --git a/testsuite/tests/typecheck/should_fail/T19978.stderr b/testsuite/tests/typecheck/should_fail/T19978.stderr
index 4328b1adda1f5be1b7055a2260a7003c6634700b..a17c6c6d957c7e92cc04cc4fefb0eb772d4bd16f 100644
--- a/testsuite/tests/typecheck/should_fail/T19978.stderr
+++ b/testsuite/tests/typecheck/should_fail/T19978.stderr
@@ -1,6 +1,6 @@
 
-T19978.hs:8:7: error: [GHC-31891]
-    • Illegal term-level use of the type constructor or class ‘Bool’
+T19978.hs:8:7: error: [GHC-01928]
+    • Illegal term-level use of the type constructor ‘Bool’
     • imported from ‘Prelude’ at T19978.hs:3:8-13
       (and originally defined in ‘GHC.Types’)
     • Perhaps use one of these:
@@ -12,7 +12,7 @@ T19978.hs:14:7: error: [GHC-88464]
     Data constructor not in scope: Let
     Suggested fix: Perhaps use ‘Left’ (imported from Prelude)
 
-T19978.hs:21:7: error: [GHC-31891]
+T19978.hs:21:7: error: [GHC-01928]
     • Illegal term-level use of the type variable ‘mytv’
     • bound at T19978.hs:20:15
     • Perhaps use one of these:
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_idv.hs b/testsuite/tests/vdq-rta/should_compile/T23739_idv.hs
new file mode 100644
index 0000000000000000000000000000000000000000..04dfd6b10658589f673abb276bfd9230238f8354
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_idv.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23739_idv where
+
+idv :: forall a -> a -> a
+idv t x = x :: t
+
+idv_bsig :: forall a -> a -> a
+idv_bsig t (x :: t) = x
+
+idv_lam :: forall a -> a -> a
+idv_lam = \t x -> x :: t
+
+idv_lam_bsig :: forall a -> a -> a
+idv_lam_bsig = \t (x :: t) -> x
+
+idv_eta :: forall a -> a -> a
+idv_eta = idv
+
+idv_t2t :: forall a -> a -> a
+idv_t2t t = idv t
+
+idv_vta :: forall a -> a -> a
+idv_vta t = id @t
+
+idv_sig :: forall a -> a -> a
+idv_sig t = id :: t -> t
+
+idv_wild :: forall a -> a -> a
+idv_wild _ x = x
+
+idv_wild_bsig :: forall a -> a -> a
+idv_wild_bsig (_ :: k) (x :: t) = x :: (t :: k)
+
+idv_sig_shuffle :: forall a -> a -> a
+idv_sig_shuffle (((t :: k1) :: k2) :: k3) x = x :: (((t :: k2) :: k1) :: k3)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_nested.hs b/testsuite/tests/vdq-rta/should_compile/T23739_nested.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ccb41b937519260c247158601bddc20474c2ed8b
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_nested.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23739_nested where
+
+import Data.Kind
+
+f :: forall a -> a -> a
+f ((type t) :: Type) x = x :: t
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_sig.hs b/testsuite/tests/vdq-rta/should_compile/T23739_sig.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b1b55794d8a6ef5810077d26cc4c9ac27b79e62c
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_sig.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T23739_sig where
+
+import Data.Kind
+import Data.Type.Bool
+import Data.Proxy
+
+data SBool b where
+  SFalse :: SBool False
+  STrue  :: SBool True
+
+class KnownBool b where
+  boolSing :: SBool b
+
+boolVal :: forall b -> KnownBool b => Bool
+boolVal b =
+  case boolSing @b of
+    SFalse -> False
+    STrue  -> True
+
+g :: forall b -> KnownBool b => If b Integer String
+g (b :: Bool) =
+  case boolSing @b of
+    SFalse -> "Hello"
+    STrue  -> 42
+
+type FromJust :: Maybe a -> a
+type family FromJust m where
+  FromJust (Just x) = x
+
+type KindOf :: k -> Type
+type KindOf (a :: k) = k
+
+h :: forall m -> Proxy (KindOf (FromJust m))
+h (m :: Maybe a) = Proxy @a
+
+hBool :: Proxy Bool
+hBool = h (Just True)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_sizeOf.hs b/testsuite/tests/vdq-rta/should_compile/T23739_sizeOf.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d560e4bce6b57f4121ab46ad7b8683b4273ff1af
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_sizeOf.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23739_sizeOf where
+
+import Foreign.Storable
+
+sizeOfVis :: forall a -> Storable a => Int
+sizeOfVis t = sizeOf (undefined :: t)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_symbolVal.hs b/testsuite/tests/vdq-rta/should_compile/T23739_symbolVal.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2c939e11040847d79318e1d6460d817dea5e3d95
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_symbolVal.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T23739_symbolVal where
+
+import Data.Kind
+import Data.Proxy
+import GHC.TypeLits
+
+-- Definition:
+symbolValVis :: forall s -> KnownSymbol s => String
+symbolValVis s = symbolVal (Proxy :: Proxy s)
+
+-- Usage:
+strHelloWorld = symbolValVis ("Hello, " `AppendSymbol` "World")
+
+-- Operator taking a term-level argument before a required type argument:
+(++.) :: String -> forall (s :: Symbol) -> KnownSymbol s => String
+s1 ++. s2 = s1 ++ symbolValVis s2
+infixr 5 ++.
+
+strTmPlusTy = "Tm" ++ "+" ++. "Ty"
+
+-------------------------------------------------
+--   Required type arguments in class methods  --
+--         and in higher-rank positions        --
+-------------------------------------------------
+
+-- Continuation-passing encoding of a list spine:
+--
+-- data Spine xs where
+--   Cons :: Spine xs -> Spine (x : xs)
+--   Nil :: Spine '[]
+--
+type WithSpine :: [k] -> Constraint
+class WithSpine xs where
+  onSpine ::
+    forall r.
+    forall xs' -> (xs' ~ xs) =>  -- workaround b/c it's not possible to make xs visible
+    ((xs ~ '[]) => r) ->
+    (forall y ys -> (xs ~ (y : ys)) => WithSpine ys => r) ->
+    r
+
+instance WithSpine '[] where
+  onSpine xs onNil _ = onNil
+
+instance forall x xs. WithSpine xs => WithSpine (x : xs) where
+  onSpine xs' _ onCons = onCons x xs
+
+type All :: (k -> Constraint) -> [k] -> Constraint
+type family All c xs where
+  All c '[] = ()
+  All c (a : as) = (c a, All c as)
+
+type KnownSymbols :: [Symbol] -> Constraint
+class All KnownSymbol ss => KnownSymbols ss
+instance All KnownSymbol ss => KnownSymbols ss
+
+symbolVals :: forall ss -> (KnownSymbols ss, WithSpine ss) => [String]
+symbolVals ss =
+  onSpine ss [] $ \s ss' ->
+    symbolValVis s : symbolVals ss'
+
+-- Reify a type-level list of strings at the term level.
+strsLoremIpsum = symbolVals ["lorem", "ipsum", "dolor", "sit", "amet"]
+
+-- Pass a required type argument to a continuation:
+withSymbolVis :: String -> (forall s -> KnownSymbol s => r) -> r
+withSymbolVis str cont =
+  case someSymbolVal str of
+    SomeSymbol (Proxy :: Proxy s) -> cont s
+
+-- Use a required type argument in a continuation:
+strLengthViaSymbol :: String -> Int
+strLengthViaSymbol str =
+  withSymbolVis str $ \s ->
+    length (symbolValVis s)
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.hs b/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a6a5eda0b0a441dee2e38182c30e9f6fa33899d4
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T23739_th_dump1 where
+
+$([d| f :: Integer -> forall a -> Num a => a
+      f n t = fromInteger n :: t
+    |])
+
+$([d| x = 42 `f` Double
+      n = f 42 Integer
+    |])
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.stderr b/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..891be2ac7482a175fa9754317bccc786677655e8
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_th_dump1.stderr
@@ -0,0 +1,12 @@
+T23739_th_dump1.hs:(6,2)-(8,7): Splicing declarations
+    [d| f :: Integer -> forall a -> Num a => a
+        f n t = fromInteger n :: t |]
+  ======>
+    f :: Integer -> forall a -> Num a => a
+    f n t = fromInteger n :: t
+T23739_th_dump1.hs:(10,2)-(12,7): Splicing declarations
+    [d| x = 42 `f` Double
+        n = f 42 Integer |]
+  ======>
+    x = (42 `f` Double)
+    n = f 42 Integer
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.hs b/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..58b8f1526297991eeb0cdd8067f6a9029ed7970a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE NoExplicitNamespaces #-}
+
+module T23739_th_pprint1 where
+
+import System.IO
+import Language.Haskell.TH
+
+do decls <-
+     [d|
+         f :: Integer -> forall a -> Num a => a
+         f n t = fromInteger @t n
+       |]
+   runIO $ hPutStrLn stderr $ pprint decls
+   return []
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.stderr b/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..34d100eb0fd4aa0579e91603e05d264fe8690e0f
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_th_pprint1.stderr
@@ -0,0 +1,3 @@
+f_0 :: GHC.Num.Integer.Integer ->
+       forall a_1 -> GHC.Num.Num a_1 => a_1
+f_0 n_2 t_3 = GHC.Num.fromInteger @t_3 n_2
diff --git a/testsuite/tests/vdq-rta/should_compile/T23739_typeRep.hs b/testsuite/tests/vdq-rta/should_compile/T23739_typeRep.hs
new file mode 100644
index 0000000000000000000000000000000000000000..a7287ab0563d246b95fcf8cdd14c4843e2f72118
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_compile/T23739_typeRep.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+
+module T23739_typeRep where
+
+import Type.Reflection
+import Data.Kind
+import GHC.TypeLits
+
+typeRepVis :: forall a -> Typeable a => TypeRep a
+typeRepVis t = typeRep @t
+
+typeRepVis_lam :: forall a -> Typeable a => TypeRep a
+typeRepVis_lam = \t -> typeRep @t
+
+typeRepVis_kforall :: forall k. forall (a :: k) -> Typeable a => TypeRep a
+typeRepVis_kforall = typeRepVis
+
+typeRepKiVis :: forall k (a :: k) -> Typeable a => TypeRep a
+typeRepKiVis k (a :: k) = typeRep @a
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_compile/all.T b/testsuite/tests/vdq-rta/should_compile/all.T
index 835d7f12fc012aaebcc5858124683f754ce147a0..55707f686ff2b11ac2e7748896f3ac11d7da7ec1 100644
--- a/testsuite/tests/vdq-rta/should_compile/all.T
+++ b/testsuite/tests/vdq-rta/should_compile/all.T
@@ -16,7 +16,15 @@ test('T23738_overlit', normal, compile, [''])
 test('T23738_nested', normal, compile, [''])
 test('T23738_wild', normal, compile, [''])
 test('T23738_sigforall', normal, compile, [''])
+test('T23739_idv', normal, compile, [''])
+test('T23739_sig', normal, compile, [''])
+test('T23739_sizeOf', normal, compile, [''])
+test('T23739_symbolVal', normal, compile, [''])
+test('T23739_typeRep', normal, compile, [''])
+test('T23739_nested', normal, compile, [''])
 
 test('T22326_th_dump1', req_th, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
+test('T23739_th_dump1', req_th, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T22326_th_pprint1', req_th, compile, [''])
+test('T23739_th_pprint1', req_th, compile, [''])
 test('T23738_th', req_th, compile, [''])
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs
index 2b8ca18a2eafa83e0fa6b0efe88973a4c812fad4..97aba2a08e7d64568209624e8fe37b51104238f4 100644
--- a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.hs
@@ -1,7 +1,6 @@
-{-# LANGUAGE ExplicitNamespaces #-}
 {-# LANGUAGE RequiredTypeArguments #-}
 
 module T22326_fail_raw_pat where
 
 f :: forall (a :: k) -> ()
-f x = ()
\ No newline at end of file
+f !x = ()
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr
index cae79feb09f417c1187c92fc2dd51c3dacb0021c..7cdc761f839a4cd45b045adaf23c0c24702a2e81 100644
--- a/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_raw_pat.stderr
@@ -1,5 +1,5 @@
 
-T22326_fail_raw_pat.hs:7:3: error: [GHC-88754]
-    • Ill-formed type pattern: x
-      Expected a type pattern introduced with the ‘type’ keyword.
-    • In an equation for ‘f’: f x = ()
+T22326_fail_raw_pat.hs:6:3: error: [GHC-88754]
+    • Ill-formed type pattern: !x
+    • In the pattern: !x
+      In an equation for ‘f’: f !x = ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.hs b/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.hs
new file mode 100644
index 0000000000000000000000000000000000000000..73329964ab1e529c3860daf71c56c0612a5e608d
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23739_fail_case where
+
+bad :: forall (b :: Bool) -> String
+bad t =
+  case t of
+    False -> "False"
+    True  -> "True"
\ No newline at end of file
diff --git a/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.stderr b/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..a75dd8fb51c921cfe55a79dab5f472392c4503ed
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T23739_fail_case.stderr
@@ -0,0 +1,14 @@
+
+T23739_fail_case.hs:7:8: error: [GHC-01928]
+    • Illegal term-level use of the type variable ‘t’
+    • bound at T23739_fail_case.hs:6:5
+    • In the expression: t
+      In the expression:
+        case t of
+          False -> "False"
+          True -> "True"
+      In an equation for ‘bad’:
+          bad t
+            = case t of
+                False -> "False"
+                True -> "True"
diff --git a/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.hs b/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.hs
new file mode 100644
index 0000000000000000000000000000000000000000..5997a35a312a375049527027beea58e693d1cd5a
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RequiredTypeArguments #-}
+
+module T23739_fail_ret where
+
+bad :: forall (a :: k) -> k
+bad t = t
diff --git a/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.stderr b/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..9c423136e9bc85c5d2049c6dd0f6e6039e1aa5dc
--- /dev/null
+++ b/testsuite/tests/vdq-rta/should_fail/T23739_fail_ret.stderr
@@ -0,0 +1,6 @@
+
+T23739_fail_ret.hs:6:9: error: [GHC-01928]
+    • Illegal term-level use of the type variable ‘t’
+    • bound at T23739_fail_ret.hs:6:5
+    • In the expression: t
+      In an equation for ‘bad’: bad t = t
diff --git a/testsuite/tests/vdq-rta/should_fail/all.T b/testsuite/tests/vdq-rta/should_fail/all.T
index 917a48be493d0ddb18936f9d50ba6a122d6a6ce4..f9cf1fe1ab60542acc2bc29b6a9851e7dcb44505 100644
--- a/testsuite/tests/vdq-rta/should_fail/all.T
+++ b/testsuite/tests/vdq-rta/should_fail/all.T
@@ -16,3 +16,5 @@ test('T23738_fail_wild', normal, compile_fail, [''])
 test('T23738_fail_implicit_tv', normal, compile_fail, [''])
 test('T23738_fail_var', normal, compile_fail, [''])
 test('T24176', normal, compile_fail, [''])
+test('T23739_fail_ret', normal, compile_fail, [''])
+test('T23739_fail_case', normal, compile_fail, [''])
\ No newline at end of file