diff --git a/compiler/GHC/Builtin/Names/TH.hs b/compiler/GHC/Builtin/Names/TH.hs
index 0ea14689274bade5b91e30779e9aea08afee2834..af9ef6c9529a6bfc46caa349ddf5e909181bb10b 100644
--- a/compiler/GHC/Builtin/Names/TH.hs
+++ b/compiler/GHC/Builtin/Names/TH.hs
@@ -48,15 +48,17 @@ templateHaskellNames = [
     conPName, tildePName, bangPName, infixPName,
     asPName, wildPName, recPName, listPName, sigPName, viewPName,
     typePName,
+    -- ArgPat
+    visAPName, invisAPName,
     -- FieldPat
     fieldPatName,
     -- Match
     matchName,
     -- Clause
-    clauseName,
+    clauseArgName,
     -- Exp
     varEName, conEName, litEName, appEName, appTypeEName, infixEName,
-    infixAppName, sectionLName, sectionRName, lamEName, lamCaseEName,
+    infixAppName, sectionLName, sectionRName, lamArgEName, lamCaseEName,
     lamCasesEName, tupEName, unboxedTupEName, unboxedSumEName,
     condEName, multiIfEName, letEName, caseEName, doEName, mdoEName, compEName,
     fromEName, fromThenEName, fromToEName, fromThenToEName,
@@ -159,7 +161,8 @@ templateHaskellNames = [
     liftClassName, quoteClassName,
 
     -- And the tycons
-    qTyConName, nameTyConName, patTyConName, fieldPatTyConName, matchTyConName,
+    qTyConName, nameTyConName, patTyConName, argPatTyConName,
+    fieldPatTyConName, matchTyConName,
     expQTyConName, fieldExpTyConName, predTyConName,
     stmtTyConName,  decsTyConName, conTyConName, bangTypeTyConName,
     varBangTypeTyConName, typeQTyConName, expTyConName, decTyConName,
@@ -204,7 +207,7 @@ liftClassName = thCls (fsLit "Lift") liftClassKey
 quoteClassName :: Name
 quoteClassName = thCls (fsLit "Quote") quoteClassKey
 
-qTyConName, nameTyConName, fieldExpTyConName, patTyConName,
+qTyConName, nameTyConName, fieldExpTyConName, patTyConName, argPatTyConName,
     fieldPatTyConName, expTyConName, decTyConName, typeTyConName,
     matchTyConName, clauseTyConName, funDepTyConName, predTyConName,
     codeTyConName, injAnnTyConName, overlapTyConName, decsTyConName,
@@ -213,6 +216,7 @@ qTyConName             = thTc (fsLit "Q")              qTyConKey
 nameTyConName          = thTc (fsLit "Name")           nameTyConKey
 fieldExpTyConName      = thTc (fsLit "FieldExp")       fieldExpTyConKey
 patTyConName           = thTc (fsLit "Pat")            patTyConKey
+argPatTyConName        = thTc (fsLit "ArgPat")         argPatTyConKey
 fieldPatTyConName      = thTc (fsLit "FieldPat")       fieldPatTyConKey
 expTyConName           = thTc (fsLit "Exp")            expTyConKey
 decTyConName           = thTc (fsLit "Dec")            decTyConKey
@@ -289,6 +293,12 @@ sigPName   = libFun (fsLit "sigP")   sigPIdKey
 viewPName  = libFun (fsLit "viewP")  viewPIdKey
 typePName  = libFun (fsLit "typeP")  typePIdKey
 
+-- data ArgPat = ...
+visAPName, invisAPName :: Name
+
+visAPName   = libFun (fsLit "visAP")  visAPIdKey
+invisAPName = libFun (fsLit "invisAP")  invisAPIdKey
+
 -- type FieldPat = ...
 fieldPatName :: Name
 fieldPatName = libFun (fsLit "fieldPat") fieldPatIdKey
@@ -298,12 +308,12 @@ matchName :: Name
 matchName = libFun (fsLit "match") matchIdKey
 
 -- data Clause = ...
-clauseName :: Name
-clauseName = libFun (fsLit "clause") clauseIdKey
+clauseArgName :: Name
+clauseArgName = libFun (fsLit "clauseArg") clauseArgIdKey
 
 -- data Exp = ...
 varEName, conEName, litEName, appEName, appTypeEName, infixEName, infixAppName,
-    sectionLName, sectionRName, lamEName, lamCaseEName, lamCasesEName, tupEName,
+    sectionLName, sectionRName, lamArgEName, lamCaseEName, lamCasesEName, tupEName,
     unboxedTupEName, unboxedSumEName, condEName, multiIfEName, letEName,
     caseEName, doEName, mdoEName, compEName, staticEName, unboundVarEName,
     labelEName, implicitParamVarEName, getFieldEName, projectionEName, typeEName :: Name
@@ -316,7 +326,7 @@ infixEName            = libFun (fsLit "infixE")            infixEIdKey
 infixAppName          = libFun (fsLit "infixApp")          infixAppIdKey
 sectionLName          = libFun (fsLit "sectionL")          sectionLIdKey
 sectionRName          = libFun (fsLit "sectionR")          sectionRIdKey
-lamEName              = libFun (fsLit "lamE")              lamEIdKey
+lamArgEName           = libFun (fsLit "lamArgE")           lamArgEIdKey
 lamCaseEName          = libFun (fsLit "lamCaseE")          lamCaseEIdKey
 lamCasesEName         = libFun (fsLit "lamCasesE")         lamCasesEIdKey
 tupEName              = libFun (fsLit "tupE")              tupEIdKey
@@ -680,7 +690,7 @@ quoteClassKey = mkPreludeClassUnique 201
 -- Check in GHC.Builtin.Names if you want to change this
 
 expTyConKey, matchTyConKey, clauseTyConKey, qTyConKey, expQTyConKey,
-    patTyConKey,
+    patTyConKey, argPatTyConKey,
     stmtTyConKey, conTyConKey, typeQTyConKey, typeTyConKey,
     tyVarBndrUnitTyConKey, tyVarBndrSpecTyConKey, tyVarBndrVisTyConKey,
     decTyConKey, bangTypeTyConKey, varBangTypeTyConKey,
@@ -696,6 +706,7 @@ clauseTyConKey          = mkPreludeTyConUnique 202
 qTyConKey               = mkPreludeTyConUnique 203
 expQTyConKey            = mkPreludeTyConUnique 204
 patTyConKey             = mkPreludeTyConUnique 206
+argPatTyConKey          = mkPreludeTyConUnique 207
 stmtTyConKey            = mkPreludeTyConUnique 209
 conTyConKey             = mkPreludeTyConUnique 210
 typeQTyConKey           = mkPreludeTyConUnique 211
@@ -834,6 +845,12 @@ sigPIdKey         = mkPreludeMiscIdUnique 253
 viewPIdKey        = mkPreludeMiscIdUnique 254
 typePIdKey        = mkPreludeMiscIdUnique 255
 
+-- data ArgPat = ...
+
+visAPIdKey, invisAPIdKey :: Unique
+visAPIdKey        = mkPreludeMiscIdUnique 256
+invisAPIdKey      = mkPreludeMiscIdUnique 257
+
 -- type FieldPat = ...
 fieldPatIdKey :: Unique
 fieldPatIdKey       = mkPreludeMiscIdUnique 260
@@ -843,13 +860,13 @@ matchIdKey :: Unique
 matchIdKey          = mkPreludeMiscIdUnique 261
 
 -- data Clause = ...
-clauseIdKey :: Unique
-clauseIdKey         = mkPreludeMiscIdUnique 262
+clauseArgIdKey :: Unique
+clauseArgIdKey         = mkPreludeMiscIdUnique 262
 
 
 -- data Exp = ...
 varEIdKey, conEIdKey, litEIdKey, appEIdKey, appTypeEIdKey, infixEIdKey,
-    infixAppIdKey, sectionLIdKey, sectionRIdKey, lamEIdKey, lamCaseEIdKey,
+    infixAppIdKey, sectionLIdKey, sectionRIdKey, lamArgEIdKey, lamCaseEIdKey,
     lamCasesEIdKey, tupEIdKey, unboxedTupEIdKey, unboxedSumEIdKey, condEIdKey,
     multiIfEIdKey, letEIdKey, caseEIdKey, doEIdKey, compEIdKey,
     fromEIdKey, fromThenEIdKey, fromToEIdKey, fromThenToEIdKey,
@@ -865,7 +882,7 @@ infixEIdKey            = mkPreludeMiscIdUnique 275
 infixAppIdKey          = mkPreludeMiscIdUnique 276
 sectionLIdKey          = mkPreludeMiscIdUnique 277
 sectionRIdKey          = mkPreludeMiscIdUnique 278
-lamEIdKey              = mkPreludeMiscIdUnique 279
+lamArgEIdKey           = mkPreludeMiscIdUnique 279
 lamCaseEIdKey          = mkPreludeMiscIdUnique 280
 lamCasesEIdKey         = mkPreludeMiscIdUnique 281
 tupEIdKey              = mkPreludeMiscIdUnique 282
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index f2c489396f82394a7e607cd20d7117504227af92..5561dad9c05b8f997321afe006ab3dfe4f4603a6 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -1486,10 +1486,11 @@ matchGroupArity :: MatchGroup (GhcPass id) body -> Arity
 -- Precondition: MatchGroup is non-empty
 -- This is called before type checking, when mg_arg_tys is not set
 matchGroupArity (MG { mg_alts = alts })
-  | L _ (alt1:_) <- alts = length (hsLMatchPats alt1)
+  | L _ (alt1:_) <- alts = count (isVisArgPat . unLoc) (hsLMatchPats alt1)
   | otherwise            = panic "matchGroupArity"
 
-hsLMatchPats :: LMatch (GhcPass id) body -> [LPat (GhcPass id)]
+
+hsLMatchPats :: LMatch (GhcPass id) body -> [LArgPat (GhcPass id)]
 hsLMatchPats (L _ (Match { m_pats = pats })) = pats
 
 -- We keep the type checker happy by providing EpAnnComments.  They
@@ -1537,14 +1538,14 @@ pprPatBind pat grhss
 pprMatch :: (OutputableBndrId idR, Outputable body)
          => Match (GhcPass idR) body -> SDoc
 pprMatch (Match { m_pats = pats, m_ctxt = ctxt, m_grhss = grhss })
-  = sep [ sep (herald : map (nest 2 . pprParendLPat appPrec) other_pats)
+  = sep [ sep (herald : map (nest 2 . pprParendLArgPat appPrec) other_pats)
         , nest 2 (pprGRHSs ctxt grhss) ]
   where
     -- lam_cases_result: we don't simply return (empty, pats) to avoid
     -- introducing an additional `nest 2` via the empty herald
     lam_cases_result = case pats of
                           []     -> (empty, [])
-                          (p:ps) -> (pprParendLPat appPrec p, ps)
+                          (p:ps) -> (pprParendLArgPat appPrec p, ps)
 
     (herald, other_pats)
         = case ctxt of
@@ -1563,9 +1564,9 @@ pprMatch (Match { m_pats = pats, m_ctxt = ctxt, m_grhss = grhss })
                         | null rest -> (pp_infix, [])           -- x &&& y = e
                         | otherwise -> (parens pp_infix, rest)  -- (x &&& y) z = e
                         where
-                          pp_infix = pprParendLPat opPrec p1
+                          pp_infix = pprParendLArgPat opPrec p1
                                      <+> pprInfixOcc fun
-                                     <+> pprParendLPat opPrec p2
+                                     <+> pprParendLArgPat opPrec p2
                      _ -> pprPanic "pprMatch" (ppr ctxt $$ ppr pats)
 
             LamAlt LamSingle                       -> (char '\\', pats)
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 4917e18a85ddeee1484bfbaa87112c2f77583405..23747fe7dc50d52b2b149391a4cae73fcc3bb117 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -439,6 +439,11 @@ deriving instance Data (Pat GhcPs)
 deriving instance Data (Pat GhcRn)
 deriving instance Data (Pat GhcTc)
 
+-- deriving instance (DataIdLR p p) => Data (ArgPat p)
+deriving instance Data (ArgPat GhcPs)
+deriving instance Data (ArgPat GhcRn)
+deriving instance Data (ArgPat GhcTc)
+
 deriving instance Data ConPatTc
 
 deriving instance Data (HsConPatTyArg GhcPs)
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index cedc2adaeb2f127fc33f329b4fb798d89a410605..4c2ddd220e44bfaee0ba0d74c883af3c903214a3 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -22,7 +22,8 @@
 -}
 
 module GHC.Hs.Pat (
-        Pat(..), LPat,
+        Pat(..), LPat, ArgPat(..), LArgPat,
+        isInvisArgPat, isVisArgPat, mapVisPat,
         EpAnnSumPat(..),
         ConPatTc (..),
         ConLikeP,
@@ -38,17 +39,20 @@ module GHC.Hs.Pat (
         hsRecFields, hsRecFieldSel, hsRecFieldId, hsRecFieldsArgs,
         hsRecUpdFieldId, hsRecUpdFieldOcc, hsRecUpdFieldRdr,
 
-        mkPrefixConPat, mkCharLitPat, mkNilPat,
+        mkPrefixConPat, mkCharLitPat, mkNilPat, mkVisPat, mkVisPatX,
+        mkRetainedVisPat,
+
+        Erasure(..),
 
         isSimplePat, isPatSyn,
         looksLazyPatBind,
         isBangedLPat,
-        gParPat, patNeedsParens, parenthesizePat,
+        gParPat, patNeedsParens, parenthesizePat, parenthesizeLArgPat,
         isIrrefutableHsPatHelper, isIrrefutableHsPatHelperM, isBoringHsPat,
 
         collectEvVarsPat, collectEvVarsPats,
 
-        pprParendLPat, pprConArgs,
+        pprParendLArgPat, pprParendLPat, pprConArgs,
         pprLPat
     ) where
 
@@ -182,6 +186,87 @@ type instance XConPatTyArg GhcTc = NoExtField
 
 type instance XHsFieldBind _ = [AddEpAnn]
 
+type instance XVisPat GhcPs = NoExtField
+type instance XVisPat GhcRn = NoExtField
+type instance XVisPat GhcTc = Erasure
+
+type instance XInvisPat GhcPs = EpToken "@"
+type instance XInvisPat GhcRn = NoExtField
+type instance XInvisPat GhcTc = Type
+
+type instance XXArgPat (GhcPass _) = DataConCantHappen
+
+-- Erasure is the property of an argument that determines whether the argument
+-- is erased at compile-time or retained in runtime (GHC Proposal #378).
+--
+--   Erased   <=> the pattern corresponds to a forall-bound variable,
+--                e.g. f :: forall a -> blah
+--                     f pat = ...    -- pat is erased
+--
+--   Retained <=> the pattern corresponds to a function argument,
+--                e.g. f :: Int -> blah
+--                     f pat = ...    -- pat is retained
+--
+-- See Note [Invisible binders in functions]
+data Erasure = Erased | Retained
+  deriving (Data)
+
+{- Note [Invisible binders in functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC Proposal #448 (section 1.5 Type arguments in lambda patterns) introduces
+binders for invisible type arguments (@a-binders) in function equations and
+lambdas, e.g.
+
+  1.  {-# LANGUAGE TypeAbstractions #-}
+      id1 :: a -> a
+      id1 @t x = x :: t     -- @t-binder on the LHS of a function equation
+
+  2.  {-# LANGUAGE TypeAbstractions #-}
+      ex :: (Int8, Int16)
+      ex = higherRank (\ @a x -> maxBound @a - x )
+                            -- @a-binder in a lambda pattern in an argument
+                            -- to a higher-order function
+      higherRank :: (forall a. (Num a, Bounded a) => a -> a) -> (Int8, Int16)
+      higherRank f = (f 42, f 42)
+
+In the AST, patterns in function equations and lambdas are represented with
+ArgPat, which is roughly equivalent to:
+    data ArgPat p
+      = VisPat   (LPat p)
+      | InvisPat (LHsType p)
+
+Each pattern is either visible (not prefixed with @) or invisible (prefixed with @):
+    f :: forall a. forall b -> forall c. Int -> ...
+    f @a b @c x  = ...
+
+In this example, the arg-patterns are
+    1. InvisPat @a     -- in the type sig: forall a.
+    2. VisPat b        -- in the type sig: forall b ->
+    3. InvisPat @c     -- in the type sig: forall c.
+    4. VisPat x        -- in the type sig: Int ->
+
+Invisible patterns are always type patterns, i.e. they are matched with
+forall-bound type variables in the signature. Consequently, those variables (and
+their binders) are erased during compilation, having no effect on program
+execution at runtime.
+
+Visible patterns, on the other hand, may be matched with ordinary function
+arguments (Int ->) as well as required type arguments (forall b ->). This means
+that a visible pattern may either be erased or retained, and we only find out in
+the type checker, namely in tcMatchPats, where we match up all arg-patterns with
+quantifiers from the type signature.
+
+In other words, invisible patterns are always /erased/, while visible patterns
+are sometimes /erased/ and sometimes /retained/. To record this distinction, we
+store a flag in XVisPat:
+  data Erasure = Erased | Retained
+  type instance XVisPat GhcTc = Erasure
+
+The desugarer has no use for erased patterns, as the type checker generates
+HsWrappers to bind the corresponding type variables. Erased patterns are simply
+discarded by calling filterOutErasedPats.
+-}
+
 -- ---------------------------------------------------------------------
 
 -- API Annotations types
@@ -311,6 +396,15 @@ pprPatBndr var
                                               -- but is it worth it?
       False -> pprPrefixOcc var
 
+instance OutputableBndrId p => Outputable (ArgPat (GhcPass p)) where
+    ppr (InvisPat _ tvb) = char '@' <> ppr tvb
+    ppr (VisPat _ lpat)  = ppr lpat
+
+pprParendLArgPat :: (OutputableBndrId p)
+              => PprPrec -> LArgPat (GhcPass p) -> SDoc
+pprParendLArgPat p (L _ (VisPat _ lpat))    = pprParendLPat p lpat
+pprParendLArgPat _ (L _ (InvisPat _ typat)) = char '@' <> ppr typat
+
 pprParendLPat :: (OutputableBndrId p)
               => PprPrec -> LPat (GhcPass p) -> SDoc
 pprParendLPat p = pprParendPat p . unLoc
@@ -449,6 +543,19 @@ mkCharLitPat :: SourceText -> Char -> LPat GhcTc
 mkCharLitPat src c = mkPrefixConPat charDataCon
                           [noLocA $ LitPat noExtField (HsCharPrim src c)] []
 
+-- | A helper function that constructs an argument pattern (LArgPat) from a pattern (LPat)
+mkVisPat :: XVisPat (GhcPass pass) ~ NoExtField => LPat (GhcPass pass) -> LArgPat (GhcPass pass)
+mkVisPat = mkVisPatX noExtField
+
+mkVisPatX :: XVisPat (GhcPass pass) -> LPat (GhcPass pass) -> LArgPat (GhcPass pass)
+mkVisPatX x lpat = L (getLoc lpat) (VisPat x lpat)
+
+mkRetainedVisPat :: forall pass. IsPass pass => LPat (GhcPass pass) -> LArgPat (GhcPass pass)
+mkRetainedVisPat = case ghcPass @pass of
+  GhcPs -> mkVisPat
+  GhcRn -> mkVisPat
+  GhcTc -> mkVisPatX Retained
+
 {-
 ************************************************************************
 *                                                                      *
@@ -850,6 +957,14 @@ parenthesizePat p lpat@(L loc pat)
   | patNeedsParens p pat = L loc (gParPat lpat)
   | otherwise            = lpat
 
+
+parenthesizeLArgPat :: IsPass p
+                   => PprPrec
+                   -> LArgPat (GhcPass p)
+                   -> LArgPat (GhcPass p)
+parenthesizeLArgPat p (L l (VisPat x lpat))   = L l (VisPat x (parenthesizePat p lpat))
+parenthesizeLArgPat _ argpat@(L _ InvisPat{}) = argpat
+
 {-
 % Collect all EvVars from all constructor patterns
 -}
@@ -896,6 +1011,7 @@ collectEvVarsPat pat =
 -}
 
 type instance Anno (Pat (GhcPass p)) = SrcSpanAnnA
+type instance Anno (ArgPat (GhcPass p)) = SrcSpanAnnA
 type instance Anno (HsOverLit (GhcPass p)) = EpAnnCO
 type instance Anno ConLike = SrcSpanAnnN
 type instance Anno (HsFieldBind lhs rhs) = SrcSpanAnnA
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index 8e3cb7da4bedd5dc382deb3cbac4689f40cd4de9..347f7c9a130f0a72978288fb88331c236de71b79 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -44,7 +44,7 @@ module GHC.Hs.Utils(
   -- * Terms
   mkHsPar, mkHsApp, mkHsAppWith, mkHsApps, mkHsAppsWith, mkHsSyntaxApps,
   mkHsAppType, mkHsAppTypes, mkHsCaseAlt,
-  mkSimpleMatch, unguardedGRHSs, unguardedRHS,
+  mkSimpleMatch, mkSimpleMatchArg, unguardedGRHSs, unguardedRHS,
   mkMatchGroup, mkLamCaseMatchGroup, mkMatch, mkPrefixFunRhs, mkHsLam, mkHsIf,
   mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo,
   mkHsDictLet, mkHsLams,
@@ -98,6 +98,7 @@ module GHC.Hs.Utils(
   collectHsBindsBinders, collectHsBindBinders, collectMethodBinders,
 
   collectPatBinders, collectPatsBinders,
+  collectLArgPatBinders, collectLArgPatsBinders,
   collectLStmtsBinders, collectStmtsBinders,
   collectLStmtBinders, collectStmtBinders,
   CollectPass(..), CollectFlag(..),
@@ -185,11 +186,22 @@ mkHsPar e = L (getLoc e) (gHsPar e)
 mkSimpleMatch :: (Anno (Match (GhcPass p) (LocatedA (body (GhcPass p))))
                         ~ SrcSpanAnnA,
                   Anno (GRHS (GhcPass p) (LocatedA (body (GhcPass p))))
-                        ~ EpAnn NoEpAnns)
+                        ~ EpAnn NoEpAnns,
+                  XVisPat (GhcPass p) ~ NoExtField)
               => HsMatchContext (LIdP (NoGhcTc (GhcPass p)))
               -> [LPat (GhcPass p)] -> LocatedA (body (GhcPass p))
               -> LMatch (GhcPass p) (LocatedA (body (GhcPass p)))
 mkSimpleMatch ctxt pats rhs
+  = mkSimpleMatchArg ctxt (map mkVisPat pats) rhs
+
+mkSimpleMatchArg :: (Anno (Match (GhcPass p) (LocatedA (body (GhcPass p))))
+                        ~ SrcSpanAnnA,
+                  Anno (GRHS (GhcPass p) (LocatedA (body (GhcPass p))))
+                        ~ EpAnn NoEpAnns)
+              => HsMatchContext (LIdP (NoGhcTc (GhcPass p)))
+              -> [LArgPat (GhcPass p)] -> LocatedA (body (GhcPass p))
+              -> LMatch (GhcPass p) (LocatedA (body (GhcPass p)))
+mkSimpleMatchArg ctxt pats rhs
   = L loc $
     Match { m_ext = noAnn, m_ctxt = ctxt, m_pats = pats
           , m_grhss = unguardedGRHSs (locA loc) rhs noAnn }
@@ -269,7 +281,8 @@ mkHsAppType e t = addCLocA t_body e (HsAppType noExtField e paren_wct)
 mkHsAppTypes :: LHsExpr GhcRn -> [LHsWcType GhcRn] -> LHsExpr GhcRn
 mkHsAppTypes = foldl' mkHsAppType
 
-mkHsLam :: (IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin)
+mkHsLam :: (IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin,
+            XVisPat (GhcPass p) ~ NoExtField)
         => [LPat (GhcPass p)]
         -> LHsExpr (GhcPass p)
         -> LHsExpr (GhcPass p)
@@ -299,11 +312,12 @@ mkHsSyntaxApps _ NoSyntaxExprTc args = pprPanic "mkHsSyntaxApps" (ppr args)
 mkHsCaseAlt :: (Anno (GRHS (GhcPass p) (LocatedA (body (GhcPass p))))
                      ~ EpAnn NoEpAnns,
                  Anno (Match (GhcPass p) (LocatedA (body (GhcPass p))))
-                        ~ SrcSpanAnnA)
+                        ~ SrcSpanAnnA,
+                  IsPass p)
             => LPat (GhcPass p) -> (LocatedA (body (GhcPass p)))
             -> LMatch (GhcPass p) (LocatedA (body (GhcPass p)))
 mkHsCaseAlt pat expr
-  = mkSimpleMatch CaseAlt [pat] expr
+  = mkSimpleMatchArg CaseAlt [mkRetainedVisPat pat] expr
 
 nlHsTyApp :: Id -> [Type] -> LHsExpr GhcTc
 nlHsTyApp fun_id tys
@@ -890,7 +904,7 @@ spanHsLocaLBinds (HsIPBinds _ (IPBinds _ bs))
 ------------
 -- | Convenience function using 'mkFunBind'.
 -- This is for generated bindings only, do not use for user-written code.
-mkSimpleGeneratedFunBind :: SrcSpan -> RdrName -> [LPat GhcPs]
+mkSimpleGeneratedFunBind :: SrcSpan -> RdrName -> [LArgPat GhcPs]
                          -> LHsExpr GhcPs -> LHsBind GhcPs
 mkSimpleGeneratedFunBind loc fun pats expr
   = L (noAnnSrcSpan loc) $ mkFunBind (Generated OtherExpansion SkipPmc) (L (noAnnSrcSpan loc) fun)
@@ -908,14 +922,14 @@ mkPrefixFunRhs n = FunRhs { mc_fun        = n
 ------------
 mkMatch :: forall p. IsPass p
         => HsMatchContext (LIdP (NoGhcTc (GhcPass p)))
-        -> [LPat (GhcPass p)]
+        -> [LArgPat (GhcPass p)]
         -> LHsExpr (GhcPass p)
         -> HsLocalBinds (GhcPass p)
         -> LMatch (GhcPass p) (LHsExpr (GhcPass p))
 mkMatch ctxt pats expr binds
   = noLocA (Match { m_ext   = noAnn
                   , m_ctxt  = ctxt
-                  , m_pats  = map mkParPat pats
+                  , m_pats  = pats
                   , m_grhss = GRHSs emptyComments (unguardedRHS noAnn noSrcSpan expr) binds })
 
 {-
@@ -1210,6 +1224,22 @@ collectPatsBinders
 collectPatsBinders flag pats = foldr (collect_lpat flag) [] pats
 
 
+collectLArgPatBinders
+    :: CollectPass p
+    => CollectFlag p
+    -> LArgPat p
+    -> [IdP p]
+collectLArgPatBinders flag pat = collect_largpat flag pat []
+
+
+collectLArgPatsBinders
+    :: CollectPass p
+    => CollectFlag p
+    -> [LArgPat p]
+    -> [IdP p]
+collectLArgPatsBinders flag pats = foldr (collect_largpat flag) [] pats
+
+
 -------------
 
 -- | Indicate if evidence binders and type variable binders have
@@ -1240,6 +1270,19 @@ collect_lpat :: forall p. CollectPass p
              -> [IdP p]
 collect_lpat flag pat bndrs = collect_pat flag (unXRec @p pat) bndrs
 
+collect_largpat :: forall p. (CollectPass p)
+                => CollectFlag p
+                -> LArgPat p
+                -> [IdP p]
+                -> [IdP p]
+collect_largpat flag arg_pat bndrs   = case (unXRec @p arg_pat) of
+  VisPat   _ pat -> collect_lpat flag pat bndrs
+  InvisPat _ tp  -> case flag of
+    CollNoDictBinders   -> bndrs
+    CollWithDictBinders -> bndrs
+    CollVarTyVarBinders -> collectTyPatBndrs tp ++ bndrs
+  XArgPat{}      -> bndrs
+
 collect_pat :: forall p. CollectPass p
             => CollectFlag p
             -> Pat p
diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs
index 65a13d3f37e4923e9f5b31cd2001591b06a6bd5d..ad53694c06863140a2f541cb8a738cab9b328401 100644
--- a/compiler/GHC/HsToCore/Arrows.hs
+++ b/compiler/GHC/HsToCore/Arrows.hs
@@ -532,7 +532,7 @@ dsCmd ids local_vars stack_ty res_ty
           = (L _ [L _ (Match { m_pats  = pats
                              , m_grhss = GRHSs _ [L _ (GRHS _ [] body)] _ })]) }))
         env_ids
-  = dsCmdLam ids local_vars stack_ty res_ty pats body env_ids
+  = dsCmdLam ids local_vars stack_ty res_ty (filterOutErasedPats pats) body env_ids
 
 dsCmd ids local_vars stack_ty res_ty
       (HsCmdLam _ lam_variant match@MG { mg_ext = MatchGroupTc {mg_arg_tys = arg_tys} } )
@@ -1208,7 +1208,7 @@ leavesMatch :: LMatch GhcTc (LocatedA (body GhcTc))
 leavesMatch (L _ (Match { m_pats = pats
                         , m_grhss = GRHSs _ grhss binds }))
   = let
-        defined_vars = mkVarSet (collectPatsBinders CollWithDictBinders pats)
+        defined_vars = mkVarSet (collectLArgPatsBinders CollWithDictBinders pats)
                         `unionVarSet`
                        mkVarSet (collectLocalBinders CollWithDictBinders binds)
     in
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index a0c21155284831ab90db51a04ec85aec07ade868..8b01f64d6ecc5402c0d953016868faeed282aad7 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -834,9 +834,9 @@ dsDo ctx stmts
         mfix_app     = nlHsSyntaxApps mfix_op [mfix_arg]
         match_group  = MatchGroupTc [unrestricted tup_ty] body_ty (Generated OtherExpansion SkipPmc)
         mfix_arg     = noLocA $ HsLam noAnn LamSingle
-                           (MG { mg_alts = noLocA [mkSimpleMatch
+                           (MG { mg_alts = noLocA [mkSimpleMatchArg
                                                     (LamAlt LamSingle)
-                                                    [mfix_pat] body]
+                                                    [mkRetainedVisPat mfix_pat] body]
                                , mg_ext = match_group
                                })
         mfix_pat     = noLocA $ LazyPat noExtField $ mkBigLHsPatTupId rec_tup_pats
diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs
index f75d73790f8acbce0980b13a502709a85dd37e53..0a5b45e08282176636e78c00a9de2263865ba1e7 100644
--- a/compiler/GHC/HsToCore/Match.hs
+++ b/compiler/GHC/HsToCore/Match.hs
@@ -785,7 +785,7 @@ matchWrapper ctxt scrs (MG { mg_alts = L _ matches'
                             selectMatchVars (zipWithEqual "matchWrapper"
                                               (\a b -> (scaledMult a, unLoc b))
                                                 arg_tys
-                                                (hsLMatchPats m))
+                                                (filterOutErasedPats $ hsLMatchPats m))
 
         -- Pattern match check warnings for /this match-group/.
         -- @rhss_nablas@ is a flat list of covered Nablas for each RHS.
@@ -819,7 +819,7 @@ matchWrapper ctxt scrs (MG { mg_alts = L _ matches'
     mk_eqn_info :: LMatch GhcTc (LHsExpr GhcTc) -> (Nablas, NonEmpty Nablas) -> DsM EquationInfo
     mk_eqn_info (L _ (Match { m_pats = pats, m_grhss = grhss })) (pat_nablas, rhss_nablas)
       = do { dflags <- getDynFlags
-           ; let upats = map (decideBangHood dflags) pats
+           ; let upats = map (decideBangHood dflags) (filterOutErasedPats pats)
            -- pat_nablas is the covered set *after* matching the pattern, but
            -- before any of the GRHSs. We extend the environment with pat_nablas
            -- (via updPmNablas) so that the where-clause of 'grhss' can profit
@@ -844,11 +844,13 @@ matchWrapper ctxt scrs (MG { mg_alts = L _ matches'
       $ replicate (length (grhssGRHSs m)) ldi_nablas
 
     is_pat_syn_match :: Origin -> LMatch GhcTc (LHsExpr GhcTc) -> Bool
-    is_pat_syn_match origin (L _ (Match _ _ [l_pat] _)) | isDoExpansionGenerated origin = isPatSyn l_pat
+    is_pat_syn_match origin (L _ (Match _ _ [L _ (VisPat _ l_pat)] _)) | isDoExpansionGenerated origin
+                         = isPatSyn l_pat
     is_pat_syn_match _ _ = False
     -- generated match pattern that is not a wildcard
     non_gen_wc :: Origin -> LMatch GhcTc (LHsExpr GhcTc) -> Bool
-    non_gen_wc origin (L _ (Match _ _ ([L _ (WildPat _)]) _)) = not . isDoExpansionGenerated $ origin
+    non_gen_wc origin (L _ (Match _ _ ([L _ (VisPat _ (L _ (WildPat _)))]) _))
+                   = not . isDoExpansionGenerated $ origin
     non_gen_wc _ _ = True
 
 {- Note [Long-distance information in matchWrapper]
diff --git a/compiler/GHC/HsToCore/Pmc/Desugar.hs b/compiler/GHC/HsToCore/Pmc/Desugar.hs
index e7b9775563187b8973bbf7c6b6f94441ee816661..05e3e2e61826297dfceb3b627fdb6410d49fbf27 100644
--- a/compiler/GHC/HsToCore/Pmc/Desugar.hs
+++ b/compiler/GHC/HsToCore/Pmc/Desugar.hs
@@ -38,7 +38,7 @@ import GHC.Core.Coercion
 import GHC.Tc.Types.Evidence (HsWrapper(..), isIdHsWrapper)
 import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr)
 import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper)
-import GHC.HsToCore.Utils (isTrueLHsExpr, selectMatchVar, decideBangHood)
+import GHC.HsToCore.Utils (isTrueLHsExpr, selectMatchVar, filterOutErasedPats, decideBangHood)
 import GHC.HsToCore.Match.Literal (dsLit, dsOverLit)
 import GHC.HsToCore.Monad
 import GHC.Core.TyCo.Rep
@@ -334,8 +334,9 @@ desugarMatches vars matches =
 
 -- Desugar a single match
 desugarMatch :: [Id] -> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PmMatch Pre)
-desugarMatch vars (L match_loc (Match { m_pats = pats, m_grhss = grhss })) = do
+desugarMatch vars (L match_loc (Match { m_pats = arg_pats, m_grhss = grhss })) = do
   dflags <- getDynFlags
+  let pats = filterOutErasedPats arg_pats
   -- decideBangHood: See Note [Desugaring -XStrict matches in Pmc]
   let banged_pats = map (decideBangHood dflags) pats
   pats'  <- concat <$> zipWithM desugarLPat vars banged_pats
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index 97075c0c47cb8fa4c4a8d20b76d725c9ab907edc..90530e28a3c4fea4cdef7804e707ad7c7d1710b7 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -1726,7 +1726,7 @@ the choice in ExpandedThingRn, but it seems simpler to consult the flag (again).
 -- Building representations of auxiliary structures like Match, Clause, Stmt,
 
 repMatchTup ::  LMatch GhcRn (LHsExpr GhcRn) -> MetaM (Core (M TH.Match))
-repMatchTup (L _ (Match { m_pats = [p]
+repMatchTup (L _ (Match { m_pats = [L _ (VisPat _ p)]
                         , m_grhss = GRHSs _ guards wheres })) =
   do { ss1 <- mkGenSyms (collectPatBinders CollNoDictBinders p)
      ; addBinds ss1 $ do {
@@ -1736,14 +1736,14 @@ repMatchTup (L _ (Match { m_pats = [p]
      ; gs    <- repGuards guards
      ; match <- repMatch p1 gs ds
      ; wrapGenSyms (ss1++ss2) match }}}
-repMatchTup _ = panic "repMatchTup: case alt with more than one arg"
+repMatchTup _ = panic "repMatchTup: case alt with more than one arg or with invisible pattern"
 
 repClauseTup ::  LMatch GhcRn (LHsExpr GhcRn) -> MetaM (Core (M TH.Clause))
 repClauseTup (L _ (Match { m_pats = ps
                          , m_grhss = GRHSs _ guards  wheres })) =
-  do { ss1 <- mkGenSyms (collectPatsBinders CollNoDictBinders ps)
+  do { ss1 <- mkGenSyms (collectLArgPatsBinders CollNoDictBinders ps)
      ; addBinds ss1 $ do {
-       ps1 <- repLPs ps
+       ps1 <- repLMPs ps
      ; (ss2,ds) <- repBinds wheres
      ; addBinds ss2 $ do {
        gs <- repGuards guards
@@ -2076,10 +2076,10 @@ repLambda :: LMatch GhcRn (LHsExpr GhcRn) -> MetaM (Core (M TH.Exp))
 repLambda (L _ (Match { m_pats = ps
                       , m_grhss = GRHSs _ [L _ (GRHS _ [] e)]
                                               (EmptyLocalBinds _) } ))
- = do { let bndrs = collectPatsBinders CollNoDictBinders ps ;
+ = do { let bndrs = collectLArgPatsBinders CollNoDictBinders ps ;
       ; ss  <- mkGenSyms bndrs
       ; lam <- addBinds ss (
-                do { xs <- repLPs ps; body <- repLE e; repLam xs body })
+                do { xs <- repLMPs ps; body <- repLE e; repLam xs body })
       ; wrapGenSyms ss lam }
 
 repLambda (L _ m) = notHandled (ThGuardedLambdas m)
@@ -2099,6 +2099,15 @@ repLPs ps = repListM patTyConName repLP ps
 repLP :: LPat GhcRn -> MetaM (Core (M TH.Pat))
 repLP p = repP (unLoc p)
 
+-- Process a list of arg patterns
+repLMPs :: [LArgPat GhcRn] -> MetaM (Core ([M TH.ArgPat]))
+repLMPs ps = repListM argPatTyConName repLMP ps
+
+repLMP :: LArgPat GhcRn -> MetaM (Core (M TH.ArgPat))
+repLMP (L _ (VisPat _ p))     = do {p' <- repLP p; repAPvis p'}
+repLMP (L _ (InvisPat _ t)) = do {t' <- repLTy (hstp_body t); repAPinvis t'}
+
+
 repP :: Pat GhcRn -> MetaM (Core (M TH.Pat))
 repP (WildPat _)        = repPwild
 repP (LitPat _ l)       = do { l2 <- repLiteral l; repPlit l2 }
@@ -2407,6 +2416,12 @@ repPsig (MkC p) (MkC t) = rep2 sigPName [p, t]
 repPtype :: Core (M TH.Type) -> MetaM (Core (M TH.Pat))
 repPtype (MkC t) = rep2 typePName [t]
 
+repAPvis :: Core (M TH.Pat) -> MetaM (Core (M TH.ArgPat))
+repAPvis (MkC t) = rep2 visAPName [t]
+
+repAPinvis :: Core (M TH.Type) -> MetaM (Core (M TH.ArgPat))
+repAPinvis (MkC t) = rep2 invisAPName [t]
+
 --------------- Expressions -----------------
 repVarOrCon :: Name -> Core TH.Name -> MetaM (Core (M TH.Exp))
 repVarOrCon vc str
@@ -2430,8 +2445,8 @@ repApp (MkC x) (MkC y) = rep2 appEName [x,y]
 repAppType :: Core (M TH.Exp) -> Core (M TH.Type) -> MetaM (Core (M TH.Exp))
 repAppType (MkC x) (MkC y) = rep2 appTypeEName [x,y]
 
-repLam :: Core [(M TH.Pat)] -> Core (M TH.Exp) -> MetaM (Core (M TH.Exp))
-repLam (MkC ps) (MkC e) = rep2 lamEName [ps, e]
+repLam :: Core [(M TH.ArgPat)] -> Core (M TH.Exp) -> MetaM (Core (M TH.Exp))
+repLam (MkC ps) (MkC e) = rep2 lamArgEName [ps, e]
 
 repLamCase :: Core [(M TH.Match)] -> MetaM (Core (M TH.Exp))
 repLamCase (MkC ms) = rep2 lamCaseEName [ms]
@@ -2567,8 +2582,8 @@ repFromThenTo (MkC x) (MkC y) (MkC z) = rep2 fromThenToEName [x,y,z]
 repMatch :: Core (M TH.Pat) -> Core (M TH.Body) -> Core [(M TH.Dec)] -> MetaM (Core (M TH.Match))
 repMatch (MkC p) (MkC bod) (MkC ds) = rep2 matchName [p, bod, ds]
 
-repClause :: Core [(M TH.Pat)] -> Core (M TH.Body) -> Core [(M TH.Dec)] -> MetaM (Core (M TH.Clause))
-repClause (MkC ps) (MkC bod) (MkC ds) = rep2 clauseName [ps, bod, ds]
+repClause :: Core [(M TH.ArgPat)] -> Core (M TH.Body) -> Core [(M TH.Dec)] -> MetaM (Core (M TH.Clause))
+repClause (MkC ps) (MkC bod) (MkC ds) = rep2 clauseArgName [ps, bod, ds]
 
 -------------- Dec -----------------------------
 repVal :: Core (M TH.Pat) -> Core (M TH.Body) -> Core [(M TH.Dec)] -> MetaM (Core (M TH.Dec))
diff --git a/compiler/GHC/HsToCore/Ticks.hs b/compiler/GHC/HsToCore/Ticks.hs
index 5c93f9dbebedd799230ed63b76f9ad526d986cbe..13ee946d6e8e778dd24548ffd49826416488cfcd 100644
--- a/compiler/GHC/HsToCore/Ticks.hs
+++ b/compiler/GHC/HsToCore/Ticks.hs
@@ -643,7 +643,7 @@ addTickMatch :: Bool -> Bool -> Bool {-Is this Do Expansion-} ->  Match GhcTc (L
              -> TM (Match GhcTc (LHsExpr GhcTc))
 addTickMatch isOneOfMany isLambda isDoExp match@(Match { m_pats = pats
                                                        , m_grhss = gRHSs }) =
-  bindLocals (collectPatsBinders CollNoDictBinders pats) $ do
+  bindLocals (collectLArgPatsBinders CollNoDictBinders pats) $ do
     gRHSs' <- addTickGRHSs isOneOfMany isLambda isDoExp gRHSs
     return $ match { m_grhss = gRHSs' }
 
@@ -904,7 +904,7 @@ addTickCmdMatchGroup mg@(MG { mg_alts = (L l matches) }) = do
 
 addTickCmdMatch :: Match GhcTc (LHsCmd GhcTc) -> TM (Match GhcTc (LHsCmd GhcTc))
 addTickCmdMatch match@(Match { m_pats = pats, m_grhss = gRHSs }) =
-  bindLocals (collectPatsBinders CollNoDictBinders pats) $ do
+  bindLocals (collectLArgPatsBinders CollNoDictBinders pats) $ do
     gRHSs' <- addTickCmdGRHSs gRHSs
     return $ match { m_grhss = gRHSs' }
 
diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs
index eb87b024456de3b2189d82142097c9bd75ff49eb..95d7de7149f1c34fb0085fca6c6d98fcca14c6ed 100644
--- a/compiler/GHC/HsToCore/Utils.hs
+++ b/compiler/GHC/HsToCore/Utils.hs
@@ -41,7 +41,9 @@ module GHC.HsToCore.Utils (
 
         selectSimpleMatchVarL, selectMatchVars, selectMatchVar,
         mkOptTickBox, mkBinaryTickBox, decideBangHood,
-        isTrueLHsExpr
+        isTrueLHsExpr,
+
+        filterOutErasedPats
     ) where
 
 import GHC.Prelude
@@ -86,7 +88,7 @@ import GHC.Tc.Types.Evidence
 
 import Control.Monad    ( zipWithM )
 import Data.List.NonEmpty (NonEmpty(..))
-import Data.Maybe (maybeToList)
+import Data.Maybe (maybeToList, mapMaybe)
 import qualified Data.List.NonEmpty as NEL
 
 {-
@@ -1092,3 +1094,29 @@ isTrueLHsExpr (L _ (XExpr (HsBinTick ixT _ e)))
 
 isTrueLHsExpr (L _ (HsPar _ e)) = isTrueLHsExpr e
 isTrueLHsExpr _                 = Nothing
+
+-- Drop user-written arg-patterns for erased arguments, i.e. @-binders and
+-- required type arguments:
+--
+--  f :: forall a. forall b -> Int -> blah
+--  f @a b c = ...
+--
+-- In this example:
+--
+--  * InvisPat        @a   -- filtered out (corresponds to forall a.)
+--  * VisPat Erased   b    -- filtered out (corresponds to forall b ->)
+--  * VisPat Retained c    -- kept         (corresponds to Int ->)
+--
+-- filterOutErasedPats [@a, b, c] = [c]
+--
+-- We have no use for erased patterns in the desugarer. The type checker has
+-- already produced HsWrappers to bind the corresponding type variables.
+--
+-- See Note [Invisible binders in functions] in GHC.Hs.Pat
+filterOutErasedPats :: [LArgPat GhcTc] -> [LPat GhcTc]
+filterOutErasedPats xs = mapMaybe (to_lpat . unLoc) xs
+  where
+    to_lpat :: ArgPat GhcTc -> Maybe (LPat GhcTc)
+    to_lpat (VisPat Retained pat) = Just pat
+    to_lpat (VisPat Erased _)     = Nothing
+    to_lpat (InvisPat _ _)        = Nothing
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index 11bf27223885aa6f67225ba55a4426bf98c5525d..09cc0dfef19a1910938accc079e04a982ea7238b 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -502,6 +502,15 @@ patScopes rsp useScope patScope xs =
   map (\(RS sc a) -> PS rsp useScope sc a) $
     listScopes patScope xs
 
+argPatScopes
+  :: Maybe Span
+  -> Scope
+  -> Scope
+  -> [LArgPat (GhcPass p)]
+  -> [PScoped (LArgPat (GhcPass p))]
+argPatScopes rsp useScope patScope xs =
+  map (\(RS sc a) -> PS rsp useScope sc a) $ listScopes patScope xs
+
 -- | 'listScopes' specialised to 'HsConPatTyArg'
 taScopes
   :: Scope
@@ -921,6 +930,12 @@ instance HiePass p => ToHie (HsPatSynDir (GhcPass p)) where
     ExplicitBidirectional mg -> toHie mg
     _ -> pure []
 
+instance HiePass p => ToHie (PScoped (GenLocated SrcSpanAnnA (ArgPat (GhcPass p)))) where
+  toHie (PS mb sc1 sc2 (L _ (VisPat _ pat))) =
+    toHie (PS mb sc1 sc2 pat)
+  toHie (PS _ sc1 sc2 (L _ (InvisPat _ tp))) =
+    toHie $ TS (ResolvedScopes [sc1, sc2]) tp
+
 instance ( HiePass p
          , Data (body (GhcPass p))
          , AnnoBody p body
@@ -930,7 +945,7 @@ instance ( HiePass p
     Match{m_ctxt=mctx, m_pats = pats, m_grhss =  grhss } ->
       [ toHieHsMatchContext @p mctx
       , let rhsScope = mkScope $ grhss_span grhss
-          in toHie $ patScopes Nothing rhsScope NoScope pats
+          in toHie $ argPatScopes Nothing rhsScope NoScope pats
       , toHie grhss
       ]
 
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 3c7fcb98709d41e03d2a7d7e7aa1e6ebc0014b43..01eea6721f42832ee57b418300b3a451e0bd9365 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -2865,8 +2865,7 @@ aexp    :: { ECP }
         | 'let' binds 'in' exp          {  ECP $
                                            unECP $4 >>= \ $4 ->
                                            mkHsLetPV (comb2 $1 $>) (epTok $1) (unLoc $2) (epTok $3) $4 }
-        | '\\' apats '->' exp
-                   {  ECP $
+        | '\\' argpats '->' exp { ECP $
                       unECP $4 >>= \ $4 ->
                       mkHsLamPV (comb2 $1 $>) LamSingle
                             (sLLl $1 $>
@@ -2879,7 +2878,7 @@ aexp    :: { ECP }
         | '\\' 'lcase' altslist(pats1)
             {  ECP $ $3 >>= \ $3 ->
                  mkHsLamPV (comb2 $1 $>) LamCase $3 [mj AnnLam $1,mj AnnCase $2] }
-        | '\\' 'lcases' altslist(apats)
+        | '\\' 'lcases' altslist(argpats)
             {  ECP $ $3 >>= \ $3 ->
                  mkHsLamPV (comb2 $1 $>) LamCases $3 [mj AnnLam $1,mj AnnCases $2] }
         | 'if' exp optSemi 'then' exp optSemi 'else' exp
@@ -3366,14 +3365,25 @@ pat     :  exp          {% (checkPattern <=< runPV) (unECP $1) }
 
 -- 'pats1' does the same thing as 'pat', but returns it as a singleton
 -- list so that it can be used with a parameterized production rule
-pats1   :: { [LPat GhcPs] }
-pats1   : pat { [ $1 ] }
+--
+-- It is used only for parsing patterns in `\case` and `case of`
+pats1   :: { [LArgPat GhcPs] }
+pats1   : pat { [ mkVisPat $1 ] }
 
 bindpat :: { LPat GhcPs }
 bindpat :  exp            {% -- See Note [Parser-Validator Details] in GHC.Parser.PostProcess
                              checkPattern_details incompleteDoBlock
                                               (unECP $1) }
 
+argpat   :: { LArgPat GhcPs }
+argpat    : apat                  { mkVisPat $1 }
+          | PREFIX_AT atype       { L (getLocAnn (reLoc $2)) (InvisPat (epTok $1) (mkHsTyPat noAnn $2)) }
+
+argpats :: { [LArgPat GhcPs] }
+          : argpat argpats            { $1 : $2 }
+          | {- empty -}               { [] }
+
+
 apat   :: { LPat GhcPs }
 apat    : aexp                  {% (checkPattern <=< runPV) (unECP $1) }
 
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 5725fd13bccad8587325bef06fa1558badcebb64..f27bc529c94b8fdfffc1c9122db37307cbf42688 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -730,7 +730,7 @@ mkPatSynMatchGroup (L loc patsyn_name) (L ld decls) =
                wrongNameBindingErr (locA loc) decl
            ; match <- case details of
                PrefixCon _ pats -> return $ Match { m_ext = noAnn
-                                                  , m_ctxt = ctxt, m_pats = pats
+                                                  , m_ctxt = ctxt, m_pats = map mkVisPat pats
                                                   , m_grhss = rhs }
                    where
                      ctxt = FunRhs { mc_fun = ln
@@ -739,7 +739,7 @@ mkPatSynMatchGroup (L loc patsyn_name) (L ld decls) =
 
                InfixCon p1 p2 -> return $ Match { m_ext = noAnn
                                                 , m_ctxt = ctxt
-                                                , m_pats = [p1, p2]
+                                                , m_pats = map mkVisPat [p1, p2]
                                                 , m_grhss = rhs }
                    where
                      ctxt = FunRhs { mc_fun = ln
@@ -1182,6 +1182,11 @@ checkPattern = runPV . checkLPat
 checkPattern_details :: ParseContext -> PV (LocatedA (PatBuilder GhcPs)) -> P (LPat GhcPs)
 checkPattern_details extraDetails pp = runPV_details extraDetails (pp >>= checkLPat)
 
+checkLArgPat :: LocatedA (ArgPatBuilder GhcPs) -> PV (LArgPat GhcPs)
+checkLArgPat (L l (ArgPatBuilderVisPat p))
+  = L l <$> (VisPat noExtField <$> checkPat l (L l p) [] [])
+checkLArgPat (L l (ArgPatBuilderArgPat p)) = return (L l p)
+
 checkLPat :: LocatedA (PatBuilder GhcPs) -> PV (LPat GhcPs)
 checkLPat e@(L l _) = checkPat l e [] []
 
@@ -1193,8 +1198,6 @@ checkPat loc (L l e@(PatBuilderVar (L ln c))) tyargs args
       , pat_con = L ln c
       , pat_args = PrefixCon tyargs args
       }
-  | not (null tyargs) =
-      patFail (locA l) . PsErrInPat e $ PEIP_TypeArgs tyargs
   | (not (null args) && patIsRec c) = do
       ctx <- askParseContext
       patFail (locA l) . PsErrInPat e $ PEIP_RecPattern args YesPatIsRecursive ctx
@@ -1312,11 +1315,11 @@ checkFunBind :: SrcStrictness
              -> [AddEpAnn]
              -> LocatedN RdrName
              -> LexicalFixity
-             -> [LocatedA (PatBuilder GhcPs)]
+             -> [LocatedA (ArgPatBuilder GhcPs)]
              -> Located (GRHSs GhcPs (LHsExpr GhcPs))
              -> P (HsBind GhcPs)
 checkFunBind strictness locF ann fun is_infix pats (L _ grhss)
-  = do  ps <- runPV_details extraDetails (mapM checkLPat pats)
+  = do  ps <- runPV_details extraDetails (mapM checkLArgPat pats)
         let match_span = noAnnSrcSpan $ locF
         return (makeFunBind fun (L (noAnnSrcSpan $ locA match_span)
                  [L match_span (Match { m_ext = ann
@@ -1390,33 +1393,48 @@ checkDoAndIfThenElse err guardExpr semiThen thenExpr semiElse elseExpr
 
 isFunLhs :: LocatedA (PatBuilder GhcPs)
       -> P (Maybe (LocatedN RdrName, LexicalFixity,
-                   [LocatedA (PatBuilder GhcPs)],[AddEpAnn]))
+                   [LocatedA (ArgPatBuilder GhcPs)],[AddEpAnn]))
 -- A variable binding is parsed as a FunBind.
 -- Just (fun, is_infix, arg_pats) if e is a function LHS
 isFunLhs e = go e [] [] []
  where
+   mk = fmap ArgPatBuilderVisPat
+
    go (L _ (PatBuilderVar (L loc f))) es ops cps
        | not (isRdrDataCon f)        = return (Just (L loc f, Prefix, es, (reverse ops) ++ cps))
-   go (L _ (PatBuilderApp f e)) es       ops cps = go f (e:es) ops cps
-   go (L l (PatBuilderPar _ e _)) es@(_:_) ops cps
-                                      = let
-                                          (o,c) = mkParensEpAnn (realSrcSpan $ locA l)
-                                        in
-                                          go e es (o:ops) (c:cps)
+   go (L _ (PatBuilderApp f e))   es       ops cps = go f (mk e:es) ops cps
+   go (L l (PatBuilderPar _ e _)) es@(_:_) ops cps = go e es (o:ops) (c:cps)
+      -- NB: es@(_:_) means that there must be an arg after the parens for the
+      -- LHS to be a function LHS. This corresponds to the Haskell Report's definition
+      -- of funlhs.
+     where
+       (o,c) = mkParensEpAnn (realSrcSpan $ locA l)
    go (L loc (PatBuilderOpApp l (L loc' op) r anns)) es ops cps
-        | not (isRdrDataCon op)         -- We have found the function!
-        = return (Just (L loc' op, Infix, (l:r:es), (anns ++ reverse ops ++ cps)))
-        | otherwise                     -- Infix data con; keep going
-        = do { mb_l <- go l es ops cps
-             ; case mb_l of
-                 Just (op', Infix, j : k : es', anns')
-                   -> return (Just (op', Infix, j : op_app : es', anns'))
-                   where
-                     op_app = L loc (PatBuilderOpApp k
-                               (L loc' op) r (reverse ops++cps))
-                 _ -> return Nothing }
+      | not (isRdrDataCon op)         -- We have found the function!
+      = return (Just (L loc' op, Infix, (mk l:mk r:es), (anns ++ reverse ops ++ cps)))
+      | otherwise                     -- Infix data con; keep going
+      = do { mb_l <- go l es ops cps
+           ; return (reassociate =<< mb_l) }
+        where
+          reassociate (op', Infix, j : L k_loc (ArgPatBuilderVisPat k) : es', anns')
+            = Just (op', Infix, j : op_app : es', anns')
+            where
+              op_app = mk $ L loc (PatBuilderOpApp (L k_loc k)
+                                    (L loc' op) r (reverse ops ++ cps))
+          reassociate _other = Nothing
+   go (L _ (PatBuilderAppType pat tok ty_pat@(HsTP _ (L loc _)))) es ops cps
+             = go pat (L loc (ArgPatBuilderArgPat invis_pat) : es) ops cps
+             where invis_pat = InvisPat tok ty_pat
    go _ _ _ _ = return Nothing
 
+data ArgPatBuilder p
+  = ArgPatBuilderVisPat (PatBuilder p)
+  | ArgPatBuilderArgPat (ArgPat p)
+
+instance Outputable (ArgPatBuilder GhcPs) where
+  ppr (ArgPatBuilderVisPat p) = ppr p
+  ppr (ArgPatBuilderArgPat p) = ppr p
+
 mkBangTy :: [AddEpAnn] -> SrcStrictness -> LHsType GhcPs -> HsType GhcPs
 mkBangTy anns strictness =
   HsBangTy anns (HsSrcBang NoSourceText NoSrcUnpack strictness)
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index a47b5a06b330506c0334db0771c00baeea92b353..12edfa5087f681cf9a77a7b9e18b9f33ded89f44 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -1304,7 +1304,7 @@ rnMatch' :: (AnnoBody body)
          -> Match GhcPs (LocatedA (body GhcPs))
          -> RnM (Match GhcRn (LocatedA (body GhcRn)), FreeVars)
 rnMatch' ctxt rnBody (Match { m_ctxt = mf, m_pats = pats, m_grhss = grhss })
-  = rnPats ctxt pats $ \ pats' -> do
+  = rnArgPats ctxt pats $ \ pats' -> do
         { (grhss', grhss_fvs) <- rnGRHSs ctxt rnBody grhss
         ; let mf' = case (ctxt, mf) of
                       (FunRhs { mc_fun = L _ funid }, FunRhs { mc_fun = L lf _ })
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index fd169a7e0b42dc7154d8999dca23dd569777b553..0261e1da09fcb0cc9fc1ac184fc5c6859f87c548 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -1539,8 +1539,8 @@ checkPrecMatch :: Name -> MatchGroup GhcRn body -> RnM ()
 checkPrecMatch op (MG { mg_alts = (L _ ms) })
   = mapM_ check ms
   where
-    check (L _ (Match { m_pats = (L l1 p1)
-                               : (L l2 p2)
+    check (L _ (Match { m_pats = (L _ (VisPat _ (L l1 p1)))
+                               : (L _ (VisPat _ (L l2 p2)))
                                : _ }))
       = setSrcSpan (locA $ combineSrcSpansA l1 l2) $
         do checkPrec op p1 False
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 5665c282b9eb5c6013ec1505084fbb2cc056093d..6c4c3bf4f51f1dd7e34776a548d276f9525bb4dc 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -23,7 +23,7 @@ general, all of these functions return a renamed thing, and a set of
 free variables.
 -}
 module GHC.Rename.Pat (-- main entry points
-              rnPat, rnPats, rnBindPat,
+              rnPat, rnPats, rnArgPats, rnBindPat,
 
               NameMaker, applyNameMaker,     -- a utility for making names:
               localRecNameMaker, topRecNameMaker,  --   sometimes we want to make local names,
@@ -417,36 +417,54 @@ There are various entry points to renaming patterns, depending on
 --   * local namemaker
 --   * unused and duplicate checking
 --   * no fixities
-rnPats :: Traversable f
-       => HsMatchContextRn   -- For error messages
-       -> f (LPat GhcPs)
-       -> (f (LPat GhcRn) -> RnM (a, FreeVars))
-       -> RnM (a, FreeVars)
-rnPats ctxt pats thing_inside
-  = do  { envs_before <- getRdrEnvs
-
-          -- (1) rename the patterns, bringing into scope all of the term variables
-          -- (2) then do the thing inside.
-        ; unCpsRn (rnLPatsAndThen (matchNameMaker ctxt) pats) $ \ pats' -> do
-        { -- Check for duplicated and shadowed names
-          -- Must do this *after* renaming the patterns
-          -- See Note [Collect binders only after renaming] in GHC.Hs.Utils
-          -- Because we don't bind the vars all at once, we can't
-          --    check incrementally for duplicates;
-          -- Nor can we check incrementally for shadowing, else we'll
-          --    complain *twice* about duplicates e.g. f (x,x) = ...
-          --
-          -- See Note [Don't report shadowing for pattern synonyms]
-        ; let bndrs = collectPatsBinders CollVarTyVarBinders (toList pats')
-        ; addErrCtxt doc_pat $
-          if isPatSynCtxt ctxt
-             then checkDupNames bndrs
-             else checkDupAndShadowedNames envs_before bndrs
-        ; thing_inside pats' } }
+
+-- rn_pats_general is the generalisation of three functions:
+--    rnArgPats, rnPats, rnPat
+-- Those are the only call sites, so we inline it for improved performance.
+-- Kind of like a macro.
+{-# INLINE rn_pats_general #-}
+rn_pats_general :: Traversable f =>
+  (NameMaker -> f (LocatedA (pat GhcPs)) -> CpsRn  (f (LocatedA (pat GhcRn))))
+  -> (CollectFlag GhcRn -> [LocatedA (pat GhcRn)] -> [Name])
+  -> HsMatchContextRn
+  -> f (LocatedA (pat GhcPs))
+  -> (f (LocatedA (pat GhcRn)) -> RnM (r, FreeVars))
+  -> RnM (r, FreeVars)
+rn_pats_general rn_pats_and_then collect_pats_binders ctxt pats thing_inside = do
+  envs_before <- getRdrEnvs
+
+  -- (1) rename the patterns, bringing into scope all of the term variables
+  -- (2) then do the thing inside.
+  unCpsRn (rn_pats_and_then (matchNameMaker ctxt) pats) $ \ pats' -> do
+    -- Check for duplicated and shadowed names
+    -- Must do this *after* renaming the patterns
+    -- See Note [Collect binders only after renaming] in GHC.Hs.Utils
+    -- Because we don't bind the vars all at once, we can't
+    --    check incrementally for duplicates;
+    -- Nor can we check incrementally for shadowing, else we'll
+    --    complain *twice* about duplicates e.g. f (x,x) = ...
+    --
+    -- See Note [Don't report shadowing for pattern synonyms]
+    let bndrs = collect_pats_binders CollVarTyVarBinders (toList pats')
+    addErrCtxt doc_pat $
+      if isPatSynCtxt ctxt
+         then checkDupNames bndrs
+         else checkDupAndShadowedNames envs_before bndrs
+    thing_inside pats'
   where
     doc_pat = text "In" <+> pprMatchContext ctxt
-{-# SPECIALIZE rnPats :: HsMatchContextRn -> [LPat GhcPs] -> ([LPat GhcRn] -> RnM (a, FreeVars)) -> RnM (a, FreeVars) #-}
-{-# SPECIALIZE rnPats :: HsMatchContextRn -> Identity (LPat GhcPs) -> (Identity (LPat GhcRn) -> RnM (a, FreeVars)) -> RnM (a, FreeVars) #-}
+
+rnArgPats :: HsMatchContextRn
+          -> [LArgPat GhcPs]
+          -> ([LArgPat GhcRn] -> RnM (a, FreeVars))
+          -> RnM (a, FreeVars)
+rnArgPats = rn_pats_general rnLArgPatsAndThen collectLArgPatsBinders
+
+rnPats :: HsMatchContextRn   -- For error messages
+       -> [LPat GhcPs]
+       -> ([LPat GhcRn] -> RnM (a, FreeVars))
+       -> RnM (a, FreeVars)
+rnPats = rn_pats_general (mapM . rnLPatAndThen) collectPatsBinders
 
 rnPat :: HsMatchContextRn      -- For error messages
       -> LPat GhcPs
@@ -454,7 +472,8 @@ rnPat :: HsMatchContextRn      -- For error messages
       -> RnM (a, FreeVars)     -- Variables bound by pattern do not
                                -- appear in the result FreeVars
 rnPat ctxt pat thing_inside
-  = rnPats ctxt (Identity pat) (thing_inside . runIdentity)
+       = rn_pats_general (mapM . rnLPatAndThen) collectPatsBinders
+            ctxt (Identity pat) (thing_inside . runIdentity)
 
 applyNameMaker :: NameMaker -> LocatedN RdrName -> RnM (LocatedN Name)
 applyNameMaker mk rdr = do { (n, _fvs) <- runCps (newPatLName mk rdr)
@@ -483,10 +502,21 @@ rnBindPat name_maker pat = runCps (rnLPatAndThen name_maker pat)
 *********************************************************
 -}
 
+rnLArgPatsAndThen :: NameMaker -> [LArgPat GhcPs] -> CpsRn [LArgPat GhcRn]
+rnLArgPatsAndThen mk = mapM (wrapSrcSpanCps rnArgPatAndThen) where
+  rnArgPatAndThen (VisPat x p) = do
+    p' <- rnLPatAndThen mk p
+    pure (VisPat x p')
+  rnArgPatAndThen (InvisPat _ tp) = do
+    liftCps $ unlessXOptM LangExt.TypeAbstractions $
+      addErr (TcRnIllegalInvisibleTypePattern tp)
+    tp' <- rnHsTyPat HsTypePatCtx tp
+    pure (InvisPat noExtField tp')
+
 -- ----------- Entry point 3: rnLPatAndThen -------------------
 -- General version: parameterized by how you make new names
 
-rnLPatsAndThen :: Traversable f => NameMaker -> f (LPat GhcPs) -> CpsRn (f (LPat GhcRn))
+rnLPatsAndThen :: NameMaker -> [LPat GhcPs] -> CpsRn [LPat GhcRn]
 rnLPatsAndThen mk = mapM (rnLPatAndThen mk)
   -- Despite the map, the monad ensures that each pattern binds
   -- variables that may be mentioned in subsequent patterns in the list
diff --git a/compiler/GHC/Rename/Utils.hs b/compiler/GHC/Rename/Utils.hs
index 1c827a06d6251f89f0c0445fac518654acac52e5..4012b55365eb5b42514747c82536fbaea62716ef 100644
--- a/compiler/GHC/Rename/Utils.hs
+++ b/compiler/GHC/Rename/Utils.hs
@@ -763,7 +763,7 @@ genVarPat n = wrapGenSpan $ VarPat noExtField (wrapGenSpan n)
 genWildPat :: LPat GhcRn
 genWildPat = wrapGenSpan $ WildPat noExtField
 
-genSimpleFunBind :: Name -> [LPat GhcRn]
+genSimpleFunBind :: Name -> [LArgPat GhcRn]
                  -> LHsExpr GhcRn -> LHsBind GhcRn
 genSimpleFunBind fun pats expr
   = L genA $ genFunBind (L genN fun)
@@ -793,21 +793,21 @@ genHsLet bindings body = HsLet noExtField bindings body
 
 genHsLamDoExp :: (IsPass p, XMG (GhcPass p) (LHsExpr (GhcPass p)) ~ Origin)
         => HsDoFlavour
-        -> [LPat (GhcPass p)]
+        -> [LArgPat (GhcPass p)]
         -> LHsExpr (GhcPass p)
         -> LHsExpr (GhcPass p)
 genHsLamDoExp doFlav pats body = mkHsPar (wrapGenSpan $ HsLam noAnn LamSingle matches)
   where
     matches = mkMatchGroup (doExpansionOrigin doFlav)
                            (wrapGenSpan [genSimpleMatch (StmtCtxt (HsDoStmt doFlav)) pats' body])
-    pats' = map (parenthesizePat appPrec) pats
+    pats' = map (parenthesizeLArgPat appPrec) pats
 
 
 genHsCaseAltDoExp :: (Anno (GRHS (GhcPass p) (LocatedA (body (GhcPass p))))
                      ~ EpAnnCO,
                  Anno (Match (GhcPass p) (LocatedA (body (GhcPass p))))
                         ~ SrcSpanAnnA)
-            => HsDoFlavour -> LPat (GhcPass p) -> (LocatedA (body (GhcPass p)))
+            => HsDoFlavour -> LArgPat (GhcPass p) -> (LocatedA (body (GhcPass p)))
             -> LMatch (GhcPass p) (LocatedA (body (GhcPass p)))
 genHsCaseAltDoExp doFlav pat expr
   = genSimpleMatch (StmtCtxt (HsDoStmt doFlav)) [pat] expr
@@ -818,7 +818,7 @@ genSimpleMatch :: (Anno (Match (GhcPass p) (LocatedA (body (GhcPass p))))
                   Anno (GRHS (GhcPass p) (LocatedA (body (GhcPass p))))
                         ~ EpAnnCO)
               => HsMatchContext (LIdP (NoGhcTc (GhcPass p)))
-              -> [LPat (GhcPass p)] -> LocatedA (body (GhcPass p))
+              -> [LArgPat (GhcPass p)] -> LocatedA (body (GhcPass p))
               -> LMatch (GhcPass p) (LocatedA (body (GhcPass p)))
 genSimpleMatch ctxt pats rhs
   = wrapGenSpan $
diff --git a/compiler/GHC/Tc/Deriv/Functor.hs b/compiler/GHC/Tc/Deriv/Functor.hs
index 2503cc5c29608000d2f9e053c4d3792015e1f6e2..9af48ec300b24cec1171fde95cfecc9ab024d777 100644
--- a/compiler/GHC/Tc/Deriv/Functor.hs
+++ b/compiler/GHC/Tc/Deriv/Functor.hs
@@ -644,7 +644,7 @@ mkSimpleConMatch ctxt fold extra_pats con insides = do
           else nlParPat bare_pat
     rhs <- fold con_name
                 (zipWith (\i v -> i $ nlHsVar v) insides vars_needed)
-    return $ mkMatch ctxt (extra_pats ++ [pat]) rhs emptyLocalBinds
+    return $ mkMatch ctxt (map mkVisPat $ extra_pats ++ [pat]) rhs emptyLocalBinds
 
 -- "Con a1 a2 a3 -> fmap (\b2 -> Con a1 b2 a3) (traverse f a2)"
 --
@@ -694,7 +694,7 @@ mkSimpleConMatch2 ctxt fold extra_pats con insides = do
               in mkHsLam (map nlVarPat bs) (nlHsApps con_name vars)
 
     rhs <- fold con_expr exps
-    return $ mkMatch ctxt (extra_pats ++ [pat]) rhs emptyLocalBinds
+    return $ mkMatch ctxt (map mkVisPat $ extra_pats ++ [pat]) rhs emptyLocalBinds
 
 -- "case x of (a1,a2,a3) -> fold [x1 a1, x2 a2, x3 a3]"
 mkSimpleTupleCase :: Monad m => ([LPat GhcPs] -> DataCon -> [a]
@@ -880,7 +880,7 @@ gen_Foldable_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
           parts <- sequence $ foldDataConArgs ft_null con dit
           case convert parts of
             Nothing -> return $
-              mkMatch null_match_ctxt [nlParPat (nlWildConPat con)]
+              mkMatch null_match_ctxt [mkVisPat $ nlParPat (nlWildConPat con)]
                 false_Expr emptyLocalBinds
             Just cp -> match_null [] con cp
 
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 0cc3ac1f71f4bdf969c982498c663fc445930c79..852fa0e86be45c6906ce0b9c139d66590cc203d4 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -423,11 +423,12 @@ gen_Ord_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
       = emptyBag
 
     negate_expr = nlHsApp (nlHsVar not_RDR)
-    lE = mkSimpleGeneratedFunBind loc le_RDR [a_Pat, b_Pat] $
+    pats = map mkVisPat [a_Pat, b_Pat]
+    lE = mkSimpleGeneratedFunBind loc le_RDR pats $
         negate_expr (nlHsApp (nlHsApp (nlHsVar lt_RDR) b_Expr) a_Expr)
-    gT = mkSimpleGeneratedFunBind loc gt_RDR [a_Pat, b_Pat] $
+    gT = mkSimpleGeneratedFunBind loc gt_RDR pats $
         nlHsApp (nlHsApp (nlHsVar lt_RDR) b_Expr) a_Expr
-    gE = mkSimpleGeneratedFunBind loc ge_RDR [a_Pat, b_Pat] $
+    gE = mkSimpleGeneratedFunBind loc ge_RDR pats $
         negate_expr (nlHsApp (nlHsApp (nlHsVar lt_RDR) a_Expr) b_Expr)
 
     get_tag con = dataConTag con - fIRST_TAG
@@ -447,7 +448,7 @@ gen_Ord_binds loc dit@(DerivInstTys{ dit_rep_tc = tycon
     mkOrdOp :: OrdOp -> LHsBind GhcPs
     -- Returns a binding   op a b = ... compares a and b according to op ....
     mkOrdOp op
-      = mkSimpleGeneratedFunBind loc (ordMethRdr op) [a_Pat, b_Pat]
+      = mkSimpleGeneratedFunBind loc (ordMethRdr op) (map mkVisPat [a_Pat, b_Pat])
                         (mkOrdOpRhs op)
 
     mkOrdOpRhs :: OrdOp -> LHsExpr GhcPs
@@ -676,7 +677,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
     occ_nm = getOccString tycon
 
     succ_enum tag2con_RDR maxtag_RDR
-      = mkSimpleGeneratedFunBind loc succ_RDR [a_Pat] $
+      = mkSimpleGeneratedFunBind loc succ_RDR [mkVisPat a_Pat] $
         untag_Expr [(a_RDR, ah_RDR)] $
         nlHsIf (nlHsApps eq_RDR [nlHsVar maxtag_RDR,
                                nlHsVarApps intDataCon_RDR [ah_RDR]])
@@ -686,7 +687,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
                                         nlHsIntLit 1]))
 
     pred_enum tag2con_RDR
-      = mkSimpleGeneratedFunBind loc pred_RDR [a_Pat] $
+      = mkSimpleGeneratedFunBind loc pred_RDR [mkVisPat a_Pat] $
         untag_Expr [(a_RDR, ah_RDR)] $
         nlHsIf (nlHsApps eq_RDR [nlHsIntLit 0,
                                nlHsVarApps intDataCon_RDR [ah_RDR]])
@@ -698,7 +699,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
                                                 (mkIntegralLit (-1 :: Int)))]))
 
     to_enum tag2con_RDR maxtag_RDR
-      = mkSimpleGeneratedFunBind loc toEnum_RDR [a_Pat] $
+      = mkSimpleGeneratedFunBind loc toEnum_RDR [mkVisPat a_Pat] $
         nlHsIf (nlHsApps and_RDR
                 [nlHsApps ge_RDR [nlHsVar a_RDR, nlHsIntLit 0],
                  nlHsApps le_RDR [ nlHsVar a_RDR
@@ -707,7 +708,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
              (illegal_toEnum_tag occ_nm maxtag_RDR)
 
     enum_from tag2con_RDR maxtag_RDR
-      = mkSimpleGeneratedFunBind loc enumFrom_RDR [a_Pat] $
+      = mkSimpleGeneratedFunBind loc enumFrom_RDR [mkVisPat a_Pat] $
           untag_Expr [(a_RDR, ah_RDR)] $
           nlHsApps map_RDR
                 [nlHsVar tag2con_RDR,
@@ -716,7 +717,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
                             (nlHsVar maxtag_RDR))]
 
     enum_from_then tag2con_RDR maxtag_RDR
-      = mkSimpleGeneratedFunBind loc enumFromThen_RDR [a_Pat, b_Pat] $
+      = mkSimpleGeneratedFunBind loc enumFromThen_RDR (map mkVisPat [a_Pat, b_Pat]) $
           untag_Expr [(a_RDR, ah_RDR), (b_RDR, bh_RDR)] $
           nlHsApp (nlHsVarApps map_RDR [tag2con_RDR]) $
             nlHsPar (enum_from_then_to_Expr
@@ -729,7 +730,7 @@ gen_Enum_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
                            ))
 
     from_enum
-      = mkSimpleGeneratedFunBind loc fromEnum_RDR [a_Pat] $
+      = mkSimpleGeneratedFunBind loc fromEnum_RDR [mkVisPat a_Pat] $
           untag_Expr [(a_RDR, ah_RDR)] $
           (nlHsVarApps intDataCon_RDR [ah_RDR])
 
@@ -848,7 +849,7 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
       ]
 
     enum_range tag2con_RDR
-      = mkSimpleGeneratedFunBind loc range_RDR [nlTuplePat [a_Pat, b_Pat] Boxed] $
+      = mkSimpleGeneratedFunBind loc range_RDR [mkVisPat $ nlTuplePat [a_Pat, b_Pat] Boxed] $
           untag_Expr [(a_RDR, ah_RDR)] $
           untag_Expr [(b_RDR, bh_RDR)] $
           nlHsApp (nlHsVarApps map_RDR [tag2con_RDR]) $
@@ -858,9 +859,9 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
 
     enum_index
       = mkSimpleGeneratedFunBind loc unsafeIndex_RDR
-                [noLocA (AsPat noAnn (noLocA c_RDR)
+                (map mkVisPat [noLocA (AsPat noAnn (noLocA c_RDR)
                            (nlTuplePat [a_Pat, nlWildPat] Boxed)),
-                                d_Pat] (
+                                d_Pat]) (
            untag_Expr [(a_RDR, ah_RDR)] (
            untag_Expr [(d_RDR, dh_RDR)] (
            let
@@ -874,7 +875,7 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
 
     -- This produces something like `(ch >= ah) && (ch <= bh)`
     enum_inRange
-      = mkSimpleGeneratedFunBind loc inRange_RDR [nlTuplePat [a_Pat, b_Pat] Boxed, c_Pat] $
+      = mkSimpleGeneratedFunBind loc inRange_RDR (map mkVisPat [nlTuplePat [a_Pat, b_Pat] Boxed, c_Pat]) $
           untag_Expr [(a_RDR, ah_RDR)] (
           untag_Expr [(b_RDR, bh_RDR)] (
           untag_Expr [(c_RDR, ch_RDR)] (
@@ -908,7 +909,7 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
     --------------------------------------------------------------
     single_con_range
       = mkSimpleGeneratedFunBind loc range_RDR
-          [nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed] $
+          [mkVisPat $ nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed] $
         noLocA (mkHsComp ListComp stmts con_expr)
       where
         stmts = zipWith3Equal "single_con_range" mk_qual as_needed bs_needed cs_needed
@@ -920,8 +921,8 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
     ----------------
     single_con_index
       = mkSimpleGeneratedFunBind loc unsafeIndex_RDR
-                [nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed,
-                 con_pat cs_needed]
+                (map mkVisPat [nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed,
+                 con_pat cs_needed])
         -- We need to reverse the order we consider the components in
         -- so that
         --     range (l,u) !! index (l,u) i == i   -- when i is in range
@@ -946,8 +947,8 @@ gen_Ix_binds loc (DerivInstTys{dit_rep_tc = tycon}) = do
     ------------------
     single_con_inRange
       = mkSimpleGeneratedFunBind loc inRange_RDR
-                [nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed,
-                 con_pat cs_needed] $
+                (map mkVisPat [nlTuplePat [con_pat as_needed, con_pat bs_needed] Boxed,
+                 con_pat cs_needed]) $
           if con_arity == 0
              -- If the product type has no fields, inRange is trivially true
              -- (see #12853).
@@ -1414,7 +1415,7 @@ gen_Data_binds loc (DerivInstTys{dit_rep_tc = rep_tc})
         ------------ gunfold
     gunfold_bind = mkSimpleGeneratedFunBind loc
                      gunfold_RDR
-                     [k_Pat, z_Pat, if n_cons == 1 then nlWildPat else c_Pat]
+                     (map mkVisPat [k_Pat, z_Pat, if n_cons == 1 then nlWildPat else c_Pat])
                      gunfold_rhs
 
     gunfold_rhs
@@ -1455,7 +1456,7 @@ gen_Data_binds loc (DerivInstTys{dit_rep_tc = rep_tc})
       = mkSimpleGeneratedFunBind
           loc
           dataTypeOf_RDR
-          [nlWildPat]
+          [mkVisPat nlWildPat]
           (nlHsVar dataT_RDR)
 
         ------------ gcast1/2
@@ -1479,7 +1480,7 @@ gen_Data_binds loc (DerivInstTys{dit_rep_tc = rep_tc})
                 | tycon_kind `tcEqKind` kind2 = mk_gcast dataCast2_RDR gcast2_RDR
                 | otherwise                 = emptyBag
     mk_gcast dataCast_RDR gcast_RDR
-      = unitBag (mkSimpleGeneratedFunBind loc dataCast_RDR [nlVarPat f_RDR]
+      = unitBag (mkSimpleGeneratedFunBind loc dataCast_RDR [mkVisPat $ nlVarPat f_RDR]
                                  (nlHsVar gcast_RDR `nlHsApp` nlHsVar f_RDR))
 
 
@@ -2285,7 +2286,7 @@ mkFunBindSE arity loc fun pats_and_exprs
   = mkRdrFunBindSE arity (L (noAnnSrcSpan loc) fun) matches
   where
     matches = [mkMatch (mkPrefixFunRhs (L (noAnnSrcSpan loc) fun))
-                               (map (parenthesizePat appPrec) p) e
+                               (map (parenthesizeLArgPat appPrec . mkVisPat) p) e
                                emptyLocalBinds
               | (p,e) <-pats_and_exprs]
 
@@ -2306,7 +2307,7 @@ mkFunBindEC arity loc fun catch_all pats_and_exprs
   = mkRdrFunBindEC arity catch_all (L (noAnnSrcSpan loc) fun) matches
   where
     matches = [ mkMatch (mkPrefixFunRhs (L (noAnnSrcSpan loc) fun))
-                                (map (parenthesizePat appPrec) p) e
+                                (map (parenthesizeLArgPat appPrec . mkVisPat) p) e
                                 emptyLocalBinds
               | (p,e) <- pats_and_exprs ]
 
@@ -2333,7 +2334,7 @@ mkRdrFunBindEC arity catch_all fun@(L loc _fun_rdr) matches
    -- See #4302
    matches' = if null matches
               then [mkMatch (mkPrefixFunRhs fun)
-                            (replicate (arity - 1) nlWildPat ++ [z_Pat])
+                            (replicate (arity - 1) (mkVisPat nlWildPat) ++ [mkVisPat z_Pat])
                             (catch_all $ nlHsCase z_Expr [])
                             emptyLocalBinds]
               else matches
@@ -2353,7 +2354,7 @@ mkRdrFunBindSE arity fun@(L loc fun_rdr) matches
    -- See #4302
    matches' = if null matches
               then [mkMatch (mkPrefixFunRhs fun)
-                            (replicate arity nlWildPat)
+                            (replicate arity (mkVisPat nlWildPat))
                             (error_Expr str) emptyLocalBinds]
               else matches
    str = fsLit "Void " `appendFS` occNameFS (rdrNameOcc fun_rdr)
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index e4ec0325ecde2fdfa3646f309659a1a5e22e2ba4..a068e9394c041e0b53859a3898ee7872fa39fbec 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1899,6 +1899,12 @@ instance Diagnostic TcRnMessage where
           WarningTxt{} -> text "WARNING"
           DeprecatedTxt{} -> text "DEPRECATED"
 
+    TcRnIllegalInvisibleTypePattern tp -> mkSimpleDecorated $
+      text "Illegal invisible type pattern:" <+> ppr tp
+
+    TcRnInvisPatWithNoForAll tp -> mkSimpleDecorated $
+      text "Invisible type pattern" <+> ppr tp <+> text "has no associated forall"
+
   diagnosticReason :: TcRnMessage -> DiagnosticReason
   diagnosticReason = \case
     TcRnUnknownMessage m
@@ -2525,6 +2531,10 @@ instance Diagnostic TcRnMessage where
       -> ErrorWithoutFlag
     TcRnNamespacedWarningPragmaWithoutFlag{}
       -> ErrorWithoutFlag
+    TcRnIllegalInvisibleTypePattern{}
+      -> ErrorWithoutFlag
+    TcRnInvisPatWithNoForAll{}
+      -> ErrorWithoutFlag
 
   diagnosticHints = \case
     TcRnUnknownMessage m
@@ -3185,6 +3195,10 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnNamespacedWarningPragmaWithoutFlag{}
       -> [suggestExtension LangExt.ExplicitNamespaces]
+    TcRnIllegalInvisibleTypePattern{}
+      -> [suggestExtension LangExt.TypeAbstractions]
+    TcRnInvisPatWithNoForAll{}
+      -> noHints
 
   diagnosticCode = constructorCode
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index c855e6d3dc5888392b01d1bf25998e867e53cd9f..e1a4ff1c3d1efb456966b49481149c6817cc9c15 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -4212,8 +4212,35 @@ data TcRnMessage where
   -}
   TcRnNamespacedWarningPragmaWithoutFlag :: WarnDecl GhcPs -> TcRnMessage
 
-  deriving Generic
+  {-| TcRnInvisPatWithNoForAll is an error raised when invisible type pattern
+      is used without associated `forall` in types
+
+      Examples:
+
+        f :: Int
+        f @t = 5
+
+        g :: [a -> a]
+        g = [\ @t x -> x :: t]
+
+      Test cases: T17694c T17594d
+  -}
+  TcRnInvisPatWithNoForAll :: HsTyPat GhcRn -> TcRnMessage
 
+  {-| TcRnIllegalInvisibleTypePattern is an error raised when invisible type pattern
+      is used without the TypeAbstractions extension enabled
+
+      Example:
+
+        {-# LANGUAGE NoTypeAbstractions #-}
+        id :: a -> a
+        id @t x = x
+
+      Test cases: T17694b
+  -}
+  TcRnIllegalInvisibleTypePattern :: HsTyPat GhcPs -> TcRnMessage
+
+  deriving Generic
 
 ----
 
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 6b22d661875934904c9c713001f372e82dee2a1c..2c0576fd661ecfe9fea50ded53a61722910498cc 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -1141,15 +1141,28 @@ At a call site we may have calls looking like this
 At definition sites we may have type /patterns/ to abstract over type variables
    fi           x       = rhs   -- Inferred: no type pattern
    fs           x       = rhs   -- Specified: type pattern omitted
-   fs @a       (x :: a) = rhs   -- Specified: type pattern supplied (NB: not implemented)
+   fs @a       (x :: a) = rhs   -- Specified: type pattern supplied
    fr (type a) (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier used
    fr a        (x :: a) = rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
 
-Type patterns in lambdas work the same way as they do in a function LHS
-   fs = \           x       -> rhs   -- Specified: type pattern omitted
-   fs = \ @a       (x :: a) -> rhs   -- Specified: type pattern supplied (NB: not implemented)
-   fr = \ (type a) (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier used
-   fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
+Type patterns in lambdas mostly work the same way as they do in a function LHS,
+except for @-binders
+   OK:  fs = \           x       -> rhs   -- Specified: type pattern omitted
+   Bad: fs = \ @a       (x :: a) -> rhs   -- Specified: type pattern supplied
+   OK:  fr = \ (type a) (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier used
+   OK:  fr = \ a        (x :: a) -> rhs   -- Required: type pattern is compulsory, `type` qualifier omitted
+
+When it comes to @-binders in lambdas, they do work, but only in a limited set
+of circumstances:
+  * the lambda occurs as an argument to a higher-rank function or constructor
+      higher-rank function:  h :: (forall a. blah) -> ...
+      call site:             x = h (\ @a -> ... )
+  * the lambda is annotated with an inline type signature:
+      (\ @a -> ... ) :: forall a. blah
+  * the lambda is a field in a data structure, whose type is impredicative
+      [ \ @a -> ... ] :: [forall a. blah]
+  * the @-binder is not the first binder in the lambda:
+      \ x @a -> ...
 
 Type patterns may also occur in a constructor pattern. Consider the following data declaration
    data T where
@@ -1221,7 +1234,7 @@ Syntax of abstractions in Pat
       \ (MkT @a  (x :: a)) -> rhs    -- ConPat (c.o. Pat) and HsConPatTyArg (c.o. HsConPatTyArg)
       \ (type a) (x :: a)  -> rhs    -- EmbTyPat (c.o. Pat)
       \ a        (x :: a)  -> rhs    -- VarPat (c.o. Pat)
-      \ @a       (x :: a)  -> rhs    -- to be decided       (NB. not implemented)
+      \ @a       (x :: a)  -> rhs    -- InvisPat (c.o. ArgPat)
 
 * A HsTyPat is not necessarily a plain variable. At the very least,
   we support kind signatures and wildcards:
diff --git a/compiler/GHC/Tc/Gen/Do.hs b/compiler/GHC/Tc/Gen/Do.hs
index eac8687b0113f87f72c6397ddccc99c454d78e74..41079067115bb55cd7aa6f81be99a837f049882a 100644
--- a/compiler/GHC/Tc/Gen/Do.hs
+++ b/compiler/GHC/Tc/Gen/Do.hs
@@ -166,10 +166,10 @@ expand_do_stmts do_or_lc
   do expand_stmts <- expand_do_stmts do_or_lc lstmts
      -- NB: No need to wrap the expansion with an ExpandedStmt
      -- as we want to flatten the rec block statements into its parent do block anyway
-     return $ mkHsApps (wrapGenSpan bind_fun)                           -- (>>=)
-                      [ (wrapGenSpan mfix_fun) `mkHsApp` mfix_expr      -- (mfix (do block))
-                      , genHsLamDoExp do_or_lc [ mkBigLHsVarPatTup all_ids ]     --        (\ x ->
-                                       expand_stmts                  --               stmts')
+     return $ mkHsApps (wrapGenSpan bind_fun)                                           -- (>>=)
+                      [ (wrapGenSpan mfix_fun) `mkHsApp` mfix_expr                      -- (mfix (do block))
+                      , genHsLamDoExp do_or_lc [ mkVisPat $ mkBigLHsVarPatTup all_ids ] --        (\ x ->
+                                       expand_stmts                                     --               stmts')
                       ]
   where
     local_only_ids = local_ids \\ later_ids -- get unique local rec ids;
@@ -186,7 +186,7 @@ expand_do_stmts do_or_lc
     do_block     :: LHsExpr GhcRn
     do_block     = L loc $ HsDo noExtField do_or_lc do_stmts
     mfix_expr    :: LHsExpr GhcRn
-    mfix_expr    = genHsLamDoExp do_or_lc [ wrapGenSpan (LazyPat noExtField $ mkBigLHsVarPatTup all_ids) ]
+    mfix_expr    = genHsLamDoExp do_or_lc [ mkVisPat $ wrapGenSpan (LazyPat noExtField $ mkBigLHsVarPatTup all_ids) ]
                                           $ do_block
                              -- NB: LazyPat because we do not want to eagerly evaluate the pattern
                              -- and potentially loop forever
@@ -204,7 +204,7 @@ mk_failable_expr doFlav pat@(L loc _) expr fail_op =
 
      ; if irrf_pat                        -- don't wrap with fail block if
                                           -- the pattern is irrefutable
-       then return $ genHsLamDoExp doFlav [pat] expr
+       then return $ genHsLamDoExp doFlav [mkVisPat pat] expr
        else L loc <$> mk_fail_block doFlav pat expr fail_op
      }
 
@@ -213,12 +213,12 @@ mk_fail_block :: HsDoFlavour -> LPat GhcRn -> LHsExpr GhcRn -> FailOperator GhcR
 mk_fail_block doFlav pat@(L ploc _) e (Just (SyntaxExprRn fail_op)) =
   do  dflags <- getDynFlags
       return $ HsLam noAnn LamSingle $ mkMatchGroup (doExpansionOrigin doFlav)     -- \
-                (wrapGenSpan [ genHsCaseAltDoExp doFlav pat e               --  pat -> expr
+                (wrapGenSpan [ genHsCaseAltDoExp doFlav (mkVisPat pat) e           --  pat -> expr
                              , fail_alt_case dflags pat fail_op      --  _   -> fail "fail pattern"
                              ])
         where
           fail_alt_case :: DynFlags -> LPat GhcRn -> HsExpr GhcRn -> LMatch GhcRn (LHsExpr GhcRn)
-          fail_alt_case dflags pat fail_op = genHsCaseAltDoExp doFlav genWildPat $
+          fail_alt_case dflags pat fail_op = genHsCaseAltDoExp doFlav (mkVisPat genWildPat) $
                                              L ploc (fail_op_expr dflags pat fail_op)
 
           fail_op_expr :: DynFlags -> LPat GhcRn -> HsExpr GhcRn -> HsExpr GhcRn
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index fbc925168991f2ce06f239fcabc5e0a357e7532b..a4b681e7bab1c6ad191a877de2ba78587cb42c71 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -1229,5 +1229,4 @@ checkArgCounts (MG { mg_alts = L _ (match1:matches) })
 
     reqd_args_in_match :: LocatedA (Match GhcRn body1) -> Arity
     -- Counts the number of /required/ args in the match
-    -- IMPORTANT: THIS WILL NEED TO CHANGE WHEN @ty BECOMES A PATTERN
-    reqd_args_in_match (L _ (Match { m_pats = pats })) = length pats
+    reqd_args_in_match (L _ (Match { m_pats = pats })) = count (isVisArgPat . unLoc) pats
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 2c22abb29f82e2502420c50da677c2946dd707c7..9ec72d27ac1f9bea6279426daba14f82747f5016 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -126,28 +126,30 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
 -----------------
 tcMatchPats :: forall a.
                HsMatchContextRn
-            -> [LPat GhcRn]             -- ^ patterns
+            -> [LArgPat GhcRn]          -- ^ patterns
             -> [ExpPatType]             -- ^ types of the patterns
             -> TcM a                    -- ^ checker for the body
-            -> TcM ([LPat GhcTc], a)
+            -> TcM ([LArgPat GhcTc], a)
 -- See Note [tcMatchPats]
 --
 -- PRECONDITION:
---    number of visible Pats in pats
---      (@a is invisible)
---  = number of visible ExpPatTypes in pat_tys
---      (ExpForAllPatTy v is visible iff b is Required)
+--    number of visible pats::[LArgPat GhcRn]   (p is visible, @p is invisible)
+--      ==
+--    number of visible pat_tys::[ExpPatType]   (ExpFunPatTy is visible,
+--                                               ExpForAllPatTy b is visible iff b is Required)
 --
 -- POSTCONDITION:
---   Returns only the /value/ patterns; see Note [tcMatchPats]
+--   number and order of output [LArgPat GhcTc]
+--      ==
+--   number and order of input  [LArgPat GhcRn]
 
 tcMatchPats match_ctxt pats pat_tys thing_inside
-  = assertPpr (count isVisibleExpPatType pat_tys == length pats)
+  = assertPpr (count isVisibleExpPatType pat_tys == count (isVisArgPat . unLoc) pats)
               (ppr pats $$ ppr pat_tys) $
        -- Check PRECONDITION
        -- When we get @patterns the (length pats) will change
     do { err_ctxt <- getErrCtxt
-       ; let loop :: [LPat GhcRn] -> [ExpPatType] -> TcM ([LPat GhcTc], a)
+       ; let loop :: [LArgPat GhcRn] -> [ExpPatType] -> TcM ([LArgPat GhcTc], a)
 
              -- No more patterns.  Discard excess pat_tys;
              -- they should all be invisible.  Example:
@@ -163,28 +165,49 @@ tcMatchPats match_ctxt pats pat_tys thing_inside
 
              -- ExpFunPatTy: expecting a value pattern
              -- tc_lpat will error if it sees a @t type pattern
-             loop (pat : pats) (ExpFunPatTy pat_ty : pat_tys)
+             loop (L l (VisPat _ pat) : pats) (ExpFunPatTy pat_ty : pat_tys)
                = do { (p, (ps, res)) <- tc_lpat pat_ty penv pat $
                                         loop pats pat_tys
-                    ; return (p:ps, res) }
+                    ; return (L l (VisPat Retained p) : ps, res) }
+                    -- This VisPat is Retained.
+                    -- See Note [Invisible binders in functions] in GHC.Hs.Pat
 
              -- ExpForAllPat: expecting a type pattern
-             loop (pat : pats) (ExpForAllPatTy bndr : pat_tys)
-               | Bndr tv vis <- bndr
+             loop all_pats@(L l apat : pats) (ExpForAllPatTy (Bndr tv vis) : pat_tys)
+               | VisPat _ pat <- apat
                , isVisibleForAllTyFlag vis
-               = do { (_p, (ps, res)) <- tc_forall_lpat tv penv pat $
+               = do { (p, (ps, res)) <- tc_forall_lpat tv penv pat $
                                         loop pats pat_tys
 
-                    ; return (ps, res) }
+                    ; return (L l (VisPat Erased p) : ps, res) }
+                    -- This VisPat is Erased.
+                    -- See Note [Invisible binders in functions] in GHC.Hs.Pat
 
-               -- Invisible forall in type, and an @a type pattern
-               -- Add an equation here when we have these
+               -- Invisible (Specified) forall in type, and an @a type pattern
                -- E.g.    f :: forall a. Bool -> a -> blah
                --         f @b True  x = rhs1  -- b is bound to skolem a
                --         f @c False y = rhs2  -- c is bound to skolem a
+               | InvisPat _ tp <- apat
+               , isSpecifiedForAllTyFlag vis
+               = do { (p, (ps, res)) <- tc_ty_pat tp tv $
+                                        loop pats pat_tys
+                    ; return (L l (InvisPat p tp) : ps, res) }
 
                | otherwise  -- Discard invisible pat_ty
-               = loop (pat:pats) pat_tys
+               = loop all_pats pat_tys
+
+             -- This case handles the user error when an InvisPat is used
+             -- without a corresponding invisible (Specified) forall in the type
+             -- E.g. 1.  f :: Int
+             --          f @a = ...   -- loop (InvisPat{} : _) []
+             --      2.  f :: Int -> Int
+             --          f @a x = ... -- loop (InvisPat{} : _) (ExpFunPatTy{} : _)
+             --      3.  f :: forall a -> Int
+             --          f @a t = ... -- loop (InvisPat{} : _) (ExpForAllPatTy (Bndr _ Required) : _)
+             --      4.  f :: forall {a}. Int
+             --          f @a t = ... -- loop (InvisPat{} : _) (ExpForAllPatTy (Bndr _ Inferred) : _)
+             loop (L loc (InvisPat _ tp) : _) _ =
+                failAt (locA loc) (TcRnInvisPatWithNoForAll tp)
 
              loop pats@(_:_) [] = pprPanic "tcMatchPats" (ppr pats)
                     -- Failure of PRECONDITION
@@ -236,11 +259,6 @@ It takes the list of patterns writen by the user, but it returns only the
 /value/ patterns.  For example:
      f :: forall a. forall b -> a -> Mabye b -> blah
      f @a w x (Just y) = ....
-tcMatchPats returns only the /value/ patterns [x, Just y].  Why?  The
-desugarer expects only value patterns.  (We could change that, but we would
-have to do so carefullly.)  However, distinguishing value patterns from type
-patterns is a bit tricky; e.g. the `w` in this example.  So it's very
-convenient to filter them out right here.
 
 
 ************************************************************************
diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs
index 714719deaa5cd531b728750f65c07f9643300476..18547b39095780c5f8b00081b587d99c0a466acb 100644
--- a/compiler/GHC/Tc/TyCl/PatSyn.hs
+++ b/compiler/GHC/Tc/TyCl/PatSyn.hs
@@ -801,8 +801,9 @@ tcPatSynMatcher (L loc ps_name) lpat prag_fn
                       }
              body' = noLocA $
                      HsLam noAnn LamSingle $
-                     MG{ mg_alts = noLocA [mkSimpleMatch (LamAlt LamSingle)
-                                                         args body]
+                     MG{ mg_alts = noLocA [mkSimpleMatchArg (LamAlt LamSingle)
+                                                         (map mkRetainedVisPat args)
+                                                         body]
                        , mg_ext = MatchGroupTc (map unrestricted [pat_ty, cont_ty, fail_ty]) res_ty gen
                        }
              match = mkMatch (mkPrefixFunRhs (L loc (idName patsyn_id))) []
@@ -943,7 +944,7 @@ tcPatSynBuilderBind prag_fn (PSB { psb_id = ps_lname@(L loc ps_name)
     mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
     mk_mg body = mkMatchGroup (Generated OtherExpansion SkipPmc) (noLocA [builder_match])
           where
-            builder_args  = [L (l2l loc) (VarPat noExtField (L loc n))
+            builder_args  = [mkVisPat (L (l2l loc) (VarPat noExtField (L loc n)))
                             | L loc n <- args]
             builder_match = mkMatch (mkPrefixFunRhs ps_lname)
                                     builder_args body
@@ -958,7 +959,7 @@ tcPatSynBuilderBind prag_fn (PSB { psb_id = ps_lname@(L loc ps_name)
                   -> MatchGroup GhcRn (LHsExpr GhcRn)
     add_dummy_arg mg@(MG { mg_alts =
                            (L l [L loc match@(Match { m_pats = pats })]) })
-      = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
+      = mg { mg_alts = L l [L loc (match { m_pats = mkVisPat nlWildPatName : pats })] }
     add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
                              pprMatches other_mg
 
diff --git a/compiler/GHC/Tc/Zonk/Type.hs b/compiler/GHC/Tc/Zonk/Type.hs
index 3cee664902435ad918271fbb0cd2ecc2da7621e5..90de9bb4abc24d9d87e14ea1dfaa4e6d17e6f465 100644
--- a/compiler/GHC/Tc/Zonk/Type.hs
+++ b/compiler/GHC/Tc/Zonk/Type.hs
@@ -884,7 +884,7 @@ zonkMatch :: Anno (GRHS GhcTc (LocatedA (body GhcTc))) ~ EpAnnCO
           -> ZonkTcM (LMatch GhcTc (LocatedA (body GhcTc)))
 zonkMatch zBody (L loc match@(Match { m_pats = pats
                                     , m_grhss = grhss }))
-  = runZonkBndrT (zonkPats pats) $ \ new_pats ->
+  = runZonkBndrT (zonkArgPats pats) $ \ new_pats ->
   do  { new_grhss <- zonkGRHSs zBody grhss
       ; return (L loc (match { m_pats = new_pats, m_grhss = new_grhss })) }
 
@@ -1476,6 +1476,15 @@ zonkRecFields (HsRecFields flds dd)
 ************************************************************************
 -}
 
+zonkArgPat :: LArgPat GhcTc ->  ZonkBndrTcM (LArgPat GhcTc)
+zonkArgPat arg_pat = wrapLocZonkBndrMA zonk_arg_pat arg_pat where
+  zonk_arg_pat (VisPat x pat) = do
+    pat' <- zonkPat pat
+    pure (VisPat x pat')
+  zonk_arg_pat (InvisPat ty tp) = do
+    ty' <- noBinders $ zonkTcTypeToTypeX ty
+    pure (InvisPat ty' tp)
+
 zonkPat :: LPat GhcTc -> ZonkBndrTcM (LPat GhcTc)
 -- Extend the environment as we go, because it's possible for one
 -- pattern to bind something that is used in another (inside or
@@ -1627,6 +1636,9 @@ zonkConStuff (RecCon (HsRecFields rpats dd))
 zonkPats :: [LPat GhcTc] -> ZonkBndrTcM [LPat GhcTc]
 zonkPats = traverse zonkPat
 
+zonkArgPats :: [LArgPat GhcTc] -> ZonkBndrTcM [LArgPat GhcTc]
+zonkArgPats = traverse zonkArgPat
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index d2ae5f8085a81d8136c412ad0015f70b99cf9207..6903e2093d91e8385197b15928e58f43d576dd05 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -1006,8 +1006,8 @@ cvtLocalDecs declDescr ds
 
 cvtClause :: HsMatchContextPs -> TH.Clause -> CvtM (Hs.LMatch GhcPs (LHsExpr GhcPs))
 cvtClause ctxt (Clause ps body wheres)
-  = do  { ps' <- cvtPats ps
-        ; let pps = map (parenthesizePat appPrec) ps'
+  = do  { ps' <- cvtArgPats ps
+        ; let pps = map (parenthesizeLArgPat appPrec) ps'
         ; g'  <- cvtGuard body
         ; ds' <- cvtLocalDecs WhereClause wheres
         ; returnLA $ Hs.Match noAnn ctxt pps (GRHSs emptyComments g' ds') }
@@ -1052,11 +1052,11 @@ cvtl e = wrapLA (cvt e)
                                -- own expression to avoid pretty-printing
                                -- oddities that can result from zero-argument
                                -- lambda expressions. See #13856.
-    cvt (LamE ps e)    = do { ps' <- cvtPats ps; e' <- cvtl e
-                            ; let pats = map (parenthesizePat appPrec) ps'
+    cvt (LamE ps e)    = do { ps' <- cvtArgPats ps; e' <- cvtl e
+                            ; let pats = map (parenthesizeLArgPat appPrec) ps'
                             ; th_origin <- getOrigin
                             ; wrapParLA (HsLam noAnn LamSingle . mkMatchGroup th_origin)
-                                        [mkSimpleMatch (LamAlt LamSingle) pats e']}
+                                        [mkSimpleMatchArg (LamAlt LamSingle) pats e']}
     cvt (LamCaseE ms)  = do { ms' <- mapM (cvtMatch $ LamAlt LamCase) ms
                             ; th_origin <- getOrigin
                             ; wrapParLA (HsLam noAnn LamCase . mkMatchGroup th_origin) ms'
@@ -1335,7 +1335,7 @@ cvtMatch ctxt (TH.Match p body decs)
                      _                -> p'
         ; g' <- cvtGuard body
         ; decs' <- cvtLocalDecs WhereClause decs
-        ; returnLA $ Hs.Match noAnn ctxt [lp] (GRHSs emptyComments g' decs') }
+        ; returnLA $ Hs.Match noAnn ctxt [mkVisPat lp] (GRHSs emptyComments g' decs') }
 
 cvtGuard :: TH.Body -> CvtM [LGRHS GhcPs (LHsExpr GhcPs)]
 cvtGuard (GuardedB pairs) = mapM cvtpair pairs
@@ -1411,6 +1411,18 @@ cvtLit _ = panic "Convert.cvtLit: Unexpected literal"
 quotedSourceText :: String -> SourceText
 quotedSourceText s = SourceText $ fsLit $ "\"" ++ s ++ "\""
 
+cvtArgPats :: [TH.ArgPat] -> CvtM [Hs.LArgPat GhcPs]
+cvtArgPats pats = mapM cvtArgPat pats
+
+cvtArgPat :: TH.ArgPat -> CvtM (Hs.LArgPat GhcPs)
+cvtArgPat pat = wrapLA (cvtap pat)
+
+cvtap :: TH.ArgPat -> CvtM (Hs.ArgPat GhcPs)
+cvtap (VisAP pat) = do { pat' <- cvtPat pat
+                       ; pure (VisPat noExtField pat')}
+cvtap (InvisAP t) = do { t' <- cvtType t
+                       ; pure (InvisPat noAnn (mkHsTyPat noAnn t'))}
+
 cvtPats :: [TH.Pat] -> CvtM [Hs.LPat GhcPs]
 cvtPats pats = mapM cvtPat pats
 
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 79f5b9d07c428379103c2734b5b17ee21d43ddf2..d50de9c4057c961beac30fa6e744bf48ee02da48 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -601,6 +601,8 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnInvalidDefaultedTyVar"                     = 45625
   GhcDiagnosticCode "TcRnIllegalTermLevelUse"                       = 01928
   GhcDiagnosticCode "TcRnNamespacedWarningPragmaWithoutFlag"        = 14995
+  GhcDiagnosticCode "TcRnInvisPatWithNoForAll"                      = 14964
+  GhcDiagnosticCode "TcRnIllegalInvisibleTypePattern"               = 78249
 
   -- TcRnTypeApplicationsDisabled
   GhcDiagnosticCode "TypeApplication"                               = 23482
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index e8f37261f99c6319016086ecdd4129c5e4d05ffd..a6ea226e864311e73e7e352b09f7b7a7f122da91 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -69,6 +69,7 @@ module GHC.Types.Var (
         ForAllTyFlag(Invisible,Required,Specified,Inferred),
         Specificity(..),
         isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag,
+        isSpecifiedForAllTyFlag,
         coreTyLamForAllTyFlag,
 
         -- * FunTyFlag
@@ -494,6 +495,11 @@ isInferredForAllTyFlag :: ForAllTyFlag -> Bool
 isInferredForAllTyFlag (Invisible InferredSpec) = True
 isInferredForAllTyFlag _                        = False
 
+isSpecifiedForAllTyFlag :: ForAllTyFlag -> Bool
+-- More restrictive than isInvisibleForAllTyFlag
+isSpecifiedForAllTyFlag (Invisible SpecifiedSpec) = True
+isSpecifiedForAllTyFlag _                         = False
+
 coreTyLamForAllTyFlag :: ForAllTyFlag
 -- ^ The ForAllTyFlag on a (Lam a e) term, where `a` is a type variable.
 -- If you want other ForAllTyFlag, use a cast.
diff --git a/compiler/Language/Haskell/Syntax/Expr.hs b/compiler/Language/Haskell/Syntax/Expr.hs
index f77d2a283a3e1d87e302015f317483adae188e59..b7b948682fa7acb3a767c58f419fd66ca1d5e8bc 100644
--- a/compiler/Language/Haskell/Syntax/Expr.hs
+++ b/compiler/Language/Haskell/Syntax/Expr.hs
@@ -979,7 +979,7 @@ data Match p body
   = Match {
         m_ext   :: XCMatch p body,
         m_ctxt  :: HsMatchContext (LIdP (NoGhcTc p)),   -- See Note [m_ctxt in Match]
-        m_pats  :: [LPat p],                            -- The patterns
+        m_pats  :: [LArgPat p],                         -- The patterns
         m_grhss :: (GRHSs p body)
   }
   | XMatch !(XXMatch p body)
diff --git a/compiler/Language/Haskell/Syntax/Extension.hs b/compiler/Language/Haskell/Syntax/Extension.hs
index 82edc341f2c4ddc3974782731b418a14dcef9491..3f43bec40d6b28ccfded309a422a0576c55a5b76 100644
--- a/compiler/Language/Haskell/Syntax/Extension.hs
+++ b/compiler/Language/Haskell/Syntax/Extension.hs
@@ -612,6 +612,14 @@ type family XCoPat       x
 type family XXPat        x
 type family XHsFieldBind x
 
+
+-- =====================================================================
+-- Type families for the ArgPat extension points
+
+type family XVisPat      x
+type family XInvisPat    x
+type family XXArgPat     x
+
 -- =====================================================================
 -- Type families for the HsTypes type families
 
diff --git a/compiler/Language/Haskell/Syntax/Pat.hs b/compiler/Language/Haskell/Syntax/Pat.hs
index a876df97f82107b613199d20fff12fb9d75921b5..d6f56707159106fe83e54d670d0994999b78aacc 100644
--- a/compiler/Language/Haskell/Syntax/Pat.hs
+++ b/compiler/Language/Haskell/Syntax/Pat.hs
@@ -20,7 +20,8 @@
 -- See Note [Language.Haskell.Syntax.* Hierarchy] for why not GHC.Hs.*
 module Language.Haskell.Syntax.Pat (
         Pat(..), LPat,
-        ConLikeP,
+        ConLikeP, ArgPat(..), LArgPat, isInvisArgPat,
+        isVisArgPat, mapVisPat,
 
         HsConPatDetails, hsConPatArgs, hsConPatTyArgs,
         HsConPatTyArg(..), XConPatTyArg,
@@ -235,6 +236,30 @@ data HsConPatTyArg p = HsConPatTyArg !(XConPatTyArg p) (HsTyPat p)
 
 type family XConPatTyArg p
 
+-- | A pattern to be used in a sequence of patterns, like what appears
+-- to the right of @f@ in @f a b True = ...@. A 'ArgPat' allows for the
+-- possibility of binding a /type variable/ with \@.
+data ArgPat pass -- See Note [Invisible binders in functions] in GHC.Hs.Pat
+  = VisPat (XVisPat pass) (LPat pass)
+  | InvisPat (XInvisPat pass) (HsTyPat (NoGhcTc pass))
+  | XArgPat !(XXArgPat pass)
+
+isInvisArgPat :: ArgPat p -> Bool
+isInvisArgPat InvisPat{} = True
+isInvisArgPat VisPat{}   = False
+isInvisArgPat XArgPat{}  = False
+
+isVisArgPat :: ArgPat pass -> Bool
+isVisArgPat VisPat{}   = True
+isVisArgPat InvisPat{} = False
+isVisArgPat XArgPat{}  = False
+
+mapVisPat :: (LPat pass -> LPat pass) -> ArgPat pass -> ArgPat pass
+mapVisPat f (VisPat x pat) = VisPat x (f pat)
+mapVisPat _ arg_pat = arg_pat
+
+type LArgPat pass =  XRec pass (ArgPat pass)
+
 -- | Haskell Constructor Pattern Details
 type HsConPatDetails p = HsConDetails (HsConPatTyArg (NoGhcTc p)) (LPat p) (HsRecFields p (LPat p))
 
diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst
index 67f4c08235302e9775109efcd3f706798807db2a..1b55c2b60257c727d3e5937b87d72e8ed7247f8e 100644
--- a/docs/users_guide/exts/type_abstractions.rst
+++ b/docs/users_guide/exts/type_abstractions.rst
@@ -94,6 +94,107 @@ already be in scope, and so are always new variables that only bind whatever typ
 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.
 
+.. _type-abstractions-in-functions:
+
+Type Abstractions in Functions
+------------------------------
+
+Type abstraction syntax can be used in lambdas and function left-hand sides to
+bring into scope type variables associated with invisible ``forall``.
+For example::
+
+    id :: forall a. a -> a
+    id @t x = x :: t
+
+Here type variables ``t`` and ``a`` stand for the same type, i.e. the first and
+only type argument of ``id``. In a call ``id @Int`` we have ``a = Int``, ``t = Int``.
+The difference is that ``a`` is in scope in the type signature, while ``t`` is
+in scope in the function equation.
+
+The scope of ``a`` can be extended to cover the function equation as well by
+enabling :extension:`ScopedTypeVariables`. Using a separate binder like ``@t``
+is the modern and more flexible alternative for that, capable of handling
+higher-rank scenarios (see the ``higherRank`` example below).
+
+When multiple variables are bound with ``@``-binders, they are matched
+left-to-right with the corresponding forall-bound variables in the type
+signature::
+
+    const :: forall a. forall b. a -> b -> a
+    const @ta @tb x  = x
+
+In this example, ``@ta`` corresponds to ``forall a.`` and ``@tb`` to
+``forall b.``. It is also possible to use ``@``-binders in combination with
+implicit quantification (i.e. no explicit forall in the signature)::
+
+    const :: a -> b -> a
+    const @ta @tb x  = x
+
+In such cases, type variables in the signature are considered to be quantified
+with an implicit ``forall`` in the order in which they appear in the signature,
+c.f. :extension:`TypeApplications`.
+
+It is not possible to match against a specific type (such as ``Maybe`` or
+``Int``) in an ``@``-binder. The binder must be irrefutable, i.e. it may take
+one of the following forms:
+
+    * type variable pattern ``@a``
+    * type variable pattern with a kind annotation ``@(f :: Type -> Type)``
+    * wildcard ``@_``, with or without a kind annotation
+
+The main advantage to using ``@``-binders over :extension:`ScopedTypeVariables`
+is the ability to use them in lambdas passed to higher-rank functions::
+
+    higherRank :: (forall a. (Num a, Bounded a) => a -> a) -> (Int8, Int16)
+    higherRank f = (f 42, f 42)
+
+    ex :: (Int8, Int16)
+    ex = higherRank (\ @a x -> maxBound @a - x )
+                       -- @a-binder in a lambda pattern in an argument
+                       -- to a higher-order function
+
+At the moment, an ``@``-binder is valid only in a limited set of circumstances:
+
+* In a function left-hand side, where the function must have an explicit
+  type signature::
+
+    f1 :: forall a. a -> forall b. b -> (a, b)
+    f1 @a x @b y = (x :: a, y :: b)        -- OK
+
+  It would be illegal to omit the type signature for ``f``, nor is it
+  possible to move the binder to a lambda on the RHS::
+
+    f2 :: forall a. a -> forall b. b -> (a, b)
+    f2 = \ @a x @b y -> (x :: a, y :: b)   -- ILLEGAL
+
+* In a lambda annotated with an inline type signature:
+  ::
+
+    f3 = (\ @a x @b y -> (x :: a, y :: b) )      -- OK
+        :: forall a. a -> forall b. b -> (a, b)
+
+* In a lambda used as an argument to a higher-rank function or data
+  constructor::
+
+    h :: (forall a. a -> forall b. b -> (a, b)) -> (Int, Bool)
+    h = ...
+
+    f4 = h (\ @a x @b y -> (x :: a, y :: b))     -- OK
+
+* In a lambda used as a field of a data structure (e.g. a list item), whose type
+  is impredicative (see :extension:`ImpredicativeTypes`)::
+
+    f5 :: [forall a. a -> a -> a]
+    f5 = [ \ @a x _ -> x :: a,
+           \ @a _ y -> y :: a ]
+
+* In a lambda of multiple arguments, where the first argument is visible, and
+  only if :extension:`DeepSubsumption` is off::
+
+    {-# LANGUAGE NoDeepSubsumption #-}
+    f6 :: () -> forall a. a -> (a, a)
+    f6 = \ _ @a x -> (x :: a, x)   -- OK
+
 .. _invisible-binders-in-type-declarations:
 
 Invisible Binders in Type Declarations
diff --git a/libraries/ghci/GHCi/TH/Binary.hs b/libraries/ghci/GHCi/TH/Binary.hs
index 6d5447e3296542de97e0b5ca2e5c38b78362d892..fd4146b4d470cdee459a48a540f819fdd29dd8d6 100644
--- a/libraries/ghci/GHCi/TH/Binary.hs
+++ b/libraries/ghci/GHCi/TH/Binary.hs
@@ -34,6 +34,7 @@ instance Binary TH.Lit
 instance Binary TH.Range
 instance Binary TH.Stmt
 instance Binary TH.Pat
+instance Binary TH.ArgPat
 instance Binary TH.Exp
 instance Binary TH.Dec
 instance Binary TH.Overlap
diff --git a/libraries/template-haskell/Language/Haskell/TH.hs b/libraries/template-haskell/Language/Haskell/TH.hs
index 22f434d4e53f80f29200fd4e1062937c7c15af31..16c8eb561f77eaf30b5a558b427d1d493c897632 100644
--- a/libraries/template-haskell/Language/Haskell/TH.hs
+++ b/libraries/template-haskell/Language/Haskell/TH.hs
@@ -85,7 +85,7 @@ module Language.Haskell.TH(
     -- ** Expressions
         Exp(..), Match(..), Body(..), Guard(..), Stmt(..), Range(..), Lit(..),
     -- ** Patterns
-        Pat(..), FieldExp, FieldPat,
+        Pat(..), ArgPat(..), FieldExp, FieldPat,
     -- ** Types
         Type(..), TyVarBndr(..), TyLit(..), Kind, Cxt, Pred, Syntax.Role(..),
         Syntax.Specificity(..),
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib.hs b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
index 88d6baa7954cfa4ea26b29cd50c355b8566a4cea..3ddd3ba757c3f765d4e789affc3695b019be2708 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib.hs
@@ -22,7 +22,7 @@ module Language.Haskell.TH.Lib (
         TyLitQ, CxtQ, PredQ, DerivClauseQ, MatchQ, ClauseQ, BodyQ, GuardQ,
         StmtQ, RangeQ, SourceStrictnessQ, SourceUnpackednessQ, BangQ,
         BangTypeQ, VarBangTypeQ, StrictTypeQ, VarStrictTypeQ, FieldExpQ, PatQ,
-        FieldPatQ, RuleBndrQ, TySynEqnQ, PatSynDirQ, PatSynArgsQ,
+        ArgPatQ, FieldPatQ, RuleBndrQ, TySynEqnQ, PatSynDirQ, PatSynArgsQ,
         FamilyResultSigQ, DerivStrategyQ,
         TyVarBndrUnit, TyVarBndrSpec, TyVarBndrVis,
 
@@ -36,6 +36,9 @@ module Language.Haskell.TH.Lib (
         listP, sigP, viewP, typeP,
         fieldPat,
 
+    -- *** Arg patterns
+        visAP, invisAP,
+
     -- *** Pattern Guards
         normalB, guardedB, normalG, normalGE, patG, patGE, match, clause,
 
diff --git a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
index 49dd55bdbb7decf960ba579cb71af8ec348bbb11..ea9875b835d3b3b8ff454c362b2da2ea7f022fd4 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Lib/Internal.hs
@@ -40,6 +40,7 @@ type CodeQ = Code Q
 
 type InfoQ               = Q Info
 type PatQ                = Q Pat
+type ArgPatQ             = Q ArgPat
 type FieldPatQ           = Q FieldPat
 type ExpQ                = Q Exp
 type DecQ                = Q Dec
@@ -168,6 +169,14 @@ viewP e p = do e' <- e
                p' <- p
                pure (ViewP e' p')
 
+visAP :: Quote m => m Pat -> m ArgPat
+visAP p = do p' <- p
+             pure (VisAP p')
+
+invisAP :: Quote m => m Type -> m ArgPat
+invisAP t = do t' <- t
+               pure (InvisAP t')
+
 fieldPat :: Quote m => Name -> m Pat -> m FieldPat
 fieldPat n p = do p' <- p
                   pure (n, p')
@@ -244,11 +253,13 @@ match p rhs ds = do { p' <- p;
 
 -- | Use with 'funD'
 clause :: Quote m => [m Pat] -> m Body -> [m Dec] -> m Clause
-clause ps r ds = do { ps' <- sequenceA ps;
-                      r' <- r;
-                      ds' <- sequenceA ds;
-                      pure (Clause ps' r' ds') }
+clause ps = clauseArg (fmap visAP ps)
 
+clauseArg :: Quote m => [m ArgPat] -> m Body -> [m Dec] -> m Clause
+clauseArg ps r ds = do { ps' <- sequenceA ps;
+                         r' <- r;
+                         ds' <- sequenceA ds;
+                         pure (Clause ps' r' ds') }
 
 ---------------------------------------------------------------------------
 -- *   Exp
@@ -296,9 +307,12 @@ sectionR :: Quote m => m Exp -> m Exp -> m Exp
 sectionR x y = infixE Nothing x (Just y)
 
 lamE :: Quote m => [m Pat] -> m Exp -> m Exp
-lamE ps e = do ps' <- sequenceA ps
-               e' <- e
-               pure (LamE ps' e')
+lamE ps = lamArgE (fmap visAP ps)
+
+lamArgE  :: Quote m => [m ArgPat] -> m Exp -> m Exp
+lamArgE ps e = do ps' <- sequenceA ps
+                  e' <- e
+                  pure (LamE ps' e')
 
 -- | Single-arg lambda
 lam1E :: Quote m => m Pat -> m Exp -> m Exp
diff --git a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
index 39f7852d8f7297346f4a857bd32a159601fa6700..610728b8ef091d58a29a2f05cf4f33fb9b0352a2 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Ppr.hs
@@ -154,7 +154,7 @@ pprExp _ (InfixE me1 op me2) = parens $ pprMaybeExp noPrec me1
                                     <+> pprInfixExp op
                                     <+> pprMaybeExp noPrec me2
 pprExp i (LamE [] e) = pprExp i e -- #13856
-pprExp i (LamE ps e) = parensIf (i > noPrec) $ char '\\' <> hsep (map (pprPat appPrec) ps)
+pprExp i (LamE ps e) = parensIf (i > noPrec) $ char '\\' <> hsep (map (pprArgPat appPrec) ps)
                                            <+> text "->" <+> ppr e
 pprExp i (LamCaseE ms)
   = parensIf (i > noPrec) $ text "\\case" $$ braces (semiSep ms)
@@ -280,7 +280,7 @@ pprBody eq body = case body of
 ------------------------------
 pprClause :: Bool -> Clause -> Doc
 pprClause eqDoc (Clause ps rhs ds)
-  = hsep (map (pprPat appPrec) ps) <+> pprBody eqDoc rhs
+  = hsep (map (pprArgPat appPrec) ps) <+> pprBody eqDoc rhs
     $$ where_clause ds
 
 ------------------------------
@@ -388,6 +388,13 @@ pprPat i (SigP p t) = parensIf (i > noPrec) $ ppr p <+> dcolon <+> ppr t
 pprPat _ (ViewP e p) = parens $ pprExp noPrec e <+> text "->" <+> pprPat noPrec p
 pprPat _ (TypeP t) = parens $ text "type" <+> ppr t
 
+instance Ppr ArgPat where
+  ppr = pprArgPat noPrec
+
+pprArgPat :: Precedence -> ArgPat -> Doc
+pprArgPat i (VisAP pat) = pprPat i pat
+pprArgPat _ (InvisAP t) = parens $ text "@" <+> ppr t
+
 ------------------------------
 instance Ppr Dec where
     ppr = ppr_dec True
diff --git a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
index ccfe35f2ced83a8368a7e59629699224e9cf8284..4baeaf9f1364661c5db702c8c782a8aa501291cb 100644
--- a/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
+++ b/libraries/template-haskell/Language/Haskell/TH/Syntax.hs
@@ -2296,12 +2296,15 @@ data Pat
   | TypeP Type                      -- ^ @{ type p }@
   deriving( Show, Eq, Ord, Data, Generic )
 
+data ArgPat = VisAP Pat | InvisAP Type
+  deriving( Show, Eq, Ord, Data, Generic )
+
 type FieldPat = (Name,Pat)
 
 data Match = Match Pat Body [Dec] -- ^ @case e of { pat -> body where decs }@
     deriving( Show, Eq, Ord, Data, Generic )
 
-data Clause = Clause [Pat] Body [Dec]
+data Clause = Clause [ArgPat] Body [Dec]
                                   -- ^ @f { p1 p2 = body where decs }@
     deriving( Show, Eq, Ord, Data, Generic )
 
@@ -2330,7 +2333,7 @@ data Exp
   | ParensE Exp                        -- ^ @{ (e) }@
                                        --
                                        -- See "Language.Haskell.TH.Syntax#infix"
-  | LamE [Pat] Exp                     -- ^ @{ \\ p1 p2 -> e }@
+  | LamE [ArgPat] Exp                  -- ^ @{ \\ p1 p2 -> e }@
   | LamCaseE [Match]                   -- ^ @{ \\case m1; m2 }@
   | LamCasesE [Clause]                 -- ^ @{ \\cases m1; m2 }@
   | TupE [Maybe Exp]                   -- ^ @{ (e1,e2) }  @
diff --git a/libraries/template-haskell/changelog.md b/libraries/template-haskell/changelog.md
index 9c33cb7971fba2d5e970be1a67d20263cd4448b6..05bf14b30a1f93cc442a9c72c6a08526a67bab1b 100644
--- a/libraries/template-haskell/changelog.md
+++ b/libraries/template-haskell/changelog.md
@@ -10,6 +10,12 @@
 
   * Extend `Pragma` with `SCCP`.
 
+  * Added new data type `ArgPat` with two constructors: `VisAP` and `InvisAP`.
+    The first one corresponds to the common patterns, and the second one is a type
+    abstraction `@t`. Were introduced new functions `visAP` ans `invisAP`. Was
+    introduced new type alias `ArgPatQ`. Added new function `pprArgPat`. Constructors
+    `Clause` and `LamE`, now use `ArgPat` instead of `Pat`. New functions `clauseArg` and `lamArgE` were added, both of which accept `[m ArgPat]`. (Ghc Proposal #448).
+
 ## 2.21.0.0
 
   * Record fields now belong to separate `NameSpace`s, keyed by the parent of
diff --git a/testsuite/tests/ghc-api/T6145.hs b/testsuite/tests/ghc-api/T6145.hs
index 2b55c1267de60a0ee0e7f54ce9df4e02bc5789fc..9e3c93538064b062cc9353bef95cbe73ced837ea 100644
--- a/testsuite/tests/ghc-api/T6145.hs
+++ b/testsuite/tests/ghc-api/T6145.hs
@@ -41,8 +41,8 @@ main = do
         = not (isEmptyBag (filterBag isDataCon bs))
       isDataCon (L l (f@FunBind {}))
         | (MG _ (L _ (m:_))) <- fun_matches f,
-          ((L _ (c@ConPat{})):_)<-hsLMatchPats m,
-          (L l _)<-pat_con c
+          ((L _ ((VisPat _ (L _ c@ConPat{})))):_)<-hsLMatchPats m,
+          (L l _) <- pat_con c
         = isGoodSrcSpan (locA l) -- Check that the source location is a good one
       isDataCon _
         = False
diff --git a/testsuite/tests/ghci/scripts/T11098.stdout b/testsuite/tests/ghci/scripts/T11098.stdout
index 7ff13067685b3fdf8eeab8e9729405aceb18be9b..b53a47b117c7deccacf923ac19f16641a4f03d21 100644
--- a/testsuite/tests/ghci/scripts/T11098.stdout
+++ b/testsuite/tests/ghci/scripts/T11098.stdout
@@ -1,3 +1,3 @@
-[SigD foo_1 (AppT (AppT ArrowT (VarT a_0)) (VarT a_0)),FunD foo_1 [Clause [VarP x_2] (NormalB (VarE x_2)) []]]
-"[SigD foo_ (AppT (AppT ArrowT (VarT _a_)) (VarT _a_)),FunD foo_ [Clause [VarP x_] (NormalB (VarE x_)) []]]"
-[SigD foo_6 (ForallT [PlainTV _a_5 SpecifiedSpec] [] (AppT (AppT ArrowT (VarT _a_5)) (VarT _a_5))),FunD foo_6 [Clause [VarP x_7] (NormalB (VarE x_7)) []]]
+[SigD foo_1 (AppT (AppT ArrowT (VarT a_0)) (VarT a_0)),FunD foo_1 [Clause [VisAP (VarP x_2)] (NormalB (VarE x_2)) []]]
+"[SigD foo_ (AppT (AppT ArrowT (VarT _a_)) (VarT _a_)),FunD foo_ [Clause [VisAP (VarP x_)] (NormalB (VarE x_)) []]]"
+[SigD foo_6 (ForallT [PlainTV _a_5 SpecifiedSpec] [] (AppT (AppT ArrowT (VarT _a_5)) (VarT _a_5))),FunD foo_6 [Clause [VisAP (VarP x_7)] (NormalB (VarE x_7)) []]]
diff --git a/testsuite/tests/overloadedrecflds/should_compile/T22424.hs b/testsuite/tests/overloadedrecflds/should_compile/T22424.hs
index fc88f6a93d488c30377ad4cf50197047e00d4f6a..47b2d5f5950ab02946801f85c51b7676328b107a 100644
--- a/testsuite/tests/overloadedrecflds/should_compile/T22424.hs
+++ b/testsuite/tests/overloadedrecflds/should_compile/T22424.hs
@@ -22,7 +22,8 @@ $(do
     x1 <- newName "x1"
     x2 <- newName "x2"
     let expr = UInfixE (VarE fld1 `AppE` VarE x1) (VarE '(&&)) (VarE fld2 `AppE` VarE x2)
-        fun_decl = FunD fun [Clause [VarP x1, VarP x2] (NormalB expr) []]
+        pats = [VarP x1, VarP x2]
+        fun_decl = FunD fun [Clause (map VisAP pats) (NormalB expr) []]
     pure [r1,r2,fun_decl]
  )
 
@@ -35,6 +36,7 @@ $(do
     x1 <- newName "x1"
     x2 <- newName "x2"
     let expr = UInfixE (VarE fld1 `AppE` VarE x1) (VarE '(&&)) (VarE fld2 `AppE` VarE x2)
-        fun_decl = FunD fun [Clause [VarP x1, VarP x2] (NormalB expr) []]
+        pats = [VarP x1, VarP x2]
+        fun_decl = FunD fun [Clause (map VisAP pats) (NormalB expr) []]
     pure [r1,r2,fun_decl]
  )
diff --git a/testsuite/tests/parser/should_compile/DumpSemis.stderr b/testsuite/tests/parser/should_compile/DumpSemis.stderr
index c60897d6d2ae4f5d448bd7cae17f48e553ee09cc..a77e6247afb31fbb129bd3ad1f92055d67ed5abd 100644
--- a/testsuite/tests/parser/should_compile/DumpSemis.stderr
+++ b/testsuite/tests/parser/should_compile/DumpSemis.stderr
@@ -1673,17 +1673,26 @@
                [])
               (EpaComments
                []))
-             (VarPat
+             (VisPat
               (NoExtField)
               (L
                (EpAnn
                 (EpaSpan { DumpSemis.hs:32:3 })
-                (NameAnnTrailing
+                (AnnListItem
                  [])
                 (EpaComments
                  []))
-               (Unqual
-                {OccName: x}))))]
+               (VarPat
+                (NoExtField)
+                (L
+                 (EpAnn
+                  (EpaSpan { DumpSemis.hs:32:3 })
+                  (NameAnnTrailing
+                   [])
+                  (EpaComments
+                   []))
+                 (Unqual
+                  {OccName: x}))))))]
            (GRHSs
             (EpaComments
              [])
@@ -2103,17 +2112,26 @@
                [])
               (EpaComments
                []))
-             (VarPat
+             (VisPat
               (NoExtField)
               (L
                (EpAnn
                 (EpaSpan { DumpSemis.hs:36:5 })
-                (NameAnnTrailing
+                (AnnListItem
                  [])
                 (EpaComments
                  []))
-               (Unqual
-                {OccName: x}))))]
+               (VarPat
+                (NoExtField)
+                (L
+                 (EpAnn
+                  (EpaSpan { DumpSemis.hs:36:5 })
+                  (NameAnnTrailing
+                   [])
+                  (EpaComments
+                   []))
+                 (Unqual
+                  {OccName: x}))))))]
            (GRHSs
             (EpaComments
              [])
@@ -2198,23 +2216,32 @@
                           [])
                          (EpaComments
                           []))
-                        (NPat
-                         []
+                        (VisPat
+                         (NoExtField)
                          (L
                           (EpAnn
                            (EpaSpan { DumpSemis.hs:39:6 })
-                           (NoEpAnns)
+                           (AnnListItem
+                            [])
                            (EpaComments
                             []))
-                          (OverLit
-                           (NoExtField)
-                           (HsIntegral
-                            (IL
-                             (SourceText 0)
-                             (False)
-                             (0)))))
-                         (Nothing)
-                         (NoExtField)))]
+                          (NPat
+                           []
+                           (L
+                            (EpAnn
+                             (EpaSpan { DumpSemis.hs:39:6 })
+                             (NoEpAnns)
+                             (EpaComments
+                              []))
+                            (OverLit
+                             (NoExtField)
+                             (HsIntegral
+                              (IL
+                               (SourceText 0)
+                               (False)
+                               (0)))))
+                           (Nothing)
+                           (NoExtField)))))]
                       (GRHSs
                        (EpaComments
                         [])
@@ -2265,23 +2292,32 @@
                           [])
                          (EpaComments
                           []))
-                        (NPat
-                         []
+                        (VisPat
+                         (NoExtField)
                          (L
                           (EpAnn
                            (EpaSpan { DumpSemis.hs:40:6 })
-                           (NoEpAnns)
+                           (AnnListItem
+                            [])
                            (EpaComments
                             []))
-                          (OverLit
-                           (NoExtField)
-                           (HsIntegral
-                            (IL
-                             (SourceText 1)
-                             (False)
-                             (1)))))
-                         (Nothing)
-                         (NoExtField)))]
+                          (NPat
+                           []
+                           (L
+                            (EpAnn
+                             (EpaSpan { DumpSemis.hs:40:6 })
+                             (NoEpAnns)
+                             (EpaComments
+                              []))
+                            (OverLit
+                             (NoExtField)
+                             (HsIntegral
+                              (IL
+                               (SourceText 1)
+                               (False)
+                               (1)))))
+                           (Nothing)
+                           (NoExtField)))))]
                       (GRHSs
                        (EpaComments
                         [])
@@ -2334,23 +2370,32 @@
                           [])
                          (EpaComments
                           []))
-                        (NPat
-                         []
+                        (VisPat
+                         (NoExtField)
                          (L
                           (EpAnn
                            (EpaSpan { DumpSemis.hs:41:6 })
-                           (NoEpAnns)
+                           (AnnListItem
+                            [])
                            (EpaComments
                             []))
-                          (OverLit
-                           (NoExtField)
-                           (HsIntegral
-                            (IL
-                             (SourceText 2)
-                             (False)
-                             (2)))))
-                         (Nothing)
-                         (NoExtField)))]
+                          (NPat
+                           []
+                           (L
+                            (EpAnn
+                             (EpaSpan { DumpSemis.hs:41:6 })
+                             (NoEpAnns)
+                             (EpaComments
+                              []))
+                            (OverLit
+                             (NoExtField)
+                             (HsIntegral
+                              (IL
+                               (SourceText 2)
+                               (False)
+                               (2)))))
+                           (Nothing)
+                           (NoExtField)))))]
                       (GRHSs
                        (EpaComments
                         [])
@@ -2405,23 +2450,32 @@
                           [])
                          (EpaComments
                           []))
-                        (NPat
-                         []
+                        (VisPat
+                         (NoExtField)
                          (L
                           (EpAnn
                            (EpaSpan { DumpSemis.hs:42:6 })
-                           (NoEpAnns)
+                           (AnnListItem
+                            [])
                            (EpaComments
                             []))
-                          (OverLit
-                           (NoExtField)
-                           (HsIntegral
-                            (IL
-                             (SourceText 3)
-                             (False)
-                             (3)))))
-                         (Nothing)
-                         (NoExtField)))]
+                          (NPat
+                           []
+                           (L
+                            (EpAnn
+                             (EpaSpan { DumpSemis.hs:42:6 })
+                             (NoEpAnns)
+                             (EpaComments
+                              []))
+                            (OverLit
+                             (NoExtField)
+                             (HsIntegral
+                              (IL
+                               (SourceText 3)
+                               (False)
+                               (3)))))
+                           (Nothing)
+                           (NoExtField)))))]
                       (GRHSs
                        (EpaComments
                         [])
diff --git a/testsuite/tests/parser/should_compile/KindSigs.stderr b/testsuite/tests/parser/should_compile/KindSigs.stderr
index 0a47367548493ea37902bcb93df1193608004407..53d40e8919ede20f0b1431dde4bd69be00bbc226 100644
--- a/testsuite/tests/parser/should_compile/KindSigs.stderr
+++ b/testsuite/tests/parser/should_compile/KindSigs.stderr
@@ -954,8 +954,17 @@
                [])
               (EpaComments
                []))
-             (WildPat
-              (NoExtField)))
+             (VisPat
+              (NoExtField)
+              (L
+               (EpAnn
+                (EpaSpan { KindSigs.hs:23:5 })
+                (AnnListItem
+                 [])
+                (EpaComments
+                 []))
+               (WildPat
+                (NoExtField)))))
            ,(L
              (EpAnn
               (EpaSpan { KindSigs.hs:23:7 })
@@ -963,8 +972,17 @@
                [])
               (EpaComments
                []))
-             (WildPat
-              (NoExtField)))]
+             (VisPat
+              (NoExtField)
+              (L
+               (EpAnn
+                (EpaSpan { KindSigs.hs:23:7 })
+                (AnnListItem
+                 [])
+                (EpaComments
+                 []))
+               (WildPat
+                (NoExtField)))))]
            (GRHSs
             (EpaComments
              [])
diff --git a/testsuite/tests/parser/should_fail/T18251d.hs b/testsuite/tests/parser/should_fail/T18251d.hs
deleted file mode 100644
index 76864b6e728c02b7ded5362a085e89a3e8122d12..0000000000000000000000000000000000000000
--- a/testsuite/tests/parser/should_fail/T18251d.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-{-# LANGUAGE ExplicitForAll #-}
-
-module T18251d where
-
-f :: forall a. a -> ()
-f @a _ = ()
diff --git a/testsuite/tests/parser/should_fail/T18251d.stderr b/testsuite/tests/parser/should_fail/T18251d.stderr
deleted file mode 100644
index 61b535f9735ad2839a4d3b0f6d00ef744e60d8f0..0000000000000000000000000000000000000000
--- a/testsuite/tests/parser/should_fail/T18251d.stderr
+++ /dev/null
@@ -1,4 +0,0 @@
-
-T18251d.hs:6:1: error: [GHC-07626]
-    Parse error in pattern: f @a
-                              Type applications in patterns are only allowed on data constructors.
diff --git a/testsuite/tests/parser/should_fail/all.T b/testsuite/tests/parser/should_fail/all.T
index d72776725110d1519a1b3690e5da231e956e7aab..a442431bd8d6ba357407c47c14257063a327d792 100644
--- a/testsuite/tests/parser/should_fail/all.T
+++ b/testsuite/tests/parser/should_fail/all.T
@@ -170,7 +170,6 @@ test('T18130Fail', normal, compile_fail, [''])
 test('T18251a', normal, compile_fail, [''])
 test('T18251b', normal, compile_fail, [''])
 test('T18251c', normal, compile_fail, [''])
-test('T18251d', normal, compile_fail, [''])
 test('T18251e', normal, compile_fail, [''])
 test('T18251f', normal, compile_fail, [''])
 test('T12446', normal, compile_fail, [''])
diff --git a/testsuite/tests/rename/should_fail/T17594b.hs b/testsuite/tests/rename/should_fail/T17594b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..bd7efaad6509c2bb1a7d9285925ffd3dfb5f0cb8
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T17594b.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE ScopedTypeVariables, ImpredicativeTypes, TemplateHaskell, NoTypeAbstractions #-}
+module T17594b where
+
+import qualified Language.Haskell.TH as TH
+
+id1 :: forall a. a -> a
+id1 @t x = x
+
+id2 :: forall a. Bool -> a -> a
+id2 @t False x = x :: t
+id2 True x = x
+
+id3 :: a -> a
+id3 @t x = x :: t
+
+id4 :: forall a b c. a -> b -> c -> forall d e f. d -> e -> f -> (a, b, c, d, e, f)
+id4 @t1 @t2 @t3 x1 x2 x3 @t4 @t5 @t6 x4 x5 x6 = (x1 :: t1, x2 :: t2, x3 :: t3, x4 :: t4, x5 :: t5, x6 :: t6)
+
+id_r_N_t :: (forall a. a -> a) -> a -> a
+id_r_N_t @t f = f @t
+
+id5 = id_r_N_t (\ @t x -> x :: t)
+
+id6 :: forall a. a -> a
+id6 = \ @t x -> x :: t
+
+id7 :: forall a b c d e f. Int
+id7 @t1 @t2 = let _ = () in \ @t3 -> case () of () -> \ @t4 @t5 -> \ @t6 -> 42
+
+id8 :: (forall a. a -> a, forall a. a -> a)
+id8 = (\ @t x -> x, id1)
+
+id9 :: [forall a. a -> a]
+id9 = [\ @t x -> x, id1, id3, id5, id6, fst id8, snd id8]
+
+id10 :: a -> a
+id10 @($(TH.varT (TH.mkName "t"))) x = x :: t
diff --git a/testsuite/tests/rename/should_fail/T17594b.stderr b/testsuite/tests/rename/should_fail/T17594b.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..e74145f6f0a09ad42788bc0b9e58a36b7fd877fa
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T17594b.stderr
@@ -0,0 +1,84 @@
+
+T17594b.hs:7:6: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:10:6: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:14:6: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:6: error: [GHC-78249]
+    Illegal invisible type pattern: t1
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:10: error: [GHC-78249]
+    Illegal invisible type pattern: t2
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:14: error: [GHC-78249]
+    Illegal invisible type pattern: t3
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:27: error: [GHC-78249]
+    Illegal invisible type pattern: t4
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:31: error: [GHC-78249]
+    Illegal invisible type pattern: t5
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:17:35: error: [GHC-78249]
+    Illegal invisible type pattern: t6
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:20:11: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:22:20: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:25:10: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:6: error: [GHC-78249]
+    Illegal invisible type pattern: t1
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:10: error: [GHC-78249]
+    Illegal invisible type pattern: t2
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:32: error: [GHC-78249]
+    Illegal invisible type pattern: t3
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:58: error: [GHC-78249]
+    Illegal invisible type pattern: t4
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:62: error: [GHC-78249]
+    Illegal invisible type pattern: t5
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:28:71: error: [GHC-78249]
+    Illegal invisible type pattern: t6
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:31:11: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:34:11: error: [GHC-78249]
+    Illegal invisible type pattern: t
+    Suggested fix: Perhaps you intended to use TypeAbstractions
+
+T17594b.hs:37:7: error: [GHC-78249]
+    Illegal invisible type pattern: ($(TH.varT (TH.mkName "t")))
+    Suggested fix: Perhaps you intended to use TypeAbstractions
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 4991d618ab1faad24fe7df26b5a8c6e62e8dac29..038aa8c465fa89dfd38361a8238d79bb32e55bfa 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -223,4 +223,5 @@ test('T23740h', normal, compile_fail, [''])
 test('T23740i', req_th, compile_fail, [''])
 test('T23740j', normal, compile_fail, [''])
 test('T23570', [extra_files(['T23570_aux.hs'])], multimod_compile_fail, ['T23570', '-v0'])
-test('T23570b', [extra_files(['T23570_aux.hs'])], multimod_compile, ['T23570b', '-v0'])
\ No newline at end of file
+test('T23570b', [extra_files(['T23570_aux.hs'])], multimod_compile, ['T23570b', '-v0'])
+test('T17594b', req_th, compile_fail, [''])
diff --git a/testsuite/tests/showIface/DocsInHiFileTH.hs b/testsuite/tests/showIface/DocsInHiFileTH.hs
index 4186c6a8764458bcbc54fd684f57c59285ab8f2b..e9a76ad5b13ce97583a00a08b036dd85de463aa9 100644
--- a/testsuite/tests/showIface/DocsInHiFileTH.hs
+++ b/testsuite/tests/showIface/DocsInHiFileTH.hs
@@ -172,7 +172,7 @@ do
   let defBang = bang noSourceUnpackedness noSourceStrictness
   patSynVarName <- newName "a"
   sequenceA
-    [ funD_doc (mkName "qux") [clause [ [p| a |], [p| b |] ] (normalB [e| () |]) []]
+    [ funD_doc (mkName "qux") [clause [[p| a |], [p| b |] ] (normalB [e| () |]) []]
         (Just "This is qux") [Just "Arg uno", Just "Arg dos"]
 
     , dataD_doc (cxt []) (mkName "Quux") [] Nothing
diff --git a/testsuite/tests/th/T10945.hs b/testsuite/tests/th/T10945.hs
index d9a24663ab363cd808ffb05666c9514b2eb7d08e..4fdbc306ef98b1c6657dba93ca198315c5249c60 100644
--- a/testsuite/tests/th/T10945.hs
+++ b/testsuite/tests/th/T10945.hs
@@ -10,5 +10,5 @@ $$(return [
                  []
                  (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a"))))
  , FunD (mkName "m")
-        [Clause [VarP (mkName "x")] (NormalB (VarE (mkName "x"))) []]
+        [Clause [VisAP $ VarP (mkName "x")] (NormalB (VarE (mkName "x"))) []]
  ])
diff --git a/testsuite/tests/th/T3899a.hs b/testsuite/tests/th/T3899a.hs
index 1b5e7d69c1b83bf658394d423cae2aacedc075c4..5f5f96bf61642015a6a80616634a3777bd690432 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]))
+     return $ LamE [VisAP $ foldr (\v prev -> ParensP (ConP 'Cons [] [VarP v,prev]))
                        (ConP 'Nil [] []) xs]
                    (TupE $ map (Just . VarE) xs)
diff --git a/testsuite/tests/th/T5379.hs b/testsuite/tests/th/T5379.hs
index 47ec3e8f586b1af08a7f22e18886586e755be390..8e5ae7a6481cf26375b03ec38ba2df4934164f82 100644
--- a/testsuite/tests/th/T5379.hs
+++ b/testsuite/tests/th/T5379.hs
@@ -4,7 +4,7 @@ module Main where
 import Language.Haskell.TH
 
 $( [d| g = 0
-       h = $( return $ LamE [VarP (mkName "g")] (VarE 'g) ) |] )
+       h = $( return $ LamE [VisAP $ VarP (mkName "g")] (VarE 'g) ) |] )
          -- The 'g should bind to the g=0 definition
 
 -- Should print 0, not 1!
diff --git a/testsuite/tests/th/T5508.hs b/testsuite/tests/th/T5508.hs
index ee82e8ff9b871c7eec0f18b0c010360e2ca74ae7..cd0a4e0973c6c4c74d59185130b0966b76ef143e 100644
--- a/testsuite/tests/th/T5508.hs
+++ b/testsuite/tests/th/T5508.hs
@@ -5,5 +5,6 @@ module T5508 where
 import Language.Haskell.TH
 
 thb = $(do { let x = mkName "x"
-                 v = return (LamE [VarP x] $ VarE x)
+                 p = VarP x
+                 v = return (LamE [VisAP p] $ VarE x)
            ; [| $v . id |] })
diff --git a/testsuite/tests/th/T5508.stderr b/testsuite/tests/th/T5508.stderr
index 02fddac6c788df24c333a7ac2d93bbeada5862cc..138c3185fee13d094752b1241dc427ed1117df11 100644
--- a/testsuite/tests/th/T5508.stderr
+++ b/testsuite/tests/th/T5508.stderr
@@ -1,6 +1,7 @@
-T5508.hs:(7,8)-(9,29): Splicing expression
+T5508.hs:(7,8)-(10,29): Splicing expression
     do let x = mkName "x"
-           v = return (LamE [VarP x] $ VarE x)
+           p = VarP x
+           v = return (LamE [VisAP p] $ VarE x)
        [| $v . id |]
        pending(rn) [<spn, v>]
   ======>
diff --git a/testsuite/tests/th/T5700a.hs b/testsuite/tests/th/T5700a.hs
index 39d39b16a1b7b4397a55a2b581b8e1498de9493b..9a38535233e5432d5432c00d8b436b7b73bfbb1c 100644
--- a/testsuite/tests/th/T5700a.hs
+++ b/testsuite/tests/th/T5700a.hs
@@ -9,7 +9,7 @@ class C a where
 mkC :: Name -> Q [Dec]
 mkC n = return
   [InstanceD Nothing [] (AppT (ConT ''C) (ConT n))
-    [ FunD 'inlinable [Clause [WildP] (NormalB (ConE '())) []],
-      PragmaD (InlineP 'inlinable Inline FunLike AllPhases)    
-    ] 
+    [ FunD 'inlinable [Clause [VisAP WildP] (NormalB (ConE '())) []],
+      PragmaD (InlineP 'inlinable Inline FunLike AllPhases)
+    ]
   ]
diff --git a/testsuite/tests/th/T8625.stdout b/testsuite/tests/th/T8625.stdout
index 13e058d15ca4d7bcb2e92a871b5b7e6b7b0f353f..c21b979fac13a86214361941758d79d57663cb96 100644
--- a/testsuite/tests/th/T8625.stdout
+++ b/testsuite/tests/th/T8625.stdout
@@ -1,2 +1,2 @@
 [InstanceD Nothing [AppT (AppT EqualityT (VarT y_0)) (AppT (AppT ArrowT (VarT t_1)) (VarT t_1))] (AppT (ConT Ghci1.Member) (ConT GHC.Types.Bool)) []]
-[SigD f_4 (ForallT [] [AppT (AppT EqualityT (VarT y_2)) (AppT (AppT ArrowT (VarT t_3)) (VarT t_3))] (AppT (AppT ArrowT (VarT y_2)) (VarT t_3))),FunD f_4 [Clause [VarP x_5] (NormalB (VarE x_5)) []]]
+[SigD f_4 (ForallT [] [AppT (AppT EqualityT (VarT y_2)) (AppT (AppT ArrowT (VarT t_3)) (VarT t_3))] (AppT (AppT ArrowT (VarT y_2)) (VarT t_3))),FunD f_4 [Clause [VisAP (VarP x_5)] (NormalB (VarE x_5)) []]]
diff --git a/testsuite/tests/th/T8761.hs b/testsuite/tests/th/T8761.hs
index b8177ff3ee68e06f65067b2bcd27efb43e8f5654..d43a284a84dbabb9d1b87e9824cf5e2ea4c44b29 100644
--- a/testsuite/tests/th/T8761.hs
+++ b/testsuite/tests/th/T8761.hs
@@ -28,7 +28,7 @@ do
       [qx3,qy3,qz3] = map mkName ["qx3", "qy3", "qz3"]
       patP          = tupP [tupP [varP qx3, varP qy3], listP [varP qz3]]
       patE          = tupE [tupE [varE qx3, varE qy3], listE [varE qz3]]
-      cls           = clause [varP qx3, varP qy3, varP qz3] (normalB patE) []
+      cls           = clause ([varP qx3, varP qy3, varP qz3]) (normalB patE) []
       recordPat     = patSynD nm3 (recordPatSyn [qx3,qy3,qz3])
                         (explBidir [cls]) patP
 
diff --git a/testsuite/tests/th/T8761.stderr b/testsuite/tests/th/T8761.stderr
index 0817e4b7a6e41cdb6188aa7dc823a6bc98c397bf..2ebbc0587b555ebd52ba4ec141ea6c12e51e56cb 100644
--- a/testsuite/tests/th/T8761.stderr
+++ b/testsuite/tests/th/T8761.stderr
@@ -20,7 +20,7 @@ T8761.hs:(16,1)-(39,13): Splicing declarations
            [qx3, qy3, qz3] = map mkName ["qx3", "qy3", "qz3"]
            patP = tupP [tupP [varP qx3, varP qy3], listP [varP qz3]]
            patE = tupE [tupE [varE qx3, varE qy3], listE [varE qz3]]
-           cls = clause [varP qx3, varP qy3, varP qz3] (normalB patE) []
+           cls = clause ([varP qx3, varP qy3, varP qz3]) (normalB patE) []
            recordPat
              = patSynD nm3 (recordPatSyn [qx3, qy3, qz3]) (explBidir [cls]) patP
        pats <- sequence [prefixPat, infixPat, recordPat]
diff --git a/testsuite/tests/th/T9022.hs b/testsuite/tests/th/T9022.hs
index 9c676aa7d0cceab8f1d1a355bde8e65f8273b33c..8cf60ff943640d1fd54f662b8cc043b093939a09 100644
--- a/testsuite/tests/th/T9022.hs
+++ b/testsuite/tests/th/T9022.hs
@@ -16,5 +16,5 @@ foo = barD
        xName = mkName "x"
        returnVarE = VarE $ mkName "return"
        xVarE = VarE xName
-       manyArgs = map argP [0..9]
+       manyArgs = map (VisAP . argP) [0..9]
        argP n = VarP $ mkName $ "arg" ++ show n
diff --git a/testsuite/tests/th/TH_repPatSig_asserts.hs b/testsuite/tests/th/TH_repPatSig_asserts.hs
index c9ea09dc99de02a18e4e7d884bff1bc673c4bfb1..a99e0db4bab98ea2316dde366002e8f8af5f6c6b 100644
--- a/testsuite/tests/th/TH_repPatSig_asserts.hs
+++ b/testsuite/tests/th/TH_repPatSig_asserts.hs
@@ -7,7 +7,7 @@ assertFoo decsQ = do
   decs <- decsQ
   case decs of
     [ SigD _ (AppT (AppT ArrowT (ConT t1)) (ConT t2)),
-      FunD _ [Clause [SigP (VarP _) (ConT t3)] (NormalB (VarE _)) []] ]
+      FunD _ [Clause [VisAP (SigP (VarP _) (ConT t3))] (NormalB (VarE _)) []] ]
       | t1 == ''Int && t2 == ''Int && t3 == ''Int -> return []
     _  -> do reportError $ "Unexpected quote contents: " ++ show decs
              return []
@@ -16,11 +16,11 @@ assertCon :: Q Exp -> Q [Dec]
 assertCon expQ = do
   exp <- expQ
   case exp of
-    LamE [SigP (VarP _) (AppT (AppT ArrowT (AppT (AppT (ConT eitherT)
+    LamE [VisAP (SigP (VarP _) (AppT (AppT ArrowT (AppT (AppT (ConT eitherT)
                                                        (ConT charT1))
                                                  (ConT intT1)))
                               (AppT (AppT (TupleT 2) (ConT charT2))
-                                    (ConT intT2)))]
+                                    (ConT intT2))))]
          (VarE _)
       | eitherT == ''Either &&
         charT1 == ''Char &&
@@ -34,7 +34,7 @@ assertVar :: Q Exp -> Q [Dec]
 assertVar expQ = do
   exp <- expQ
   case exp of
-    LamE [SigP (VarP x) (AppT (ConT _) (VarT a))]
+    LamE [VisAP (SigP (VarP x) (AppT (ConT _) (VarT a)))]
          (CaseE (VarE x1) [Match (ConP _ [] [VarP y])
                                  (NormalB (SigE (VarE y1) (VarT a1))) []])
       | x1 == x &&
diff --git a/testsuite/tests/th/TH_spliceD1_Lib.hs b/testsuite/tests/th/TH_spliceD1_Lib.hs
index 47ffa4e4e672bd8b239d66b620389830f8300416..6d5b01ee10dff35ecf457ce0acbb502b628f0ac6 100644
--- a/testsuite/tests/th/TH_spliceD1_Lib.hs
+++ b/testsuite/tests/th/TH_spliceD1_Lib.hs
@@ -7,7 +7,7 @@ foo :: Q [Dec]
 foo = sequence [funD (mkName "f")
        [
          clause
-           [varP $ mkName "c",varP $ mkName "c"]
+           ([varP $ mkName "c",varP $ mkName "c"])
            (normalB $ [| undefined |])
            []
        ]]
diff --git a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
index 095d71c63838dd6b251960cd4c61ceb3b27b5113..80a82498374e49f73bdbee5a880d0533db027073 100644
--- a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
+++ b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
@@ -1,5 +1,5 @@
 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))))
+LamE [VisAP (VarP x)] (InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2))))
 [DataD [] Foo [] Nothing [NormalC Foo []] []]
 ConP GHC.Tuple.Prim.() [] []
 AppT ListT (ConT GHC.Types.Int)
diff --git a/testsuite/tests/typecheck/should_compile/T17594a.hs b/testsuite/tests/typecheck/should_compile/T17594a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..54b4bdd5064a3ac5978430b593ff323cecfbf4eb
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17594a.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE ScopedTypeVariables, ImpredicativeTypes, TemplateHaskell, LambdaCase, TypeAbstractions, BlockArguments #-}
+module T17594a where
+
+import qualified Language.Haskell.TH as TH
+
+id1 :: forall a. a -> a
+id1 @t x = x
+
+id2 :: forall a. Bool -> a -> a
+id2 @t False x = x :: t
+id2 True x = x
+
+id3 :: a -> a
+id3 @t x = x :: t
+
+id4 :: forall a b c. a -> b -> c -> forall d e f. d -> e -> f -> (a, b, c, d, e, f)
+id4 @t1 @t2 @t3 x1 x2 x3 @t4 @t5 @t6 x4 x5 x6 = (x1 :: t1, x2 :: t2, x3 :: t3, x4 :: t4, x5 :: t5, x6 :: t6)
+
+id5 :: (forall a. a -> a, forall a. a -> a)
+id5 = (\ @t x -> x, id1)
+
+id6 :: [forall a. a -> a]
+id6 = [\ @t x -> x, id1, id3, fst id5, snd id5, id8]
+
+id7 :: a -> a
+id7 @($(TH.varT (TH.mkName "t"))) x = x :: t
+
+id_r_N_t :: (forall a. Bool -> a -> a) -> a -> a
+id_r_N_t @t f = f @t False
+
+id8 = id_r_N_t (\ @t _ x -> x :: t)
+
+id9 :: forall a. a -> a
+id9 = id_r_N_t \cases
+  @t True x -> x :: t
+  False x -> x
diff --git a/testsuite/tests/typecheck/should_compile/T17594f.hs b/testsuite/tests/typecheck/should_compile/T17594f.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3a462fc0c8894a1f69a13e9e34d5559128d734c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17594f.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TypeFamilies,
+             BlockArguments,
+             QualifiedDo,
+             DataKinds,
+             RequiredTypeArguments,
+             ImpredicativeTypes,
+             TypeAbstractions #-}
+
+module Main where
+
+import Data.Kind
+
+-- This test case collects ALL recent features
+
+main :: IO ()
+main = demo False
+
+demo :: Bool -> IO ()
+demo b = Main.do -- this do-notation doesn't work without recent patch that expands HsDo at renamer
+  x <- doubleOrInt b -- doesn't check without impredicative types
+  let v = x + 1
+  print v
+
+(>>=) = ($)
+
+doubleOrInt ::  Bool -> forall r. (forall a. (Num a, Show a) => a -> r) -> r
+doubleOrInt True  f = wrap [Num, Show] @Double 4.15 \ @a -> f -- hack to convert (Num a, (Show a, ())) into (Num a, Show a)
+doubleOrInt False f = f @Int 14 -- but you can simply use `f`
+
+-- This function without RequiredTypeArguments would have ambiguous type
+wrap :: forall c -> forall a. Constraints c a => a -> (forall a. Constraints c a => a -> r) -> r
+wrap _ a f = f a
+
+type Constraints :: [Type -> Constraint] -> Type -> Constraint
+type family Constraints c a where
+ Constraints '[] _ = ()
+ Constraints (c : cs) a = (c a, Constraints cs a)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c5f0e08ec171fa86c6b43ef26a7548e4d7285985..a2f4b3ea7521f21b17c118612f881df346cd4b6f 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -908,4 +908,6 @@ test('T23918', normal, compile, [''])
 test('T17564', normal, compile, [''])
 test('T24146', normal, compile, [''])
 test('T22788', normal, compile, [''])
-test('T21206', normal, compile, [''])
\ No newline at end of file
+test('T21206', normal, compile, [''])
+test('T17594a', req_th, compile, [''])
+test('T17594f', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T17594c.hs b/testsuite/tests/typecheck/should_fail/T17594c.hs
new file mode 100644
index 0000000000000000000000000000000000000000..5ebf0a2354fe5d3f177d503a8ca8137e20bc0003
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594c.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeAbstractions #-}
+module T17594c where
+
+id' :: forall a. [a]
+id' = [\ @t -> undefined :: t]
diff --git a/testsuite/tests/typecheck/should_fail/T17594c.stderr b/testsuite/tests/typecheck/should_fail/T17594c.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..878f9393558dd6cd6312885551b05b9a30995a94
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594c.stderr
@@ -0,0 +1,6 @@
+
+T17594c.hs:5:11: error: [GHC-14964]
+    • Invisible type pattern t has no associated forall
+    • In the expression: \ @t -> undefined :: t
+      In the expression: [\ @t -> undefined :: t]
+      In an equation for ‘id'’: id' = [\ @t -> undefined :: t]
diff --git a/testsuite/tests/typecheck/should_fail/T17594d.hs b/testsuite/tests/typecheck/should_fail/T17594d.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3f55fef38883f44b05d907c80e30c4a4a9af89dd
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594d.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeAbstractions #-}
+
+module T17594d where
+
+-- We want this code to check, but currently it doesn't
+-- because inference mode for type abstractions is not
+-- implemented yet
+id' @t x = x :: t
diff --git a/testsuite/tests/typecheck/should_fail/T17594d.stderr b/testsuite/tests/typecheck/should_fail/T17594d.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..c9917d917659f671d046f166081e5f3178d7ef5a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594d.stderr
@@ -0,0 +1,4 @@
+
+T17594d.hs:8:6: error: [GHC-14964]
+    • Invisible type pattern t has no associated forall
+    • In an equation for ‘id'’: id' @t x = x :: t
diff --git a/testsuite/tests/typecheck/should_fail/T17594g.hs b/testsuite/tests/typecheck/should_fail/T17594g.hs
new file mode 100644
index 0000000000000000000000000000000000000000..122a93ff3ac2323e0760226cfdca7e60edd3d858
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594g.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeAbstractions #-}
+
+module T17594g where
+
+id' :: forall {a}. a -> a
+id' @a x = x
diff --git a/testsuite/tests/typecheck/should_fail/T17594g.stderr b/testsuite/tests/typecheck/should_fail/T17594g.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..f070c722215e542eb87dcf53acdb40912466b4d0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17594g.stderr
@@ -0,0 +1,4 @@
+
+T17594g.hs:6:6: error: [GHC-14964]
+    • Invisible type pattern a has no associated forall
+    • In an equation for ‘id'’: id' @a x = x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4268a9b7f36d18a63ca3f2828675967ae2577785..6aa934348f51346990c9c20b5ecf242b75bed999 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -717,3 +717,7 @@ test('T24279', normal, compile_fail, [''])
 test('DoExpansion1', normal, compile, ['-fdefer-type-errors'])
 test('DoExpansion2', normal, compile, ['-fdefer-type-errors'])
 test('DoExpansion3', normal, compile, ['-fdefer-type-errors'])
+
+test('T17594c', normal, compile_fail, [''])
+test('T17594d', normal, compile_fail, [''])
+test('T17594g', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_run/T17594e.hs b/testsuite/tests/typecheck/should_run/T17594e.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f4647e5abc7b11ccb7a018896491c82689ba14de
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T17594e.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeAbstractions #-}
+
+import Data.Int
+
+higherRank :: (forall a. (Num a, Bounded a) => a -> a) -> (Int8, Int16)
+higherRank f = (f 42, f 42)
+
+ex :: (Int8, Int16)
+ex = higherRank (\ @a x -> maxBound @a - x )
+
+main = print ex
diff --git a/testsuite/tests/typecheck/should_run/T17594e.stdout b/testsuite/tests/typecheck/should_run/T17594e.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..c56709ee1cdeb02ac1d02be69dad25b5cdec9981
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/T17594e.stdout
@@ -0,0 +1 @@
+(85,32725)
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index 5d33c00809fc5fea5a3de5cf50c780f9571a6a70..4e189e0adb8e0188e862c420f31dd459164baddc 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -171,6 +171,7 @@ test('T21973a', [exit_code(1)], compile_and_run, [''])
 test('T21973b', normal, compile_and_run, [''])
 test('T23761', normal, compile_and_run, [''])
 test('T23761b', normal, compile_and_run, [''])
+test('T17594e', normal, compile_and_run, [''])
 
 # Tests for expanding do before typechecking (Impredicative + RebindableSyntax)
 test('T18324', normal, compile_and_run, [''])
diff --git a/utils/check-exact/ExactPrint.hs b/utils/check-exact/ExactPrint.hs
index 7db4c4c77c05814921ea215baa14ad220c3c751b..00072fc3dc5105e3d29304cc64dd01366ebbb8e3 100644
--- a/utils/check-exact/ExactPrint.hs
+++ b/utils/check-exact/ExactPrint.hs
@@ -4733,6 +4733,24 @@ instance ExactPrint (Pat GhcPs) where
 
 -- ---------------------------------------------------------------------
 
+instance ExactPrint (ArgPat GhcPs) where
+  getAnnotationEntry (VisPat _ pat) = getAnnotationEntry pat
+  getAnnotationEntry InvisPat{}     = NoEntryVal
+
+  setAnnotationAnchor (VisPat x pat) anc ts cs = VisPat x (setAnnotationAnchor pat anc ts cs)
+  setAnnotationAnchor a@(InvisPat _ _) _ _ _   = a
+
+  exact (VisPat x pat) = do
+    pat' <- markAnnotated pat
+    pure (VisPat x pat')
+
+  exact (InvisPat tokat tp) = do
+    tokat' <- markEpToken tokat
+    tp' <- markAnnotated tp
+    pure (InvisPat tokat' tp')
+
+-- ---------------------------------------------------------------------
+
 instance ExactPrint (HsPatSigType GhcPs) where
   getAnnotationEntry = const NoEntryVal
   setAnnotationAnchor a _ _ _ = a