From 2afbddb0f24df20cfc42279bb8695f91bbd3c1e0 Mon Sep 17 00:00:00 2001
From: Andrei Borzenkov <andreyborzenkov2002@gmail.com>
Date: Mon, 26 Jun 2023 19:12:08 +0400
Subject: [PATCH] Type patterns (#22478, #18986)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Improved name resolution and type checking of type patterns in constructors:

1. HsTyPat: a new dedicated data type that represents type patterns in
   HsConPatDetails instead of reusing HsPatSigType

2. rnHsTyPat: a new function that renames a type
   pattern and collects its binders into three groups:
    - explicitly bound type variables, excluding locally bound
      variables
    - implicitly bound type variables from kind signatures
      (only if ScopedTypeVariables are enabled)
    - named wildcards (only from kind signatures)
2a. rnHsPatSigTypeBindingVars: removed in favour of rnHsTyPat
2b. rnImplcitTvBndrs: removed because no longer needed

3. collect_pat: updated to collect type variable binders from type patterns
   (this means that types and terms use the same infrastructure to detect
   conflicting bindings, unused variables and name shadowing)
3a. CollVarTyVarBinders: a new CollectFlag constructor that enables
    collection of type variables

4. tcHsTyPat: a new function that typechecks type patterns, capable of
   handling polymorphic kinds.
   See Note [Type patterns: binders and unifiers]

Examples of code that is now accepted:

   f = \(P @a) -> \(P @a) -> ...  -- triggers -Wname-shadowing

   g :: forall a. Proxy a -> ...
   g (P @a) = ...                 -- also triggers -Wname-shadowing

   h (P @($(TH.varT (TH.mkName "t")))) = ...
                                  -- t is bound at splice time

   j (P @(a :: (x,x))) = ...      -- (x,x) is no longer rejected

   data T where
     MkT :: forall (f :: forall k. k -> Type).
       f Int -> f Maybe -> T
   k :: T -> ()
   k (MkT @f (x :: f Int) (y :: f Maybe)) = ()
                                  -- f :: forall k. k -> Type

Examples of code that is rejected with better error messages:

  f (Left @a @a _) = ...
  -- new message:
  --     • Conflicting definitions for ‘a’
  --       Bound at: Test.hs:1:11
  --                 Test.hs:1:14

Examples of code that is now rejected:

  {-# OPTIONS_GHC -Werror=unused-matches #-}
  f (P @a) = ()
  -- Defined but not used: type variable ‘a’
---
 compiler/GHC/Hs/Decls.hs                      |   4 +-
 compiler/GHC/Hs/Instances.hs                  |   5 +
 compiler/GHC/Hs/Pat.hs                        |   4 +-
 compiler/GHC/Hs/Type.hs                       |  38 +-
 compiler/GHC/Hs/Utils.hs                      |  32 +-
 compiler/GHC/HsToCore/Quote.hs                |   2 +-
 compiler/GHC/Iface/Ext/Ast.hs                 |  14 +-
 compiler/GHC/Parser/PostProcess.hs            |   2 +-
 compiler/GHC/Parser/Types.hs                  |   2 +-
 compiler/GHC/Rename/HsType.hs                 | 150 ++----
 compiler/GHC/Rename/Pat.hs                    | 428 +++++++++++++++++-
 compiler/GHC/Rename/Splice.hs                 |  22 +-
 compiler/GHC/Rename/Splice.hs-boot            |   2 +
 compiler/GHC/Rename/Utils.hs                  |  10 +-
 compiler/GHC/Tc/Errors/Ppr.hs                 |  23 +-
 compiler/GHC/Tc/Errors/Types.hs               |  29 +-
 compiler/GHC/Tc/Gen/HsType.hs                 | 191 +++++++-
 compiler/GHC/Tc/Gen/Pat.hs                    |   7 +-
 compiler/GHC/Tc/TyCl.hs                       |   2 +-
 compiler/GHC/Tc/TyCl/Instance.hs              |   3 +-
 compiler/GHC/Tc/Utils/TcMType.hs              |   8 +-
 compiler/GHC/ThToHs.hs                        |   4 +-
 compiler/GHC/Types/Error/Codes.hs             |   4 +-
 compiler/GHC/Types/Name/Reader.hs             |   6 +-
 compiler/Language/Haskell/Syntax/Decls.hs     |  12 +-
 compiler/Language/Haskell/Syntax/Extension.hs |   5 +
 compiler/Language/Haskell/Syntax/Pat.hs       |   9 +-
 compiler/Language/Haskell/Syntax/Type.hs      |  11 +-
 testsuite/tests/gadt/T18191.stderr            |   6 +-
 .../tests/rename/should_compile/T22478a.hs    |  83 ++++
 testsuite/tests/rename/should_compile/all.T   |   1 +
 testsuite/tests/rename/should_fail/T22478b.hs |  27 ++
 .../tests/rename/should_fail/T22478b.stderr   |  48 ++
 testsuite/tests/rename/should_fail/T22478d.hs |  14 +
 .../tests/rename/should_fail/T22478d.stderr   |   8 +
 testsuite/tests/rename/should_fail/T22478e.hs |  12 +
 .../tests/rename/should_fail/T22478e.stderr   |  29 ++
 testsuite/tests/rename/should_fail/T22478f.hs |   9 +
 .../tests/rename/should_fail/T22478f.stderr   |   8 +
 .../tests/rename/should_fail/T7943.stderr     |   3 +-
 .../tests/rename/should_fail/T9077.stderr     |   4 +-
 testsuite/tests/rename/should_fail/all.T      |   4 +
 .../tests/typecheck/should_compile/T18986a.hs |  22 +
 .../tests/typecheck/should_compile/T18986b.hs |  40 ++
 .../tests/typecheck/should_compile/all.T      |   3 +-
 .../tests/typecheck/should_fail/T22478c.hs    |  11 +
 .../typecheck/should_fail/T22478c.stderr      |  19 +
 .../TyAppPat_NonlinearMultiAppPat.stderr      |   8 +-
 .../TyAppPat_NonlinearMultiPat.stderr         |  32 +-
 .../TyAppPat_NonlinearSinglePat.stderr        |   7 +-
 .../TyAppPat_ScopedTyVarConflict.hs           |   1 +
 .../TyAppPat_ScopedTyVarConflict.stderr       |  12 +-
 testsuite/tests/typecheck/should_fail/all.T   |   1 +
 utils/check-exact/ExactPrint.hs               |  16 +-
 54 files changed, 1203 insertions(+), 254 deletions(-)
 create mode 100644 testsuite/tests/rename/should_compile/T22478a.hs
 create mode 100644 testsuite/tests/rename/should_fail/T22478b.hs
 create mode 100644 testsuite/tests/rename/should_fail/T22478b.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T22478d.hs
 create mode 100644 testsuite/tests/rename/should_fail/T22478d.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T22478e.hs
 create mode 100644 testsuite/tests/rename/should_fail/T22478e.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T22478f.hs
 create mode 100644 testsuite/tests/rename/should_fail/T22478f.stderr
 create mode 100644 testsuite/tests/typecheck/should_compile/T18986a.hs
 create mode 100644 testsuite/tests/typecheck/should_compile/T18986b.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T22478c.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T22478c.stderr

diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index 07bcba6cc436..2e469e8fe55e 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -49,7 +49,7 @@ module GHC.Hs.Decls (
   TyFamDefltDecl, LTyFamDefltDecl,
   DataFamInstDecl(..), LDataFamInstDecl,
   pprDataFamInstFlavour, pprTyFamInstDecl, pprHsFamInstLHS,
-  FamEqn(..), TyFamInstEqn, LTyFamInstEqn, HsTyPats,
+  FamEqn(..), TyFamInstEqn, LTyFamInstEqn, HsFamEqnPats,
   LClsInstDecl, ClsInstDecl(..),
 
   -- ** Standalone deriving declarations
@@ -867,7 +867,7 @@ pprDataFamInstFlavour DataFamInstDecl
 pprHsFamInstLHS :: (OutputableBndrId p)
    => IdP (GhcPass p)
    -> HsOuterFamEqnTyVarBndrs (GhcPass p)
-   -> HsTyPats (GhcPass p)
+   -> HsFamEqnPats (GhcPass p)
    -> LexicalFixity
    -> Maybe (LHsContext (GhcPass p))
    -> SDoc
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 441b290cbbe5..54bbbd098593 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -488,6 +488,11 @@ deriving instance Data (HsPatSigType GhcPs)
 deriving instance Data (HsPatSigType GhcRn)
 deriving instance Data (HsPatSigType GhcTc)
 
+-- deriving instance (DataIdLR p p) => Data (HsTyPat p)
+deriving instance Data (HsTyPat GhcPs)
+deriving instance Data (HsTyPat GhcRn)
+deriving instance Data (HsTyPat GhcTc)
+
 -- deriving instance (DataIdLR p p) => Data (HsForAllTelescope p)
 deriving instance Data (HsForAllTelescope GhcPs)
 deriving instance Data (HsForAllTelescope GhcRn)
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index a6a7fbd3e66a..78306bd24a32 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -28,7 +28,7 @@ module GHC.Hs.Pat (
         HsPatExpansion(..),
         XXPatGhcTc(..),
 
-        HsConPatDetails, hsConPatArgs,
+        HsConPatDetails, hsConPatArgs, hsConPatTyArgs,
         HsConPatTyArg(..),
         HsRecFields(..), HsFieldBind(..), LHsFieldBind,
         HsRecField, LHsRecField,
@@ -260,7 +260,7 @@ hsRecUpdFieldOcc = fmap unambiguousFieldOcc . hfbLHS
 ************************************************************************
 -}
 
-instance Outputable (HsPatSigType p) => Outputable (HsConPatTyArg p) where
+instance Outputable (HsTyPat p) => Outputable (HsConPatTyArg p) where
   ppr (HsConPatTyArg _ ty) = char '@' <> ppr ty
 
 instance (Outputable arg, Outputable (XRec p (HsRecField p arg)), XRec p RecFieldsDotDot ~ Located RecFieldsDotDot)
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 595bfe5326c8..5368dd75625a 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -37,6 +37,7 @@ module GHC.Hs.Type (
         HsOuterTyVarBndrs(..), HsOuterFamEqnTyVarBndrs, HsOuterSigTyVarBndrs,
         HsWildCardBndrs(..),
         HsPatSigType(..), HsPSRn(..),
+        HsTyPat(..), HsTyPatRn(..),
         HsSigType(..), LHsSigType, LHsSigWcType, LHsWcType,
         HsTupleSort(..),
         HsContext, LHsContext, fromMaybeContext,
@@ -68,14 +69,15 @@ module GHC.Hs.Type (
         hsOuterTyVarNames, hsOuterExplicitBndrs, mapHsOuterImplicit,
         mkHsOuterImplicit, mkHsOuterExplicit,
         mkHsImplicitSigType, mkHsExplicitSigType,
-        mkHsWildCardBndrs, mkHsPatSigType,
+        mkHsWildCardBndrs, mkHsPatSigType, mkHsTyPat,
         mkEmptyWildCardBndrs,
         mkHsForAllVisTele, mkHsForAllInvisTele,
         mkHsQTvs, hsQTvExplicit, emptyLHsQTvs,
         isHsKindedTyVar, hsTvbAllKinded,
         hsScopedTvs, hsScopedKvs, hsWcScopedTvs, dropWildCards,
         hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
-        hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
+        hsLTyVarName, hsLTyVarNames, hsForAllTelescopeNames,
+        hsLTyVarLocName, hsExplicitLTyVarNames,
         splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
         splitLHsForAllTyInvis, splitLHsForAllTyInvis_KP, splitLHsQualTy,
@@ -218,6 +220,10 @@ type instance XHsPS GhcPs = EpAnnCO
 type instance XHsPS GhcRn = HsPSRn
 type instance XHsPS GhcTc = HsPSRn
 
+type instance XHsTP GhcPs = EpAnnCO
+type instance XHsTP GhcRn = HsTyPatRn
+type instance XHsTP GhcTc = DataConCantHappen
+
 -- | The extension field for 'HsPatSigType', which is only used in the
 -- renamer onwards. See @Note [Pattern signature binders and scoping]@.
 data HsPSRn = HsPSRn
@@ -226,7 +232,22 @@ data HsPSRn = HsPSRn
   }
   deriving Data
 
+-- HsTyPatRn is the extension field for `HsTyPat`, after renaming
+-- E.g. pattern K @(Maybe (_x, a, b::Proxy k)
+-- In the type pattern @(Maybe ...):
+--    '_x' is a named wildcard
+--    'a'  is explicitly bound
+--    'k'  is implicitly bound
+-- See Note [Implicit and explicit type variable binders] in GHC.Rename.Pat
+data HsTyPatRn = HsTPRn
+  { hstp_nwcs    :: [Name] -- ^ Wildcard names
+  , hstp_imp_tvs :: [Name] -- ^ Implicitly bound variable names
+  , hstp_exp_tvs :: [Name] -- ^ Explicitly bound variable names
+  }
+  deriving Data
+
 type instance XXHsPatSigType (GhcPass _) = DataConCantHappen
+type instance XXHsTyPat      (GhcPass _) = DataConCantHappen
 
 type instance XHsSig (GhcPass _) = NoExtField
 type instance XXHsSigType (GhcPass _) = DataConCantHappen
@@ -275,6 +296,10 @@ mkHsPatSigType :: EpAnnCO -> LHsType GhcPs -> HsPatSigType GhcPs
 mkHsPatSigType ann x = HsPS { hsps_ext  = ann
                             , hsps_body = x }
 
+mkHsTyPat :: EpAnnCO -> LHsType GhcPs -> HsTyPat GhcPs
+mkHsTyPat ann x = HsTP { hstp_ext  = ann
+                       , hstp_body = x }
+
 mkEmptyWildCardBndrs :: thing -> HsWildCardBndrs GhcRn thing
 mkEmptyWildCardBndrs x = HsWC { hswc_body = x
                               , hswc_ext  = [] }
@@ -449,6 +474,10 @@ hsLTyVarName = hsTyVarName . unLoc
 hsLTyVarNames :: [LHsTyVarBndr flag (GhcPass p)] -> [IdP (GhcPass p)]
 hsLTyVarNames = map hsLTyVarName
 
+hsForAllTelescopeNames :: HsForAllTelescope (GhcPass p) -> [IdP (GhcPass p)]
+hsForAllTelescopeNames (HsForAllVis _ bndrs) = hsLTyVarNames bndrs
+hsForAllTelescopeNames (HsForAllInvis _ bndrs) = hsLTyVarNames bndrs
+
 hsExplicitLTyVarNames :: LHsQTyVars (GhcPass p) -> [IdP (GhcPass p)]
 -- Explicit variables only
 hsExplicitLTyVarNames qtvs = map hsLTyVarName (hsQTvExplicit qtvs)
@@ -1061,6 +1090,11 @@ instance (OutputableBndrId p)
     ppr (HsPS { hsps_body = ty }) = ppr ty
 
 
+instance (OutputableBndrId p)
+       => Outputable (HsTyPat (GhcPass p)) where
+    ppr (HsTP { hstp_body = ty }) = ppr ty
+
+
 instance (OutputableBndrId p)
        => Outputable (HsTyLit (GhcPass p)) where
     ppr = ppr_tylit
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index a81ded653383..809278d47431 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -1184,11 +1184,16 @@ collectPatsBinders flag pats = foldr (collect_lpat flag) [] pats
 
 -------------
 
--- | Indicate if evidence binders have to be collected.
+-- | Indicate if evidence binders and type variable binders have
+--   to be collected.
 --
--- This type is used as a boolean (should we collect evidence binders or not?)
--- but also to pass an evidence that the AST has been typechecked when we do
--- want to collect evidence binders, otherwise these binders are not available.
+-- This type enumerates the modes of collecting bound variables
+--                     | evidence |   type    |   term    |  ghc  |
+--                     | binders  | variables | variables |  pass |
+--                     --------------------------------------------
+-- CollNoDictBinders   |  no      |    no     |    yes    |  any  |
+-- CollWithDictBinders |  yes     |    no     |    yes    | GhcTc |
+-- CollVarTyVarBinders |  no      |    yes    |    yes    | GhcRn |
 --
 -- See Note [Dictionary binders in ConPatOut]
 data CollectFlag p where
@@ -1196,6 +1201,9 @@ data CollectFlag p where
     CollNoDictBinders   :: CollectFlag p
     -- | Collect evidence binders
     CollWithDictBinders :: CollectFlag GhcTc
+    -- | Collect variable and type variable binders, but no evidence binders
+    CollVarTyVarBinders :: CollectFlag GhcRn
+
 
 collect_lpat :: forall p. CollectPass p
              => CollectFlag p
@@ -1223,7 +1231,10 @@ collect_pat flag pat bndrs = case pat of
   LitPat _ _            -> bndrs
   NPat {}               -> bndrs
   NPlusKPat _ n _ _ _ _ -> unXRec @p n : bndrs
-  SigPat _ pat _        -> collect_lpat flag pat bndrs
+  SigPat _ pat sig      -> case flag of
+    CollVarTyVarBinders -> collect_lpat flag pat bndrs
+                            ++ collectPatSigBndrs sig
+    _                   -> collect_lpat flag pat bndrs
   XPat ext              -> collectXXPat @p flag ext bndrs
   SplicePat ext _       -> collectXSplicePat @p flag ext bndrs
   -- See Note [Dictionary binders in ConPatOut]
@@ -1231,11 +1242,22 @@ collect_pat flag pat bndrs = case pat of
     CollNoDictBinders   -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
     CollWithDictBinders -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
                            ++ collectEvBinders (cpt_binds (pat_con_ext pat))
+    CollVarTyVarBinders -> foldr (collect_lpat flag) bndrs (hsConPatArgs ps)
+                           ++ concatMap collectConPatTyArgBndrs (hsConPatTyArgs ps)
 
 collectEvBinders :: TcEvBinds -> [Id]
 collectEvBinders (EvBinds bs)   = foldr add_ev_bndr [] bs
 collectEvBinders (TcEvBinds {}) = panic "ToDo: collectEvBinders"
 
+collectConPatTyArgBndrs :: HsConPatTyArg GhcRn -> [Name]
+collectConPatTyArgBndrs (HsConPatTyArg _ tp) = collectTyPatBndrs tp
+
+collectTyPatBndrs :: HsTyPat GhcRn -> [Name]
+collectTyPatBndrs (HsTP (HsTPRn nwcs imp_tvs exp_tvs) _) = nwcs ++ imp_tvs ++ exp_tvs
+
+collectPatSigBndrs :: HsPatSigType GhcRn -> [Name]
+collectPatSigBndrs (HsPS (HsPSRn nwcs imp_tvs) _) = nwcs ++ imp_tvs
+
 add_ev_bndr :: EvBind -> [Id] -> [Id]
 add_ev_bndr (EvBind { eb_lhs = b }) bs | isId b    = b:bs
                                        | otherwise = bs
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index dc3dc2c96e79..69db68f8652b 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -2095,7 +2095,7 @@ repP (ConPat NoExtField dc details)
  = do { con_str <- lookupLOcc dc
       ; case details of
          PrefixCon tyargs ps -> do { qs <- repLPs ps
-                                   ; let unwrapTyArg (HsConPatTyArg _ t) = unLoc (hsps_body t)
+                                   ; let unwrapTyArg (HsConPatTyArg _ t) = unLoc (hstp_body t)
                                    ; ts <- repListM typeTyConName (repTy . unwrapTyArg) tyargs
                                    ; repPcon con_str ts qs }
          RecCon rec   -> do { fps <- repListM fieldPatTyConName rep_fld (rec_flds rec)
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index cd055de481ad..3a7b8452aa53 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -507,11 +507,11 @@ taScopes
   :: Scope
   -> Scope
   -> [HsConPatTyArg (GhcPass a)]
-  -> [TScoped (HsPatSigType (GhcPass a))]
+  -> [TScoped (HsTyPat (GhcPass a))]
 taScopes scope rhsScope xs =
   map (\(RS sc a) -> TS (ResolvedScopes [scope, sc]) (unLoc a)) $
-    listScopes rhsScope (map (\(HsConPatTyArg _ hsps) -> L (getLoc $ hsps_body hsps) hsps) xs)
-  -- We make the HsPatSigType into a Located one by using the location of the underlying LHsType.
+    listScopes rhsScope (map (\(HsConPatTyArg _ hstp) -> L (getLoc $ hstp_body hstp) hstp) xs)
+  -- We make the HsTyPat into a Located one by using the location of the underlying LHsType.
   -- We then strip off the redundant location information afterward, and take the union of the given scope and those to the right when forming the TS.
 
 -- | 'listScopes' specialised to 'TVScoped' things
@@ -1039,7 +1039,7 @@ instance HiePass p => ToHie (PScoped (LocatedA (Pat (GhcPass p)))) where
             ExpansionPat _ p -> [ toHie $ PS rsp scope pscope (L ospan p) ]
     where
       contextify :: a ~ LPat (GhcPass p) => HsConDetails (HsConPatTyArg GhcRn) a (HsRecFields (GhcPass p) a)
-                 -> HsConDetails (TScoped (HsPatSigType GhcRn)) (PScoped a) (RContext (HsRecFields (GhcPass p) (PScoped a)))
+                 -> HsConDetails (TScoped (HsTyPat GhcRn)) (PScoped a) (RContext (HsRecFields (GhcPass p) (PScoped a)))
       contextify (PrefixCon tyargs args) =
         PrefixCon (taScopes scope argscope tyargs)
                   (patScopes rsp scope pscope args)
@@ -1062,6 +1062,12 @@ instance ToHie (TScoped (HsPatSigType GhcRn)) where
       ]
   -- See Note [Scoping Rules for SigPat]
 
+instance ToHie (TScoped (HsTyPat GhcRn)) where
+  toHie (TS sc (HsTP (HsTPRn wcs imp_tvs exp_tvs) body@(L span _))) = concatM $
+      [ bindingsOnly $ map (C $ TyVarBind (mkScopeA span) sc) (wcs ++ imp_tvs ++ exp_tvs)
+      , toHie body
+      ]
+
 instance ( ToHie (LocatedA (body (GhcPass p)))
          , HiePass p
          , AnnoBody p body
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index d37744ab4136..8c665027e518 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -1838,7 +1838,7 @@ instance DisambECP (PatBuilder GhcPs) where
   mkHsAppTypePV l p at t = do
     cs <- getCommentsFor (locA l)
     let anns = EpAnn (spanAsAnchor (getLocA t)) NoEpAnns cs
-    return $ L l (PatBuilderAppType p at (mkHsPatSigType anns t))
+    return $ L l (PatBuilderAppType p at (mkHsTyPat anns t))
   mkHsIfPV l _ _ _ _ _ _ = addFatalError $ mkPlainErrorMsgEnvelope l PsErrIfThenElseInPat
   mkHsDoPV l _ _ _       = addFatalError $ mkPlainErrorMsgEnvelope l PsErrDoNotationInPat
   mkHsParPV l lpar p rpar   = return $ L (noAnnSrcSpan l) (PatBuilderPar lpar p rpar)
diff --git a/compiler/GHC/Parser/Types.hs b/compiler/GHC/Parser/Types.hs
index 2e38c22f692b..779062bca82e 100644
--- a/compiler/GHC/Parser/Types.hs
+++ b/compiler/GHC/Parser/Types.hs
@@ -55,7 +55,7 @@ data PatBuilder p
   = PatBuilderPat (Pat p)
   | PatBuilderPar (LHsToken "(" p) (LocatedA (PatBuilder p)) (LHsToken ")" p)
   | PatBuilderApp (LocatedA (PatBuilder p)) (LocatedA (PatBuilder p))
-  | PatBuilderAppType (LocatedA (PatBuilder p)) (LHsToken "@" p) (HsPatSigType GhcPs)
+  | PatBuilderAppType (LocatedA (PatBuilder p)) (LHsToken "@" p) (HsTyPat GhcPs)
   | PatBuilderOpApp (LocatedA (PatBuilder p)) (LocatedN RdrName)
                     (LocatedA (PatBuilder p)) (EpAnn [AddEpAnn])
   | PatBuilderVar (LocatedN RdrName)
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 39d9f21f14c7..f88bc1e7afd8 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -14,11 +14,11 @@ module GHC.Rename.HsType (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext, rnMaybeContext,
         rnLHsKind, rnLHsTypeArgs,
-        rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
-        HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
+        rnHsSigType, rnHsWcType, rnHsTyLit,
+        HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType, rnHsPatSigKind,
         newTyVarNameRn,
         rnConDeclFields,
-        lookupField,
+        lookupField, mkHsOpTyRn,
         rnLTyVar,
 
         rnScaledLHsType,
@@ -37,7 +37,9 @@ module GHC.Rename.HsType (
         extractHsTysRdrTyVars, extractRdrKindSigVars,
         extractConDeclGADTDetailsTyVars, extractDataDefnKindVars,
         extractHsOuterTvBndrs, extractHsTyArgRdrKiTyVars,
-        nubL, nubN
+        nubL, nubN,
+        -- Error helpers
+        badKindSigErr
   ) where
 
 import GHC.Prelude
@@ -79,8 +81,6 @@ import qualified GHC.LanguageExtensions as LangExt
 import Language.Haskell.Syntax.Basic (FieldLabelString(..))
 
 import Data.List (nubBy, partition)
-import qualified Data.List.NonEmpty as NE
-import Data.List.NonEmpty (NonEmpty(..))
 import Control.Monad
 
 {-
@@ -138,7 +138,7 @@ rnHsSigWcType doc (HsWC { hswc_body =
        ; (nwc_rdrs', imp_tv_nms) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
        ; bindHsOuterTyVarBndrs doc Nothing imp_tv_nms outer_bndrs $ \outer_bndrs' ->
-    do { (wcs, body_ty', fvs) <- rnWcBody doc nwc_rdrs body_ty
+    do { (wcs, body_ty', fvs) <- rnWcBodyType doc nwc_rdrs body_ty
        ; pure ( HsWC  { hswc_ext = wcs, hswc_body = L loc $
                 HsSig { sig_ext = noExtField
                       , sig_bndrs = outer_bndrs', sig_body = body_ty' }}
@@ -149,6 +149,21 @@ rnHsPatSigType :: HsPatSigTypeScoping
                -> HsPatSigType GhcPs
                -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
                -> RnM (a, FreeVars)
+rnHsPatSigType = rnHsPatSigTyKi TypeLevel
+
+rnHsPatSigKind :: HsPatSigTypeScoping
+               -> HsDocContext
+               -> HsPatSigType GhcPs
+               -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
+               -> RnM (a, FreeVars)
+rnHsPatSigKind = rnHsPatSigTyKi KindLevel
+
+rnHsPatSigTyKi :: TypeOrKind
+               -> HsPatSigTypeScoping
+               -> HsDocContext
+               -> HsPatSigType GhcPs
+               -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
+               -> RnM (a, FreeVars)
 -- Used for
 --   - Pattern type signatures, which are only allowed with ScopedTypeVariables
 --   - Signatures on binders in a RULE, which are allowed even if
@@ -156,7 +171,7 @@ rnHsPatSigType :: HsPatSigTypeScoping
 -- Wildcards are allowed
 --
 -- See Note [Pattern signature binders and scoping] in GHC.Hs.Type
-rnHsPatSigType scoping ctx sig_ty thing_inside
+rnHsPatSigTyKi level scoping ctx sig_ty thing_inside
   = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
        ; checkErr ty_sig_okay (unexpectedPatSigTypeErr sig_ty)
        ; free_vars <- filterInScopeM (extractHsTyRdrTyVars pat_sig_ty)
@@ -166,7 +181,7 @@ rnHsPatSigType scoping ctx sig_ty thing_inside
                AlwaysBind -> tv_rdrs
                NeverBind  -> []
        ; rnImplicitTvOccs Nothing implicit_bndrs $ \ imp_tvs ->
-    do { (nwcs, pat_sig_ty', fvs1) <- rnWcBody ctx nwc_rdrs pat_sig_ty
+    do { (nwcs, pat_sig_ty', fvs1) <- rnWcBodyTyKi level ctx nwc_rdrs pat_sig_ty
        ; let sig_names = HsPSRn { hsps_nwcs = nwcs, hsps_imp_tvs = imp_tvs }
              sig_ty'   = HsPS { hsps_ext = sig_names, hsps_body = pat_sig_ty' }
        ; (res, fvs2) <- thing_inside sig_ty'
@@ -179,59 +194,20 @@ rnHsWcType ctxt (HsWC { hswc_body = hs_ty })
   = do { free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
        ; (nwc_rdrs', _) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
-       ; (wcs, hs_ty', fvs) <- rnWcBody ctxt nwc_rdrs hs_ty
+       ; (wcs, hs_ty', fvs) <- rnWcBodyType ctxt nwc_rdrs hs_ty
        ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = hs_ty' }
        ; return (sig_ty', fvs) }
 
--- Similar to rnHsWcType, but rather than requiring free variables in the type to
--- already be in scope, we are going to require them not to be in scope,
--- and we bind them.
-rnHsPatSigTypeBindingVars :: HsDocContext
-                          -> HsPatSigType GhcPs
-                          -> (HsPatSigType GhcRn -> RnM (r, FreeVars))
-                          -> RnM (r, FreeVars)
-rnHsPatSigTypeBindingVars ctxt sigType thing_inside = case sigType of
-  (HsPS { hsps_body = hs_ty }) -> do
-    rdr_env <- getLocalRdrEnv
-    let (varsInScope, varsNotInScope) =
-          partition (inScope rdr_env . unLoc) (extractHsTyRdrTyVars hs_ty)
-    -- TODO: Resolve and remove this comment.
-    -- This next bit is in some contention. The original proposal #126
-    -- (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0126-type-applications-in-patterns.rst)
-    -- says that in-scope variables are fine here: don't bind them, just use
-    -- the existing vars, like in type signatures. An amendment #291
-    -- (https://github.com/ghc-proposals/ghc-proposals/pull/291) says that the
-    -- use of an in-scope variable should *shadow* an in-scope tyvar, like in
-    -- terms. In an effort to make forward progress, the current implementation
-    -- just rejects any use of an in-scope variable, meaning GHC will accept
-    -- a subset of programs common to both variants. If this comment still exists
-    -- in mid-to-late 2021 or thereafter, we have done a poor job on following
-    -- up on this point.
-    -- Example:
-    --   f :: forall a. ...
-    --   f (MkT @a ...) = ...
-    -- Should the inner `a` refer to the outer one? shadow it? We are, as yet, undecided,
-    -- so we currently reject.
-    when (not (null varsInScope)) $
-      addErr $ TcRnBindVarAlreadyInScope varsInScope
-    (wcVars, ibVars) <- partition_nwcs varsNotInScope
-    rnImplicitTvBndrs ctxt Nothing ibVars $ \ ibVars' -> do
-      (wcVars', hs_ty', fvs) <- rnWcBody ctxt wcVars hs_ty
-      let sig_ty = HsPS
-            { hsps_body = hs_ty'
-            , hsps_ext = HsPSRn
-              { hsps_nwcs    = wcVars'
-              , hsps_imp_tvs = ibVars'
-              }
-            }
-      (res, fvs') <- thing_inside sig_ty
-      return (res, fvs `plusFV` fvs')
-
-rnWcBody :: HsDocContext -> [LocatedN RdrName] -> LHsType GhcPs
+
+rnWcBodyType :: HsDocContext -> [LocatedN RdrName] -> LHsType GhcPs
+  -> RnM ([Name], LHsType GhcRn, FreeVars)
+rnWcBodyType = rnWcBodyTyKi TypeLevel
+
+rnWcBodyTyKi :: TypeOrKind -> HsDocContext -> [LocatedN RdrName] -> LHsType GhcPs
          -> RnM ([Name], LHsType GhcRn, FreeVars)
-rnWcBody ctxt nwc_rdrs hs_ty
+rnWcBodyTyKi level ctxt nwc_rdrs hs_ty
   = do { nwcs <- mapM newLocalBndrRn nwc_rdrs
-       ; let env = RTKE { rtke_level = TypeLevel
+       ; let env = RTKE { rtke_level = level
                         , rtke_what  = RnTypeBody
                         , rtke_nwcs  = mkNameSet nwcs
                         , rtke_ctxt  = ctxt }
@@ -422,32 +398,6 @@ type signature, since the type signature implicitly carries their binding
 sites. This is less precise, but more accurate.
 -}
 
--- | Create fresh type variables for binders, disallowing multiple occurrences of the same variable. Similar to `rnImplicitTvOccs` except that duplicate occurrences will
--- result in an error, and the source locations of the variables are not adjusted, as these variable occurrences are themselves the binding sites for the type variables,
--- rather than the variables being implicitly bound by a signature.
-rnImplicitTvBndrs :: HsDocContext
-                  -> Maybe assoc
-                  -- ^ @'Just' _@ => an associated type decl
-                  -> FreeKiTyVars
-                  -- ^ Surface-syntax free vars that we will implicitly bind.
-                  -- Duplicate variables will cause a compile-time error regarding repeated bindings.
-                  -> ([Name] -> RnM (a, FreeVars))
-                  -> RnM (a, FreeVars)
-rnImplicitTvBndrs ctx mb_assoc implicit_vs_with_dups thing_inside
-  = do { implicit_vs <- forM (NE.groupAllWith unLoc $ implicit_vs_with_dups) $ \case
-           (x :| []) -> return x
-           (x :| _) -> do
-             addErr $ TcRnBindMultipleVariables ctx x
-             return x
-
-       ; traceRn "rnImplicitTvBndrs" $
-         vcat [ ppr implicit_vs_with_dups, ppr implicit_vs ]
-
-       ; vars <- mapM (newTyVarNameRn mb_assoc) implicit_vs
-
-       ; bindLocalNamesFV vars $
-         thing_inside vars }
-
 {- ******************************************************
 *                                                       *
            LHsType and HsType
@@ -616,17 +566,19 @@ rnHsTyKi env ty@(HsRecTy _ flds)
        ; (flds', fvs) <- rnConDeclFields ctxt fls flds
        ; return (HsRecTy noExtField flds', fvs) }
   where
-    get_fields (ConDeclCtx names)
+    get_fields ctxt@(ConDeclCtx names)
       = do res <- concatMapM (lookupConstructorFields . unLoc) names
            if equalLength res names
            -- Lookup can fail when the record syntax is incorrect, e.g.
            -- data D = D Int { fld :: Bool }. See T7943.
            then return res
-           else err
-    get_fields _ = err
+           else err ctxt
+    get_fields ctxt = err ctxt
 
-    err =
-      do { addErr $ TcRnIllegalRecordSyntax (Left ty)
+    err ctxt =
+      do { addErr $
+            TcRnWithHsDocContext ctxt $
+            TcRnIllegalRecordSyntax (Left ty)
          ; return [] }
 
 rnHsTyKi env (HsFunTy u mult ty1 ty2)
@@ -645,7 +597,7 @@ rnHsTyKi env listTy@(HsListTy x ty)
 
 rnHsTyKi env (HsKindSig x ty k)
   = do { kind_sigs_ok <- xoptM LangExt.KindSignatures
-       ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
+       ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) k)
        ; (k', sig_fvs)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
        ; (ty', lhs_fvs) <- bindSigTyVarsFV (hsScopedKvs k') $
                            rnLHsTyKi env ty
@@ -671,13 +623,8 @@ rnHsTyKi env sumTy@(HsSumTy x tys)
 rnHsTyKi env tyLit@(HsTyLit src t)
   = do { data_kinds <- xoptM LangExt.DataKinds
        ; unless data_kinds (addErr (dataKindsErr env tyLit))
-       ; when (negLit t) (addErr $ TcRnNegativeNumTypeLiteral tyLit)
-       ; return (HsTyLit src (rnHsTyLit t), emptyFVs) }
-  where
-    negLit :: HsTyLit (GhcPass p) -> Bool
-    negLit (HsStrTy _ _) = False
-    negLit (HsNumTy _ i) = i < 0
-    negLit (HsCharTy _ _) = False
+       ; t' <- rnHsTyLit t
+       ; return (HsTyLit src t', emptyFVs) }
 
 rnHsTyKi env (HsAppTy _ ty1 ty2)
   = do { (ty1', fvs1) <- rnLHsTyKi env ty1
@@ -742,10 +689,13 @@ rnHsTyKi env (HsWildCardTy _)
        ; return (HsWildCardTy noExtField, emptyFVs) }
 
 
-rnHsTyLit :: HsTyLit GhcPs -> HsTyLit GhcRn
-rnHsTyLit (HsStrTy x s) = HsStrTy x s
-rnHsTyLit (HsNumTy x i) = HsNumTy x i
-rnHsTyLit (HsCharTy x c) = HsCharTy x c
+rnHsTyLit :: HsTyLit GhcPs -> RnM (HsTyLit GhcRn)
+rnHsTyLit (HsStrTy x s) = pure (HsStrTy x s)
+rnHsTyLit tyLit@(HsNumTy x i) = do
+  when (i < 0) $
+    addErr $ TcRnNegativeNumTypeLiteral tyLit
+  pure (HsNumTy x i)
+rnHsTyLit (HsCharTy x c) = pure (HsCharTy x c)
 
 
 rnHsArrow :: RnTyKiEnv -> HsArrow GhcPs -> RnM (HsArrow GhcRn, FreeVars)
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 312629c0fad4..59e596a37934 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -1,11 +1,14 @@
-{-# LANGUAGE TypeApplications    #-}
-{-# LANGUAGE DeriveFunctor       #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE RankNTypes          #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE ViewPatterns        #-}
-{-# LANGUAGE DisambiguateRecordFields #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE DeriveFunctor              #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE RankNTypes                 #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE ViewPatterns               #-}
+{-# LANGUAGE DisambiguateRecordFields   #-}
+{-# LANGUAGE NamedFieldPuns             #-}
+{-# LANGUAGE DerivingStrategies         #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 
 {-
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
@@ -41,7 +44,7 @@ module GHC.Rename.Pat (-- main entry points
 import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Rename.Expr ( rnLExpr )
-import {-# SOURCE #-} GHC.Rename.Splice ( rnSplicePat )
+import {-# SOURCE #-} GHC.Rename.Splice ( rnSplicePat, rnSpliceTyPat )
 
 import GHC.Hs
 import GHC.Tc.Errors.Types
@@ -53,7 +56,7 @@ import GHC.Rename.Utils    ( newLocalBndrRn, bindLocalNames
                            , warnUnusedMatches, newLocalBndrRn
                            , checkUnusedRecordWildcard
                            , checkDupNames, checkDupAndShadowedNames
-                           , wrapGenSpan, genHsApps, genLHsVar, genHsIntegralLit, warnForallIdentifier )
+                           , wrapGenSpan, genHsApps, genLHsVar, genHsIntegralLit, warnForallIdentifier, delLocalNames, typeAppErr )
 import GHC.Rename.HsType
 import GHC.Builtin.Names
 
@@ -67,6 +70,7 @@ import GHC.Types.SourceText
 import GHC.Utils.Misc
 import GHC.Data.FastString ( uniqCompareFS )
 import GHC.Data.List.SetOps( removeDups )
+import GHC.Data.Bag ( Bag, unitBag, unionBags, emptyBag, listToBag, bagToList )
 import GHC.Utils.Outputable
 import GHC.Utils.Panic.Plain
 import GHC.Types.SrcLoc
@@ -76,14 +80,21 @@ import GHC.Builtin.Types   ( nilDataCon )
 import GHC.Core.DataCon
 import qualified GHC.LanguageExtensions as LangExt
 
-import Control.Monad       ( when, ap, guard )
+import Control.Monad       ( when, ap, guard, unless )
 import Data.Foldable
 import Data.Function       ( on )
 import Data.Functor.Identity ( Identity (..) )
 import qualified Data.List.NonEmpty as NE
 import Data.Maybe
 import Data.Ratio
-
+import qualified Data.Semigroup as S
+import Control.Monad.Trans.Writer.CPS
+import Control.Monad.Trans.Class
+import Control.Monad.Trans.Reader
+import Data.Functor ((<&>))
+import GHC.Rename.Doc (rnLHsDoc)
+import GHC.Types.Hint
+import GHC.Types.Fixity (LexicalFixity(..))
 
 {-
 *********************************************************
@@ -426,7 +437,7 @@ rnPats ctxt pats thing_inside
           --    complain *twice* about duplicates e.g. f (x,x) = ...
           --
           -- See Note [Don't report shadowing for pattern synonyms]
-        ; let bndrs = collectPatsBinders CollNoDictBinders (toList pats')
+        ; let bndrs = collectPatsBinders CollVarTyVarBinders (toList pats')
         ; addErrCtxt doc_pat $
           if isPatSynCtxt ctxt
              then checkDupNames bndrs
@@ -647,7 +658,7 @@ rnConPatAndThen mk con (PrefixCon tyargs pats)
           addErrTc $ TcRnTypeApplicationsDisabled (TypeApplicationInPattern arg)
 
     rnConPatTyArg (HsConPatTyArg at t) = do
-      t' <- liftCpsWithCont $ rnHsPatSigTypeBindingVars HsTypeCtx t
+      t' <- rnHsTyPat HsTypePatCtx t
       return (HsConPatTyArg at t')
 
 rnConPatAndThen mk con (InfixCon pat1 pat2)
@@ -1088,3 +1099,392 @@ rnOverLit origLit
                   ; return ((lit' { ol_val = negateOverLitVal val }, Just negate_name)
                                   , fvs1 `plusFV` fvs2) }
           else return ((lit', Nothing), fvs1) }
+
+
+rnHsTyPat :: HsDocContext
+          -> HsTyPat GhcPs
+          -> CpsRn (HsTyPat GhcRn)
+rnHsTyPat ctxt sigType = case sigType of
+  (HsTP { hstp_body = hs_ty }) -> do
+    (hs_ty', tpb) <- runTPRnM (rn_lty_pat hs_ty) ctxt
+    pure HsTP
+          { hstp_body = hs_ty'
+          , hstp_ext = buildHsTyPatRn tpb
+          }
+
+-- | Type pattern renaming monad
+-- For the OccSet in the ReaderT, see Note [Locally bound names in type patterns]
+-- For the HsTyPatRnBuilderRn in the WriterT, see Note [Implicit and explicit type variable binders]
+-- For the CpsRn base monad, see Note [CpsRn monad]
+-- For why we need CpsRn in TPRnM see Note [Left-to-right scoping of type patterns]
+newtype TPRnM a =
+  MkTPRnM (ReaderT (HsDocContext, OccSet) (WriterT HsTyPatRnBuilder CpsRn) a)
+  deriving newtype (Functor, Applicative, Monad)
+
+runTPRnM :: TPRnM a -> HsDocContext -> CpsRn (a, HsTyPatRnBuilder)
+runTPRnM (MkTPRnM thing_inside) doc_ctxt = runWriterT $ runReaderT thing_inside (doc_ctxt, emptyOccSet)
+
+askLocals :: TPRnM OccSet
+askLocals = MkTPRnM (asks snd)
+
+askDocContext :: TPRnM HsDocContext
+askDocContext = MkTPRnM (asks fst)
+
+tellTPB :: HsTyPatRnBuilder -> TPRnM ()
+tellTPB = MkTPRnM . lift . tell
+
+liftRnFV :: RnM (a, FreeVars) -> TPRnM a
+liftRnFV = liftTPRnCps . liftCpsFV
+
+liftRn :: RnM a -> TPRnM a
+liftRn = liftTPRnCps . liftCps
+
+liftRnWithCont :: (forall r. (b -> RnM (r, FreeVars)) -> RnM (r, FreeVars)) -> TPRnM b
+liftRnWithCont cont = liftTPRnCps (liftCpsWithCont cont)
+
+liftTPRnCps :: CpsRn a -> TPRnM a
+liftTPRnCps = MkTPRnM . lift . lift
+
+liftTPRnRaw ::
+  ( forall r .
+    HsDocContext ->
+    OccSet ->
+    ((a, HsTyPatRnBuilder) -> RnM (r, FreeVars)) ->
+    RnM (r, FreeVars)
+  ) -> TPRnM a
+liftTPRnRaw cont = MkTPRnM $ ReaderT $ \(doc_ctxt, locals) -> writerT $ liftCpsWithCont (cont doc_ctxt locals)
+
+unTPRnRaw ::
+  TPRnM a ->
+  HsDocContext ->
+  OccSet ->
+  ((a, HsTyPatRnBuilder) -> RnM (r, FreeVars)) ->
+  RnM (r, FreeVars)
+unTPRnRaw (MkTPRnM m) doc_ctxt locals = unCpsRn $ runWriterT $ runReaderT m (doc_ctxt, locals)
+
+wrapSrcSpanTPRnM :: (a -> TPRnM b) -> LocatedAn ann a -> TPRnM (LocatedAn ann b)
+wrapSrcSpanTPRnM fn (L loc a) = do
+  a' <- fn a
+  pure (L loc a')
+
+lookupTypeOccTPRnM :: RdrName -> TPRnM Name
+lookupTypeOccTPRnM rdr_name = liftRnFV $ do
+  name <- lookupTypeOccRn rdr_name
+  pure (name, unitFV name)
+
+-- | A variant of HsTyPatRn that uses Bags for efficient concatenation.
+-- See Note [Implicit and explicit type variable binders]
+data HsTyPatRnBuilder =
+  HsTPRnB {
+    hstpb_nwcs :: Bag Name,
+    hstpb_imp_tvs :: Bag Name,
+    hstpb_exp_tvs :: Bag Name
+  }
+
+tpb_exp_tv :: Name -> HsTyPatRnBuilder
+tpb_exp_tv name = mempty {hstpb_exp_tvs = unitBag name}
+
+tpb_hsps :: HsPSRn -> HsTyPatRnBuilder
+tpb_hsps HsPSRn {hsps_nwcs, hsps_imp_tvs} =
+  mempty {
+    hstpb_nwcs = listToBag hsps_nwcs,
+    hstpb_imp_tvs = listToBag hsps_imp_tvs
+  }
+
+instance Semigroup HsTyPatRnBuilder where
+  HsTPRnB nwcs1 imp_tvs1 exptvs1 <> HsTPRnB nwcs2 imp_tvs2 exptvs2 =
+    HsTPRnB
+      (nwcs1    `unionBags` nwcs2)
+      (imp_tvs1 `unionBags` imp_tvs2)
+      (exptvs1  `unionBags` exptvs2)
+
+instance Monoid HsTyPatRnBuilder where
+  mempty = HsTPRnB emptyBag emptyBag emptyBag
+
+buildHsTyPatRn :: HsTyPatRnBuilder -> HsTyPatRn
+buildHsTyPatRn HsTPRnB {hstpb_nwcs, hstpb_imp_tvs, hstpb_exp_tvs} =
+  HsTPRn {
+    hstp_nwcs =    bagToList hstpb_nwcs,
+    hstp_imp_tvs = bagToList hstpb_imp_tvs,
+    hstp_exp_tvs = bagToList hstpb_exp_tvs
+  }
+
+rn_lty_pat :: LHsType GhcPs -> TPRnM (LHsType GhcRn)
+rn_lty_pat (L l hs_ty) = do
+  hs_ty' <- rn_ty_pat hs_ty
+  pure (L l hs_ty')
+
+rn_ty_pat_var :: LocatedN RdrName -> TPRnM (LocatedN Name)
+rn_ty_pat_var lrdr@(L l rdr) = do
+  locals <- askLocals
+  if isRdrTyVar rdr
+    && not (elemOccSet (occName rdr) locals) -- See Note [Locally bound names in type patterns]
+
+    then do -- binder
+      name <- liftTPRnCps $ newPatName (LamMk True) lrdr
+      tellTPB (tpb_exp_tv name)
+      pure (L l name)
+
+    else do -- usage
+      name <- lookupTypeOccTPRnM rdr
+      pure (L l name)
+
+-- | Rename type patterns
+--
+-- For the difference between `rn_ty_pat` and `rnHsTyKi` see Note [CpsRn monad]
+-- and Note [Implicit and explicit type variable binders]
+rn_ty_pat :: HsType GhcPs -> TPRnM (HsType GhcRn)
+rn_ty_pat (HsTyVar an prom lrdr) = do
+  name <- rn_ty_pat_var lrdr
+  pure (HsTyVar an prom name)
+
+rn_ty_pat (HsForAllTy an tele body) = liftTPRnRaw $ \ctxt locals thing_inside ->
+  bindHsForAllTelescope ctxt tele $ \tele' -> do
+    let
+      tele_names = hsForAllTelescopeNames tele'
+      locals' = locals `extendOccSetList` map occName tele_names
+
+    unTPRnRaw (rn_lty_pat body) ctxt locals' $ \(body', tpb) ->
+      delLocalNames tele_names $ -- locally bound names do not scope over the continuation
+        thing_inside ((HsForAllTy an tele' body'), tpb)
+
+rn_ty_pat (HsQualTy an lctx body) = do
+  lctx' <- wrapSrcSpanTPRnM (mapM rn_lty_pat) lctx
+  body' <- rn_lty_pat body
+  pure (HsQualTy an lctx' body')
+
+rn_ty_pat (HsAppTy _ fun_ty arg_ty) = do
+  fun_ty' <- rn_lty_pat fun_ty
+  arg_ty' <- rn_lty_pat arg_ty
+  pure (HsAppTy noExtField fun_ty' arg_ty')
+
+rn_ty_pat (HsAppKindTy _ ty at ki) = do
+  kind_app <- liftRn $ xoptM LangExt.TypeApplications
+  unless kind_app (liftRn $ addErr (typeAppErr KindLevel ki))
+  ty' <- rn_lty_pat ty
+  ki' <- rn_lty_pat ki
+  pure (HsAppKindTy noExtField ty' at ki')
+
+rn_ty_pat (HsFunTy an mult lhs rhs) = do
+  lhs' <- rn_lty_pat lhs
+  mult' <- rn_ty_pat_arrow mult
+  rhs' <- rn_lty_pat rhs
+  pure (HsFunTy an mult' lhs' rhs')
+
+rn_ty_pat (HsListTy an ty) = do
+  ty' <- rn_lty_pat ty
+  pure (HsListTy an ty')
+
+rn_ty_pat (HsTupleTy an con tys) = do
+  tys' <- mapM rn_lty_pat tys
+  pure (HsTupleTy an con tys')
+
+rn_ty_pat (HsSumTy an tys) = do
+  tys' <- mapM rn_lty_pat tys
+  pure (HsSumTy an tys')
+
+rn_ty_pat (HsOpTy _ prom ty1 l_op ty2) = do
+  ty1' <- rn_lty_pat ty1
+  l_op' <- rn_ty_pat_var l_op
+  ty2' <- rn_lty_pat ty2
+  fix  <- liftRn $ lookupTyFixityRn l_op'
+  let op_name = unLoc l_op'
+  when (isDataConName op_name && not (isPromoted prom)) $
+    liftRn $ addDiagnostic (TcRnUntickedPromotedThing $ UntickedConstructor Infix op_name)
+  liftRn $ mkHsOpTyRn prom l_op' fix ty1' ty2'
+
+rn_ty_pat (HsParTy an ty) = do
+  ty' <- rn_lty_pat ty
+  pure (HsParTy an ty')
+
+rn_ty_pat (HsIParamTy an n ty) = do
+  ty' <- rn_lty_pat ty
+  pure (HsIParamTy an n ty')
+
+rn_ty_pat (HsStarTy an unicode) =
+  pure (HsStarTy an unicode)
+
+rn_ty_pat (HsDocTy an ty haddock_doc) = do
+  ty' <- rn_lty_pat ty
+  haddock_doc' <- liftRn $ rnLHsDoc haddock_doc
+  pure (HsDocTy an ty' haddock_doc')
+
+rn_ty_pat ty@(HsExplicitListTy _ prom tys) = do
+  data_kinds <- liftRn $ xoptM LangExt.DataKinds
+  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel ty))
+
+  unless (isPromoted prom) $
+    liftRn $ addDiagnostic (TcRnUntickedPromotedThing $ UntickedExplicitList)
+
+  tys' <- mapM rn_lty_pat tys
+  pure (HsExplicitListTy noExtField prom tys')
+
+rn_ty_pat ty@(HsExplicitTupleTy _ tys) = do
+  data_kinds <- liftRn $ xoptM LangExt.DataKinds
+  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel ty))
+  tys' <- mapM rn_lty_pat tys
+  pure (HsExplicitTupleTy noExtField tys')
+
+rn_ty_pat tyLit@(HsTyLit src t) = do
+  data_kinds <- liftRn $ xoptM LangExt.DataKinds
+  unless data_kinds (liftRn $ addErr (TcRnDataKindsError TypeLevel tyLit))
+  t' <- liftRn $ rnHsTyLit t
+  pure (HsTyLit src t')
+
+rn_ty_pat (HsWildCardTy _) =
+  pure (HsWildCardTy noExtField)
+
+rn_ty_pat (HsKindSig an ty ki) = do
+  ctxt <- askDocContext
+  kind_sigs_ok <- liftRn $ xoptM LangExt.KindSignatures
+  unless kind_sigs_ok (liftRn $ badKindSigErr ctxt ki)
+  ~(HsPS hsps ki') <- liftRnWithCont $
+                      rnHsPatSigKind AlwaysBind ctxt (HsPS noAnn ki)
+  ty' <- rn_lty_pat ty
+  tellTPB (tpb_hsps hsps)
+  pure (HsKindSig an ty' ki')
+
+rn_ty_pat (HsSpliceTy _ splice) = do
+  res <- liftRnFV $ rnSpliceTyPat splice
+  case res of
+    (rn_splice, HsUntypedSpliceTop mfs pat) -> do -- Splice was top-level and thus run, creating LHsType GhcPs
+        pat' <- rn_lty_pat pat
+        pure (HsSpliceTy (HsUntypedSpliceTop mfs (mb_paren pat')) rn_splice)
+    (rn_splice, HsUntypedSpliceNested splice_name) ->
+        pure (HsSpliceTy (HsUntypedSpliceNested splice_name) rn_splice) -- Splice was nested and thus already renamed
+  where
+    mb_paren :: LHsType GhcRn -> LHsType GhcRn
+    mb_paren lhs_ty@(L loc hs_ty)
+      | hsTypeNeedsParens maxPrec hs_ty = L loc (HsParTy noAnn lhs_ty)
+      | otherwise                       = lhs_ty
+
+rn_ty_pat (HsBangTy an bang_src lty) = do
+  ctxt <- askDocContext
+  lty'@(L _ ty') <- rn_lty_pat lty
+  liftRn $ addErr $
+    TcRnWithHsDocContext ctxt $
+    TcRnUnexpectedAnnotation ty' bang_src
+  pure (HsBangTy an bang_src lty')
+
+rn_ty_pat ty@HsRecTy{} = do
+  ctxt <- askDocContext
+  liftRn $ addErr $
+    TcRnWithHsDocContext ctxt $
+    TcRnIllegalRecordSyntax (Left ty)
+  pure (HsWildCardTy noExtField) -- trick to avoid `failWithTc`
+
+rn_ty_pat ty@(XHsType{}) = do
+  ctxt <- askDocContext
+  liftRnFV $ rnHsType ctxt ty
+
+rn_ty_pat_arrow :: HsArrow GhcPs -> TPRnM (HsArrow GhcRn)
+rn_ty_pat_arrow (HsUnrestrictedArrow arr) = pure (HsUnrestrictedArrow arr)
+rn_ty_pat_arrow (HsLinearArrow (HsPct1 pct1 arr)) = pure (HsLinearArrow (HsPct1 pct1 arr))
+rn_ty_pat_arrow (HsLinearArrow (HsLolly arr)) = pure (HsLinearArrow (HsLolly arr))
+rn_ty_pat_arrow (HsExplicitMult pct p arr)
+  = rn_lty_pat p <&> (\mult -> HsExplicitMult pct mult arr)
+
+
+{- Note [Locally bound names in type patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type patterns can bind local names using forall. Compare the following examples:
+  f (Proxy @(Either a b)) = ...
+  g (Proxy @(forall a . Either a b)) = ...
+
+In `f` both `a` and `b` are bound by the pattern and scope over the RHS of f.
+In `g` only `b` is bound by the pattern, whereas `a` is locally bound in the pattern
+and does not scope over the RHS of `g`.
+
+We track locally bound names in the `OccSet` in `TPRnM` monad, and use it to
+decide whether occurences of type variables are usages or bindings.
+
+The check is done in `rn_ty_pat_var`
+
+Note [Implicit and explicit type variable binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type patterns are renamed differently from ordinary types.
+  * Types are renamed by `rnHsType` where all type variable occurences are considered usages
+  * Type patterns are renamed by `rnHsTyPat` where some type variable occurences are usages
+    and other are bindings
+
+Here is an example:
+  {-# LANGUAGE ScopedTypeVariables #-}
+  f :: forall b. Proxy _ -> ...
+  f (Proxy @(x :: (a, b))) = ...
+
+In the (x :: (a,b)) type pattern
+  * `x` is a type variable explicitly bound by type pattern
+  * `a` is a type variable implicitly bound in a pattern signature
+  * `b` is a usage of type variable bound by the outer forall
+
+This classification is clear to us in `rnHsTyPat`, but it is also useful in later passes, such
+as `collectPatBinders` and `tcHsTyPat`, so we store it in the extension field of `HsTyPat`, namely
+`HsTyPatRn`.
+
+To collect lists of those variables efficiently we use `HsTyPatRnBuilder` which is exactly like
+`HsTyPatRn`, but uses Bags.
+
+Note [Left-to-right scoping of type patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In term-level patterns, we use continuation passing to implement left-to-right
+scoping, see Note [CpsRn monad]. Left-to-right scoping manifests itself when
+e.g. view patterns are involved:
+
+  f (x, g x -> Just y) = ...
+
+Here the first occurrence of `x` is a binder, and the second occurrence is a
+use of `x` in a view pattern. This example does not work if we swap the
+components of the tuple:
+
+  f (g x -> Just y, x) = ...
+  --  ^^^
+  -- Variable not in scope: x
+
+In type patterns there are no view patterns, but there is a different feature
+that is served well by left-to-right scoping: kind annotations. Compare:
+
+  f (Proxy @(T k (a :: k))) = ...
+  g (Proxy @(T (a :: k) k)) = ...
+
+In `f`, the first occurrence of `k` is an explicit binder,
+  and the second occurrence is a usage. Simple.
+In `g`, the first occurrence of `k` is an implicit binder,
+  and then the second occurrence is an explicit binder that shadows it.
+
+So we get two different results after renaming:
+
+  f (Proxy @(T k1 (a :: k1))) = ...
+  g (Proxy @(T (a :: k1) k2)) = ...
+
+This makes GHC accept the first example but rejects the second example with an
+error about duplicate binders.
+
+One could argue that we don't want order-sensitivity here. Historically, we
+used a different principle when renaming types: collect all free variables,
+bind them on the outside, and then rename all occurrences as usages.
+This approach does not scale to multiple patterns. Consider:
+
+  f' (MkP @k @(a :: k)) = ...
+  g' (MkP @(a :: k) @k) = ...
+
+Here a difference in behavior is inevitable, as we rename type patterns
+one at a time. Could we perhaps concatenate the free variables from all
+type patterns in a ConPat? But then we still get the same problem one level up,
+when we have multiple patterns in a function LHS
+
+  f'' (Proxy @k) (Proxy @(a :: k)) = ...
+  g'' (Proxy @(a :: k)) (Proxy @k) = ...
+
+And if we tried to avoid order sensitivity at this level, then we'd still be left
+with lambdas:
+
+  f''' (Proxy @k)        = \(Proxy @(a :: k)) -> ...
+  g''' (Proxy @(a :: k)) = \(Proxy @k)        -> ...
+
+
+So we have at least three options where we could do free variable extraction:
+HsConPatTyArg, ConPat, or a Match (used to represent a function LHS). And none
+of those would be general enough. Rather than make an arbitrary choice, we
+embrace left-to-right scoping in types and implement it with CPS, just like
+it's done for view patterns in terms.
+-}
diff --git a/compiler/GHC/Rename/Splice.hs b/compiler/GHC/Rename/Splice.hs
index f91a6f66b1c7..0a38dc7a6b33 100644
--- a/compiler/GHC/Rename/Splice.hs
+++ b/compiler/GHC/Rename/Splice.hs
@@ -7,7 +7,7 @@ module GHC.Rename.Splice (
         -- Typed splices
         rnTypedSplice,
         -- Untyped splices
-        rnSpliceType, rnUntypedSpliceExpr, rnSplicePat, rnSpliceDecl,
+        rnSpliceType, rnUntypedSpliceExpr, rnSplicePat, rnSpliceTyPat, rnSpliceDecl,
 
         -- Brackets
         rnTypedBracket, rnUntypedBracket,
@@ -741,6 +741,26 @@ rnSplicePat splice
               -- Wrap the result of the quasi-quoter in parens so that we don't
               -- lose the outermost location set by runQuasiQuote (#7918)
 
+-- | Rename a splice type pattern. Much the same as `rnSplicePat`, but works with LHsType instead of LPat
+rnSpliceTyPat :: HsUntypedSplice GhcPs -> RnM ( (HsUntypedSplice GhcRn, HsUntypedSpliceResult (LHsType GhcPs))
+                                            , FreeVars)
+rnSpliceTyPat splice
+  = rnUntypedSpliceGen run_ty_pat_splice pend_ty_pat_splice splice
+  where
+    pend_ty_pat_splice name rn_splice
+      = (makePending UntypedTypeSplice name rn_splice
+        , (rn_splice, HsUntypedSpliceNested name)) -- HsType splice is nested and thus simply renamed
+
+    run_ty_pat_splice rn_splice
+      = do { traceRn "rnSpliceTyPat: untyped pattern splice" empty
+           ; (ty, mod_finalizers) <-
+                runRnSplice UntypedTypeSplice runMetaT ppr rn_splice
+             -- See Note [Delaying modFinalizers in untyped splices].
+           ; let t = HsUntypedSpliceTop (ThModFinalizers mod_finalizers) ty
+           ; return ((rn_splice, t), emptyFVs) }
+              -- Wrap the result of the quasi-quoter in parens so that we don't
+              -- lose the outermost location set by runQuasiQuote (#7918)
+
 ----------------------
 rnSpliceDecl :: SpliceDecl GhcPs -> RnM (SpliceDecl GhcRn, FreeVars)
 rnSpliceDecl (SpliceDecl _ (L loc splice) flg)
diff --git a/compiler/GHC/Rename/Splice.hs-boot b/compiler/GHC/Rename/Splice.hs-boot
index 7a67c41d1945..786e88e988d7 100644
--- a/compiler/GHC/Rename/Splice.hs-boot
+++ b/compiler/GHC/Rename/Splice.hs-boot
@@ -8,6 +8,8 @@ import GHC.Types.Name.Set
 rnSpliceType :: HsUntypedSplice GhcPs -> RnM (HsType GhcRn, FreeVars)
 rnSplicePat  :: HsUntypedSplice GhcPs -> RnM ( (HsUntypedSplice GhcRn, HsUntypedSpliceResult (LPat GhcPs))
                                              , FreeVars)
+rnSpliceTyPat  :: HsUntypedSplice GhcPs -> RnM ( (HsUntypedSplice GhcRn, HsUntypedSpliceResult (LHsType GhcPs))
+                                             , FreeVars)
 rnSpliceDecl :: SpliceDecl GhcPs -> RnM (SpliceDecl GhcRn, FreeVars)
 
 rnTopSpliceDecls :: HsUntypedSplice GhcPs -> RnM ([LHsDecl GhcPs], FreeVars)
diff --git a/compiler/GHC/Rename/Utils.hs b/compiler/GHC/Rename/Utils.hs
index 9cf7af183af9..81fb803e51fc 100644
--- a/compiler/GHC/Rename/Utils.hs
+++ b/compiler/GHC/Rename/Utils.hs
@@ -26,7 +26,7 @@ module GHC.Rename.Utils (
 
         newLocalBndrRn, newLocalBndrsRn,
 
-        bindLocalNames, bindLocalNamesFV,
+        bindLocalNames, bindLocalNamesFV, delLocalNames,
 
         addNameClashErrRn, mkNameClashErr,
 
@@ -108,6 +108,14 @@ bindLocalNamesFV names enclosed_scope
   = do  { (result, fvs) <- bindLocalNames names enclosed_scope
         ; return (result, delFVs names fvs) }
 
+delLocalNames :: [Name] -> RnM a -> RnM a
+delLocalNames names
+  = updLclCtxt $ \ lcl_env ->
+    let th_bndrs' = delListFromNameEnv (tcl_th_bndrs lcl_env) names
+        rdr_env'  = minusLocalRdrEnvList (tcl_rdr lcl_env) (map occName names)
+    in lcl_env { tcl_th_bndrs = th_bndrs'
+               , tcl_rdr      = rdr_env' }
+
 -------------------------------------
 checkDupRdrNames :: [LocatedN RdrName] -> RnM ()
 -- Check for duplicated names in a binding group
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index aa472c1e8166..332d7963f61d 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -991,6 +991,7 @@ instance Diagnostic TcRnMessage where
     TcRnIllegalRecordSyntax either_ty_ty
       -> mkSimpleDecorated $
            text "Record syntax is illegal here:" <+> either ppr ppr either_ty_ty
+
     TcRnInvalidVisibleKindArgument arg ty
       -> mkSimpleDecorated $
            text "Cannot apply function of kind" <+> quotes (ppr ty)
@@ -1613,20 +1614,6 @@ instance Diagnostic TcRnMessage where
          2 (vcat [ text "Expected:" <+> ppr fam_tc_name
                  , text "  Actual:" <+> ppr eqn_tc_name ])
 
-    TcRnBindVarAlreadyInScope tv_names_in_scope
-      -> mkSimpleDecorated $
-        vcat
-          [ text "Type variable" <> plural tv_names_in_scope
-            <+> hcat (punctuate (text ",") (map (quotes . ppr) tv_names_in_scope))
-            <+> isOrAre tv_names_in_scope
-            <+> text "already in scope."
-          , text "Type applications in patterns must bind fresh variables, without shadowing."
-          ]
-
-    TcRnBindMultipleVariables ctx tv_name_w_loc
-      -> mkSimpleDecorated $
-        text "Variable" <+> text "`" <> ppr tv_name_w_loc <> text "'" <+> text "would be bound multiple times by" <+> pprHsDocContext ctx <> text "."
-
     TcRnUnexpectedKindVar tv_name
       -> mkSimpleDecorated $ text "Unexpected kind variable" <+> quotes (ppr tv_name)
 
@@ -2395,10 +2382,6 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnTyFamNameMismatch{}
       -> ErrorWithoutFlag
-    TcRnBindVarAlreadyInScope{}
-      -> ErrorWithoutFlag
-    TcRnBindMultipleVariables{}
-      -> ErrorWithoutFlag
     TcRnUnexpectedKindVar{}
       -> ErrorWithoutFlag
     TcRnNegativeNumTypeLiteral{}
@@ -3060,10 +3043,6 @@ instance Diagnostic TcRnMessage where
       -> [suggestExtension LangExt.IncoherentInstances]
     TcRnTyFamNameMismatch{}
       -> noHints
-    TcRnBindVarAlreadyInScope{}
-      -> noHints
-    TcRnBindMultipleVariables{}
-      -> noHints
     TcRnUnexpectedKindVar{}
       -> [suggestExtension LangExt.PolyKinds]
     TcRnNegativeNumTypeLiteral{}
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 8862b05e03e7..43da4e8b8378 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -513,6 +513,8 @@ data TcRnMessage where
                  rename/should_fail/T2723
                  rename/should_compile/T3262
                  driver/werror
+                 rename/should_fail/T22478d
+                 typecheck/should_fail/TyAppPat_ScopedTyVarConflict
   -}
   TcRnShadowedName :: OccName -> ShadowedNameProvenance -> TcRnMessage
 
@@ -728,7 +730,7 @@ data TcRnMessage where
      Test cases: th/T8412
                  typecheck/should_fail/T8306
   -}
-  TcRnNegativeNumTypeLiteral :: HsType GhcPs -> TcRnMessage
+  TcRnNegativeNumTypeLiteral :: HsTyLit GhcPs -> TcRnMessage
 
   {-| TcRnIllegalWildcardsInConstructor is an error that occurs whenever
       the record wildcards '..' are used inside a constructor without labeled fields.
@@ -1937,25 +1939,6 @@ data TcRnMessage where
  -}
   TcRnCapturedTermName :: RdrName -> Either [GlobalRdrElt] Name -> TcRnMessage
 
-  {-| TcRnTypeMultipleOccurenceOfBindVar is an error that occurs if a bound
-      type variable's name is already in use.
-    Example:
-      f :: forall a. ...
-      f (MkT @a ...) = ...
-
-    Test cases: TyAppPat_ScopedTyVarConflict TyAppPat_NonlinearMultiPat TyAppPat_NonlinearMultiAppPat
-  -}
-  TcRnBindVarAlreadyInScope :: [LocatedN RdrName] -> TcRnMessage
-
-  {-| TcRnBindMultipleVariables is an error that occurs in the case of
-    multiple occurrences of a bound variable.
-    Example:
-      foo (MkFoo @(a,a) ...) = ...
-
-    Test case: typecheck/should_fail/TyAppPat_NonlinearSinglePat
-  -}
-  TcRnBindMultipleVariables :: HsDocContext -> LocatedN RdrName -> TcRnMessage
-
   {-| TcRnTypeEqualityOutOfScope is a warning (controlled by -Wtype-equality-out-of-scope)
       that occurs when the type equality (a ~ b) is not in scope.
 
@@ -2237,6 +2220,7 @@ data TcRnMessage where
 
     Test cases: parser/should_fail/unpack_inside_type
                 typecheck/should_fail/T7210
+                rename/should_fail/T22478b
   -}
   TcRnUnexpectedAnnotation :: !(HsType GhcRn) -> !HsSrcBang -> TcRnMessage
 
@@ -2247,6 +2231,7 @@ data TcRnMessage where
 
     Test cases: rename/should_fail/T7943
                 rename/should_fail/T9077
+                rename/should_fail/T22478b
   -}
   TcRnIllegalRecordSyntax :: Either (HsType GhcPs) (HsType GhcRn) -> TcRnMessage
 
@@ -4047,7 +4032,9 @@ data TcRnMessage where
 
     Test cases:
       dsrun006, mdofail002, mdofail003, mod23, mod24, qq006, rnfail001,
-      rnfail004, SimpleFail6, T14114, T16110_Fail1, tcfail038, TH_spliceD1
+      rnfail004, SimpleFail6, T14114, T16110_Fail1, tcfail038, TH_spliceD1,
+      T22478b, TyAppPat_NonlinearMultiAppPat, TyAppPat_NonlinearMultiPat,
+      TyAppPat_NonlinearSinglePat,
   -}
   TcRnBindingNameConflict :: !RdrName -- ^ The conflicting name
                           -> !(NE.NonEmpty SrcSpan)
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 71d1c5952387..4ae70b02d0c4 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -69,7 +69,7 @@ module GHC.Tc.Gen.HsType (
         tcMult,
 
         -- Pattern type signatures
-        tcHsPatSigType,
+        tcHsPatSigType, tcHsTyPat,
         HoleMode(..),
 
         -- Error messages
@@ -747,7 +747,7 @@ There is also the possibility of mentioning a wildcard
 -}
 
 tcFamTyPats :: TyCon
-            -> HsTyPats GhcRn                -- Patterns
+            -> HsFamEqnPats GhcRn                -- Patterns
             -> TcM (TcType, TcKind)          -- (lhs_type, lhs_kind)
 -- Check the LHS of a type/data family instance
 -- e.g.   type instance F ty1 .. tyn = ...
@@ -4165,34 +4165,122 @@ tcHsPatSigType ctxt hole_mode
   (HsPS { hsps_ext  = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
         , hsps_body = hs_ty })
   ctxt_kind
+  = tc_type_in_pat ctxt hole_mode hs_ty sig_wcs sig_ns ctxt_kind
+
+
+-- Typecheck type patterns, in data constructor patterns, e.g
+--    f (MkT @a @(Maybe b) ...) = ...
+--
+-- We have two competely separate typing rules,
+--   one for binder type patterns  (handled by `tc_bndr_in_pat`)
+--   one for unifier type patterns (handled by `tc_type_in_pat`)
+-- The two cases are distingished by `tyPatToBndr`.
+-- See Note [Type patterns: binders and unifiers]
+tcHsTyPat :: HsTyPat GhcRn               -- The type pattern
+          -> Kind                        -- What kind is expected
+          -> TcM ( [(Name, TcTyVar)]     -- Wildcards
+                 , [(Name, TcTyVar)]     -- The new bit of type environment, binding
+                                         -- the scoped type variables
+                 , TcType)               -- The type
+tcHsTyPat hs_pat@(HsTP{hstp_ext = hstp_rn, hstp_body = hs_ty}) expected_kind
+  = case tyPatToBndr hs_pat of
+    Nothing   -> tc_unif_in_pat hs_ty wcs all_ns (TheKind expected_kind)
+    Just bndr -> tc_bndr_in_pat bndr  wcs imp_ns  expected_kind
+  where
+    all_ns = imp_ns ++ exp_ns
+    HsTPRn{hstp_nwcs = wcs, hstp_imp_tvs = imp_ns, hstp_exp_tvs = exp_ns} = hstp_rn
+    tc_unif_in_pat = tc_type_in_pat TypeAppCtxt HM_TyAppPat
+
+-- `tc_bndr_in_pat` is used in type patterns to handle the binders case.
+-- See Note [Type patterns: binders and unifiers]
+tc_bndr_in_pat :: HsTyVarBndr flag GhcRn
+               -> [Name]  -- All named wildcards in type
+               -> [Name]  -- Implicit (but not explicit) binders in type
+               -> Kind    -- Expected kind
+               -> TcM ( [(Name, TcTyVar)]     -- Wildcards
+                      , [(Name, TcTyVar)]     -- The new bit of type environment, binding
+                                              -- the scoped type variables
+                      , TcType)               -- The type
+tc_bndr_in_pat bndr wcs imp_ns expected_kind = do
+  traceTc "tc_bndr_in_pat 1" (ppr expected_kind)
+  case bndr of
+    UserTyVar _ _ (L _ name) -> do
+      tv <- newPatTyVar name expected_kind
+      pure ([], [(name,tv)], mkTyVarTy tv)
+    KindedTyVar _ _ (L _ name) ki -> do
+      tkv_prs <- mapM new_implicit_tv imp_ns
+      wcs <- addTypeCtxt ki              $
+             solveEqualities "tc_bndr_in_pat" $
+               -- See Note [Failure in local type signatures]
+               -- and c.f #16033
+             bindNamedWildCardBinders wcs $ \ wcs ->
+             tcExtendNameTyVarEnv tkv_prs $
+             do { sig_kind <- tcLHsKindSig (TyVarBndrKindCtxt name) ki
+                ; discardResult $
+                  unifyKind (Just (NameThing name)) sig_kind expected_kind
+                ; pure wcs }
+
+      mapM_ emitNamedTypeHole wcs
+
+      tv <- newPatTyVar name expected_kind
+
+      traceTc "tc_bndr_in_pat 2" $ vcat
+        [ text "expected_kind" <+> ppr expected_kind
+        , text "wcs" <+> ppr wcs
+        , text "(name,tv)" <+>  ppr (name,tv)
+        , text "tkv_prs" <+> ppr tkv_prs]
+
+      pure (wcs, (name,tv) : tkv_prs, mkTyVarTy tv)
+  where
+    new_implicit_tv name
+      = do { kind <- newMetaKindVar
+           ; tv   <- newPatTyVar name kind
+             -- NB: tv's Name is fresh
+           ; return (name, tv) }
+
+-- * In type patterns `tc_type_in_pat` is used to handle the unifiers case.
+--   See Note [Type patterns: binders and unifiers]
+--
+-- * In patterns `tc_type_in_pat` is used to check pattern signatures.
+tc_type_in_pat :: UserTypeCtxt
+               -> HoleMode -- HM_Sig when in a SigPat, HM_TyAppPat when in a ConPat checking type applications.
+               -> LHsType GhcRn          -- The type in pattern
+               -> [Name]                 -- All named wildcards in type
+               -> [Name]                 -- All binders in type
+               -> ContextKind                -- What kind is expected
+               -> TcM ( [(Name, TcTyVar)]     -- Wildcards
+                      , [(Name, TcTyVar)]     -- The new bit of type environment, binding
+                                              -- the scoped type variables
+                      , TcType)       -- The type
+tc_type_in_pat ctxt hole_mode hs_ty wcs ns ctxt_kind
   = addSigCtxt ctxt hs_ty $
-    do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
+    do { tkv_prs <- mapM new_implicit_tv ns
        ; mode <- mkHoleMode TypeLevel hole_mode
-       ; (wcs, sig_ty)
-            <- addTypeCtxt hs_ty                     $
-               solveEqualities "tcHsPatSigType" $
+       ; (wcs, ty)
+            <- addTypeCtxt hs_ty                $
+               solveEqualities "tc_type_in_pat" $
                  -- See Note [Failure in local type signatures]
                  -- and c.f #16033
-               bindNamedWildCardBinders sig_wcs $ \ wcs ->
-               tcExtendNameTyVarEnv sig_tkv_prs $
+               bindNamedWildCardBinders wcs $ \ wcs ->
+               tcExtendNameTyVarEnv tkv_prs $
                do { ek     <- newExpectedKind ctxt_kind
-                  ; sig_ty <- tc_lhs_type mode hs_ty ek
-                  ; return (wcs, sig_ty) }
+                  ; ty <- tc_lhs_type mode hs_ty ek
+                  ; return (wcs, ty) }
 
         ; mapM_ emitNamedTypeHole wcs
 
-          -- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
+          -- ty might have tyvars that are at a higher TcLevel (if hs_ty
           -- contains a forall). Promote these.
           -- Ex: f (x :: forall a. Proxy a -> ()) = ... x ...
           -- When we instantiate x, we have to compare the kind of the argument
           -- to a's kind, which will be a metavariable.
           -- kindGeneralizeNone does this:
-        ; kindGeneralizeNone sig_ty
-        ; sig_ty <- liftZonkM $ zonkTcType sig_ty
-        ; checkValidType ctxt sig_ty
+        ; kindGeneralizeNone ty
+        ; ty <- liftZonkM $ zonkTcType ty
+        ; checkValidType ctxt ty
 
-        ; traceTc "tcHsPatSigType" (ppr sig_tkv_prs)
-        ; return (wcs, sig_tkv_prs, sig_ty) }
+        ; traceTc "tc_type_in_pat" (ppr tkv_prs)
+        ; return (wcs, tkv_prs, ty) }
   where
     new_implicit_tv name
       = do { kind <- newMetaKindVar
@@ -4200,13 +4288,76 @@ tcHsPatSigType ctxt hole_mode
                        RuleSigCtxt rname _  -> do
                         skol_info <- mkSkolemInfo (RuleSkol rname)
                         newSkolemTyVar skol_info name kind
-                       _              -> newPatSigTyVar name kind
+                       _              -> newPatTyVar name kind
                        -- See Note [Typechecking pattern signature binders]
-             -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
+             -- NB: tv's Name may be fresh (in the case of newPatTyVar)
            ; return (name, tv) }
 
-{- Note [Typechecking pattern signature binders]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- See Note [Type patterns: binders and unifiers]
+tyPatToBndr :: HsTyPat GhcRn -> Maybe (HsTyVarBndr () GhcRn)
+tyPatToBndr HsTP{hstp_body = (L _ hs_ty)} = go hs_ty where
+  go :: HsType GhcRn -> Maybe (HsTyVarBndr () GhcRn)
+  go (HsParTy _ (L _ ty)) = go ty
+  go (HsTyVar an _ name)
+    | isTyVarName (unLoc name)
+    = Just (UserTyVar an () name)
+  go (HsKindSig an (L _ (HsTyVar _ _ name)) ki)
+    | isTyVarName (unLoc name)
+    = Just (KindedTyVar an () name ki)
+  go _ = Nothing
+
+{- Note [Type patterns: binders and unifiers]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A type pattern, of type `HsTyPat`, represents a type argument in a data
+constructor pattern.  For example
+    f (MkT @a @(Maybe b) p q) = ...
+Here the `@a` and `@(Maybe b)` are type patterns.  In general, then a
+`HsTyPat` is represented by a `HsType`.
+
+However, for /typechecking/ purposes (only) we distinguish two categories of
+type pattern:
+* Binder type patterns
+* Unifier type patterns
+
+Binder type patterns are a subset of type patterns described by the following grammar:
+
+  tp_bndr ::=
+      tv                    -- type variable
+    | tv '::' kind          -- type variable with kind annotation
+    | '(' tp_bndr ')'       -- parentheses
+
+This subset of HsTyPat can be represented by HsTyVarBndr, which is also used
+in foralls and type declaration headers. We could also extend this with wildcards (#23501).
+
+Unifier type patterns include all other forms of type patterns, such as `Maybe x`.
+This distinction allows the typechecker to accept more programs.
+Consider this example from #18986:
+
+  data T where
+    MkT :: forall (f :: forall k. k -> Type).
+      f Int -> f Maybe -> T
+
+  k :: T -> ()
+  k (MkT @f (x :: f Int) (y :: f Maybe)) = ()
+
+In general case (if we treat `f` as a unifier) we would create a metavariable for its kind:
+  f :: kappa
+Checking `x :: f Int` would unify
+  kappa := Type -> Type
+and then checking `y :: f Maybe` would unify
+  kappa := (Type -> Type) -> Type
+leading to a type error:
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+
+However, `@f` is a simple type variable binder, we don't need a metavariable for its kind, we
+can add it directly to the context with its polymorphic kind:
+  f :: forall k . k -> Type
+This way both `f Int` and `f Maybe` can be accepted because `k` can be instantiated differently at
+each call site.
+
+Note [Typechecking pattern signature binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Type variables in the type environment] in GHC.Tc.Utils.
 Consider
 
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 266ca228aac3..a45c6c42b60a 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1426,12 +1426,7 @@ tcConTyArgs tenv penv prs thing_inside
 
 tcConTyArg :: Subst -> Checker (HsConPatTyArg GhcRn, TyVar) ()
 tcConTyArg tenv penv (HsConPatTyArg _ rn_ty, con_tv) thing_inside
-  = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind
-               -- AnyKind is a bit suspect: it really should be the kind gotten
-               -- from instantiating the constructor type. But this would be
-               -- hard to get right, because earlier type patterns might influence
-               -- the kinds of later patterns. In any case, it all gets checked
-               -- by the calls to unifyType below which unifies kinds
+  = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsTyPat rn_ty (substTy tenv (varType con_tv))
 
        ; case NE.nonEmpty sig_ibs of
            Just sig_ibs_ne | inPatBind penv ->
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 6f657a5be880..2fe004d96dc2 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -3290,7 +3290,7 @@ generalising over the type of a rewrite rule.
 --------------------------
 tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo
                    -> HsOuterFamEqnTyVarBndrs GhcRn     -- Implicit and explicit binders
-                   -> HsTyPats GhcRn                    -- Patterns
+                   -> HsFamEqnPats GhcRn                    -- Patterns
                    -> LHsType GhcRn                     -- RHS
                    -> TcM ([TyVar], [TcType], TcType)   -- (tyvars, pats, rhs)
 -- Used only for type families, not data families
diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs
index d74f948f9abd..f0eddac776f1 100644
--- a/compiler/GHC/Tc/TyCl/Instance.hs
+++ b/compiler/GHC/Tc/TyCl/Instance.hs
@@ -902,7 +902,7 @@ TyVarEnv will simply be empty, and there is nothing to worry about.
 tcDataFamInstHeader
     :: AssocInstInfo -> SkolemInfo -> TyCon -> HsOuterFamEqnTyVarBndrs GhcRn
     -> LexicalFixity -> Maybe (LHsContext GhcRn)
-    -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn)
+    -> HsFamEqnPats GhcRn -> Maybe (LHsKind GhcRn)
     -> NewOrData
     -> TcM ([TcTyVar], [TcType], TcKind, TcThetaType)
          -- All skolem TcTyVars, all zonked so it's clear what the free vars are
@@ -2458,4 +2458,3 @@ instDeclCtxt2 dfun_ty
 inst_decl_ctxt :: SDoc -> SDoc
 inst_decl_ctxt doc = hang (text "In the instance declaration for")
                         2 (quotes doc)
-
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 1e111fa83e56..55cad5847284 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -56,7 +56,7 @@ module GHC.Tc.Utils.TcMType (
   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
   newMetaTyVarTyVarX,
   newTyVarTyVar, cloneTyVarTyVar,
-  newPatSigTyVar, newSkolemTyVar, newWildCardX,
+  newPatTyVar, newSkolemTyVar, newWildCardX,
 
   --------------------------------
   -- Expected types
@@ -796,15 +796,15 @@ newConcreteTyVar reason fs kind
   where
     assert_msg = text "newConcreteTyVar: non-concrete kind" <+> ppr kind
 
-newPatSigTyVar :: Name -> Kind -> TcM TcTyVar
-newPatSigTyVar name kind
+newPatTyVar :: Name -> Kind -> TcM TcTyVar
+newPatTyVar name kind
   = do { details <- newMetaDetails TauTv
        ; uniq <- newUnique
        ; let name' = name `setNameUnique` uniq
              tyvar = mkTcTyVar name' kind details
          -- Don't use cloneMetaTyVar;
          -- same reasoning as in newTyVarTyVar
-       ; traceTc "newPatSigTyVar" (ppr tyvar)
+       ; traceTc "newPatTyVar" (ppr tyvar)
        ; return tyvar }
 
 cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index c6418f161773..4b35c92cba92 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -604,7 +604,7 @@ cvt_datainst_hdr :: TH.Cxt -> Maybe [TH.TyVarBndr ()] -> TH.Type
                -> CvtM ( LHsContext GhcPs
                        , LocatedN RdrName
                        , HsOuterFamEqnTyVarBndrs GhcPs
-                       , HsTyPats GhcPs)
+                       , HsFamEqnPats GhcPs)
 cvt_datainst_hdr cxt bndrs tys
   = do { cxt' <- cvtContext funPrec cxt
        ; bndrs' <- traverse (mapM cvt_tv) bndrs
@@ -1438,7 +1438,7 @@ cvtp (ConP s ts ps)    = do { s' <- cNameN s
                             ; ps' <- cvtPats ps
                             ; ts' <- mapM cvtType ts
                             ; let pps = map (parenthesizePat appPrec) ps'
-                                  pts = map (\t -> HsConPatTyArg noHsTok (mkHsPatSigType noAnn t)) ts'
+                                  pts = map (\t -> HsConPatTyArg noHsTok (mkHsTyPat noAnn t)) ts'
                             ; return $ ConPat
                                 { pat_con_ext = noAnn
                                 , pat_con = s'
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index b1aadbfb58a8..bfeb3e4a4d91 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -475,8 +475,6 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnDifferentExportWarnings"                   = 92878
   GhcDiagnosticCode "TcRnIncompleteExportWarnings"                  = 94721
   GhcDiagnosticCode "TcRnIllegalTypeOperatorDecl"                   = 50649
-  GhcDiagnosticCode "TcRnBindVarAlreadyInScope"                     = 69710
-  GhcDiagnosticCode "TcRnBindMultipleVariables"                     = 92957
   GhcDiagnosticCode "TcRnIllegalKind"                               = 64861
   GhcDiagnosticCode "TcRnUnexpectedPatSigType"                      = 74097
   GhcDiagnosticCode "TcRnIllegalKindSignature"                      = 91382
@@ -851,6 +849,8 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "PsErrUnexpectedTypeAppInDecl"                  = 45054
   GhcDiagnosticCode "TcRnUnpromotableThing"                         = 88634
   GhcDiagnosticCode "UntouchableVariable"                           = 34699
+  GhcDiagnosticCode "TcRnBindVarAlreadyInScope"                     = 69710
+  GhcDiagnosticCode "TcRnBindMultipleVariables"                     = 92957
 
 {- *********************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Types/Name/Reader.hs b/compiler/GHC/Types/Name/Reader.hs
index 6f2db7435617..92cf4ac9b972 100644
--- a/compiler/GHC/Types/Name/Reader.hs
+++ b/compiler/GHC/Types/Name/Reader.hs
@@ -45,7 +45,7 @@ module GHC.Types.Name.Reader (
         LocalRdrEnv, emptyLocalRdrEnv, extendLocalRdrEnv, extendLocalRdrEnvList,
         lookupLocalRdrEnv, lookupLocalRdrOcc,
         elemLocalRdrEnv, inLocalRdrEnvScope,
-        localRdrEnvElts, minusLocalRdrEnv,
+        localRdrEnvElts, minusLocalRdrEnv, minusLocalRdrEnvList,
 
         -- * Global mapping of 'RdrName' to 'GlobalRdrElt's
         GlobalRdrEnvX, GlobalRdrEnv, IfGlobalRdrEnv,
@@ -486,6 +486,10 @@ minusLocalRdrEnv :: LocalRdrEnv -> OccEnv a -> LocalRdrEnv
 minusLocalRdrEnv lre@(LRE { lre_env = env }) occs
   = lre { lre_env = minusOccEnv env occs }
 
+minusLocalRdrEnvList :: LocalRdrEnv -> [OccName] -> LocalRdrEnv
+minusLocalRdrEnvList lre@(LRE { lre_env = env }) occs
+  = lre { lre_env = delListFromOccEnv env occs }
+
 {-
 Note [Local bindings with Exact Names]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/Language/Haskell/Syntax/Decls.hs b/compiler/Language/Haskell/Syntax/Decls.hs
index d5948849b4bd..2a369bd7cefb 100644
--- a/compiler/Language/Haskell/Syntax/Decls.hs
+++ b/compiler/Language/Haskell/Syntax/Decls.hs
@@ -49,7 +49,7 @@ module Language.Haskell.Syntax.Decls (
   TyFamInstDecl(..), LTyFamInstDecl,
   TyFamDefltDecl, LTyFamDefltDecl,
   DataFamInstDecl(..), LDataFamInstDecl,
-  FamEqn(..), TyFamInstEqn, LTyFamInstEqn, HsTyPats,
+  FamEqn(..), TyFamInstEqn, LTyFamInstEqn, HsFamEqnPats,
   LClsInstDecl, ClsInstDecl(..),
 
   -- ** Standalone deriving declarations
@@ -1283,8 +1283,12 @@ type LTyFamInstEqn pass = XRec pass (TyFamInstEqn pass)
 
 -- For details on above see Note [exact print annotations] in GHC.Parser.Annotation
 
--- | Haskell Type Patterns
-type HsTyPats pass = [LHsTypeArg pass]
+-- | HsFamEqnPats represents patterns on the left-hand side of a type instance,
+-- e.g. `type instance F @k (a :: k) = a` has patterns `@k` and `(a :: k)`.
+--
+-- HsFamEqnPats used to be called HsTyPats but it was renamed to avoid confusion
+-- with a different notion of type patterns, see #23657.
+type HsFamEqnPats pass = [LHsTypeArg pass]
 
 {- Note [Family instance declaration binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1374,7 +1378,7 @@ data FamEqn pass rhs
        { feqn_ext    :: XCFamEqn pass rhs
        , feqn_tycon  :: LIdP pass
        , feqn_bndrs  :: HsOuterFamEqnTyVarBndrs pass -- ^ Optional quantified type vars
-       , feqn_pats   :: HsTyPats pass
+       , feqn_pats   :: HsFamEqnPats pass
        , feqn_fixity :: LexicalFixity -- ^ Fixity used in the declaration
        , feqn_rhs    :: rhs
        }
diff --git a/compiler/Language/Haskell/Syntax/Extension.hs b/compiler/Language/Haskell/Syntax/Extension.hs
index 0072e60ab630..4069bb8cf00b 100644
--- a/compiler/Language/Haskell/Syntax/Extension.hs
+++ b/compiler/Language/Haskell/Syntax/Extension.hs
@@ -640,6 +640,11 @@ type family XXHsWildCardBndrs  x b
 type family XHsPS x
 type family XXHsPatSigType x
 
+-- -------------------------------------
+-- HsTyPat type families
+type family XHsTP x
+type family XXHsTyPat x
+
 -- -------------------------------------
 -- HsType type families
 type family XForAllTy        x
diff --git a/compiler/Language/Haskell/Syntax/Pat.hs b/compiler/Language/Haskell/Syntax/Pat.hs
index 5e6f12c4b856..8ff31fd8dbeb 100644
--- a/compiler/Language/Haskell/Syntax/Pat.hs
+++ b/compiler/Language/Haskell/Syntax/Pat.hs
@@ -22,7 +22,7 @@ module Language.Haskell.Syntax.Pat (
         Pat(..), LPat,
         ConLikeP,
 
-        HsConPatDetails, hsConPatArgs,
+        HsConPatDetails, hsConPatArgs, hsConPatTyArgs,
         HsConPatTyArg(..),
         HsRecFields(..), HsFieldBind(..), LHsFieldBind,
         HsRecField, LHsRecField,
@@ -233,7 +233,7 @@ type family ConLikeP x
 data HsConPatTyArg p =
   HsConPatTyArg
     !(LHsToken "@" p)
-     (HsPatSigType p)
+     (HsTyPat p)
 
 -- | Haskell Constructor Pattern Details
 type HsConPatDetails p = HsConDetails (HsConPatTyArg (NoGhcTc p)) (LPat p) (HsRecFields p (LPat p))
@@ -243,6 +243,11 @@ hsConPatArgs (PrefixCon _ ps) = ps
 hsConPatArgs (RecCon fs)      = Data.List.map (hfbRHS . unXRec @p) (rec_flds fs)
 hsConPatArgs (InfixCon p1 p2) = [p1,p2]
 
+hsConPatTyArgs :: forall p. HsConPatDetails p -> [HsConPatTyArg (NoGhcTc p)]
+hsConPatTyArgs (PrefixCon tyargs _) = tyargs
+hsConPatTyArgs (RecCon _)           = []
+hsConPatTyArgs (InfixCon _ _)       = []
+
 -- | Haskell Record Fields
 --
 -- HsRecFields is used only for patterns and expressions (not data type
diff --git a/compiler/Language/Haskell/Syntax/Type.hs b/compiler/Language/Haskell/Syntax/Type.hs
index f6947552e104..731df9c3e03d 100644
--- a/compiler/Language/Haskell/Syntax/Type.hs
+++ b/compiler/Language/Haskell/Syntax/Type.hs
@@ -33,6 +33,7 @@ module Language.Haskell.Syntax.Type (
         HsWildCardBndrs(..),
         HsPatSigType(..),
         HsSigType(..), LHsSigType, LHsSigWcType, LHsWcType,
+        HsTyPat(..), LHsTyPat,
         HsTupleSort(..),
         HsContext, LHsContext,
         HsTyLit(..),
@@ -359,7 +360,7 @@ hsQTvExplicit = hsq_explicit
 -- the forall-or-nothing rule. These are used to represent the outermost
 -- quantification in:
 --    * Type signatures (LHsSigType/LHsSigWcType)
---    * Patterns in a type/data family instance (HsTyPats)
+--    * Patterns in a type/data family instance (HsFamEqnPats)
 --
 -- We support two forms:
 --   HsOuterImplicit (implicit quantification, added by renamer)
@@ -448,6 +449,14 @@ type LHsWcType    pass = HsWildCardBndrs pass (LHsType pass)    -- Wildcard only
 -- | Located Haskell Signature Wildcard Type
 type LHsSigWcType pass = HsWildCardBndrs pass (LHsSigType pass) -- Both
 
+data HsTyPat pass
+  = HsTP { hstp_ext  :: XHsTP pass   -- ^ After renamer: 'HsTyPatRn'
+         , hstp_body :: LHsType pass -- ^ Main payload (the type itself)
+    }
+  | XHsTyPat !(XXHsTyPat pass)
+
+type LHsTyPat  pass = XRec pass (HsTyPat pass)
+
 -- | A type signature that obeys the @forall@-or-nothing rule. In other
 -- words, an 'LHsType' that uses an 'HsOuterSigTyVarBndrs' to represent its
 -- outermost type variable quantification.
diff --git a/testsuite/tests/gadt/T18191.stderr b/testsuite/tests/gadt/T18191.stderr
index 8e5662bec311..b1e727278618 100644
--- a/testsuite/tests/gadt/T18191.stderr
+++ b/testsuite/tests/gadt/T18191.stderr
@@ -16,11 +16,13 @@ T18191.hs:15:21: error: [GHC-71492]
     • In the definition of data constructor ‘MkZ1’
 
 T18191.hs:15:31: error: [GHC-89246]
-    Record syntax is illegal here: {unZ1 :: (a, b)}
+    • Record syntax is illegal here: {unZ1 :: (a, b)}
+    • In the definition of data constructor ‘MkZ1’
 
 T18191.hs:16:19: error: [GHC-71492]
     • GADT constructor type signature cannot contain nested ‘forall’s or contexts
     • In the definition of data constructor ‘MkZ2’
 
 T18191.hs:16:27: error: [GHC-89246]
-    Record syntax is illegal here: {unZ1 :: (a, b)}
+    • Record syntax is illegal here: {unZ1 :: (a, b)}
+    • In the definition of data constructor ‘MkZ2’
diff --git a/testsuite/tests/rename/should_compile/T22478a.hs b/testsuite/tests/rename/should_compile/T22478a.hs
new file mode 100644
index 000000000000..2f1d2e1f6afa
--- /dev/null
+++ b/testsuite/tests/rename/should_compile/T22478a.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE LinearTypes #-}
+{-# LANGUAGE UnboxedSums #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module T22478a where
+
+import Data.Kind (Type, Constraint)
+import GHC.Exts (Multiplicity(Many))
+import qualified Language.Haskell.TH as TH
+
+data P (a :: k) where
+  MkP :: forall {k} (a :: k). P a
+
+data T (a :: Type) = MkT
+
+data V a b = MkV
+
+data E = E :+ E | E :* E
+
+infixl 6 :+
+infixl 7 :*
+
+fAppTy :: T (Maybe Int) -> (P Maybe, P Int)
+fAppTy (MkT @(f a)) = (MkP @f, MkP @a)
+
+fAppKindTy :: T (P @(Type -> Constraint) Num) -> (P Type, P Constraint, P Num)
+fAppKindTy (MkT @(P @(k1 -> k2) c)) = (MkP @k1, MkP @k2, MkP @c)
+
+fOpTy :: T (Either Int Bool) -> (P Either, P Int, P Bool)
+fOpTy (MkT @(a `op` b)) = (MkP @op, MkP @a, MkP @b)
+
+fQualTy :: T ((Ord a, Num a) => a) -> (P (Ord a), P (Num a), P a)
+fQualTy (MkT @((c1, c2) => a)) = (MkP @c1, MkP @c2, MkP @a)
+
+fFunTy :: T (Int -> Bool) -> (P Int, P Bool, P Many)
+fFunTy (MkT @(a %m -> b)) = (MkP @a, MkP @b, MkP @m)
+
+fListTy :: T [Int] -> P Int
+fListTy (MkT @[a]) = MkP @a
+
+fTupleTy :: T (Int, Bool) -> (P Int, P Bool)
+fTupleTy (MkT @(a, b)) = (MkP @a, MkP @b)
+
+fSumTy :: P (# Int | Bool #) -> (P Int, P Bool)
+fSumTy (MkP @(# a | b #)) = (MkP @a, MkP @b)
+
+fExplicitListTy :: P '[Int, Bool] -> (P Int, P Bool)
+fExplicitListTy (MkP @'[a, b]) = (MkP @a, MkP @b)
+
+fExplicitTupleTy :: P '(Maybe, Functor) -> (P Maybe, P Functor)
+fExplicitTupleTy (MkP @'(m, f)) = (MkP @m, MkP @f)
+
+fKindSig :: P Maybe -> (P Maybe, P (Type -> Type))
+fKindSig (MkP @(t :: k)) = (MkP @t, MkP @k)
+
+fForallTy :: T (forall a. a -> b) -> P b
+fForallTy (MkT @(forall a. a -> b)) = MkP @b
+
+fIParamTy :: T ((?t :: Type) => Int) -> P Type
+fIParamTy (MkT @((?t :: k) => Int)) = MkP @k
+
+fTyLit :: P "hello" -> ()
+fTyLit (MkP @"hello") = ()
+
+fDependentBind :: P (V k (a :: k)) -> V k a
+fDependentBind (MkP @(V k (a :: k))) = MkV @k @a
+
+fArityCheck :: P (a :* b :+ c :* d) -> ()
+fArityCheck (MkP @(a :* b :+ c :* d)) = ()
+
+fShadowing :: T a -> T b -> T b
+fShadowing (MkT @a) = \(MkT @a) -> MkT @a
+
+fSpliceTy :: T Int -> P Int
+fSpliceTy (MkT @($(TH.varT (TH.mkName "t")))) = MkP @t
+
+fKindSigTwoX :: P (Nothing @(a, a)) -> ()
+fKindSigTwoX (MkP @(Nothing :: Maybe (t, t))) = ()  -- Accepted (multiple occurrences of ‘t’ notwithstanding)
+
+fTypeSigTwoX (MkP :: P (a,a)) = ()                  -- Accepted (multiple occurrences of ‘a’ notwithstanding)
diff --git a/testsuite/tests/rename/should_compile/all.T b/testsuite/tests/rename/should_compile/all.T
index fc4188723bbd..eaf4e30a250c 100644
--- a/testsuite/tests/rename/should_compile/all.T
+++ b/testsuite/tests/rename/should_compile/all.T
@@ -220,3 +220,4 @@ test('ExportWarnings3', extra_files(['ExportWarnings_base.hs', 'ExportWarnings_a
 test('ExportWarnings4', extra_files(['ExportWarnings_base.hs', 'ExportWarnings_aux.hs']), multimod_compile, ['ExportWarnings4', '-v0 -Wno-duplicate-exports -Wx-custom'])
 test('ExportWarnings5', extra_files(['ExportWarnings_base.hs', 'ExportWarnings_aux.hs']), multimod_compile, ['ExportWarnings5', '-v0 -Wno-duplicate-exports -Wx-custom'])
 test('ExportWarnings6', normal, compile, ['-Wincomplete-export-warnings'])
+test('T22478a', req_th, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/T22478b.hs b/testsuite/tests/rename/should_fail/T22478b.hs
new file mode 100644
index 000000000000..67dac9f50f3a
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478b.hs
@@ -0,0 +1,27 @@
+module T22478b where
+
+import Data.Kind (Type)
+
+data P (a :: k) where
+  MkP :: forall {k} (a :: k). P a
+
+data T (a :: Type) = MkT
+
+data V a b = MkV
+
+
+fOutOfOrder :: P (V (a :: k) k) -> V k a
+fOutOfOrder (MkP @(V (a :: k) k)) = MkV @k @a
+
+fBangTy (MkP @(!Int)) = ()
+
+fForAllTyScope :: T (forall a. a -> b) -> P b
+fForAllTyScope (MkT @(forall a. a -> b)) = const @_ @a (MkP @b) undefined
+
+fRecordTy (MkP @{fld :: Int}) = ()
+
+fConflict1 (MkP @(V a a)) = ()
+fConflict2 (x :: a) (MkP @a) = ()
+fConflict3 (MkP @a) (MkP @a) = ()
+fConflict4 (MkV @a @a) = ()
+fConflict5 (MkV @_a @_a) = ()
diff --git a/testsuite/tests/rename/should_fail/T22478b.stderr b/testsuite/tests/rename/should_fail/T22478b.stderr
new file mode 100644
index 000000000000..55e27639dd2b
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478b.stderr
@@ -0,0 +1,48 @@
+
+T22478b.hs:14:14: error: [GHC-10498]
+    • Conflicting definitions for ‘k’
+      Bound at: T22478b.hs:14:14-32
+                T22478b.hs:14:31
+    • In an equation for ‘fOutOfOrder’
+
+T22478b.hs:16:10: error: [GHC-18932]
+    • Unexpected strictness annotation: Int
+      strictness annotation cannot appear nested inside a type
+    • In a type argument in a pattern
+
+T22478b.hs:19:54: error: [GHC-76037]
+    Not in scope: type variable ‘a’
+
+T22478b.hs:21:12: error: [GHC-89246]
+    • Record syntax is illegal here: {fld :: Int}
+    • In a type argument in a pattern
+
+T22478b.hs:23:21: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: T22478b.hs:23:21
+                T22478b.hs:23:23
+    • In an equation for ‘fConflict1’
+
+T22478b.hs:24:13: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: T22478b.hs:24:13-18
+                T22478b.hs:24:27
+    • In an equation for ‘fConflict2’
+
+T22478b.hs:25:18: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: T22478b.hs:25:18
+                T22478b.hs:25:27
+    • In an equation for ‘fConflict3’
+
+T22478b.hs:26:18: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: T22478b.hs:26:18
+                T22478b.hs:26:21
+    • In an equation for ‘fConflict4’
+
+T22478b.hs:27:18: error: [GHC-10498]
+    • Conflicting definitions for ‘_a’
+      Bound at: T22478b.hs:27:18-19
+                T22478b.hs:27:22-23
+    • In an equation for ‘fConflict5’
diff --git a/testsuite/tests/rename/should_fail/T22478d.hs b/testsuite/tests/rename/should_fail/T22478d.hs
new file mode 100644
index 000000000000..0fd4c028045d
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478d.hs
@@ -0,0 +1,14 @@
+{-# OPTIONS_GHC -Werror=name-shadowing #-}
+
+module T22478d where
+
+import Data.Kind (Type)
+
+data T (a :: Type) = MkT
+
+fShadowing1 (MkT @a) = g (MkT @a)
+  where
+    g (MkT @a) = ()
+
+fShadowing2 :: T a -> T b -> T b
+fShadowing2 (MkT @a) = \(MkT @a) -> MkT @a
diff --git a/testsuite/tests/rename/should_fail/T22478d.stderr b/testsuite/tests/rename/should_fail/T22478d.stderr
new file mode 100644
index 000000000000..26561f4aa486
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478d.stderr
@@ -0,0 +1,8 @@
+
+T22478d.hs:11:13: error: [GHC-63397] [-Wname-shadowing (in -Wall), Werror=name-shadowing]
+    This binding for ‘a’ shadows the existing binding
+      bound at T22478d.hs:9:19
+
+T22478d.hs:14:31: error: [GHC-63397] [-Wname-shadowing (in -Wall), Werror=name-shadowing]
+    This binding for ‘a’ shadows the existing binding
+      bound at T22478d.hs:14:19
diff --git a/testsuite/tests/rename/should_fail/T22478e.hs b/testsuite/tests/rename/should_fail/T22478e.hs
new file mode 100644
index 000000000000..0d90014b5b69
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478e.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE NoTypeApplications, NoKindSignatures, NoDataKinds #-}
+module T where
+
+data Proxy a = P
+
+f (P @[a,b])    = ()
+g (P @1)        = ()
+h (P @(t @k))   = ()
+j (P @(t :: k)) = ()
+k (P @('(a,b))) = ()
+l (P @"str")    = ()
+d (P @'c')      = ()
diff --git a/testsuite/tests/rename/should_fail/T22478e.stderr b/testsuite/tests/rename/should_fail/T22478e.stderr
new file mode 100644
index 000000000000..22b2e8b46ddb
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478e.stderr
@@ -0,0 +1,29 @@
+
+T22478e.hs:6:4: error: [GHC-68567]
+    Illegal type: ‘[a, b]’
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22478e.hs:7:4: error: [GHC-68567]
+    Illegal type: ‘1’
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22478e.hs:8:4: error: [GHC-23482]
+    Illegal visible kind application: @k
+    Suggested fix: Perhaps you intended to use TypeApplications
+
+T22478e.hs:9:13: error: [GHC-49378]
+    • Illegal kind signature ‘k’
+    • In a type argument in a pattern
+    Suggested fix: Perhaps you intended to use KindSignatures
+
+T22478e.hs:10:4: error: [GHC-68567]
+    Illegal type: ‘'(a, b)’
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22478e.hs:11:4: error: [GHC-68567]
+    Illegal type: ‘"str"’
+    Suggested fix: Perhaps you intended to use DataKinds
+
+T22478e.hs:12:4: error: [GHC-68567]
+    Illegal type: ‘'c'’
+    Suggested fix: Perhaps you intended to use DataKinds
diff --git a/testsuite/tests/rename/should_fail/T22478f.hs b/testsuite/tests/rename/should_fail/T22478f.hs
new file mode 100644
index 000000000000..ed1593869136
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478f.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -Werror=unticked-promoted-constructors #-}
+module T where
+
+data Proxy a = P
+data Op a b = a :- b
+
+f (P @[a,b])     = ()
+g (P @(a :- b)) = ()
diff --git a/testsuite/tests/rename/should_fail/T22478f.stderr b/testsuite/tests/rename/should_fail/T22478f.stderr
new file mode 100644
index 000000000000..91bc2a37689f
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T22478f.stderr
@@ -0,0 +1,8 @@
+
+T22478f.hs:8:4: error: [GHC-49957] [-Wunticked-promoted-constructors, Werror=unticked-promoted-constructors]
+    Unticked promoted list.
+    Suggested fix: Add a promotion tick, e.g. '[x,y,z].
+
+T22478f.hs:9:4: error: [GHC-49957] [-Wunticked-promoted-constructors, Werror=unticked-promoted-constructors]
+    Unticked promoted constructor: :-
+    Suggested fix: Use ':- instead of :-
diff --git a/testsuite/tests/rename/should_fail/T7943.stderr b/testsuite/tests/rename/should_fail/T7943.stderr
index 352d4c1f4064..bf9b267ffaf7 100644
--- a/testsuite/tests/rename/should_fail/T7943.stderr
+++ b/testsuite/tests/rename/should_fail/T7943.stderr
@@ -1,3 +1,4 @@
 
 T7943.hs:4:21: error: [GHC-89246]
-    Record syntax is illegal here: {bar :: String}
+    • Record syntax is illegal here: {bar :: String}
+    • In the definition of data constructor ‘B’
diff --git a/testsuite/tests/rename/should_fail/T9077.stderr b/testsuite/tests/rename/should_fail/T9077.stderr
index c20800b12f9d..7d4fb31dbf37 100644
--- a/testsuite/tests/rename/should_fail/T9077.stderr
+++ b/testsuite/tests/rename/should_fail/T9077.stderr
@@ -1,2 +1,4 @@
 
-T9077.hs:3:12: error: [GHC-89246] Record syntax is illegal here: {}
+T9077.hs:3:12: error: [GHC-89246]
+    • Record syntax is illegal here: {}
+    • In the type signature for ‘main’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 2eccda4e9e61..0ae4848a2ea1 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -205,3 +205,7 @@ test('T16635b', normal, compile_fail, [''])
 test('T16635c', normal, compile_fail, [''])
 test('T23512a', normal, compile_fail, [''])
 test('DifferentExportWarnings', normal, multimod_compile_fail, ['DifferentExportWarnings', '-v0'])
+test('T22478b', normal, compile_fail, [''])
+test('T22478d', normal, compile_fail, [''])
+test('T22478e', normal, compile_fail, [''])
+test('T22478f', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T18986a.hs b/testsuite/tests/typecheck/should_compile/T18986a.hs
new file mode 100644
index 000000000000..91a57833b4c6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18986a.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, RankNTypes, PolyKinds, TypeApplications,
+             ScopedTypeVariables, TypeFamilies #-}
+
+module T18986a where
+
+import Data.Kind (Type)
+
+data T where
+  MkT :: forall (f :: forall k. k -> Type).
+    f Int -> f Maybe -> T
+
+type family Id a where
+  Id a = a
+
+k1 :: T -> ()
+k1 (MkT @(f :: forall k . k -> Type) (x :: f Int) (y :: f Maybe)) = ()
+
+k2 :: T -> ()
+k2 (MkT @f (x :: f Int) (y :: f Maybe)) = ()
+
+k3 :: T -> ()
+k3 (MkT @(f :: forall k . k -> Type) (x :: Id f (Id Int)) (y :: f Maybe)) = ()
diff --git a/testsuite/tests/typecheck/should_compile/T18986b.hs b/testsuite/tests/typecheck/should_compile/T18986b.hs
new file mode 100644
index 000000000000..be97a020ab88
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18986b.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE GADTs, RankNTypes, PolyKinds, TypeApplications,
+             ScopedTypeVariables, TypeFamilies, DataKinds #-}
+
+module T18986b where
+
+import Data.Kind (Type)
+import Data.Type.Equality
+import Data.Proxy
+
+type T :: (forall k. k -> Type) -> k1 -> k2 -> Type
+data T f a b where
+  MkT :: forall (f :: forall k. k -> Type) a b.
+    f a -> f b -> T f a b
+
+type family Id a where
+  Id a = a
+
+k1 :: forall (f :: forall k. k -> Type). T f Int Maybe -> T f Either True -> f :~: f
+k1
+  (MkT @(f :: forall k . k -> Type) (x :: f Int) (y :: f Maybe))
+  (MkT @(g :: forall k . k -> Type) (a :: f Either) (b :: g True))
+  = Refl :: f :~: g
+
+k2 :: forall (f :: forall k. k -> Type). T f Int Maybe -> T f Either True -> f :~: f
+k2
+  (MkT @f (x :: f Int) (y :: f Maybe))
+  (MkT @g (a :: f Either) (b :: g True))
+  = Refl :: f :~: g
+
+k3 :: forall (f :: forall k. k -> Type). T f Int Maybe -> T f Either True -> f :~: f
+k3
+  (MkT @(f :: forall k . k -> Type) (x :: Id f (Id Int)) (y :: Id f (Id Maybe)))
+  (MkT @g (a :: Id f (Id Either)) (b :: Id g (Id True)))
+  = Refl :: Id f :~: Id g
+
+k4 :: T Proxy Int Maybe -> T Proxy Either True -> Proxy :~: Proxy
+k4
+  (MkT @f (x :: f Int) (y :: f Maybe))
+  (MkT @g (a :: f Either) (b :: g True))
+  = Refl :: f :~: g
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index edcc812181e5..358bf2ce5932 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -886,4 +886,5 @@ test('T22560e', normal, compile, [''])
 test('T23514b', normal, compile, [''])
 test('T23514c', normal, compile, [''])
 test('T22537', normal, compile, [''])
-
+test('T18986a', normal, compile, [''])
+test('T18986b', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T22478c.hs b/testsuite/tests/typecheck/should_fail/T22478c.hs
new file mode 100644
index 000000000000..2bda42955043
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22478c.hs
@@ -0,0 +1,11 @@
+module T22478c where
+
+
+import Data.Kind (Type, Constraint)
+import GHC.Exts (Multiplicity(Many))
+
+data T (a :: Type) = MkT
+
+
+fShadowing :: T a -> T b -> T a
+fShadowing (MkT @a) = \(MkT @a) -> MkT @a
diff --git a/testsuite/tests/typecheck/should_fail/T22478c.stderr b/testsuite/tests/typecheck/should_fail/T22478c.stderr
new file mode 100644
index 000000000000..25697fc0cea1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T22478c.stderr
@@ -0,0 +1,19 @@
+
+T22478c.hs:11:36: error: [GHC-25897]
+    • Couldn't match type ‘b’ with ‘a’
+      Expected: T a
+        Actual: T b
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          fShadowing :: forall a b. T a -> T b -> T a
+        at T22478c.hs:10:1-31
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          fShadowing :: forall a b. T a -> T b -> T a
+        at T22478c.hs:10:1-31
+    • In the expression: MkT @a
+      In the expression: \ (MkT @a) -> MkT @a
+      In an equation for ‘fShadowing’:
+          fShadowing (MkT @a) = \ (MkT @a) -> MkT @a
+    • Relevant bindings include
+        fShadowing :: T a -> T b -> T a (bound at T22478c.hs:11:1)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
index 757ed8f18369..c025dd452e59 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
@@ -1,4 +1,6 @@
 
-TyAppPat_NonlinearMultiAppPat.hs:13:6: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiAppPat.hs:13:13: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiAppPat.hs:13:13
+                TyAppPat_NonlinearMultiAppPat.hs:13:16
+    • In an equation for ‘foo’
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
index 3641e4b39df9..c37ecfbe3526 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
@@ -1,16 +1,24 @@
 
-TyAppPat_NonlinearMultiPat.hs:10:19: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:10:15: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:10:15
+                TyAppPat_NonlinearMultiPat.hs:10:28
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:11:18: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:11:12: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:11:12
+                TyAppPat_NonlinearMultiPat.hs:11:27
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:12:19: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:12:15: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:12:15
+                TyAppPat_NonlinearMultiPat.hs:12:25
+    • In an equation for ‘foo’
 
-TyAppPat_NonlinearMultiPat.hs:13:18: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_NonlinearMultiPat.hs:13:12: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearMultiPat.hs:13:12
+                TyAppPat_NonlinearMultiPat.hs:13:24
+    • In an equation for ‘foo’
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
index c0118ccf82ac..e3786c002173 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
@@ -1,3 +1,6 @@
 
-TyAppPat_NonlinearSinglePat.hs:13:6: error: [GHC-92957]
-    Variable `a' would be bound multiple times by a type argument.
+TyAppPat_NonlinearSinglePat.hs:13:14: error: [GHC-10498]
+    • Conflicting definitions for ‘a’
+      Bound at: TyAppPat_NonlinearSinglePat.hs:13:14
+                TyAppPat_NonlinearSinglePat.hs:13:16
+    • In an equation for ‘foo’
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
index 6906ed627b2d..98101c60c296 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Werror=name-shadowing #-}
 
 module Main where
 
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
index eea80116d812..a94d6e2bcabb 100644
--- a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
@@ -1,8 +1,8 @@
 
-TyAppPat_ScopedTyVarConflict.hs:10:6: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_ScopedTyVarConflict.hs:11:15: error: [GHC-63397] [-Wname-shadowing (in -Wall), Werror=name-shadowing]
+    This binding for ‘a’ shadows the existing binding
+      bound at TyAppPat_ScopedTyVarConflict.hs:10:15
 
-TyAppPat_ScopedTyVarConflict.hs:11:6: error: [GHC-69710]
-    Type variable ‘a’ is already in scope.
-    Type applications in patterns must bind fresh variables, without shadowing.
+TyAppPat_ScopedTyVarConflict.hs:12:12: error: [GHC-63397] [-Wname-shadowing (in -Wall), Werror=name-shadowing]
+    This binding for ‘a’ shadows the existing binding
+      bound at TyAppPat_ScopedTyVarConflict.hs:10:15
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 93c5849c82dc..406fffb6ab33 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -698,3 +698,4 @@ test('VisFlag4', normal, compile_fail, [''])
 test('VisFlag5', normal, compile_fail, [''])
 test('T22684', normal, compile_fail, [''])
 test('T23514a', normal, compile_fail, [''])
+test('T22478c', normal, compile_fail, [''])
diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs
index 0bca51750718..7cd8d18d994d 100644
--- a/utils/check-exact/ExactPrint.hs
+++ b/utils/check-exact/ExactPrint.hs
@@ -1624,7 +1624,7 @@ exactDataFamInstDecl an top_lvl
            -> EP w m ( EpAnn [AddEpAnn]
                      , LocatedN RdrName
                      , HsOuterTyVarBndrs () GhcPs
-                     , HsTyPats GhcPs
+                     , HsFamEqnPats GhcPs
                      , Maybe (LHsContext GhcPs))
     pp_hdr mctxt = do
       an0 <- case top_lvl of
@@ -1944,13 +1944,13 @@ exactHsFamInstLHS ::
    => EpAnn [AddEpAnn]
    -> LocatedN RdrName
    -> HsOuterTyVarBndrs () GhcPs
-   -> HsTyPats GhcPs
+   -> HsFamEqnPats GhcPs
    -> LexicalFixity
    -> Maybe (LHsContext GhcPs)
    -> EP w m ( EpAnn [AddEpAnn]
              , LocatedN RdrName
              , HsOuterTyVarBndrs () GhcPs
-             , HsTyPats GhcPs, Maybe (LHsContext GhcPs))
+             , HsFamEqnPats GhcPs, Maybe (LHsContext GhcPs))
 exactHsFamInstLHS an thing bndrs typats fixity mb_ctxt = do
   an0 <- markEpAnnL an lidl AnnForall
   bndrs' <- markAnnotated bndrs
@@ -1960,7 +1960,7 @@ exactHsFamInstLHS an thing bndrs typats fixity mb_ctxt = do
   return (an2, thing', bndrs', typats', mb_ctxt')
   where
     exact_pats :: (Monad m, Monoid w)
-      => EpAnn [AddEpAnn] -> HsTyPats GhcPs -> EP w m (EpAnn [AddEpAnn], LocatedN RdrName, HsTyPats GhcPs)
+      => EpAnn [AddEpAnn] -> HsFamEqnPats GhcPs -> EP w m (EpAnn [AddEpAnn], LocatedN RdrName, HsFamEqnPats GhcPs)
     exact_pats an' (patl:patr:pats)
       | Infix <- fixity
       = let exact_op_app = do
@@ -4680,6 +4680,14 @@ instance ExactPrint (HsPatSigType GhcPs) where
     ty' <- markAnnotated ty
     return (HsPS an ty')
 
+instance ExactPrint (HsTyPat GhcPs) where
+  getAnnotationEntry = const NoEntryVal
+  setAnnotationAnchor a _ _ = a
+
+  exact (HsTP an ty) = do
+    ty' <- markAnnotated ty
+    return (HsTP an ty')
+
 -- ---------------------------------------------------------------------
 
 instance ExactPrint (HsOverLit GhcPs) where
-- 
GitLab