From 0dbd729e211da80d640a30be164d365547c75f99 Mon Sep 17 00:00:00 2001
From: Andrei Borzenkov <andreyborzenkov2002@gmail.com>
Date: Wed, 16 Aug 2023 18:41:18 +0400
Subject: [PATCH] Parser, renamer, type checker for @a-binders (#17594)

GHC Proposal 448 introduces binders for invisible type arguments
(@a-binders) in various contexts. This patch implements @-binders
in lambda patterns and function equations:

  {-# LANGUAGE TypeAbstractions #-}

  id1 :: a -> a
  id1 @t x = x :: t      -- @t-binder on the LHS of a function equation

  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

Syntax
------

To represent those @-binders in the AST, the list of patterns in Match
now uses ArgPat instead of Pat:

  data Match p body
     = Match {
         ...
-        m_pats  :: [LPat p],
+        m_pats  :: [LArgPat p],
         ...
   }

+ data ArgPat pass
+   = VisPat (XVisPat pass) (LPat pass)
+   | InvisPat (XInvisPat pass) (HsTyPat (NoGhcTc pass))
+   | XArgPat !(XXArgPat pass)

The VisPat constructor represents patterns for visible arguments,
which include ordinary value-level arguments and required type arguments
(neither is prefixed with a @), while InvisPat represents invisible type
arguments (prefixed with a @).

Parser
------

In the grammar (Parser.y), the lambda and lambda-cases productions of
aexp non-terminal were updated to accept argpats instead of apats:

  aexp : ...
-        | '\\' apats '->' exp
+        | '\\' argpats '->' exp
         ...
-        | '\\' 'lcases' altslist(apats)
+        | '\\' 'lcases' altslist(argpats)
         ...

+ argpat : apat
+        | PREFIX_AT atype

Function left-hand sides did not require any changes to the grammar, as
they were already parsed with productions capable of parsing @-binders.
Those binders were being rejected in post-processing (isFunLhs), and now
we accept them.

In Parser.PostProcess, patterns are constructed with the help of
PatBuilder, which is used as an intermediate data structure when
disambiguating between FunBind and PatBind. In this patch we define
ArgPatBuilder to accompany PatBuilder. ArgPatBuilder is a short-lived
data structure produced in isFunLhs and consumed in checkFunBind.

Renamer
-------

Renaming of @-binders builds upon prior work on type patterns,
implemented in 2afbddb0f24, which guarantees proper scoping and
shadowing behavior of bound type variables.

This patch merely defines rnLArgPatsAndThen to process a mix of visible
and invisible patterns:

+ rnLArgPatsAndThen :: NameMaker -> [LArgPat GhcPs] -> CpsRn [LArgPat GhcRn]
+ rnLArgPatsAndThen mk = mapM (wrapSrcSpanCps rnArgPatAndThen) where
+   rnArgPatAndThen (VisPat x p)    = ... rnLPatAndThen ...
+   rnArgPatAndThen (InvisPat _ tp) = ... rnHsTyPat ...

Common logic between rnArgPats and rnPats is factored out into the
rn_pats_general helper.

Type checker
------------

Type-checking of @-binders builds upon prior work on lazy skolemisation,
implemented in f5d3e03c56f.

This patch extends tcMatchPats to handle @-binders. Now it takes and
returns a list of LArgPat rather than LPat:

  tcMatchPats ::
              ...
-             -> [LPat GhcRn]
+             -> [LArgPat GhcRn]
              ...
-             -> TcM ([LPat GhcTc], a)
+             -> TcM ([LArgPat GhcTc], a)

Invisible binders in the Match are matched up with invisible (Specified)
foralls in the type. This is done with a new clause in the `loop` worker
of tcMatchPats:

  loop :: [LArgPat GhcRn] -> [ExpPatType] -> TcM ([LArgPat GhcTc], a)
  loop (L l apat : pats) (ExpForAllPatTy (Bndr tv vis) : pat_tys)
    ...
    -- NEW CLAUSE:
    | InvisPat _ tp <- apat, isSpecifiedForAllTyFlag vis
    = ...

In addition to that, tcMatchPats no longer discards type patterns. This
is done by filterOutErasedPats in the desugarer instead.

x86_64-linux-deb10-validate+debug_info
Metric Increase:
    MultiLayerModulesTH_OneShot
---
 compiler/GHC/Builtin/Names/TH.hs              |  43 +++--
 compiler/GHC/Hs/Expr.hs                       |  13 +-
 compiler/GHC/Hs/Instances.hs                  |   5 +
 compiler/GHC/Hs/Pat.hs                        | 124 ++++++++++++-
 compiler/GHC/Hs/Utils.hs                      |  59 ++++++-
 compiler/GHC/HsToCore/Arrows.hs               |   4 +-
 compiler/GHC/HsToCore/Expr.hs                 |   4 +-
 compiler/GHC/HsToCore/Match.hs                |  10 +-
 compiler/GHC/HsToCore/Pmc/Desugar.hs          |   5 +-
 compiler/GHC/HsToCore/Quote.hs                |  35 ++--
 compiler/GHC/HsToCore/Ticks.hs                |   4 +-
 compiler/GHC/HsToCore/Utils.hs                |  32 +++-
 compiler/GHC/Iface/Ext/Ast.hs                 |  17 +-
 compiler/GHC/Parser.y                         |  20 ++-
 compiler/GHC/Parser/PostProcess.hs            |  66 ++++---
 compiler/GHC/Rename/Bind.hs                   |   2 +-
 compiler/GHC/Rename/HsType.hs                 |   4 +-
 compiler/GHC/Rename/Pat.hs                    |  92 ++++++----
 compiler/GHC/Rename/Utils.hs                  |  10 +-
 compiler/GHC/Tc/Deriv/Functor.hs              |   6 +-
 compiler/GHC/Tc/Deriv/Generate.hs             |  53 +++---
 compiler/GHC/Tc/Errors/Ppr.hs                 |  14 ++
 compiler/GHC/Tc/Errors/Types.hs               |  29 ++-
 compiler/GHC/Tc/Gen/App.hs                    |  27 ++-
 compiler/GHC/Tc/Gen/Do.hs                     |  16 +-
 compiler/GHC/Tc/Gen/Match.hs                  |   3 +-
 compiler/GHC/Tc/Gen/Pat.hs                    |  64 ++++---
 compiler/GHC/Tc/TyCl/PatSyn.hs                |   9 +-
 compiler/GHC/Tc/Zonk/Type.hs                  |  14 +-
 compiler/GHC/ThToHs.hs                        |  24 ++-
 compiler/GHC/Types/Error/Codes.hs             |   2 +
 compiler/GHC/Types/Var.hs                     |   6 +
 compiler/Language/Haskell/Syntax/Expr.hs      |   2 +-
 compiler/Language/Haskell/Syntax/Extension.hs |   8 +
 compiler/Language/Haskell/Syntax/Pat.hs       |  27 ++-
 docs/users_guide/exts/type_abstractions.rst   | 101 +++++++++++
 libraries/ghci/GHCi/TH/Binary.hs              |   1 +
 .../template-haskell/Language/Haskell/TH.hs   |   2 +-
 .../Language/Haskell/TH/Lib.hs                |   5 +-
 .../Language/Haskell/TH/Lib/Internal.hs       |  28 ++-
 .../Language/Haskell/TH/Ppr.hs                |  11 +-
 .../Language/Haskell/TH/Syntax.hs             |   7 +-
 libraries/template-haskell/changelog.md       |   6 +
 testsuite/tests/ghc-api/T6145.hs              |   4 +-
 testsuite/tests/ghci/scripts/T11098.stdout    |   6 +-
 .../should_compile/T22424.hs                  |   6 +-
 .../parser/should_compile/DumpSemis.stderr    | 166 ++++++++++++------
 .../parser/should_compile/KindSigs.stderr     |  26 ++-
 testsuite/tests/parser/should_fail/T18251d.hs |   6 -
 .../tests/parser/should_fail/T18251d.stderr   |   4 -
 testsuite/tests/parser/should_fail/all.T      |   1 -
 testsuite/tests/rename/should_fail/T17594b.hs |  37 ++++
 .../tests/rename/should_fail/T17594b.stderr   |  84 +++++++++
 testsuite/tests/rename/should_fail/all.T      |   3 +-
 testsuite/tests/showIface/DocsInHiFileTH.hs   |   2 +-
 testsuite/tests/th/T10945.hs                  |   2 +-
 testsuite/tests/th/T3899a.hs                  |   2 +-
 testsuite/tests/th/T5379.hs                   |   2 +-
 testsuite/tests/th/T5508.hs                   |   3 +-
 testsuite/tests/th/T5508.stderr               |   5 +-
 testsuite/tests/th/T5700a.hs                  |   6 +-
 testsuite/tests/th/T8625.stdout               |   2 +-
 testsuite/tests/th/T8761.hs                   |   2 +-
 testsuite/tests/th/T8761.stderr               |   2 +-
 testsuite/tests/th/T9022.hs                   |   2 +-
 testsuite/tests/th/TH_repPatSig_asserts.hs    |   8 +-
 testsuite/tests/th/TH_spliceD1_Lib.hs         |   2 +-
 .../overloaded/TH_overloaded_extract.stdout   |   2 +-
 .../tests/typecheck/should_compile/T17594a.hs |  36 ++++
 .../tests/typecheck/should_compile/T17594f.hs |  37 ++++
 .../tests/typecheck/should_compile/all.T      |   4 +-
 .../tests/typecheck/should_fail/T17594c.hs    |   5 +
 .../typecheck/should_fail/T17594c.stderr      |   6 +
 .../tests/typecheck/should_fail/T17594d.hs    |   8 +
 .../typecheck/should_fail/T17594d.stderr      |   4 +
 .../tests/typecheck/should_fail/T17594g.hs    |   6 +
 .../typecheck/should_fail/T17594g.stderr      |   4 +
 testsuite/tests/typecheck/should_fail/all.T   |   4 +
 .../tests/typecheck/should_run/T17594e.hs     |  11 ++
 .../tests/typecheck/should_run/T17594e.stdout |   1 +
 testsuite/tests/typecheck/should_run/all.T    |   1 +
 utils/check-exact/ExactPrint.hs               |  18 ++
 82 files changed, 1224 insertions(+), 320 deletions(-)
 delete mode 100644 testsuite/tests/parser/should_fail/T18251d.hs
 delete mode 100644 testsuite/tests/parser/should_fail/T18251d.stderr
 create mode 100644 testsuite/tests/rename/should_fail/T17594b.hs
 create mode 100644 testsuite/tests/rename/should_fail/T17594b.stderr
 create mode 100644 testsuite/tests/typecheck/should_compile/T17594a.hs
 create mode 100644 testsuite/tests/typecheck/should_compile/T17594f.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594c.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594c.stderr
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594d.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594d.stderr
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594g.hs
 create mode 100644 testsuite/tests/typecheck/should_fail/T17594g.stderr
 create mode 100644 testsuite/tests/typecheck/should_run/T17594e.hs
 create mode 100644 testsuite/tests/typecheck/should_run/T17594e.stdout

diff --git a/compiler/GHC/Builtin/Names/TH.hs b/compiler/GHC/Builtin/Names/TH.hs
index 0ea14689274b..af9ef6c9529a 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 f2c489396f82..5561dad9c05b 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 4917e18a85dd..23747fe7dc50 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 cedc2adaeb2f..4c2ddd220e44 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 8e3cb7da4bed..347f7c9a130f 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 65a13d3f37e4..ad53694c0686 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 a0c211552848..8b01f64d6ecc 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 f75d73790f8a..0a5b45e08282 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 e7b977556318..05e3e2e61826 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 97075c0c47cb..90530e28a3c4 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 5c93f9dbebed..13ee946d6e8e 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 eb87b024456d..95d7de7149f1 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 11bf27223885..09cc0dfef19a 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 3c7fcb98709d..01eea6721f42 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 5725fd13bcca..f27bc529c94b 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 a47b5a06b330..12edfa5087f6 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 fd169a7e0b42..0261e1da09fc 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 5665c282b9eb..6c4c3bf4f51f 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 1c827a06d625..4012b55365eb 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 2503cc5c2960..9af48ec300b2 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 0cc3ac1f71f4..852fa0e86be4 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 e4ec0325ecde..a068e9394c04 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 c855e6d3dc58..e1a4ff1c3d1e 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 6b22d6618759..2c0576fd661e 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 eac8687b0113..41079067115b 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 fbc925168991..a4b681e7bab1 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 2c22abb29f82..9ec72d27ac1f 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 714719deaa5c..18547b390957 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 3cee66490243..90de9bb4abc2 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 d2ae5f8085a8..6903e2093d91 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 79f5b9d07c42..d50de9c4057c 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 e8f37261f99c..a6ea226e8643 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 f77d2a283a3e..b7b948682fa7 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 82edc341f2c4..3f43bec40d6b 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 a876df97f821..d6f567071591 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 67f4c0823530..1b55c2b60257 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 6d5447e32965..fd4146b4d470 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 22f434d4e53f..16c8eb561f77 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 88d6baa7954c..3ddd3ba757c3 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 49dd55bdbb7d..ea9875b835d3 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 39f7852d8f72..610728b8ef09 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 ccfe35f2ced8..4baeaf9f1364 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 9c33cb7971fb..05bf14b30a1f 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 2b55c1267de6..9e3c93538064 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 7ff13067685b..b53a47b117c7 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 fc88f6a93d48..47b2d5f5950a 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 c60897d6d2ae..a77e6247afb3 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 0a4736754849..53d40e8919ed 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 76864b6e728c..000000000000
--- 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 61b535f9735a..000000000000
--- 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 d72776725110..a442431bd8d6 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 000000000000..bd7efaad6509
--- /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 000000000000..e74145f6f0a0
--- /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 4991d618ab1f..038aa8c465fa 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 4186c6a87644..e9a76ad5b13c 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 d9a24663ab36..4fdbc306ef98 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 1b5e7d69c1b8..5f5f96bf6164 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 47ec3e8f586b..8e5ae7a6481c 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 ee82e8ff9b87..cd0a4e0973c6 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 02fddac6c788..138c3185fee1 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 39d39b16a1b7..9a38535233e5 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 13e058d15ca4..c21b979fac13 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 b8177ff3ee68..d43a284a84db 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 0817e4b7a6e4..2ebbc0587b55 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 9c676aa7d0cc..8cf60ff94364 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 c9ea09dc99de..a99e0db4bab9 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 47ffa4e4e672..6d5b01ee10df 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 095d71c63838..80a82498374e 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 000000000000..54b4bdd5064a
--- /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 000000000000..3a462fc0c889
--- /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 c5f0e08ec171..a2f4b3ea7521 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 000000000000..5ebf0a2354fe
--- /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 000000000000..878f9393558d
--- /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 000000000000..3f55fef38883
--- /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 000000000000..c9917d917659
--- /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 000000000000..122a93ff3ac2
--- /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 000000000000..f070c722215e
--- /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 4268a9b7f36d..6aa934348f51 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 000000000000..f4647e5abc7b
--- /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 000000000000..c56709ee1cde
--- /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 5d33c00809fc..4e189e0adb8e 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 7db4c4c77c05..00072fc3dc51 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
-- 
GitLab