Implement type applications in patterns

The haddock submodule is also updated so that it understands the changes
to patterns.

31 files changed, 404 insertions, 171 deletions

diff --git a/compiler/GHC/Hs/Binds.hs b/compiler/GHC/Hs/Binds.hs
index 41db2d5f85..270dc97364 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 dcb810ed7e..882303373f 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 3033806ddd..a1d59699c5 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 ad950883f4..dde27857ec 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 e530110cda..0051eaa2c9 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 72e4fe99c3..0f80c61d65 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 c1479d7c9a..c7eeaec586 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 12c9a49278..bd48a19024 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 ca6ad7f483..39817044cc 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 98b23dab25..1abe0fc9dc 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 7f2d0b5d85..7f675e8253 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 70bb33b7d0..3917998c3e 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 5ec88929fe..e9de7eea78 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 cf93890532..582b47535d 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 c4b411b1c3..a26f6809c6 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 1b4151cfb7..a59e4a882f 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 21f74a878e..f291830ea2 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 26795def9f..ba7ca1d9c1 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 953d3c2c9b..30fef1b980 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 cd5d431ee1..9cf422a92e 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 e0deda3b1d..92ae90bedd 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 b0f15d3d19..74b93624f0 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 2e93ad882d..3acf9d83d2 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 f41f99be2d..6748e8a4c4 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 5500c7692c..8507c0d7ff 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 ec9d1da5e9..bbbd528830 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 468410400f..dfb6e4fe3e 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 1378eda16e..50d4f72610 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 3f5b10f343..13b5da759f 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 85587c29f8..a1ca04b487 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 57b5696439..5bde24bb12 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