diff --git a/compiler/GHC/Hs/Binds.hs b/compiler/GHC/Hs/Binds.hs
index 41db2d5f85bdffe8f33b887f49c881b2abdd0b95..270dc97364d189de64238805e89856cf55d16b67 100644
--- a/compiler/GHC/Hs/Binds.hs
+++ b/compiler/GHC/Hs/Binds.hs
@@ -51,6 +51,7 @@ import GHC.Utils.Panic
 import Data.Data hiding ( Fixity )
 import Data.List hiding ( foldr )
 import Data.Function
+import Data.Void
 
 {-
 ************************************************************************
@@ -766,7 +767,7 @@ instance (OutputableBndrId l, OutputableBndrId r,
 
       ppr_details = case details of
           InfixCon v1 v2 -> hsep [ppr v1, pprInfixOcc psyn, ppr v2]
-          PrefixCon vs   -> hsep (pprPrefixOcc psyn : map ppr vs)
+          PrefixCon _ vs -> hsep (pprPrefixOcc psyn : map ppr vs)
           RecCon vs      -> pprPrefixOcc psyn
                             <> braces (sep (punctuate comma (map ppr vs)))
 
@@ -1229,7 +1230,9 @@ pprMinimalSig (L _ bf) = ppr (fmap unLoc bf)
 -}
 
 -- | Haskell Pattern Synonym Details
-type HsPatSynDetails pass = HsConDetails (LIdP pass) [RecordPatSynField (LIdP pass)]
+type HsPatSynDetails pass = HsConDetails Void (LIdP pass) [RecordPatSynField (LIdP pass)]
+-- The Void argument to HsConDetails here is a reflection of the fact that
+-- type applications are not allowed in declarations of pattern synonyms at present.
 
 -- See Note [Record PatSyn Fields]
 -- | Record Pattern Synonym Field
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index dcb810ed7ebac93660421ba17271d8938a400836..882303373fe6ef9d6aed1a071fd8908d95c4902a 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -128,6 +128,7 @@ import GHC.Unit.Module.Warnings
 import GHC.Data.Bag
 import GHC.Data.Maybe
 import Data.Data        hiding (TyCon,Fixity, Infix)
+import Data.Void
 
 {-
 ************************************************************************
@@ -1617,7 +1618,9 @@ or contexts in two parts:
 
 -- | The arguments in a Haskell98-style data constructor.
 type HsConDeclH98Details pass
-   = HsConDetails (HsScaled pass (LBangType pass)) (XRec pass [LConDeclField pass])
+   = HsConDetails Void (HsScaled pass (LBangType pass)) (XRec pass [LConDeclField pass])
+-- The Void argument to HsConDetails here is a reflection of the fact that
+-- type applications are not allowed in data constructor declarations.
 
 -- | The arguments in a GADT constructor. Unlike Haskell98-style constructors,
 -- GADT constructors cannot be declared with infix syntax. As a result, we do
@@ -1716,8 +1719,8 @@ pprConDecl (ConDeclH98 { con_name = L _ con
     ppr_details (InfixCon t1 t2) = hsep [ppr (hsScaledThing t1),
                                          pprInfixOcc con,
                                          ppr (hsScaledThing t2)]
-    ppr_details (PrefixCon tys)  = hsep (pprPrefixOcc con
-                                   : map (pprHsType . unLoc . hsScaledThing) tys)
+    ppr_details (PrefixCon _ tys) = hsep (pprPrefixOcc con
+                                    : map (pprHsType . unLoc . hsScaledThing) tys)
     ppr_details (RecCon fields)  = pprPrefixOcc con
                                  <+> pprConDeclFields (unLoc fields)
     cxt = fromMaybe noLHsContext mcxt
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index 3033806ddd1b49e094248a1f0f3f711f3b74c166..a1d59699c53198c4aa43d50b0d6e20eef3066c5d 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -317,10 +317,10 @@ type instance ConLikeP GhcTc = ConLike
 
 
 -- | Haskell Constructor Pattern Details
-type HsConPatDetails p = HsConDetails (LPat p) (HsRecFields p (LPat p))
+type HsConPatDetails p = HsConDetails (HsPatSigType (NoGhcTc p)) (LPat p) (HsRecFields p (LPat p))
 
 hsConPatArgs :: HsConPatDetails p -> [LPat p]
-hsConPatArgs (PrefixCon ps)   = ps
+hsConPatArgs (PrefixCon _ ps) = ps
 hsConPatArgs (RecCon fs)      = map (hsRecFieldArg . unLoc) (rec_flds fs)
 hsConPatArgs (InfixCon p1 p2) = [p1,p2]
 
@@ -580,10 +580,10 @@ pprPat (ConPat { pat_con = con
                }
        )
   = case ghcPass @p of
-      GhcPs -> pprUserCon (unLoc con) details
-      GhcRn -> pprUserCon (unLoc con) details
+      GhcPs -> regular
+      GhcRn -> regular
       GhcTc -> sdocOption sdocPrintTypecheckerElaboration $ \case
-        False -> pprUserCon (unLoc con) details
+        False -> regular
         True  ->
           -- Tiresome; in 'GHC.Tc.Gen.Bind.tcRhs' we print out a typechecked Pat in an
           -- error message, and we want to make sure it prints nicely
@@ -595,6 +595,9 @@ pprPat (ConPat { pat_con = con
                        , cpt_dicts = dicts
                        , cpt_binds = binds
                        } = ext
+  where
+    regular :: OutputableBndr (ConLikeP (GhcPass p)) => SDoc
+    regular = pprUserCon (unLoc con) details
 pprPat (XPat ext) = case ghcPass @p of
 #if __GLASGOW_HASKELL__ < 811
   GhcPs -> noExtCon ext
@@ -611,12 +614,14 @@ pprUserCon :: (OutputableBndr con, OutputableBndrId p)
 pprUserCon c (InfixCon p1 p2) = ppr p1 <+> pprInfixOcc c <+> ppr p2
 pprUserCon c details          = pprPrefixOcc c <+> pprConArgs details
 
+
 pprConArgs :: (OutputableBndrId p)
            => HsConPatDetails (GhcPass p) -> SDoc
-pprConArgs (PrefixCon pats) = fsep (map (pprParendLPat appPrec) pats)
-pprConArgs (InfixCon p1 p2) = sep [ pprParendLPat appPrec p1
-                                  , pprParendLPat appPrec p2 ]
-pprConArgs (RecCon rpats)   = ppr rpats
+pprConArgs (PrefixCon ts pats) = fsep (pprTyArgs ts : map (pprParendLPat appPrec) pats)
+  where pprTyArgs tyargs = fsep (map (\ty -> char '@' <> ppr ty) tyargs)
+pprConArgs (InfixCon p1 p2)    = sep [ pprParendLPat appPrec p1
+                                     , pprParendLPat appPrec p2 ]
+pprConArgs (RecCon rpats)      = ppr rpats
 
 instance (Outputable arg)
       => Outputable (HsRecFields p arg) where
@@ -647,7 +652,7 @@ mkPrefixConPat :: DataCon ->
 -- Make a vanilla Prefix constructor pattern
 mkPrefixConPat dc pats tys
   = noLoc $ ConPat { pat_con = noLoc (RealDataCon dc)
-                   , pat_args = PrefixCon pats
+                   , pat_args = PrefixCon [] pats
                    , pat_con_ext = ConPatTc
                      { cpt_tvs = []
                      , cpt_dicts = []
@@ -837,7 +842,7 @@ patNeedsParens p = go
     go :: Pat (GhcPass p) -> Bool
     go (NPlusKPat {})    = p > opPrec
     go (SplicePat {})    = False
-    go (ConPat { pat_args = ds})
+    go (ConPat { pat_args = ds })
                          = conPatNeedsParens p ds
     go (SigPat {})       = p >= sigPrec
     go (ViewPat {})      = True
@@ -867,12 +872,12 @@ patNeedsParens p = go
 
 -- | @'conPatNeedsParens' p cp@ returns 'True' if the constructor patterns @cp@
 -- needs parentheses under precedence @p@.
-conPatNeedsParens :: PprPrec -> HsConDetails a b -> Bool
+conPatNeedsParens :: PprPrec -> HsConDetails t a b -> Bool
 conPatNeedsParens p = go
   where
-    go (PrefixCon args) = p >= appPrec && not (null args)
-    go (InfixCon {})    = p >= opPrec
-    go (RecCon {})      = False
+    go (PrefixCon ts args) = p >= appPrec && (not (null args) || not (null ts))
+    go (InfixCon {})       = p >= opPrec -- type args should be empty in this case
+    go (RecCon {})         = False
 
 -- | @'parenthesizePat' p pat@ checks if @'patNeedsParens' p pat@ is true, and
 -- if so, surrounds @pat@ with a 'ParPat'. Otherwise, it simply returns @pat@.
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index ad950883f4c5106f6ad8159c70477d1389a34c14..dde27857ec19c3f8afe7b784304a1dc106b103b3 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -46,7 +46,7 @@ module GHC.Hs.Type (
 
         ConDeclField(..), LConDeclField, pprConDeclFields,
 
-        HsConDetails(..),
+        HsConDetails(..), noTypeArgs,
 
         FieldOcc(..), LFieldOcc, mkFieldOcc,
         AmbiguousFieldOcc(..), mkAmbiguousFieldOcc,
@@ -107,10 +107,11 @@ import GHC.Types.SrcLoc
 import GHC.Utils.Outputable
 import GHC.Data.FastString
 import GHC.Utils.Misc ( count )
+import GHC.Parser.Annotation
 
 import Data.Data hiding ( Fixity, Prefix, Infix )
 import Data.Maybe
-import GHC.Parser.Annotation
+import Data.Void
 
 {-
 ************************************************************************
@@ -505,7 +506,7 @@ type instance XHsWC              GhcPs b = NoExtField
 type instance XHsWC              GhcRn b = [Name]
 type instance XHsWC              GhcTc b = [Name]
 
-type instance XXHsWildCardBndrs  (GhcPass _) b = NoExtCon
+type instance XXHsWildCardBndrs (GhcPass _) _ = NoExtCon
 
 -- | Types that can appear in pattern signatures, as well as the signatures for
 -- term-level binders in RULES.
@@ -1333,17 +1334,22 @@ instance OutputableBndrId p
 -- a separate data type entirely (see 'HsConDeclGADTDetails' in
 -- "GHC.Hs.Decls"). This is because GADT constructors cannot be declared with
 -- infix syntax, unlike the concepts above (#18844).
-data HsConDetails arg rec
-  = PrefixCon [arg]             -- C p1 p2 p3
+data HsConDetails tyarg arg rec
+  = PrefixCon [tyarg] [arg]     -- C @t1 @t2 p1 p2 p3
   | RecCon    rec               -- C { x = p1, y = p2 }
   | InfixCon  arg arg           -- p1 `C` p2
   deriving Data
 
-instance (Outputable arg, Outputable rec)
-         => Outputable (HsConDetails arg rec) where
-  ppr (PrefixCon args) = text "PrefixCon" <+> ppr args
-  ppr (RecCon rec)     = text "RecCon:" <+> ppr rec
-  ppr (InfixCon l r)   = text "InfixCon:" <+> ppr [l, r]
+-- | An empty list that can be used to indicate that there are no
+-- type arguments allowed in cases where HsConDetails is applied to Void.
+noTypeArgs :: [Void]
+noTypeArgs = []
+
+instance (Outputable tyarg, Outputable arg, Outputable rec)
+         => Outputable (HsConDetails tyarg arg rec) where
+  ppr (PrefixCon tyargs args) = text "PrefixCon:" <+> hsep (map (\t -> text "@" <> ppr t) tyargs) <+> ppr args
+  ppr (RecCon rec)            = text "RecCon:" <+> ppr rec
+  ppr (InfixCon l r)          = text "InfixCon:" <+> ppr [l, r]
 
 {-
 Note [ConDeclField passs]
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index e530110cda2c380a9e164aac7d500e3fca5b2629..0051eaa2c97016a1a434103da2da65c3423e62f9 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -480,28 +480,28 @@ nlConPat :: RdrName -> [LPat GhcPs] -> LPat GhcPs
 nlConPat con pats = noLoc $ ConPat
   { pat_con_ext = noExtField
   , pat_con = noLoc con
-  , pat_args = PrefixCon (map (parenthesizePat appPrec) pats)
+  , pat_args = PrefixCon [] (map (parenthesizePat appPrec) pats)
   }
 
 nlConPatName :: Name -> [LPat GhcRn] -> LPat GhcRn
 nlConPatName con pats = noLoc $ ConPat
   { pat_con_ext = noExtField
   , pat_con = noLoc con
-  , pat_args = PrefixCon (map (parenthesizePat appPrec) pats)
+  , pat_args = PrefixCon [] (map (parenthesizePat appPrec) pats)
   }
 
 nlNullaryConPat :: RdrName -> LPat GhcPs
 nlNullaryConPat con = noLoc $ ConPat
   { pat_con_ext = noExtField
   , pat_con = noLoc con
-  , pat_args = PrefixCon []
+  , pat_args = PrefixCon [] []
   }
 
 nlWildConPat :: DataCon -> LPat GhcPs
 nlWildConPat con = noLoc $ ConPat
   { pat_con_ext = noExtField
   , pat_con = noLoc $ getRdrName con
-  , pat_args = PrefixCon $
+  , pat_args = PrefixCon [] $
      replicate (dataConSourceArity con)
                nlWildPat
   }
@@ -1396,7 +1396,7 @@ lPatImplicits = hs_lpat
     hs_pat _ = []
 
     details :: Located Name -> HsConPatDetails GhcRn -> [(SrcSpan, [Name])]
-    details _ (PrefixCon ps)   = hs_lpats ps
+    details _ (PrefixCon _ ps) = hs_lpats ps
     details n (RecCon fs)      =
       [(err_loc, collectPatsBinders implicit_pats) | Just{} <- [rec_dotdot fs] ]
         ++ hs_lpats explicit_pats
diff --git a/compiler/GHC/HsToCore/Docs.hs b/compiler/GHC/HsToCore/Docs.hs
index 72e4fe99c3cf0ba0a9734f408f5181369f0785a7..0f80c61d656a41cbea91d994b031aff9b68ba73e 100644
--- a/compiler/GHC/HsToCore/Docs.hs
+++ b/compiler/GHC/HsToCore/Docs.hs
@@ -220,7 +220,7 @@ conArgDocs (ConDeclGADT{con_g_args = args, con_res_ty = res_ty}) =
 
 h98ConArgDocs :: HsConDeclH98Details GhcRn -> Map Int HsDocString
 h98ConArgDocs con_args = case con_args of
-  PrefixCon args     -> con_arg_docs 0 $ map (unLoc . hsScaledThing) args
+  PrefixCon _ args   -> con_arg_docs 0 $ map (unLoc . hsScaledThing) args
   InfixCon arg1 arg2 -> con_arg_docs 0 [ unLoc (hsScaledThing arg1)
                                        , unLoc (hsScaledThing arg2) ]
   RecCon _           -> M.empty
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index c1479d7c9a9a63cb3e3f8d431feaf68df5ac276d..c7eeaec5863af90cb7d6c4a58ab270c3d8dffba7 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -822,7 +822,7 @@ dsExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = fields
                  req_wrap = dict_req_wrap <.> mkWpTyApps in_inst_tys
 
                  pat = noLoc $ ConPat { pat_con = noLoc con
-                                      , pat_args = PrefixCon $ map nlVarPat arg_ids
+                                      , pat_args = PrefixCon [] $ map nlVarPat arg_ids
                                       , pat_con_ext = ConPatTc
                                         { cpt_tvs = ex_tvs
                                         , cpt_dicts = eqs_vars ++ theta_vars
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index 12c9a49278c8778d0aa5db26d127312b531a88fa..bd48a1902429d47546216336154cfe66452e80b3 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -573,9 +573,9 @@ push_bang_into_newtype_arg :: SrcSpan
                            -> HsConPatDetails GhcTc -> HsConPatDetails GhcTc
 -- See Note [Bang patterns and newtypes]
 -- We are transforming   !(N p)   into   (N !p)
-push_bang_into_newtype_arg l _ty (PrefixCon (arg:args))
+push_bang_into_newtype_arg l _ty (PrefixCon ts (arg:args))
   = ASSERT( null args)
-    PrefixCon [L l (BangPat noExtField arg)]
+    PrefixCon ts [L l (BangPat noExtField arg)]
 push_bang_into_newtype_arg l _ty (RecCon rf)
   | HsRecFields { rec_flds = L lf fld : flds } <- rf
   , HsRecField { hsRecFieldArg = arg } <- fld
@@ -584,7 +584,7 @@ push_bang_into_newtype_arg l _ty (RecCon rf)
                                            = L l (BangPat noExtField arg) })] })
 push_bang_into_newtype_arg l ty (RecCon rf) -- If a user writes !(T {})
   | HsRecFields { rec_flds = [] } <- rf
-  = PrefixCon [L l (BangPat noExtField (noLoc (WildPat ty)))]
+  = PrefixCon [] [L l (BangPat noExtField (noLoc (WildPat ty)))]
 push_bang_into_newtype_arg _ _ cd
   = pprPanic "push_bang_into_newtype_arg" (pprConArgs cd)
 
diff --git a/compiler/GHC/HsToCore/Match/Constructor.hs b/compiler/GHC/HsToCore/Match/Constructor.hs
index ca6ad7f483a5a53ac9ee93c2ad6e7b50e45bbda7..39817044cc4b870a288dff4393e6915fb1eec0b7 100644
--- a/compiler/GHC/HsToCore/Match/Constructor.hs
+++ b/compiler/GHC/HsToCore/Match/Constructor.hs
@@ -248,7 +248,7 @@ same_fields flds1 flds2
 selectConMatchVars :: [Scaled Type] -> ConArgPats -> DsM [Id]
 selectConMatchVars arg_tys con = case con of
                                    (RecCon {}) -> newSysLocalsDsNoLP arg_tys
-                                   (PrefixCon ps) -> selectMatchVars (zipMults arg_tys ps)
+                                   (PrefixCon _ ps) -> selectMatchVars (zipMults arg_tys ps)
                                    (InfixCon p1 p2) -> selectMatchVars (zipMults arg_tys [p1, p2])
   where
     zipMults = zipWithEqual "selectConMatchVar" (\a b -> (scaledMult a, unLoc b))
@@ -258,7 +258,7 @@ conArgPats :: [Scaled Type]-- Instantiated argument types
                           -- are probably never looked at anyway
            -> ConArgPats
            -> [Pat GhcTc]
-conArgPats _arg_tys (PrefixCon ps)   = map unLoc ps
+conArgPats _arg_tys (PrefixCon _ ps) = map unLoc ps
 conArgPats _arg_tys (InfixCon p1 p2) = [unLoc p1, unLoc p2]
 conArgPats  arg_tys (RecCon (HsRecFields { rec_flds = rpats }))
   | null rpats = map WildPat (map scaledThing arg_tys)
diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs
index 98b23dab25cb5c4cdd4bc354d30aa0e4caffad09..1abe0fc9dc7123e5bd949654256726d04d85faa4 100644
--- a/compiler/GHC/HsToCore/Pmc/Desugar.hs
+++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs
@@ -255,7 +255,7 @@ desugarListPat x pats = do
 desugarConPatOut :: Id -> ConLike -> [Type] -> [TyVar]
                  -> [EvVar] -> HsConPatDetails GhcTc -> DsM [PmGrd]
 desugarConPatOut x con univ_tys ex_tvs dicts = \case
-    PrefixCon ps                 -> go_field_pats (zip [0..] ps)
+    PrefixCon _ ps               -> go_field_pats (zip [0..] ps)
     InfixCon  p1 p2              -> go_field_pats (zip [0..] [p1,p2])
     RecCon    (HsRecFields fs _) -> go_field_pats (rec_field_ps fs)
   where
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index 7f2d0b5d854e6216c221121a1516b83b9e50dfe0..7f675e8253d2bb384641685d1e4e1e2fc16f9d01 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1884,7 +1884,7 @@ rep_bind (L loc (PatSynBind _ (PSB { psb_id   = syn
     -- their pattern-only bound right hand sides have different names,
     -- we want to treat them the same in TH. This is the reason why we
     -- need an adjusted mkGenArgSyms in the `RecCon` case below.
-    mkGenArgSyms (PrefixCon args)     = mkGenSyms (map unLoc args)
+    mkGenArgSyms (PrefixCon _ args)   = mkGenSyms (map unLoc args)
     mkGenArgSyms (InfixCon arg1 arg2) = mkGenSyms [unLoc arg1, unLoc arg2]
     mkGenArgSyms (RecCon fields)
       = do { let pats = map (unLoc . recordPatSynPatVar) fields
@@ -1910,7 +1910,7 @@ repPatSynD (MkC syn) (MkC args) (MkC dir) (MkC pat)
   = rep2 patSynDName [syn, args, dir, pat]
 
 repPatSynArgs :: HsPatSynDetails GhcRn -> MetaM (Core (M TH.PatSynArgs))
-repPatSynArgs (PrefixCon args)
+repPatSynArgs (PrefixCon _ args)
   = do { args' <- repList nameTyConName lookupLOcc args
        ; repPrefixPatSynArgs args' }
 repPatSynArgs (InfixCon arg1 arg2)
@@ -2016,7 +2016,9 @@ repP (SumPat _ p alt arity) = do { p1 <- repLP p
 repP (ConPat NoExtField dc details)
  = do { con_str <- lookupLOcc dc
       ; case details of
-         PrefixCon ps -> do { qs <- repLPs ps; repPcon con_str qs }
+         PrefixCon tyargs ps -> do { qs <- repLPs ps
+                                   ; ts <- repListM typeTyConName (repTy . unLoc . hsps_body) tyargs
+                                   ; repPcon con_str ts qs }
          RecCon rec   -> do { fps <- repListM fieldPatTyConName rep_fld (rec_flds rec)
                             ; repPrec con_str fps }
          InfixCon p1 p2 -> do { p1' <- repLP p1;
@@ -2028,7 +2030,6 @@ repP (ConPat NoExtField dc details)
    rep_fld (L _ fld) = do { MkC v <- lookupLOcc (hsRecFieldSel fld)
                           ; MkC p <- repLP (hsRecFieldArg fld)
                           ; rep2 fieldPatName [v,p] }
-
 repP (NPat _ (L _ l) Nothing _) = do { a <- repOverloadedLiteral l
                                      ; repPlit a }
 repP (ViewPat _ e p) = do { e' <- repLE e; p' <- repLP p; repPview e' p' }
@@ -2249,8 +2250,8 @@ repPunboxedSum (MkC p) alt arity
                              , mkIntExprInt platform alt
                              , mkIntExprInt platform arity ] }
 
-repPcon   :: Core TH.Name -> Core [(M TH.Pat)] -> MetaM (Core (M TH.Pat))
-repPcon (MkC s) (MkC ps) = rep2 conPName [s, ps]
+repPcon   :: Core TH.Name -> Core [(M TH.Type)] -> Core [(M TH.Pat)] -> MetaM (Core (M TH.Pat))
+repPcon (MkC s) (MkC ts) (MkC ps) = rep2 conPName [s, ts, ps]
 
 repPrec   :: Core TH.Name -> Core [M (TH.Name, TH.Pat)] -> MetaM (Core (M TH.Pat))
 repPrec (MkC c) (MkC rps) = rep2 recPName [c,rps]
@@ -2621,7 +2622,7 @@ repH98DataCon :: Located Name
 repH98DataCon con details
     = do con' <- lookupLOcc con -- See Note [Binders and occurrences]
          case details of
-           PrefixCon ps -> do
+           PrefixCon _ ps -> do
              arg_tys <- repPrefixConArgs ps
              rep2 normalCName [unC con', unC arg_tys]
            InfixCon st1 st2 -> do
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index 70bb33b7d00882d062ef6eb81535e3989a76a7c0..3917998c3e1935dec990ac8b57ae10df02b2d077 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -18,6 +18,8 @@
 Main functions for .hie file generation
 -}
 
+#include "HsVersions.h"
+
 module GHC.Iface.Ext.Ast ( mkHieFile, mkHieFileWithSource, getCompressedAsts, enrichHie) where
 
 import GHC.Utils.Outputable(ppr)
@@ -55,6 +57,7 @@ import GHC.Types.Var.Env
 import GHC.Builtin.Uniques
 import GHC.Iface.Make             ( mkIfaceExports )
 import GHC.Utils.Panic
+import GHC.Utils.Misc
 import GHC.Data.Maybe
 import GHC.Data.FastString
 
@@ -69,7 +72,7 @@ import qualified Data.ByteString as BS
 import qualified Data.Map as M
 import qualified Data.Set as S
 import Data.Data                  ( Data, Typeable )
-import Data.List                  ( foldl1' )
+import Data.Void                  ( Void, absurd )
 import Control.Monad              ( forM_ )
 import Control.Monad.Trans.State.Strict
 import Control.Monad.Trans.Reader
@@ -484,6 +487,18 @@ patScopes rsp useScope patScope xs =
   map (\(RS sc a) -> PS rsp useScope sc a) $
     listScopes patScope xs
 
+-- | 'listScopes' specialised to 'HsPatSigType'
+tScopes
+  :: Scope
+  -> Scope
+  -> [HsPatSigType (GhcPass a)]
+  -> [TScoped (HsPatSigType (GhcPass a))]
+tScopes scope rhsScope xs =
+  map (\(RS sc a) -> TS (ResolvedScopes [scope, sc]) (unLoc a)) $
+    listScopes rhsScope (map (\hsps -> L (getLoc $ hsps_body hsps) hsps) xs)
+  -- We make the HsPatSigType 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
 tvScopes
   :: TyVarScope
@@ -567,6 +582,9 @@ class ToHie a where
 class HasType a where
   getTypeNode :: a -> HieM [HieAST Type]
 
+instance ToHie Void where
+  toHie v = absurd v
+
 instance (ToHie a) => ToHie [a] where
   toHie = concatMapM toHie
 
@@ -855,7 +873,7 @@ instance HiePass p => ToHie (Located (PatSynBind (GhcPass p) (GhcPass p))) where
           varScope = mkLScope var
           patScope = mkScope $ getLoc pat
           detScope = case dets of
-            (PrefixCon args) -> foldr combineScopes NoScope $ map mkLScope args
+            (PrefixCon _ args) -> foldr combineScopes NoScope $ map mkLScope args
             (InfixCon a b) -> combineScopes (mkLScope a) (mkLScope b)
             (RecCon r) -> foldr go NoScope r
           go (RecordPatSynField a b) c = combineScopes c
@@ -863,7 +881,7 @@ instance HiePass p => ToHie (Located (PatSynBind (GhcPass p) (GhcPass p))) where
           detSpan = case detScope of
             LocalScope a -> Just a
             _ -> Nothing
-          toBind (PrefixCon args) = PrefixCon $ map (C Use) args
+          toBind (PrefixCon ts args) = ASSERT(null ts) PrefixCon ts $ map (C Use) args
           toBind (InfixCon a b) = InfixCon (C Use a) (C Use b)
           toBind (RecCon r) = RecCon $ map (PSC detSpan) r
 
@@ -945,7 +963,7 @@ instance HiePass p => ToHie (PScoped (Located (Pat (GhcPass p)))) where
                             , toHie $ L ospan wrap
                             , toHie $ map (C (EvidenceVarBind EvPatternBind evscope rsp)
                                           . L ospan) ev_vars
-                          ]
+                            ]
             ]
           HieRn ->
             [ toHie $ C Use con
@@ -985,9 +1003,10 @@ instance HiePass p => ToHie (PScoped (Located (Pat (GhcPass p)))) where
           HieRn -> []
 #endif
     where
-      contextify :: a ~ LPat (GhcPass p) => HsConDetails a (HsRecFields (GhcPass p) a)
-                 -> HsConDetails (PScoped a) (RContext (HsRecFields (GhcPass p) (PScoped a)))
-      contextify (PrefixCon args) = PrefixCon $ patScopes rsp scope pscope args
+      contextify :: a ~ LPat (GhcPass p) => HsConDetails (HsPatSigType (NoGhcTc (GhcPass p))) a (HsRecFields (GhcPass p) a)
+                 -> HsConDetails (TScoped (HsPatSigType (NoGhcTc (GhcPass p)))) (PScoped a) (RContext (HsRecFields (GhcPass p) (PScoped a)))
+      contextify (PrefixCon tyargs args) = PrefixCon (tScopes scope argscope tyargs) (patScopes rsp scope pscope args)
+        where argscope = foldr combineScopes NoScope $ map mkLScope args
       contextify (InfixCon a b) = InfixCon a' b'
         where [a', b'] = patScopes rsp scope pscope [a,b]
       contextify (RecCon r) = RecCon $ RC RecFieldMatch $ contextify_rec r
@@ -1303,8 +1322,8 @@ instance HiePass p => ToHie (RScoped (ApplicativeArg (GhcPass p))) where
     , toHie $ PS Nothing sc NoScope pat
     ]
 
-instance (ToHie arg, ToHie rec) => ToHie (HsConDetails arg rec) where
-  toHie (PrefixCon args) = toHie args
+instance (ToHie tyarg, ToHie arg, ToHie rec) => ToHie (HsConDetails tyarg arg rec) where
+  toHie (PrefixCon tyargs args) = concatM [ toHie tyargs, toHie args ]
   toHie (RecCon rec) = toHie rec
   toHie (InfixCon a b) = concatM [ toHie a, toHie b]
 
@@ -1554,9 +1573,9 @@ instance ToHie (Located (ConDecl GhcRn)) where
           rhsScope = combineScopes ctxScope argsScope
           ctxScope = maybe NoScope mkLScope ctx
           argsScope = case dets of
-            PrefixCon xs -> scaled_args_scope xs
-            InfixCon a b -> scaled_args_scope [a, b]
-            RecCon x     -> mkLScope x
+            PrefixCon _ xs -> scaled_args_scope xs
+            InfixCon a b   -> scaled_args_scope [a, b]
+            RecCon x       -> mkLScope x
     where scaled_args_scope :: [HsScaled GhcRn (LHsType GhcRn)] -> Scope
           scaled_args_scope = foldr combineScopes NoScope . map (mkLScope . hsScaledThing)
 
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 5ec88929fe1fd39541a202fdd6a5e8257e9dd77f..e9de7eea7813157b27081b12b185cb6460052d54 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -1582,7 +1582,7 @@ pattern_synonym_decl :: { LHsDecl GhcPs }
                    }}
 
 pattern_synonym_lhs :: { (Located RdrName, HsPatSynDetails GhcPs, [AddAnn]) }
-        : con vars0 { ($1, PrefixCon $2, []) }
+        : con vars0 { ($1, PrefixCon noTypeArgs $2, []) }
         | varid conop varid { ($2, InfixCon $1 $3, []) }
         | con '{' cvars1 '}' { ($1, RecCon $3, [moc $2, mcc $4] ) }
 
diff --git a/compiler/GHC/Parser/Errors.hs b/compiler/GHC/Parser/Errors.hs
index cf9389053248080d5c5198e401fe7fc321b31692..582b47535d51bcf1a809b4f850d865c2f93f2803 100644
--- a/compiler/GHC/Parser/Errors.hs
+++ b/compiler/GHC/Parser/Errors.hs
@@ -175,9 +175,6 @@ data ErrorDesc
    | ErrIfTheElseInPat
       -- ^ If-then-else syntax in pattern
 
-   | ErrTypeAppInPat
-      -- ^ Type-application in pattern
-
    | ErrLambdaCaseInPat
       -- ^ Lambda-case in pattern
 
@@ -393,6 +390,8 @@ data Hint
    | SuggestLetInDo
    | SuggestPatternSynonyms
    | SuggestInfixBindMaybeAtPat !RdrName
+   | TypeApplicationsInPatternsOnlyDataCons -- ^ Type applications in patterns are only allowed on data constructors
+
 
 data LexErrKind
    = LexErrKind_EOF        -- ^ End of input
diff --git a/compiler/GHC/Parser/Errors/Ppr.hs b/compiler/GHC/Parser/Errors/Ppr.hs
index c4b411b1c3d2f8595c54119283b3f22a8eabbbb9..a26f6809c6699609963f7d26b9a6447c5e88ccfd 100644
--- a/compiler/GHC/Parser/Errors/Ppr.hs
+++ b/compiler/GHC/Parser/Errors/Ppr.hs
@@ -263,9 +263,6 @@ pp_err = \case
    ErrIfTheElseInPat
       -> text "(if ... then ... else ...)-syntax in pattern"
 
-   ErrTypeAppInPat
-      -> text "Type applications in patterns are not yet supported"
-
    ErrLambdaCaseInPat
       -> text "(\\case ...)-syntax in pattern"
 
@@ -607,6 +604,8 @@ pp_hint = \case
          $$ if opIsAt fun
                then perhaps_as_pat
                else empty
+   TypeApplicationsInPatternsOnlyDataCons ->
+     text "Type applications in patterns are only allowed on data constructors."
 
 perhaps_as_pat :: SDoc
 perhaps_as_pat = text "Perhaps you meant an as-pattern, which must not be surrounded by whitespace"
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 1b4151cfb75724d41870836f6d1d9be609f22435..a59e4a882ff913c431bda227cafd0f783cee46be 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -575,9 +575,9 @@ mkPatSynMatchGroup (L loc patsyn_name) (L _ decls) =
         do { unless (name == patsyn_name) $
                wrongNameBindingErr loc decl
            ; match <- case details of
-               PrefixCon pats -> return $ Match { m_ext = noExtField
-                                                , m_ctxt = ctxt, m_pats = pats
-                                                , m_grhss = rhs }
+               PrefixCon _ pats -> return $ Match { m_ext = noExtField
+                                                  , m_ctxt = ctxt, m_pats = pats
+                                                  , m_grhss = rhs }
                    where
                      ctxt = FunRhs { mc_fun = ln
                                    , mc_fixity = Prefix
@@ -966,27 +966,31 @@ checkPattern_hints :: [Hint] -> PV (Located (PatBuilder GhcPs)) -> P (LPat GhcPs
 checkPattern_hints hints pp = runPV_hints hints (pp >>= checkLPat)
 
 checkLPat :: Located (PatBuilder GhcPs) -> PV (LPat GhcPs)
-checkLPat e@(L l _) = checkPat l e []
+checkLPat e@(L l _) = checkPat l e [] []
 
-checkPat :: SrcSpan -> Located (PatBuilder GhcPs) -> [LPat GhcPs]
+checkPat :: SrcSpan -> Located (PatBuilder GhcPs) -> [HsPatSigType GhcPs] -> [LPat GhcPs]
          -> PV (LPat GhcPs)
-checkPat loc (L l e@(PatBuilderVar (L _ c))) args
+checkPat loc (L l e@(PatBuilderVar (L _ c))) tyargs args
   | isRdrDataCon c = return . L loc $ ConPat
       { pat_con_ext = noExtField
       , pat_con = L l c
-      , pat_args = PrefixCon args
+      , pat_args = PrefixCon tyargs args
       }
+  | not (null tyargs) =
+      add_hint TypeApplicationsInPatternsOnlyDataCons $
+      patFail l (ppr e <+> hsep [text "@" <> ppr t | t <- tyargs])
   | not (null args) && patIsRec c =
       add_hint SuggestRecursiveDo $
       patFail l (ppr e)
-checkPat loc (L _ (PatBuilderApp f e)) args
-  = do p <- checkLPat e
-       checkPat loc f (p : args)
-checkPat loc (L _ e) []
-  = do p <- checkAPat loc e
-       return (L loc p)
-checkPat loc e _
-  = patFail loc (ppr e)
+checkPat loc (L _ (PatBuilderAppType f t)) tyargs args = do
+  checkPat loc f (t : tyargs) args
+checkPat loc (L _ (PatBuilderApp f e)) [] args = do
+  p <- checkLPat e
+  checkPat loc f [] (p : args)
+checkPat loc (L _ e) [] [] = do
+  p <- checkAPat loc e
+  return (L loc p)
+checkPat loc e _ _ = patFail loc (ppr e)
 
 checkAPat :: SrcSpan -> PatBuilder GhcPs -> PV (Pat GhcPs)
 checkAPat loc e0 = do
@@ -1517,7 +1521,7 @@ instance DisambECP (PatBuilder GhcPs) where
   type FunArg (PatBuilder GhcPs) = PatBuilder GhcPs
   superFunArg m = m
   mkHsAppPV l p1 p2     = return $ L l (PatBuilderApp p1 p2)
-  mkHsAppTypePV l _ _   = addFatalError $ Error ErrTypeAppInPat [] l
+  mkHsAppTypePV l p t   = return $ L l (PatBuilderAppType p (mkHsPatSigType t))
   mkHsIfPV l _ _ _ _ _  = addFatalError $ Error ErrIfTheElseInPat [] l
   mkHsDoPV l _ _        = addFatalError $ Error ErrDoNotationInPat [] l
   mkHsParPV l p         = return $ L l (PatBuilderPar p)
@@ -1625,7 +1629,7 @@ dataConBuilderDetails (PrefixDataConBuilder flds _)
 
 -- Normal prefix constructor, e.g.  data T = MkT A B C
 dataConBuilderDetails (PrefixDataConBuilder flds _)
-  = PrefixCon (map hsLinear (toList flds))
+  = PrefixCon noTypeArgs (map hsLinear (toList flds))
 
 -- Infix constructor, e.g. data T = Int :! Bool
 dataConBuilderDetails (InfixDataConBuilder lhs _ rhs)
diff --git a/compiler/GHC/Parser/PostProcess/Haddock.hs b/compiler/GHC/Parser/PostProcess/Haddock.hs
index 21f74a878e8b1d8cb85769b5b88396844eac2288..f291830ea2e79344b92db39078b2f486379b28a0 100644
--- a/compiler/GHC/Parser/PostProcess/Haddock.hs
+++ b/compiler/GHC/Parser/PostProcess/Haddock.hs
@@ -708,13 +708,13 @@ instance HasHaddock (Located (ConDecl GhcPs)) where
       ConDeclH98 { con_ext, con_name, con_forall, con_ex_tvs, con_mb_cxt, con_args } ->
         addConTrailingDoc (srcSpanEnd l_con_decl) $
         case con_args of
-          PrefixCon ts -> do
+          PrefixCon _ ts -> do
             con_doc' <- getConDoc (getLoc con_name)
             ts' <- traverse addHaddockConDeclFieldTy ts
             pure $ L l_con_decl $
               ConDeclH98 { con_ext, con_name, con_forall, con_ex_tvs, con_mb_cxt,
                            con_doc = con_doc',
-                           con_args = PrefixCon ts' }
+                           con_args = PrefixCon noTypeArgs ts' }
           InfixCon t1 t2 -> do
             t1' <- addHaddockConDeclFieldTy t1
             con_doc' <- getConDoc (getLoc con_name)
@@ -865,9 +865,9 @@ addConTrailingDoc l_sep =
                     doc <- selectDocString trailingDocs
                     return $ L l' (con_fld { cd_fld_doc = doc })
               con_args' <- case con_args con_decl of
-                x@(PrefixCon [])    -> x <$ reportExtraDocs trailingDocs
+                x@(PrefixCon _ [])  -> x <$ reportExtraDocs trailingDocs
                 x@(RecCon (L _ [])) -> x <$ reportExtraDocs trailingDocs
-                PrefixCon ts -> PrefixCon <$> mapLastM mk_doc_ty ts
+                PrefixCon _ ts -> PrefixCon noTypeArgs <$> mapLastM mk_doc_ty ts
                 InfixCon t1 t2 -> InfixCon t1 <$> mk_doc_ty t2
                 RecCon (L l_rec flds) -> do
                   flds' <- mapLastM mk_doc_fld flds
diff --git a/compiler/GHC/Parser/Types.hs b/compiler/GHC/Parser/Types.hs
index 26795def9f5ba7b751802b149ce5027e5f679b0d..ba7ca1d9c159700c90818dd8c0d0f2dea3df536b 100644
--- a/compiler/GHC/Parser/Types.hs
+++ b/compiler/GHC/Parser/Types.hs
@@ -41,12 +41,13 @@ pprSumOrTuple boxity = \case
         Boxed -> (text "(", text ")")
         Unboxed -> (text "(#", text "#)")
 
--- | See Note [Ambiguous syntactic categories] and Note [PatBuilder] in
--- GHC.parser.PostProcess
+
+-- | See Note [Ambiguous syntactic categories] and Note [PatBuilder]
 data PatBuilder p
   = PatBuilderPat (Pat p)
   | PatBuilderPar (Located (PatBuilder p))
   | PatBuilderApp (Located (PatBuilder p)) (Located (PatBuilder p))
+  | PatBuilderAppType (Located (PatBuilder p)) (HsPatSigType GhcPs)
   | PatBuilderOpApp (Located (PatBuilder p)) (Located RdrName) (Located (PatBuilder p))
   | PatBuilderVar (Located RdrName)
   | PatBuilderOverLit (HsOverLit GhcPs)
@@ -55,6 +56,7 @@ instance Outputable (PatBuilder GhcPs) where
   ppr (PatBuilderPat p) = ppr p
   ppr (PatBuilderPar (L _ p)) = parens (ppr p)
   ppr (PatBuilderApp (L _ p1) (L _ p2)) = ppr p1 <+> ppr p2
+  ppr (PatBuilderAppType (L _ p) t) = ppr p <+> text "@" <> ppr t
   ppr (PatBuilderOpApp (L _ p1) op (L _ p2)) = ppr p1 <+> ppr op <+> ppr p2
   ppr (PatBuilderVar v) = ppr v
   ppr (PatBuilderOverLit l) = ppr l
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index 953d3c2c9b2968f4ddebca707cd47db7e1498e9f..30fef1b9809b3dc8c0311d1ba8e92d5c3ade1aca 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -679,10 +679,10 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
          -- so that the binding locations are reported
          -- from the left-hand side
             case details of
-               PrefixCon vars ->
+               PrefixCon _ vars ->
                    do { checkDupRdrNames vars
                       ; names <- mapM lookupPatSynBndr vars
-                      ; return ( (pat', PrefixCon names)
+                      ; return ( (pat', PrefixCon noTypeArgs names)
                                , mkFVs (map unLoc names)) }
                InfixCon var1 var2 ->
                    do { checkDupRdrNames [var1, var2]
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index cd5d431ee1a662fa1a47a251f7aadf97dde11563..9cf422a92ed5115b5a03e7a8ea0077359c7dd0e1 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE CPP                 #-}
+{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE ViewPatterns        #-}
 
 {-
 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
@@ -11,7 +13,7 @@ module GHC.Rename.HsType (
         -- Type related stuff
         rnHsType, rnLHsType, rnLHsTypes, rnContext,
         rnHsKind, rnLHsKind, rnLHsTypeArgs,
-        rnHsSigType, rnHsWcType,
+        rnHsSigType, rnHsWcType, rnHsPatSigTypeBindingVars,
         HsPatSigTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
         newTyVarNameRn,
         rnConDeclFields,
@@ -26,7 +28,7 @@ module GHC.Rename.HsType (
         -- Binding related stuff
         bindHsOuterTyVarBndrs, bindHsForAllTelescope,
         bindLHsTyVarBndr, bindLHsTyVarBndrs, WarnUnusedForalls(..),
-        rnImplicitBndrs, bindSigTyVarsFV, bindHsQTyVars,
+        rnImplicitTvOccs, bindSigTyVarsFV, bindHsQTyVars,
         FreeKiTyVars,
         extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
         extractHsTysRdrTyVars, extractRdrKindSigVars,
@@ -66,8 +68,10 @@ import GHC.Data.FastString
 import GHC.Data.Maybe
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List          ( nubBy, partition )
-import Control.Monad      ( unless, when )
+import Data.List
+import qualified Data.List.NonEmpty as NE
+import Data.List.NonEmpty (NonEmpty(..))
+import Control.Monad
 
 #include "HsVersions.h"
 
@@ -153,7 +157,7 @@ rnHsPatSigType scoping ctx sig_ty thing_inside
              implicit_bndrs = case scoping of
                AlwaysBind -> tv_rdrs
                NeverBind  -> []
-       ; rnImplicitBndrs Nothing implicit_bndrs $ \ imp_tvs ->
+       ; rnImplicitTvOccs Nothing implicit_bndrs $ \ imp_tvs ->
     do { (nwcs, pat_sig_ty', fvs1) <- rnWcBody 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' }
@@ -171,6 +175,57 @@ rnHsWcType ctxt (HsWC { hswc_body = 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 $
+        vcat
+          [ text "Type variable" <> plural varsInScope
+            <+> hcat (punctuate (text ",") (map (quotes . ppr) varsInScope))
+            <+> isOrAre varsInScope
+            <+> text "already in scope."
+          , text "Type applications in patterns must bind fresh variables, without shadowing."
+          ]
+    (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 -> [Located RdrName] -> LHsType GhcPs
          -> RnM ([Name], LHsType GhcRn, FreeVars)
 rnWcBody ctxt nwc_rdrs hs_ty
@@ -322,17 +377,20 @@ rnHsSigType ctx level
   where
     env = mkTyKiEnv ctx level RnTypeBody
 
-rnImplicitBndrs :: Maybe assoc
-                -- ^ @'Just' _@ => an associated type decl
-                -> FreeKiTyVars
-                -- ^ Surface-syntax free vars that we will implicitly bind.
-                -- May have duplicates, which are removed here.
-                -> ([Name] -> RnM (a, FreeVars))
-                -> RnM (a, FreeVars)
-rnImplicitBndrs mb_assoc implicit_vs_with_dups thing_inside
+-- | Create new renamed type variables corresponding to source-level ones.
+-- Duplicates are permitted, but will be removed. This is intended especially for
+-- the case of handling the implicitly bound free variables of a type signature.
+rnImplicitTvOccs :: Maybe assoc
+                 -- ^ @'Just' _@ => an associated type decl
+                 -> FreeKiTyVars
+                 -- ^ Surface-syntax free vars that we will implicitly bind.
+                 -- May have duplicates, which are removed here.
+                 -> ([Name] -> RnM (a, FreeVars))
+                 -> RnM (a, FreeVars)
+rnImplicitTvOccs mb_assoc implicit_vs_with_dups thing_inside
   = do { let implicit_vs = nubL implicit_vs_with_dups
 
-       ; traceRn "rnImplicitBndrs" $
+       ; traceRn "rnImplicitTvOccs" $
          vcat [ ppr implicit_vs_with_dups, ppr implicit_vs ]
 
          -- Use the currently set SrcSpan as the new source location for each Name.
@@ -346,7 +404,7 @@ rnImplicitBndrs mb_assoc implicit_vs_with_dups thing_inside
 {-
 Note [Source locations for implicitly bound type variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When bringing implicitly bound type variables into scope (in rnImplicitBndrs),
+When bringing implicitly bound type variables into scope (in rnImplicitTvOccs),
 we do something peculiar: we drop the original SrcSpan attached to each
 variable and replace it with the currently set SrcSpan. Moreover, this new
 SrcSpan is usually /less/ precise than the original one, and that's OK. To see
@@ -366,6 +424,31 @@ 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.groupBy eqLocated $ sortBy cmpLocated $ implicit_vs_with_dups) $ \case
+           (x :| []) -> return x
+           (x :| _) -> do addErr $ text "Variable" <+> text "`" <> ppr x <> text "'" <+> text "would be bound multiple times by" <+> pprHsDocContext ctx <> text "."
+                          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
@@ -836,12 +919,12 @@ bindHsQTyVars doc mb_assoc body_kv_occs hsq_bndrs thing_inside
                 , text "body_remaining" <+> ppr body_remaining
                 ]
 
-       ; rnImplicitBndrs mb_assoc implicit_kvs $ \ implicit_kv_nms' ->
+       ; rnImplicitTvOccs mb_assoc implicit_kvs $ \ implicit_kv_nms' ->
          bindLHsTyVarBndrs doc NoWarnUnusedForalls mb_assoc hs_tv_bndrs $ \ rn_bndrs ->
            -- This is the only call site for bindLHsTyVarBndrs where we pass
            -- NoWarnUnusedForalls, which suppresses -Wunused-foralls warnings.
            -- See Note [Suppress -Wunused-foralls when binding LHsQTyVars].
-    do { let -- The SrcSpan that rnImplicitBndrs will attach to each Name will
+    do { let -- The SrcSpan that rnImplicitTvOccs will attach to each Name will
              -- span the entire declaration to which the LHsQTyVars belongs,
              -- which will be reflected in warning and error messages. We can
              -- be a little more precise than that by pointing to the location
@@ -895,7 +978,7 @@ Then:
   bring Names into scope.
 
 * bndr_kv_occs, body_kv_occs, and implicit_kvs can contain duplicates. All
-  duplicate occurrences are removed when we bind them with rnImplicitBndrs.
+  duplicate occurrences are removed when we bind them with rnImplicitTvOccs.
 
 Finally, you may wonder why filterFreeVarsToBind removes in-scope variables
 from bndr/body_kv_occs.  How can anything be in scope?  Answer:
@@ -999,7 +1082,7 @@ bindHsOuterTyVarBndrs :: OutputableBndrFlag flag
 bindHsOuterTyVarBndrs doc mb_cls implicit_vars outer_bndrs thing_inside =
   case outer_bndrs of
     HsOuterImplicit{} ->
-      rnImplicitBndrs mb_cls implicit_vars $ \implicit_vars' ->
+      rnImplicitTvOccs mb_cls implicit_vars $ \implicit_vars' ->
         thing_inside $ HsOuterImplicit { hso_ximplicit = implicit_vars' }
     HsOuterExplicit{hso_bndrs = exp_bndrs} ->
       -- Note: If we pass mb_cls instead of Nothing below, bindLHsTyVarBndrs
@@ -1544,7 +1627,7 @@ See Note [Ordering of implicit variables].
 
 It is common for lists of free type variables to contain duplicates. For
 example, in `f :: a -> a`, the free type variable list is [a, a]. When these
-implicitly bound variables are brought into scope (with rnImplicitBndrs),
+implicitly bound variables are brought into scope (with rnImplicitTvOccs),
 duplicates are removed with nubL.
 
 Note [Ordering of implicit variables]
@@ -1880,7 +1963,7 @@ extract_tv tv acc =
 -- Deletes duplicates in a list of Located things. This is used to:
 --
 -- * Delete duplicate occurrences of implicitly bound type/kind variables when
---   bringing them into scope (in rnImplicitBndrs).
+--   bringing them into scope (in rnImplicitTvOccs).
 --
 -- * Delete duplicate occurrences of named wildcards (in rn_hs_sig_wc_type and
 --   rnHsWcType).
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index e0deda3b1d49ad1044c5b21cd3df9e230d071731..92ae90bedd3526ee830eb2a8a01b90e1fd8a45fb 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -2234,9 +2234,9 @@ rnConDeclH98Details ::
    -> HsDocContext
    -> HsConDeclH98Details GhcPs
    -> RnM (HsConDeclH98Details GhcRn, FreeVars)
-rnConDeclH98Details _ doc (PrefixCon tys)
+rnConDeclH98Details _ doc (PrefixCon _ tys)
   = do { (new_tys, fvs) <- mapFvRn (rnScaledLHsType doc) tys
-       ; return (PrefixCon new_tys, fvs) }
+       ; return (PrefixCon noTypeArgs new_tys, fvs) }
 rnConDeclH98Details _ doc (InfixCon ty1 ty2)
   = do { (new_ty1, fvs1) <- rnScaledLHsType doc ty1
        ; (new_ty2, fvs2) <- rnScaledLHsType doc ty2
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index b0f15d3d199c176551d98e4a64cc5fff221be5b7..74b93624f0cccdbe435aa73a72c754338b5ad630 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE CPP                 #-}
 {-# LANGUAGE DeriveFunctor       #-}
 {-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE LambdaCase          #-}
 {-# LANGUAGE RankNTypes          #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies        #-}
@@ -32,7 +33,7 @@ module GHC.Rename.Pat (-- main entry points
               rnHsRecUpdFields,
 
               -- CpsRn monad
-              CpsRn, liftCps,
+              CpsRn, liftCps, liftCpsWithCont,
 
               -- Literals
               rnLit, rnOverLit,
@@ -77,7 +78,7 @@ 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, forM )
 import qualified Data.List.NonEmpty as NE
 import Data.Ratio
 
@@ -133,6 +134,9 @@ liftCpsFV rn_thing = CpsRn (\k -> do { (v,fvs1) <- rn_thing
                                      ; (r,fvs2) <- k v
                                      ; return (r, fvs1 `plusFV` fvs2) })
 
+liftCpsWithCont :: (forall r. (b -> RnM (r, FreeVars)) -> RnM (r, FreeVars)) -> CpsRn b
+liftCpsWithCont = CpsRn
+
 wrapSrcSpanCps :: (a -> CpsRn b) -> Located a -> CpsRn (Located b)
 -- Set the location, and also wrap it around the value returned
 wrapSrcSpanCps fn (L loc a)
@@ -424,7 +428,7 @@ rnPatAndThen mk (SigPat x pat sig)
        ; return (SigPat x pat' sig' ) }
   where
     rnHsPatSigTypeAndThen :: HsPatSigType GhcPs -> CpsRn (HsPatSigType GhcRn)
-    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx sig)
+    rnHsPatSigTypeAndThen sig = liftCpsWithCont (rnHsPatSigType AlwaysBind PatCtx sig)
 
 rnPatAndThen mk (LitPat x lit)
   | HsString src s <- lit
@@ -522,13 +526,15 @@ rnConPatAndThen :: NameMaker
                 -> HsConPatDetails GhcPs
                 -> CpsRn (Pat GhcRn)
 
-rnConPatAndThen mk con (PrefixCon pats)
+rnConPatAndThen mk con (PrefixCon tyargs pats)
   = do  { con' <- lookupConCps con
+        ; tyargs' <- forM tyargs $ \t ->
+            liftCpsWithCont $ rnHsPatSigTypeBindingVars HsTypeCtx t
         ; pats' <- rnLPatsAndThen mk pats
         ; return $ ConPat
             { pat_con_ext = noExtField
             , pat_con = con'
-            , pat_args = PrefixCon pats'
+            , pat_args = PrefixCon tyargs' pats'
             }
         }
 
diff --git a/compiler/GHC/Rename/Utils.hs b/compiler/GHC/Rename/Utils.hs
index 2e93ad882d530b682b13a5b8e06f3ee65e738cfd..3acf9d83d27f70551a1cbe4343013fff398723b8 100644
--- a/compiler/GHC/Rename/Utils.hs
+++ b/compiler/GHC/Rename/Utils.hs
@@ -619,6 +619,7 @@ data HsDocContext
   | ExprWithTySigCtx
   | TypBrCtx
   | HsTypeCtx
+  | HsTypePatCtx
   | GHCiCtx
   | SpliceTypeCtx (LHsType GhcPs)
   | ClassInstanceCtx
@@ -647,6 +648,7 @@ pprHsDocContext (ClassDeclCtx name)   = text "the declaration for class" <+> quo
 pprHsDocContext ExprWithTySigCtx      = text "an expression type signature"
 pprHsDocContext TypBrCtx              = text "a Template-Haskell quoted type"
 pprHsDocContext HsTypeCtx             = text "a type argument"
+pprHsDocContext HsTypePatCtx          = text "a type argument in a pattern"
 pprHsDocContext GHCiCtx               = text "GHCi input"
 pprHsDocContext (SpliceTypeCtx hs_ty) = text "the spliced type" <+> quotes (ppr hs_ty)
 pprHsDocContext ClassInstanceCtx      = text "GHC.Tc.Gen.Splice.reifyInstances"
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index f41f99be2dc824ecd9d5c2d70dc9d5660edaa91f..6748e8a4c4a3aff4eabce66f126a61c6b103c4c2 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -66,6 +66,7 @@ module GHC.Tc.Gen.HsType (
 
         -- Pattern type signatures
         tcHsPatSigType,
+        HoleMode(..),
 
         -- Error messages
         funAppCtxt, addTyConFlavCtxt
@@ -819,6 +820,9 @@ data HoleMode = HM_Sig      -- Partial type signatures: f :: _ -> Int
               | HM_VTA      -- Visible type and kind application:
                             --   f @(Maybe _)
                             --   Maybe @(_ -> _)
+              | HM_TyAppPat -- Visible type applications in patterns:
+                            --   foo (Con @_ @t x) = ...
+                            --   case x of Con @_ @t v -> ...
 
 mkMode :: TypeOrKind -> TcTyMode
 mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
@@ -835,9 +839,10 @@ mkHoleMode tyki hm
                           , mode_holes = Just (lvl,hm) }) }
 
 instance Outputable HoleMode where
-  ppr HM_Sig     = text "HM_Sig"
-  ppr HM_FamPat  = text "HM_FamPat"
-  ppr HM_VTA     = text "HM_VTA"
+  ppr HM_Sig      = text "HM_Sig"
+  ppr HM_FamPat   = text "HM_FamPat"
+  ppr HM_VTA      = text "HM_VTA"
+  ppr HM_TyAppPat = text "HM_TyAppPat"
 
 instance Outputable TcTyMode where
   ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
@@ -2103,14 +2108,16 @@ tcAnonWildCardOcc is_extra (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }
   where
      -- See Note [Wildcard names]
      wc_nm = case hole_mode of
-               HM_Sig     -> "w"
-               HM_FamPat  -> "_"
-               HM_VTA     -> "w"
+               HM_Sig      -> "w"
+               HM_FamPat   -> "_"
+               HM_VTA      -> "w"
+               HM_TyAppPat -> "_"
 
      emit_holes = case hole_mode of
                      HM_Sig     -> True
                      HM_FamPat  -> False
                      HM_VTA     -> False
+                     HM_TyAppPat -> False
 
 tcAnonWildCardOcc _ mode ty _
 -- mode_holes is Nothing.  Should not happen, because renamer
@@ -3931,7 +3938,9 @@ information about how these are printed.
 ********************************************************************* -}
 
 tcHsPatSigType :: UserTypeCtxt
+               -> HoleMode -- HM_Sig when in a SigPat, HM_TyAppPat when in a ConPat checking type applications.
                -> HsPatSigType GhcRn          -- The type signature
+               -> ContextKind                -- What kind is expected
                -> TcM ( [(Name, TcTyVar)]     -- Wildcards
                       , [(Name, TcTyVar)]     -- The new bit of type environment, binding
                                               -- the scoped type variables
@@ -3943,12 +3952,13 @@ tcHsPatSigType :: UserTypeCtxt
 --
 -- This may emit constraints
 -- See Note [Recipe for checking a signature]
-tcHsPatSigType ctxt
+tcHsPatSigType ctxt hole_mode
   (HsPS { hsps_ext  = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
         , hsps_body = hs_ty })
+  ctxt_kind
   = addSigCtxt ctxt hs_ty $
     do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
-       ; mode <- mkHoleMode TypeLevel HM_Sig
+       ; mode <- mkHoleMode TypeLevel hole_mode
        ; (wcs, sig_ty)
             <- addTypeCtxt hs_ty                     $
                solveEqualities "tcHsPatSigType" $
@@ -3956,7 +3966,7 @@ tcHsPatSigType ctxt
                  -- and c.f #16033
                bindNamedWildCardBinders sig_wcs $ \ wcs ->
                tcExtendNameTyVarEnv sig_tkv_prs $
-               do { ek     <- newOpenTypeKind
+               do { ek     <- newExpectedKind ctxt_kind
                   ; sig_ty <- tc_lhs_type mode hs_ty ek
                   ; return (wcs, sig_ty) }
 
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 5500c7692c8d1d3e8d2b2a112a1e8872c8e752ba..8507c0d7ffd8f010524b64062105887f21e090c7 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -53,6 +53,7 @@ import GHC.Builtin.Types
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.Origin
 import GHC.Core.TyCon
+import GHC.Core.Type
 import GHC.Core.DataCon
 import GHC.Core.PatSyn
 import GHC.Core.ConLike
@@ -66,7 +67,7 @@ import GHC.Utils.Outputable as Outputable
 import GHC.Utils.Panic
 import qualified GHC.LanguageExtensions as LangExt
 import Control.Arrow  ( second )
-import Control.Monad  ( when )
+import Control.Monad
 import GHC.Data.List.SetOps ( getNth )
 
 {-
@@ -554,7 +555,7 @@ Fortunately that's what matchExpectedFunTySigma returns anyway.
 
 ------------------------
 -- Data constructors
-  ConPat NoExtField con arg_pats ->
+  ConPat _ con arg_pats ->
     tcConPat penv con pat_ty arg_pats thing_inside
 
 ------------------------
@@ -736,7 +737,7 @@ tcPatSig :: Bool                    -- True <=> pattern binding
                  HsWrapper)         -- Coercion due to unification with actual ty
                                     -- Of shape:  res_ty ~ sig_ty
 tcPatSig in_pat_bind sig res_ty
- = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
+ = do  { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt HM_Sig sig OpenKind
         -- sig_tvs are the type variables free in 'sig',
         -- and not already in scope. These are the ones
         -- that should be brought into scope
@@ -890,22 +891,18 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)
         ; checkExistentials ex_tvs all_arg_tys penv
 
-        ; tenv <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
+        ; tenv1 <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
                   -- NB: Do not use zipTvSubst!  See #14154
                   -- We want to create a well-kinded substitution, so
                   -- that the instantiated type is well-kinded
 
-        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv ex_tvs
+        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv1 ex_tvs
                      -- Get location from monad, not from ex_tvs
                      -- This freshens: See Note [Freshen existentials]
                      -- Why "super"? See Note [Binding when lookup up instances]
                      -- in GHC.Core.InstEnv.
 
-        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
-              -- pat_ty' is type of the actual constructor application
-              -- pat_ty' /= pat_ty iff coi /= IdCo
-
-              arg_tys' = substScaledTys tenv arg_tys
+        ; let arg_tys' = substScaledTys tenv arg_tys
               pat_mult = scaledMult pat_ty_scaled
               arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
 
@@ -922,7 +919,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
           then do { -- The common case; no class bindings etc
                     -- (see Note [Arrows and patterns])
                     (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled
-                                                  penv arg_pats thing_inside
+                                                  tenv penv arg_pats thing_inside
                   ; let res_pat = ConPat { pat_con = header
                                          , pat_args = arg_pats'
                                          , pat_con_ext = ConPatTc
@@ -958,7 +955,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
         ; given <- newEvVars theta'
         ; (ev_binds, (arg_pats', res))
              <- checkConstraints skol_info ex_tvs' given $
-                tcConArgs (RealDataCon data_con) arg_tys_scaled penv arg_pats thing_inside
+                tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside
 
         ; let res_pat = ConPat
                 { pat_con   = header
@@ -1019,7 +1016,7 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
         ; traceTc "checkConstraints {" Outputable.empty
         ; (ev_binds, (arg_pats', res))
              <- checkConstraints skol_info ex_tvs' prov_dicts' $
-                tcConArgs (PatSynCon pat_syn) arg_tys_scaled penv arg_pats thing_inside
+                tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
 
         ; traceTc "checkConstraints }" (ppr ev_binds)
         ; let res_pat = ConPat { pat_con   = L con_span $ PatSynCon pat_syn
@@ -1125,17 +1122,84 @@ Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
    error messages; it's a purely internal thing
 -}
 
-tcConArgs :: ConLike -> [Scaled TcSigmaType]
-          -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+{-
+Note [Typechecking type applications in patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+How should we typecheck type applications in patterns, such as
+   f :: Either (Maybe a) [b] -> blah
+   f (Left @x @[y] (v::Maybe x)) = blah
+
+It's quite straightforward, and very similar to the treatment of
+pattern signatures.
+
+* Step 1: bind the newly-in-scope type variables x and y to fresh
+  unification variables, say x0 and y0.
+
+* Step 2: typecheck those type arguments, @x and @[y], to get the
+  types x0 and [y0].
+
+* Step 3: Unify those types with the type arguments we expect,
+  in this case (Maybe a) and [b].  These unifications will
+  (perhaps after the constraint solver has done its work)
+  unify   x0 := Maybe a
+          y0 := b
+  Thus we learn that x stands for (Maybe a) and y for b.
+
+Wrinkles:
+
+* Surprisingly, we can discard the coercions arising from
+  these unifications.  The *only* thing the unification does is
+  to side-effect those unification variables, so that we know
+  what type x and y stand for; and cause an error if the equality
+  is not soluble.  It's a bit like a Derived constraint arising
+  from a functional dependency.
+
+* Exactly the same works for existential arguments
+     data T where
+        MkT :: a -> a -> T
+     f :: T -> blah
+     f (MkT @x v w) = ...
+   Here we create a fresh unification variable x0 for x, and
+   unify it with the fresh existential variable bound by the pattern.
+
+* Note that both here and in pattern signatures the unification may
+  not even end up unifying the variable.  For example
+     type S a b = a
+     f :: Maybe a -> Bool
+     f (Just @(S a b) x) = True :: b
+   In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no
+   effect on the unification variable b0, to which 'b' is bound.
+   Later, in the RHS, we find that b0 must be Bool, and unify it there.
+   All is fine.
+-}
 
-tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of
-  PrefixCon arg_pats -> do
+tcConArgs :: ConLike
+          -> [Scaled TcSigmaType]
+          -> TCvSubst            -- Instantiating substitution for constructor type
+          -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
+tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
+  PrefixCon type_args arg_pats -> do
         { checkTc (con_arity == no_of_args)     -- Check correct arity
                   (arityErr (text "constructor") con_like con_arity no_of_args)
+
+        ; let con_binders = conLikeUserTyVarBinders con_like
+        ; checkTc (type_args `leLength` con_binders)
+                  (conTyArgArityErr con_like (length con_binders) (length type_args))
+
         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
-        ; (arg_pats', res) <- tcMultiple tcConArg penv pats_w_tys
-                                              thing_inside
-        ; return (PrefixCon arg_pats', res) }
+        ; (type_args', (arg_pats', res))
+            <- tcMultiple tcConTyArg penv type_args $
+               tcMultiple tcConArg penv pats_w_tys thing_inside
+
+          -- This unification is straight from Figure 7 of
+          -- "Type Variables in Patterns", Haskell'18
+        ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
+                                                        binderVars con_binders)
+          -- OK to drop coercions here. These unifications are all about
+          -- guiding inference based on a user-written type annotation
+          -- See Note [Typechecking type applications in patterns]
+
+        ; return (PrefixCon type_args arg_pats', res) }
     where
       con_arity  = conLikeArity con_like
       no_of_args = length arg_pats
@@ -1190,6 +1254,22 @@ tcConArgs con_like arg_tys penv con_args thing_inside = case con_args of
           -- dataConFieldLabels will be empty (and each field in the pattern
           -- will generate an error below).
 
+tcConTyArg :: Checker (HsPatSigType GhcRn) TcType
+tcConTyArg penv rn_ty 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 in tcConArgs, which will also unify
+               -- kinds.
+       ; when (not (null sig_ibs) && inPatBind penv) $
+           addErr (text "Binding type variables is not allowed in pattern bindings")
+       ; result <- tcExtendNameTyVarEnv sig_wcs $
+                   tcExtendNameTyVarEnv sig_ibs $
+                   thing_inside
+       ; return (arg_ty, result) }
+
 tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc)
 tcConArg penv (arg_pat, Scaled arg_mult arg_ty)
   = tc_lpat (Scaled arg_mult (mkCheckExpType arg_ty)) penv arg_pat
@@ -1211,6 +1291,14 @@ addDataConStupidTheta data_con inst_tys
          --     because the constructor might have existentials
     inst_theta = substTheta tenv stupid_theta
 
+conTyArgArityErr :: ConLike
+                 -> Int   -- expected # of arguments
+                 -> Int   -- actual # of arguments
+                 -> SDoc
+conTyArgArityErr con_like expected_number actual_number
+  = text "Too many type arguments in constructor pattern for" <+> quotes (ppr con_like) $$
+    text "Expected no more than" <+> ppr expected_number <> semi <+> text "got" <+> ppr actual_number
+
 {-
 Note [Arrows and patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index ec9d1da5e96ebb2e17205589264ebd9ee9e1495b..bbbd52883051ab8e08c83a12dd82f3fa04852eeb 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -229,7 +229,7 @@ tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
 --  If there's an explicit forall, the renamer would have already reported an
 --   error for each out-of-scope type variable used
   = do  { let ctxt = RuleSigCtxt name
-        ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty
+        ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt HM_Sig rn_ty OpenKind
         ; let id  = mkLocalId name Many id_ty
                     -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
 
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 468410400f295fb8943edeedd3237f92c0801e0e..dfb6e4fe3ed19c94bfd781cc4fdafda1dc88c173 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -1443,7 +1443,7 @@ reifyInstances th_nm th_tys
                              -- must error before proceeding to typecheck the
                              -- renamed type, as that will result in GHC
                              -- internal errors (#13837).
-               rnImplicitBndrs Nothing tv_rdrs $ \ tv_names ->
+               rnImplicitTvOccs Nothing tv_rdrs $ \ tv_names ->
                do { (rn_ty, fvs) <- rnLHsType doc rdr_ty
                   ; return ((tv_names, rn_ty), fvs) }
 
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 1378eda16ec14b41534d4325a8d4a8c4012d0d99..50d4f726107c3f206c61e26ae486e94396e48065 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -1581,7 +1581,7 @@ kcConArgTys new_or_data res_kind arg_tys = do
 -- Kind-check the types of arguments to a Haskell98 data constructor.
 kcConH98Args :: NewOrData -> Kind -> HsConDeclH98Details GhcRn -> TcM ()
 kcConH98Args new_or_data res_kind con_args = case con_args of
-  PrefixCon tys     -> kcConArgTys new_or_data res_kind tys
+  PrefixCon _ tys   -> kcConArgTys new_or_data res_kind tys
   InfixCon ty1 ty2  -> kcConArgTys new_or_data res_kind [ty1, ty2]
   RecCon (L _ flds) -> kcConArgTys new_or_data res_kind $
                        map (hsLinear . cd_fld_type . unLoc) flds
@@ -3519,7 +3519,7 @@ tcConH98Args :: ContextKind  -- expected kind of arguments
                              -- might have a specific kind
              -> HsConDeclH98Details GhcRn
              -> TcM [(Scaled TcType, HsSrcBang)]
-tcConH98Args exp_kind (PrefixCon btys)
+tcConH98Args exp_kind (PrefixCon _ btys)
   = mapM (tcConArg exp_kind) btys
 tcConH98Args exp_kind (InfixCon bty1 bty2)
   = do { bty1' <- tcConArg exp_kind bty1
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 3f5b10f34324774504df78e8dd02029476ced9e9..13b5da759fbf864dfb11161cc1ca4177199ea67b 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -626,7 +626,7 @@ collectPatSynArgInfo :: HsPatSynDetails GhcRn
                      -> ([Name], [Name], Bool)
 collectPatSynArgInfo details =
   case details of
-    PrefixCon names      -> (map unLoc names, [], False)
+    PrefixCon _ names    -> (map unLoc names, [], False)
     InfixCon name1 name2 -> (map unLoc [name1, name2], [], True)
     RecCon names         -> (vars, sels, False)
                          where
@@ -935,7 +935,7 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name
                                     (noLoc (EmptyLocalBinds noExtField))
 
     args = case details of
-              PrefixCon args     -> args
+              PrefixCon _ args   -> args
               InfixCon arg1 arg2 -> [arg1, arg2]
               RecCon args        -> map recordPatSynPatVar args
 
@@ -986,8 +986,9 @@ tcPatToExpr name args pat = go pat
                     -> Either MsgDoc (HsExpr GhcRn)
     mkPrefixConExpr lcon@(L loc _) pats
       = do { exprs <- mapM go pats
-           ; return (foldl' (\x y -> HsApp noExtField (L loc x) y)
-                            (HsVar noExtField lcon) exprs) }
+           ; let con = L loc (HsVar noExtField lcon)
+           ; return (unLoc $ mkHsApps con exprs)
+           }
 
     mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
                     -> Either MsgDoc (HsExpr GhcRn)
@@ -1001,9 +1002,9 @@ tcPatToExpr name args pat = go pat
     go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
     go1 (ConPat NoExtField con info)
       = case info of
-          PrefixCon ps  -> mkPrefixConExpr con ps
-          InfixCon l r  -> mkPrefixConExpr con [l,r]
-          RecCon fields -> mkRecordConExpr con fields
+          PrefixCon _ ps -> mkPrefixConExpr con ps
+          InfixCon l r   -> mkPrefixConExpr con [l,r]
+          RecCon fields  -> mkRecordConExpr con fields
 
     go1 (SigPat _ pat _) = go1 (unLoc pat)
         -- See Note [Type signatures and the builder expression]
@@ -1186,7 +1187,7 @@ tcCollectEx pat = go pat
     go1 _                   = empty
 
     goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
-    goConDetails (PrefixCon ps) = mergeMany . map go $ ps
+    goConDetails (PrefixCon _ ps) = mergeMany . map go $ ps
     goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
     goConDetails (RecCon HsRecFields{ rec_flds = flds })
       = mergeMany . map goRecFd $ flds
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index 85587c29f80b00cc5e79b6f54ce664f32f184576..a1ca04b4873f3e3ac1f1339b65cbe82bbca05385 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -636,8 +636,8 @@ zonk_bind env (PatSynBind x bind@(PSB { psb_id = L loc id
 zonkPatSynDetails :: ZonkEnv
                   -> HsPatSynDetails GhcTc
                   -> HsPatSynDetails GhcTc
-zonkPatSynDetails env (PrefixCon as)
-  = PrefixCon (map (zonkLIdOcc env) as)
+zonkPatSynDetails env (PrefixCon _ as)
+  = PrefixCon noTypeArgs (map (zonkLIdOcc env) as)
 zonkPatSynDetails env (InfixCon a1 a2)
   = InfixCon (zonkLIdOcc env a1) (zonkLIdOcc env a2)
 zonkPatSynDetails env (RecCon flds)
@@ -1465,9 +1465,9 @@ zonk_pat _ pat = pprPanic "zonk_pat" (ppr pat)
 ---------------------------
 zonkConStuff :: ZonkEnv -> HsConPatDetails GhcTc
              -> TcM (ZonkEnv, HsConPatDetails GhcTc)
-zonkConStuff env (PrefixCon pats)
+zonkConStuff env (PrefixCon tyargs pats)
   = do  { (env', pats') <- zonkPats env pats
-        ; return (env', PrefixCon pats') }
+        ; return (env', PrefixCon tyargs pats') }
 
 zonkConStuff env (InfixCon p1 p2)
   = do  { (env1, p1') <- zonkPat env  p1
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index 57b56964394ceef035b00afeaa6ccb465f9ee6fb..5bde24bb12c69fd457a3e507a9c01743c196d7da 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -409,7 +409,7 @@ cvtDec (TH.PatSynD nm args dir pat)
        ; returnJustL $ Hs.ValD noExtField $ PatSynBind noExtField $
            PSB noExtField nm' args' pat' dir' }
   where
-    cvtArgs (TH.PrefixPatSyn args) = Hs.PrefixCon <$> mapM vNameL args
+    cvtArgs (TH.PrefixPatSyn args) = Hs.PrefixCon noTypeArgs <$> mapM vNameL args
     cvtArgs (TH.InfixPatSyn a1 a2) = Hs.InfixCon <$> vNameL a1 <*> vNameL a2
     cvtArgs (TH.RecordPatSyn sels)
       = do { sels' <- mapM vNameL sels
@@ -578,7 +578,7 @@ cvtConstr :: TH.Con -> CvtM (LConDecl GhcPs)
 cvtConstr (NormalC c strtys)
   = do  { c'   <- cNameL c
         ; tys' <- mapM cvt_arg strtys
-        ; returnL $ mkConDeclH98 c' Nothing Nothing (PrefixCon (map hsLinear tys')) }
+        ; returnL $ mkConDeclH98 c' Nothing Nothing (PrefixCon noTypeArgs (map hsLinear tys')) }
 
 cvtConstr (RecC c varstrtys)
   = do  { c'    <- cNameL c
@@ -1292,12 +1292,14 @@ cvtp (UnboxedSumP p alt arity)
                        = do { p' <- cvtPat p
                             ; unboxedSumChecks alt arity
                             ; return $ SumPat noExtField p' alt arity }
-cvtp (ConP s ps)       = do { s' <- cNameL s; ps' <- cvtPats ps
+cvtp (ConP s ts ps)    = do { s' <- cNameL s
+                            ; ps' <- cvtPats ps
+                            ; ts' <- mapM cvtType ts
                             ; let pps = map (parenthesizePat appPrec) ps'
                             ; return $ ConPat
                                 { pat_con_ext = noExtField
                                 , pat_con = s'
-                                , pat_args = PrefixCon pps
+                                , pat_args = PrefixCon (map mkHsPatSigType ts') pps
                                 }
                             }
 cvtp (InfixP p1 s p2)  = do { s' <- cNameL s; p1' <- cvtPat p1; p2' <- cvtPat p2
diff --git a/docs/users_guide/exts/patterns.rst b/docs/users_guide/exts/patterns.rst
index f55583fb0b0abc8c9014b70f08bdfd90753734d6..ceb96c7df74c93dc64eeb6dc5d50fc3908409325 100644
--- a/docs/users_guide/exts/patterns.rst
+++ b/docs/users_guide/exts/patterns.rst
@@ -10,3 +10,4 @@ Patterns
     view_patterns
     nk_patterns
     pattern_synonyms
+    type_applications
diff --git a/docs/users_guide/exts/type_applications.rst b/docs/users_guide/exts/type_applications.rst
index d86b4854aedd9d149084d81f6ef1af81bb6d076a..08aeb8e9e5c3d3023b61834f56b242a8e21a8294 100644
--- a/docs/users_guide/exts/type_applications.rst
+++ b/docs/users_guide/exts/type_applications.rst
@@ -4,7 +4,7 @@ Visible type application
 ========================
 
 .. extension:: TypeApplications
-    :shortdesc: Enable type application syntax in terms and types.
+    :shortdesc: Enable type application syntax in terms, patterns and types.
 
     :since: 8.0.1
 
@@ -29,6 +29,10 @@ GHC also permits visible kind application, where users can declare the kind
 arguments to be instantiated in kind-polymorphic cases. Its usage parallels
 visible type application in the term level, as specified above.
 
+In addition to visible type application in terms and types, the type application
+syntax can be used in patterns matching a data constructor to bind type variables
+in that constructor's type.
+
 .. _inferred-vs-specified:
 
 Inferred vs. specified type variables
@@ -274,3 +278,80 @@ of equality over types. For example, given the following definitions: ::
 
 GHC will deem all of ``app1 id1``, ``app1 id2``, ``app2 id1``, and ``app2 id2``
 to be well typed.
+
+.. _type-applications-in-patterns:
+
+Type Applications in Patterns
+-----------------------------
+
+The type application syntax can be used in patterns that match a data
+constructor. The syntax can't be used with record patterns or infix patterns.
+This is useful in particular to bind existential type variables associated with
+a GADT data constructor as in the following example::
+
+    {-# LANGUAGE AllowAmbiguousTypes #-}
+    {-# LANGUAGE GADTs #-}
+    {-# LANGUAGE RankNTypes #-}
+    {-# LANGUAGE TypeApplications #-}
+    import Data.Proxy
+
+    data Foo where
+      Foo :: forall a. (Show a, Num a) => Foo
+
+    test :: Foo -> String
+    test x = case x of
+      Foo @t -> show @t 0
+
+    main :: IO ()
+    main = print $ test (Foo @Float)
+
+In this example, the case in ``test``` is binding an existential variable introduced
+by ``Foo`` that otherwise could not be named and used.
+
+It's possible to bind variables to any part of the type arguments to a constructor;
+there is no need for them to be existential. In addition, it's possible to "match" against
+part of the type argument using type constructors.
+
+For a somewhat-contrived example::
+
+    foo :: (Num a) => Maybe [a] -> String
+    foo (Nothing @[t]) = show (0 :: t)
+    foo (Just @[t] xs) = show (sum xs :: t)
+
+Here, we're binding the type variable t to be the type of the elements of the list type
+which is itself the argument to Maybe.
+
+The order of the type arguments specified by the type applications in a pattern is the same
+as that for an expression: either the order as given by the user in an explicit ``forall`` in the
+definition of the data constructor, or if that is not present, the order in which the type
+variables appear in its type signature from left to right.
+
+For example if we have the following declaration in GADT syntax::
+
+    data Foo :: * -> * where
+      A :: forall s t. [(t,s)] -> Foo (t,s)
+      B :: (t,s) -> Foo (t,s)
+
+Then the type arguments to ``A`` will match first ``s`` and then ``t``, while the type arguments
+to ``B`` will match first ``t`` and then ``s``.
+
+Type arguments appearing in patterns can influence the inferred type of a definition::
+
+    foo (Nothing @Int) = 0
+    foo (Just x) = x
+
+will have inferred type:: 
+
+    foo :: Maybe Int -> Int
+
+which is more restricted than what it would be without the application::
+
+    foo :: Num a => Maybe a -> a
+
+For more information and detail regarding type applications in patterns, see the paper
+`Type variables in patterns <https://arxiv.org/pdf/1806.03476>`__ by Eisenberg, Breitner
+and Peyton Jones. Relative to that paper, the implementation in GHC for now at least makes one
+additional conservative restriction, that type variables occurring in patterns must not
+already be in scope, and so are always new variables that only bind whatever type is
+matched, rather than ever referring to a variable from an outer scope. Type wildcards
+``_`` may be used in any place where no new variable needs binding.
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
index 505b9125bcf975a0864f7004bad36e0b72f15f30..1f8175a7350191125750361ce251c4d53f7f8f9f 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
@@ -162,6 +162,8 @@ import Language.Haskell.TH.Lib.Internal hiding
   , tupE
   , unboxedTupE
 
+  , conP
+
   , Role
   , InjectivityAnn
   )
@@ -349,3 +351,9 @@ doE = Internal.doE Nothing
 
 mdoE :: Quote m => [m Stmt] -> m Exp
 mdoE = Internal.mdoE Nothing
+
+-------------------------------------------------------------------------------
+-- * Patterns
+
+conP :: Quote m => Name -> [m Pat] -> m Pat
+conP n xs = Internal.conP n [] xs
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
index fa38e6a933ee7bdb4dd493840ac1d65ae6b053b2..ed1aa022c5909fa4c5f2c6edf8a6c428beff40fd 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
@@ -125,9 +125,10 @@ unboxedTupP ps = do { ps1 <- sequenceA ps; pure (UnboxedTupP ps1)}
 unboxedSumP :: Quote m => m Pat -> SumAlt -> SumArity -> m Pat
 unboxedSumP p alt arity = do { p1 <- p; pure (UnboxedSumP p1 alt arity) }
 
-conP :: Quote m => Name -> [m Pat] -> m Pat
-conP n ps = do ps' <- sequenceA ps
-               pure (ConP n ps')
+conP :: Quote m => Name -> [m Type] -> [m Pat] -> m Pat
+conP n ts ps = do ps' <- sequenceA ps
+                  ts' <- sequenceA ts
+                  pure (ConP n ts' ps')
 infixP :: Quote m => m Pat -> Name -> m Pat -> m Pat
 infixP p1 n p2 = do p1' <- p1
                     p2' <- p2
diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
index 92b2238f72d4b85436494d234b148ce0c7ed76f7..b19c74f6fb65902215cc7f7d72b7038e1f185b1d 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
@@ -304,13 +304,15 @@ pprPat i (LitP l)     = pprLit i l
 pprPat _ (VarP v)     = pprName' Applied v
 pprPat i (TupP ps)
   | [_] <- ps
-  = pprPat i (ConP (tupleDataName 1) ps)
+  = pprPat i (ConP (tupleDataName 1) [] ps)
   | otherwise
   = parens (commaSep ps)
 pprPat _ (UnboxedTupP ps) = hashParens (commaSep ps)
 pprPat _ (UnboxedSumP p alt arity) = unboxedSumBars (ppr p) alt arity
-pprPat i (ConP s ps)  = parensIf (i >= appPrec) $ pprName' Applied s
-                                              <+> sep (map (pprPat appPrec) ps)
+pprPat i (ConP s ts ps)  = parensIf (i >= appPrec) $
+      pprName' Applied s
+  <+> sep (map (\t -> char '@' <> pprParendType t) ts)
+  <+> sep (map (pprPat appPrec) ps)
 pprPat _ (ParensP p)  = parens $ pprPat noPrec p
 pprPat i (UInfixP p1 n p2)
                       = parensIf (i > unopPrec) (pprPat unopPrec p1 <+>
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index 9c47b6cfdd2447a1e0a08e7edf918512fb97f1ed..a3104ed684da9c0273b2cf2ea43bf02ec71fef48 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -1296,7 +1296,7 @@ dataToPatQ = dataToQa id litP conP
             case nameSpace n of
                 Just DataName -> do
                     ps' <- sequence ps
-                    return (ConP n ps')
+                    return (ConP n [] ps')
                 _ -> error $ "Can't construct a pattern from name "
                           ++ showName n
 
@@ -2018,7 +2018,7 @@ data Pat
   | TupP [Pat]                      -- ^ @{ (p1,p2) }@
   | UnboxedTupP [Pat]               -- ^ @{ (\# p1,p2 \#) }@
   | UnboxedSumP Pat SumAlt SumArity -- ^ @{ (\#|p|\#) }@
-  | ConP Name [Pat]                 -- ^ @data T1 = C1 t1 t2; {C1 p1 p1} = e@
+  | ConP Name [Type] [Pat]          -- ^ @data T1 = C1 t1 t2; {C1 \@ty1 p1 p2} = e@
   | InfixP Pat Name Pat             -- ^ @foo ({x :+ y}) = e@
   | UInfixP Pat Name Pat            -- ^ @foo ({x :+ y}) = e@
                                     --
diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md
index 8cd88b5ccc3d443c35b8a62d65a941e6d3883b68..356f651fd51a05cd41c58e43a552fb94e7a9448e 100644
--- a/libraries/template-haskell/changelog.md
+++ b/libraries/template-haskell/changelog.md
@@ -34,6 +34,9 @@
 
   * The argument to `TExpQ` can now be levity polymorphic.
 
+  * The types of `ConP` and `conP` have been changed to allow for an additional list
+    of type applications preceding the argument patterns.
+
 ## 2.16.0.0 *TBA*
 
   * Add support for tuple sections. (#15843) The type signatures of `TupE` and
diff --git a/testsuite/tests/hiefile/should_compile/Scopes.hs b/testsuite/tests/hiefile/should_compile/Scopes.hs
index f8a76298bb5544ca079a83504ba663300a3962bb..21766c64463c01064528cf65accfb797e8f55db3 100644
--- a/testsuite/tests/hiefile/should_compile/Scopes.hs
+++ b/testsuite/tests/hiefile/should_compile/Scopes.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE PatternSynonyms, ViewPatterns #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
 module Scopes where
 
 -- Verify that evidence bound by patern
diff --git a/testsuite/tests/hiefile/should_compile/ScopesBug.hs b/testsuite/tests/hiefile/should_compile/ScopesBug.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ea87d308d41b871b4cc0ceb614e426738bd93a71
--- /dev/null
+++ b/testsuite/tests/hiefile/should_compile/ScopesBug.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
+module ScopesBug where
+
+data Proxy (a :: k) = Proxy
+data Con k (a :: k) = Con (Proxy a)
+
+tyApp :: Con k a -> Proxy a
+tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
diff --git a/testsuite/tests/hiefile/should_compile/all.T b/testsuite/tests/hiefile/should_compile/all.T
index 489cff28d0d39f732ab591740105342354dd284a..86fbd6e20f9e55e181e482179a0d6aad38c8f9b1 100644
--- a/testsuite/tests/hiefile/should_compile/all.T
+++ b/testsuite/tests/hiefile/should_compile/all.T
@@ -19,3 +19,5 @@ test('hie010',       normal,                   compile, ['-fno-code -fwrite-ide-
 test('CPP',          normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
 test('Constructors', normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
 test('Scopes',       normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
+# See https://gitlab.haskell.org/ghc/ghc/-/issues/18425 and https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2464#note_301989
+test('ScopesBug',    expect_broken(18425),     compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
\ No newline at end of file
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index 31f8b10c25804dacc05d20ac878e0005f4067e23..262d01fc4f78a36de08728d4376b70bb166b6b17 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -52,6 +52,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [])
           (Nothing)))
        ,({ DumpParsedAst.hs:7:21-30 }
@@ -65,6 +66,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [(HsScaled
              (HsLinearArrow
               (NormalSyntax))
@@ -256,6 +258,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [(HsScaled
              (HsLinearArrow
               (NormalSyntax))
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 29377597aeb3f34010846afa0efa15bafa2886d7..61c89188c2ab4f697c4d1cb2e9141d81759cc497 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -87,6 +87,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [])
             (Nothing)))
          ,({ DumpRenamedAst.hs:9:21-30 }
@@ -99,6 +100,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
@@ -500,6 +502,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
diff --git a/testsuite/tests/parser/should_compile/T14189.stderr b/testsuite/tests/parser/should_compile/T14189.stderr
index 32ae85e4dcd0d88ee0474ee8752e808fdac713cf..52f2099d6e7d3f57cf22523c234460eb6e8dd997 100644
--- a/testsuite/tests/parser/should_compile/T14189.stderr
+++ b/testsuite/tests/parser/should_compile/T14189.stderr
@@ -41,6 +41,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
@@ -61,6 +62,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [])
             (Nothing)))
          ,({ T14189.hs:6:29-42 }
diff --git a/testsuite/tests/parser/should_fail/T18251d.stderr b/testsuite/tests/parser/should_fail/T18251d.stderr
index 4e649220700ee4b055dd2670e1a4213128548757..15825502e07537f6a09021d353f2b9c2bdc39d7b 100644
--- a/testsuite/tests/parser/should_fail/T18251d.stderr
+++ b/testsuite/tests/parser/should_fail/T18251d.stderr
@@ -1,3 +1,4 @@
 
 T18251d.hs:6:1: error:
-    Type applications in patterns are not yet supported
+    Parse error in pattern: f @a
+    Type applications in patterns are only allowed on data constructors.
diff --git a/testsuite/tests/quasiquotation/T7918A.hs b/testsuite/tests/quasiquotation/T7918A.hs
index f20dfeef596b27bb8e41a1b656f97e487fa028bf..0792ee9d1b3b07b5661966dde185b4a93165b33e 100644
--- a/testsuite/tests/quasiquotation/T7918A.hs
+++ b/testsuite/tests/quasiquotation/T7918A.hs
@@ -19,7 +19,7 @@ qq = QuasiQuoter {
                          y = VarP (mkName "y")
                      in \str -> case str of
                                   "p1" -> return $ x
-                                  "p2" -> return $ ConP 'Just [x]
+                                  "p2" -> return $ ConP 'Just [] [x]
                                   "p3" -> return $ TupP [x, y]
                                   "p4" -> return $ y
        , quoteDec  = undefined
diff --git a/testsuite/tests/quasiquotation/qq005/Expr.hs b/testsuite/tests/quasiquotation/qq005/Expr.hs
index 767d906ba4176e07523c7914855e2b3656c4db0b..bb0266684770095d465fbcc22832d38d6552e28b 100644
--- a/testsuite/tests/quasiquotation/qq005/Expr.hs
+++ b/testsuite/tests/quasiquotation/qq005/Expr.hs
@@ -97,9 +97,8 @@ parseExprPat s =  do  loc <- location
                       dataToPatQ (const Nothing `extQ` antiExprPat) expr
 
 antiExprPat :: Expr -> Maybe (Q Pat)
-antiExprPat  (AntiIntExpr v)  = Just $ conP  (mkName "IntExpr")
-                                                [varP (mkName v)]
-antiExprPat  (AntiExpr v)     = Just $ varP  (mkName v)
+antiExprPat  (AntiIntExpr v)  = Just $ conP (mkName "IntExpr") [varP (mkName v)]
+antiExprPat  (AntiExpr v)     = Just $ varP (mkName v)
 antiExprPat  _                = Nothing
 
 -- Copied from syb for the test
diff --git a/testsuite/tests/th/T3899a.hs b/testsuite/tests/th/T3899a.hs
index a63c17b0d324f18052df840b424ac1a0c17fd58b..1b5e7d69c1b83bf658394d423cae2aacedc075c4 100644
--- a/testsuite/tests/th/T3899a.hs
+++ b/testsuite/tests/th/T3899a.hs
@@ -10,6 +10,6 @@ data Nil = Nil
 
 nestedTuple n = do
      xs <- replicateM n (newName "x")
-     return $ LamE [foldr (\v prev -> ParensP (ConP 'Cons [VarP v,prev]))
-                       (ConP 'Nil []) xs]
+     return $ LamE [foldr (\v prev -> ParensP (ConP 'Cons [] [VarP v,prev]))
+                       (ConP 'Nil [] []) xs]
                    (TupE $ map (Just . VarE) xs)
diff --git a/testsuite/tests/th/TH_repPatSig_asserts.hs b/testsuite/tests/th/TH_repPatSig_asserts.hs
index 42ade65ab418b2cd496f5c88ae46d5cdf4c1578f..c9ea09dc99de02a18e4e7d884bff1bc673c4bfb1 100644
--- a/testsuite/tests/th/TH_repPatSig_asserts.hs
+++ b/testsuite/tests/th/TH_repPatSig_asserts.hs
@@ -35,7 +35,7 @@ assertVar expQ = do
   exp <- expQ
   case exp of
     LamE [SigP (VarP x) (AppT (ConT _) (VarT a))]
-         (CaseE (VarE x1) [Match (ConP _ [VarP y])
+         (CaseE (VarE x1) [Match (ConP _ [] [VarP y])
                                  (NormalB (SigE (VarE y1) (VarT a1))) []])
       | x1 == x &&
         y1 == y &&
diff --git a/testsuite/tests/th/TH_repUnboxedTuples.stderr b/testsuite/tests/th/TH_repUnboxedTuples.stderr
index 3687b77a0e8d8202083ddbd0c2a927c12b114428..b8bedac854badb4a694a2d98433682e08b18cf1a 100644
--- a/testsuite/tests/th/TH_repUnboxedTuples.stderr
+++ b/testsuite/tests/th/TH_repUnboxedTuples.stderr
@@ -1,4 +1,4 @@
-CaseE (UnboxedTupE [Just (LitE (CharL 'b')),Just (ConE GHC.Types.False)]) [Match (UnboxedTupP [LitP (CharL 'a'),ConP GHC.Types.True []]) (NormalB (UnboxedTupE [Just (LitE (StringL "One")),Just (LitE (IntegerL 1))])) [],Match (UnboxedTupP [LitP (CharL 'b'),ConP GHC.Types.False []]) (NormalB (UnboxedTupE [Just (LitE (StringL "Two")),Just (LitE (IntegerL 2))])) [],Match (UnboxedTupP [WildP,WildP]) (NormalB (UnboxedTupE [Just (LitE (StringL "Three")),Just (LitE (IntegerL 3))])) []]
+CaseE (UnboxedTupE [Just (LitE (CharL 'b')),Just (ConE GHC.Types.False)]) [Match (UnboxedTupP [LitP (CharL 'a'),ConP GHC.Types.True [] []]) (NormalB (UnboxedTupE [Just (LitE (StringL "One")),Just (LitE (IntegerL 1))])) [],Match (UnboxedTupP [LitP (CharL 'b'),ConP GHC.Types.False [] []]) (NormalB (UnboxedTupE [Just (LitE (StringL "Two")),Just (LitE (IntegerL 2))])) [],Match (UnboxedTupP [WildP,WildP]) (NormalB (UnboxedTupE [Just (LitE (StringL "Three")),Just (LitE (IntegerL 3))])) []]
 case (# 'b', GHC.Types.False #) of
     (# 'a', GHC.Types.True #) -> (# "One", 1 #)
     (# 'b', GHC.Types.False #) -> (# "Two", 2 #)
diff --git a/testsuite/tests/th/TH_unresolvedInfix.hs b/testsuite/tests/th/TH_unresolvedInfix.hs
index 3c34b976a362b15fce94380820571d3394d2afe4..d9af48491ace6520acc0ece0b6b6862e2472b88a 100644
--- a/testsuite/tests/th/TH_unresolvedInfix.hs
+++ b/testsuite/tests/th/TH_unresolvedInfix.hs
@@ -123,7 +123,7 @@ main = do
 
   -- pretty-printing of unresolved infix expressions
   let ne = ConE $ mkName "N"
-      np = ConP (mkName "N") []
+      np = ConP (mkName "N") [] []
       nt = ConT (mkName "Int")
       plusE = ConE (mkName ":+")
       plusP = (mkName ":+")
diff --git a/testsuite/tests/th/TH_unresolvedInfix.stdout b/testsuite/tests/th/TH_unresolvedInfix.stdout
index 4f81fdafa92bb58a59f464fbcd2dfa7235f4de3b..395368588191e36259023e874a31d84424eb0a50 100644
--- a/testsuite/tests/th/TH_unresolvedInfix.stdout
+++ b/testsuite/tests/th/TH_unresolvedInfix.stdout
@@ -36,8 +36,8 @@ True
 True
 InfixE (Just (InfixE (Just (ConE TH_unresolvedInfix_Lib.N)) (ConE TH_unresolvedInfix_Lib.:*) (Just (ConE TH_unresolvedInfix_Lib.N)))) (ConE TH_unresolvedInfix_Lib.:+) (Just (ConE TH_unresolvedInfix_Lib.N))
 InfixE (Just (InfixE (Just (ConE TH_unresolvedInfix_Lib.N)) (ConE TH_unresolvedInfix_Lib.:*) (Just (ConE TH_unresolvedInfix_Lib.N)))) (ConE TH_unresolvedInfix_Lib.:+) (Just (ConE TH_unresolvedInfix_Lib.N))
-InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [])
-InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [])
+InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N [] []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [] [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [] [])
+InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N [] []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [] [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [] [])
 AppT (AppT (ConT TH_unresolvedInfix_Lib.+) (AppT (AppT (ConT TH_unresolvedInfix_Lib.*) (ConT GHC.Types.Int)) (ConT GHC.Types.Int))) (ConT GHC.Types.Int)
 AppT (AppT (ConT TH_unresolvedInfix_Lib.+) (AppT (AppT (ConT TH_unresolvedInfix_Lib.*) (ConT GHC.Types.Int)) (ConT GHC.Types.Int))) (ConT GHC.Types.Int)
 N :+ (N :+ N :+ N)
diff --git a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
index e636c0c4f1d2eff94400c3c0d318abfe2a8d23ef..d245bb9cee9b600c775a06db6dcdd929f0257c49 100644
--- a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
+++ b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
@@ -1,6 +1,6 @@
 InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2)))
 LamE [VarP x] (InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2))))
 [DataD [] Foo [] Nothing [NormalC Foo []] []]
-ConP GHC.Tuple.() []
+ConP GHC.Tuple.() [] []
 AppT ListT (ConT GHC.Types.Int)
 InfixE Nothing (VarE GHC.Num.+) (Just (LitE (IntegerL 1)))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs
new file mode 100644
index 0000000000000000000000000000000000000000..7411ba07ee1afb45ef4985d3723f9233d7c69a26
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo where
+  MkFoo :: forall a. a -> (a -> String) -> Foo
+
+foo :: Foo -> String
+foo (MkFoo @a x f) = f (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs
new file mode 100644
index 0000000000000000000000000000000000000000..7e207c312a03e55c5c08be66578b3c3bad8ec6ef
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo where
+  MkFoo :: forall a b. a -> (a -> String) -> b -> (b -> String) -> Foo
+
+foo :: Foo -> String
+foo (MkFoo @u @v x f y g) = f (x :: u) ++ g (y :: v)
+
+main = do
+  print (foo (MkFoo "hello" reverse True show))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs
new file mode 100644
index 0000000000000000000000000000000000000000..bba4c1df185adcfea005cacbcc718ab34007dbbc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+data Proxy (a :: k) = Proxy
+
+data Con k (a :: k) = Con (Proxy a)
+
+tyApp :: Con k a -> Proxy a
+tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
+
+main = return ()
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs
new file mode 100644
index 0000000000000000000000000000000000000000..47812d994ddca5d61facf3aa537aa2f3677482a8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo b where
+  MkFoo :: forall b a. a -> (b -> a -> String) -> Foo b
+
+foo :: Foo b -> b -> String
+foo (MkFoo @b @a x f) u = f (u :: b) (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" (\x y -> reverse y ++ show x)) (6 :: Integer))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs
new file mode 100644
index 0000000000000000000000000000000000000000..aeaa4fcac3bb2d8e1ca729bc94d1bbe8e170e668
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Main where
+
+import Language.Haskell.TH
+
+apat :: Q Pat
+apat = [p| Just @[a] xs |]
+
+main = do
+  print ()
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs
new file mode 100644
index 0000000000000000000000000000000000000000..7a74ff8403c8dae47b9c27c93265f0ebf0160b86
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+foo :: Foo String -> String
+foo (MkFoo @a x f) = f (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..cccee20cb1f4f74ceb706bf5fa3fdecf45c4bfef
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+import Data.Maybe
+
+data Foo a where
+  MkFoo :: a -> (String -> String) -> Foo a
+
+foo :: Foo (Int, [Char], Maybe String -> Bool) -> String
+foo (MkFoo @(u, [v], f w -> x) x f) = f (unwords [show @u 5, show @v 'c', show (fmap @f not (Just (True :: x))) :: w])
+
+main = do
+  print (foo (MkFoo (6,"hello",isJust) reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f01b6067991c9036ee009a9ec8c25a7fb078d3fb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+
+module Main where
+
+data Foo a b where
+  MkFoo :: forall b a. a -> (a -> b -> String) -> Foo a b
+
+foo :: Foo a b -> b -> String
+foo (MkFoo @c @d x f) t = f (x :: d) (t :: c)
+
+main = do
+  print (foo (MkFoo True (\x y -> show x ++ show y) :: Foo Bool Integer) (6 :: Integer))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs
new file mode 100644
index 0000000000000000000000000000000000000000..89fb88d5fe664ec7277f9e58ab967f3edc7909e6
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+foo :: Foo String -> Foo String -> String
+foo (MkFoo @a x f) (MkFoo @b y g) = f (x :: a) ++ g (y :: b)
+
+main = do
+  print (foo (MkFoo "hello" reverse) (MkFoo "goodbye" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs
new file mode 100644
index 0000000000000000000000000000000000000000..e7f552277630f23620360f1f260c9f78b26d4306
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: Maybe a -> (a -> String) -> Foo a
+
+foo :: Foo String -> String
+foo (MkFoo @a (Nothing @b) f) = "nothing"
+foo (MkFoo @a (Just @b x) f) = f ((x :: b) :: a)
+
+main = do
+  print (foo (MkFoo (Just "hello") reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs
new file mode 100644
index 0000000000000000000000000000000000000000..722a9b4d635758e80750b353395e78268b83a6ec
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module Main where
+
+f :: Maybe Int -> Int
+f (Just @_ x) = x
+f Nothing = 0
+
+Just @_ x = Just "hello"
+
+Just @Int y = Just 5
+
+main = do
+  print x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3a36e779227746f387e968dbb17f4f4dee170d8f..344b4394a9dd25bdf0e0986d4c2c89e7c265bfc8 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -737,3 +737,15 @@ test('InstanceGivenOverlap2', normal, compile, [''])
 test('LocalGivenEqs', normal, compile, [''])
 test('LocalGivenEqs2', normal, compile, [''])
 test('T18891', normal, compile, [''])
+
+test('TyAppPat_Existential', normal, compile, [''])
+test('TyAppPat_ExistentialMulti', normal, compile, [''])
+test('TyAppPat_KindDependency', normal, compile, [''])
+test('TyAppPat_Universal', normal, compile, [''])
+test('TyAppPat_Mixed', normal, compile, [''])
+test('TyAppPat_TH', normal, compile, [''])
+test('TyAppPat_UniversalMulti1', normal, compile, [''])
+test('TyAppPat_UniversalMulti2', normal, compile, [''])
+test('TyAppPat_UniversalMulti3', normal, compile, [''])
+test('TyAppPat_UniversalNested', normal, compile, [''])
+test('TyAppPat_Wildcard', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d163874c8e7fb3fad58c1301f400f99644996817
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Some = forall a. Some a
+
+foo (Some @a x) = (x :: a)
+
+main = do
+  print (foo (Some (5 :: Integer)) :: Integer)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..06f7c3adcad9613440595a48d21823690ca98533
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr
@@ -0,0 +1,15 @@
+
+TyAppPat_ExistentialEscape.hs:9:20: error:
+    • Couldn't match expected type ‘p’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor: Some :: forall a. a -> Some,
+        in an equation for ‘foo’
+        at TyAppPat_ExistentialEscape.hs:9:6-14
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: Some -> p
+        at TyAppPat_ExistentialEscape.hs:9:1-26
+    • In the expression: x :: a
+      In an equation for ‘foo’: foo (Some @a x) = (x :: a)
+    • Relevant bindings include
+        x :: a (bound at TyAppPat_ExistentialEscape.hs:9:14)
+        foo :: Some -> p (bound at TyAppPat_ExistentialEscape.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4285a735727f34b751a7640d2f6728410f76e34e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data T a = MkT a a
+
+foo (MkT x @a y) = (x :: a)
+
+main = do
+  print (foo (MkT True False))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..61ab78e86cf51b5be24d23db540e4b9222e14c00
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr
@@ -0,0 +1,3 @@
+
+TyAppPat_MisplacedApplication.hs:9:6: error:
+    Parse error in pattern: MkT x
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs
new file mode 100644
index 0000000000000000000000000000000000000000..db50abb7a5cba39cde3d6f4e79ce92edadca9680
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a b where
+  MkFoo :: a -> (a -> String) -> b -> Foo a b
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Foo String String -> String
+foo (MkFoo @a @a x f y) = f (x ++ y :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse "goodbye"))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..4b891df79783ebd2b0f0f3a0ed91134a9831ec52
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
@@ -0,0 +1,4 @@
+
+TyAppPat_NonlinearMultiAppPat.hs:12:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs
new file mode 100644
index 0000000000000000000000000000000000000000..557ebb1d975388d66a2002b8da6ed11864ed3933
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Maybe String -> Maybe String -> String
+foo (Nothing @a) (Nothing @a) = ("" :: a)
+foo (Just @a x) (Nothing @a) = (x :: a)
+foo (Nothing @a) (Just @a y) = (y :: a)
+foo (Just @a x) (Just @a y) = (x ++ y :: a)
+
+main = do
+  print (foo Nothing (Just "hello"))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..48aeba149e9de4ce16dbecbc63220092601a395e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
@@ -0,0 +1,16 @@
+
+TyAppPat_NonlinearMultiPat.hs:9:19: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:10:18: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:11:19: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:12:18: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f80e6d448c2f523d55ec027484364636d44525ee
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Foo (String, String) -> String
+foo (MkFoo @(a,a) (x,y) f) = f (x :: a, y :: a)
+
+main = do
+  print (foo (MkFoo ("hello", "goodbye") (\(x,y) -> reverse y ++ reverse x)))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..b25bfcde343cb33e04aeaf05e17f08e10e9e8e3f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
@@ -0,0 +1,3 @@
+
+TyAppPat_NonlinearSinglePat.hs:12:6: error:
+    Variable `a' would be bound multiple times by a type argument.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs
new file mode 100644
index 0000000000000000000000000000000000000000..7d6b8a47a54c1c40be9eaedae0c78b71ea042936
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+foo :: Maybe a -> a
+foo (Just @Int x) = x
+foo Nothing = 0
+
+main = do
+  print (foo (Just 5))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..4d70de517c7f32a412b1a4a05cff416c0a0f038e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr
@@ -0,0 +1,11 @@
+
+TyAppPat_Nonmatching.hs:8:6: error:
+    • Couldn't match expected type ‘a’ with actual type ‘Int’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a. Maybe a -> a
+        at TyAppPat_Nonmatching.hs:7:1-19
+    • In the pattern: Just @Int x
+      In an equation for ‘foo’: foo (Just @Int x) = x
+    • Relevant bindings include
+        foo :: Maybe a -> a (bound at TyAppPat_Nonmatching.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs
new file mode 100644
index 0000000000000000000000000000000000000000..978e611501d5b4ff07471dab02b366b169a00d9f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+x :: Integer
+Just @a x = Just (5 :: Integer)
+
+main = do
+  print x
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..e0d18596e02fa70061a9d2032d40cbc5453389b7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr
@@ -0,0 +1,5 @@
+
+TyAppPat_PatternBinding.hs:8:1: error:
+    • Binding type variables is not allowed in pattern bindings
+    • In the pattern: Just @a x
+      In a pattern binding: Just @a x = Just (5 :: Integer)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs
new file mode 100644
index 0000000000000000000000000000000000000000..bd888b3bac1c76a29595682bd0251ebcc13e5033
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Some = forall a. Some a
+
+Some @a x = Some (5 :: Integer)
+
+main = do
+  print (x :: a)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..9204f8016a4a4ae61dc724f41a54a4d1ab1a2c5b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr
@@ -0,0 +1,32 @@
+
+TyAppPat_PatternBindingExistential.hs:9:1: error:
+    • Binding type variables is not allowed in pattern bindings
+    • In the pattern: Some @a x
+      In a pattern binding: Some @a x = Some (5 :: Integer)
+
+TyAppPat_PatternBindingExistential.hs:9:9: error:
+    • Couldn't match expected type ‘p’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor: Some :: forall a. a -> Some,
+        in a pattern binding
+        at TyAppPat_PatternBindingExistential.hs:9:1-9
+      ‘p’ is a rigid type variable bound by
+        the inferred type of x :: p
+        at TyAppPat_PatternBindingExistential.hs:9:1-31
+    • In the pattern: Some @a x
+      In a pattern binding: Some @a x = Some (5 :: Integer)
+
+TyAppPat_PatternBindingExistential.hs:12:3: error:
+    • Ambiguous type variable ‘a0’ arising from a use of ‘print’
+      prevents the constraint ‘(Show a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Show Ordering -- Defined in ‘GHC.Show’
+        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+        instance Show Integer -- Defined in ‘GHC.Show’
+        ...plus 22 others
+        ...plus 12 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In a stmt of a 'do' block: print (x :: a)
+      In the expression: do print (x :: a)
+      In an equation for ‘main’: main = do print (x :: a)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
new file mode 100644
index 0000000000000000000000000000000000000000..6906ed627b2dad7c2148a9e0d1251aa100e01053
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: forall a. Monoid a => Maybe a -> a
+foo (Nothing @a) = (mempty :: a)
+foo (Just @a x) = (x :: a)
+
+main = do
+  print (foo @String Nothing)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..5ce650e4beab91497eeef238aba81d650283ec71
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
@@ -0,0 +1,8 @@
+
+TyAppPat_ScopedTyVarConflict.hs:10:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_ScopedTyVarConflict.hs:11:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs
new file mode 100644
index 0000000000000000000000000000000000000000..03f44f052fe423c73b1e4d2589a1df16ce27f71d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs
@@ -0,0 +1,5 @@
+module TyAppPat_TooMany where
+
+f :: Maybe Int -> Int
+f (Just @Int @Bool x) = x
+f Nothing = 10
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..87e904491925c8e1b0da5f16db5176331acdf654
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr
@@ -0,0 +1,6 @@
+
+TyAppPat_TooMany.hs:4:4: error:
+    • Too many type arguments in constructor pattern for ‘Just’
+      Expected no more than 1; got 2
+    • In the pattern: Just @Int @Bool x
+      In an equation for ‘f’: f (Just @Int @Bool x) = x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 913d6d802945f597f46de8d7ca2e6be683f02422..3eff08d08037f47204b96a45fb20804356581802 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -593,3 +593,13 @@ test('T10709', normal, compile_fail, [''])
 test('T10709b', normal, compile_fail, [''])
 test('GivenForallLoop', normal, compile_fail, [''])
 test('T18891a', normal, compile_fail, [''])
+test('TyAppPat_ExistentialEscape', normal, compile_fail, [''])
+test('TyAppPat_MisplacedApplication', normal, compile_fail, [''])
+test('TyAppPat_NonlinearMultiAppPat', normal, compile_fail, [''])
+test('TyAppPat_NonlinearMultiPat', normal, compile_fail, [''])
+test('TyAppPat_NonlinearSinglePat', normal, compile_fail, [''])
+test('TyAppPat_Nonmatching', normal, compile_fail, [''])
+test('TyAppPat_PatternBinding', normal, compile_fail, [''])
+test('TyAppPat_PatternBindingExistential', normal, compile_fail, [''])
+test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
+test('TyAppPat_TooMany', normal, compile_fail, [''])
diff --git a/utils/haddock b/utils/haddock
index 8d260690b53f2fb6b54ba78bd13d1400d9ebd395..acf235d607879eb9542127eb0ddb42a250b5b850 160000
--- a/utils/haddock
+++ b/utils/haddock
@@ -1 +1 @@
-Subproject commit 8d260690b53f2fb6b54ba78bd13d1400d9ebd395
+Subproject commit acf235d607879eb9542127eb0ddb42a250b5b850