Implement type applications in patterns

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

48 files changed, 450 insertions, 13 deletions

diff --git a/testsuite/tests/hiefile/should_compile/Scopes.hs b/testsuite/tests/hiefile/should_compile/Scopes.hs
index f8a76298bb..21766c6446 100644
--- a/testsuite/tests/hiefile/should_compile/Scopes.hs
+++ b/testsuite/tests/hiefile/should_compile/Scopes.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE PatternSynonyms, ViewPatterns #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
 module Scopes where
 
 -- Verify that evidence bound by patern
diff --git a/testsuite/tests/hiefile/should_compile/ScopesBug.hs b/testsuite/tests/hiefile/should_compile/ScopesBug.hs
new file mode 100644
index 0000000000..ea87d308d4
--- /dev/null
+++ b/testsuite/tests/hiefile/should_compile/ScopesBug.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
+module ScopesBug where
+
+data Proxy (a :: k) = Proxy
+data Con k (a :: k) = Con (Proxy a)
+
+tyApp :: Con k a -> Proxy a
+tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
diff --git a/testsuite/tests/hiefile/should_compile/all.T b/testsuite/tests/hiefile/should_compile/all.T
index 489cff28d0..86fbd6e20f 100644
--- a/testsuite/tests/hiefile/should_compile/all.T
+++ b/testsuite/tests/hiefile/should_compile/all.T
@@ -19,3 +19,5 @@ test('hie010',       normal,                   compile, ['-fno-code -fwrite-ide-
 test('CPP',          normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
 test('Constructors', normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
 test('Scopes',       normal,                   compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
+# See https://gitlab.haskell.org/ghc/ghc/-/issues/18425 and https://gitlab.haskell.org/ghc/ghc/-/merge_requests/2464#note_301989
+test('ScopesBug',    expect_broken(18425),     compile, ['-fno-code -fwrite-ide-info -fvalidate-ide-info'])
\ No newline at end of file
diff --git a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
index 31f8b10c25..262d01fc4f 100644
--- a/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpParsedAst.stderr
@@ -52,6 +52,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [])
           (Nothing)))
        ,({ DumpParsedAst.hs:7:21-30 }
@@ -65,6 +66,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [(HsScaled
              (HsLinearArrow
               (NormalSyntax))
@@ -256,6 +258,7 @@
           []
           (Nothing)
           (PrefixCon
+           []
            [(HsScaled
              (HsLinearArrow
               (NormalSyntax))
diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
index 29377597ae..61c89188c2 100644
--- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
+++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr
@@ -87,6 +87,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [])
             (Nothing)))
          ,({ DumpRenamedAst.hs:9:21-30 }
@@ -99,6 +100,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
@@ -500,6 +502,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
diff --git a/testsuite/tests/parser/should_compile/T14189.stderr b/testsuite/tests/parser/should_compile/T14189.stderr
index 32ae85e4dc..52f2099d6e 100644
--- a/testsuite/tests/parser/should_compile/T14189.stderr
+++ b/testsuite/tests/parser/should_compile/T14189.stderr
@@ -41,6 +41,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [(HsScaled
                (HsLinearArrow
                 (NormalSyntax))
@@ -61,6 +62,7 @@
             []
             (Nothing)
             (PrefixCon
+             []
              [])
             (Nothing)))
          ,({ T14189.hs:6:29-42 }
diff --git a/testsuite/tests/parser/should_fail/T18251d.stderr b/testsuite/tests/parser/should_fail/T18251d.stderr
index 4e64922070..15825502e0 100644
--- a/testsuite/tests/parser/should_fail/T18251d.stderr
+++ b/testsuite/tests/parser/should_fail/T18251d.stderr
@@ -1,3 +1,4 @@
 
 T18251d.hs:6:1: error:
-    Type applications in patterns are not yet supported
+    Parse error in pattern: f @a
+    Type applications in patterns are only allowed on data constructors.
diff --git a/testsuite/tests/quasiquotation/T7918A.hs b/testsuite/tests/quasiquotation/T7918A.hs
index f20dfeef59..0792ee9d1b 100644
--- a/testsuite/tests/quasiquotation/T7918A.hs
+++ b/testsuite/tests/quasiquotation/T7918A.hs
@@ -19,7 +19,7 @@ qq = QuasiQuoter {
                          y = VarP (mkName "y")
                      in \str -> case str of
                                   "p1" -> return $ x
-                                  "p2" -> return $ ConP 'Just [x]
+                                  "p2" -> return $ ConP 'Just [] [x]
                                   "p3" -> return $ TupP [x, y]
                                   "p4" -> return $ y
        , quoteDec  = undefined
diff --git a/testsuite/tests/quasiquotation/qq005/Expr.hs b/testsuite/tests/quasiquotation/qq005/Expr.hs
index 767d906ba4..bb02666847 100644
--- a/testsuite/tests/quasiquotation/qq005/Expr.hs
+++ b/testsuite/tests/quasiquotation/qq005/Expr.hs
@@ -97,9 +97,8 @@ parseExprPat s =  do  loc <- location
                       dataToPatQ (const Nothing `extQ` antiExprPat) expr
 
 antiExprPat :: Expr -> Maybe (Q Pat)
-antiExprPat  (AntiIntExpr v)  = Just $ conP  (mkName "IntExpr")
-                                                [varP (mkName v)]
-antiExprPat  (AntiExpr v)     = Just $ varP  (mkName v)
+antiExprPat  (AntiIntExpr v)  = Just $ conP (mkName "IntExpr") [varP (mkName v)]
+antiExprPat  (AntiExpr v)     = Just $ varP (mkName v)
 antiExprPat  _                = Nothing
 
 -- Copied from syb for the test
diff --git a/testsuite/tests/th/T3899a.hs b/testsuite/tests/th/T3899a.hs
index a63c17b0d3..1b5e7d69c1 100644
--- a/testsuite/tests/th/T3899a.hs
+++ b/testsuite/tests/th/T3899a.hs
@@ -10,6 +10,6 @@ data Nil = Nil
 
 nestedTuple n = do
      xs <- replicateM n (newName "x")
-     return $ LamE [foldr (\v prev -> ParensP (ConP 'Cons [VarP v,prev]))
-                       (ConP 'Nil []) xs]
+     return $ LamE [foldr (\v prev -> ParensP (ConP 'Cons [] [VarP v,prev]))
+                       (ConP 'Nil [] []) xs]
                    (TupE $ map (Just . VarE) xs)
diff --git a/testsuite/tests/th/TH_repPatSig_asserts.hs b/testsuite/tests/th/TH_repPatSig_asserts.hs
index 42ade65ab4..c9ea09dc99 100644
--- a/testsuite/tests/th/TH_repPatSig_asserts.hs
+++ b/testsuite/tests/th/TH_repPatSig_asserts.hs
@@ -35,7 +35,7 @@ assertVar expQ = do
   exp <- expQ
   case exp of
     LamE [SigP (VarP x) (AppT (ConT _) (VarT a))]
-         (CaseE (VarE x1) [Match (ConP _ [VarP y])
+         (CaseE (VarE x1) [Match (ConP _ [] [VarP y])
                                  (NormalB (SigE (VarE y1) (VarT a1))) []])
       | x1 == x &&
         y1 == y &&
diff --git a/testsuite/tests/th/TH_repUnboxedTuples.stderr b/testsuite/tests/th/TH_repUnboxedTuples.stderr
index 3687b77a0e..b8bedac854 100644
--- a/testsuite/tests/th/TH_repUnboxedTuples.stderr
+++ b/testsuite/tests/th/TH_repUnboxedTuples.stderr
@@ -1,4 +1,4 @@
-CaseE (UnboxedTupE [Just (LitE (CharL 'b')),Just (ConE GHC.Types.False)]) [Match (UnboxedTupP [LitP (CharL 'a'),ConP GHC.Types.True []]) (NormalB (UnboxedTupE [Just (LitE (StringL "One")),Just (LitE (IntegerL 1))])) [],Match (UnboxedTupP [LitP (CharL 'b'),ConP GHC.Types.False []]) (NormalB (UnboxedTupE [Just (LitE (StringL "Two")),Just (LitE (IntegerL 2))])) [],Match (UnboxedTupP [WildP,WildP]) (NormalB (UnboxedTupE [Just (LitE (StringL "Three")),Just (LitE (IntegerL 3))])) []]
+CaseE (UnboxedTupE [Just (LitE (CharL 'b')),Just (ConE GHC.Types.False)]) [Match (UnboxedTupP [LitP (CharL 'a'),ConP GHC.Types.True [] []]) (NormalB (UnboxedTupE [Just (LitE (StringL "One")),Just (LitE (IntegerL 1))])) [],Match (UnboxedTupP [LitP (CharL 'b'),ConP GHC.Types.False [] []]) (NormalB (UnboxedTupE [Just (LitE (StringL "Two")),Just (LitE (IntegerL 2))])) [],Match (UnboxedTupP [WildP,WildP]) (NormalB (UnboxedTupE [Just (LitE (StringL "Three")),Just (LitE (IntegerL 3))])) []]
 case (# 'b', GHC.Types.False #) of
     (# 'a', GHC.Types.True #) -> (# "One", 1 #)
     (# 'b', GHC.Types.False #) -> (# "Two", 2 #)
diff --git a/testsuite/tests/th/TH_unresolvedInfix.hs b/testsuite/tests/th/TH_unresolvedInfix.hs
index 3c34b976a3..d9af48491a 100644
--- a/testsuite/tests/th/TH_unresolvedInfix.hs
+++ b/testsuite/tests/th/TH_unresolvedInfix.hs
@@ -123,7 +123,7 @@ main = do
 
   -- pretty-printing of unresolved infix expressions
   let ne = ConE $ mkName "N"
-      np = ConP (mkName "N") []
+      np = ConP (mkName "N") [] []
       nt = ConT (mkName "Int")
       plusE = ConE (mkName ":+")
       plusP = (mkName ":+")
diff --git a/testsuite/tests/th/TH_unresolvedInfix.stdout b/testsuite/tests/th/TH_unresolvedInfix.stdout
index 4f81fdafa9..3953685881 100644
--- a/testsuite/tests/th/TH_unresolvedInfix.stdout
+++ b/testsuite/tests/th/TH_unresolvedInfix.stdout
@@ -36,8 +36,8 @@ True
 True
 InfixE (Just (InfixE (Just (ConE TH_unresolvedInfix_Lib.N)) (ConE TH_unresolvedInfix_Lib.:*) (Just (ConE TH_unresolvedInfix_Lib.N)))) (ConE TH_unresolvedInfix_Lib.:+) (Just (ConE TH_unresolvedInfix_Lib.N))
 InfixE (Just (InfixE (Just (ConE TH_unresolvedInfix_Lib.N)) (ConE TH_unresolvedInfix_Lib.:*) (Just (ConE TH_unresolvedInfix_Lib.N)))) (ConE TH_unresolvedInfix_Lib.:+) (Just (ConE TH_unresolvedInfix_Lib.N))
-InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [])
-InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [])
+InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N [] []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [] [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [] [])
+InfixP (InfixP (ConP TH_unresolvedInfix_Lib.N [] []) TH_unresolvedInfix_Lib.:* (ConP TH_unresolvedInfix_Lib.N [] [])) TH_unresolvedInfix_Lib.:+ (ConP TH_unresolvedInfix_Lib.N [] [])
 AppT (AppT (ConT TH_unresolvedInfix_Lib.+) (AppT (AppT (ConT TH_unresolvedInfix_Lib.*) (ConT GHC.Types.Int)) (ConT GHC.Types.Int))) (ConT GHC.Types.Int)
 AppT (AppT (ConT TH_unresolvedInfix_Lib.+) (AppT (AppT (ConT TH_unresolvedInfix_Lib.*) (ConT GHC.Types.Int)) (ConT GHC.Types.Int))) (ConT GHC.Types.Int)
 N :+ (N :+ N :+ N)
diff --git a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
index e636c0c4f1..d245bb9cee 100644
--- a/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
+++ b/testsuite/tests/th/overloaded/TH_overloaded_extract.stdout
@@ -1,6 +1,6 @@
 InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2)))
 LamE [VarP x] (InfixE (Just (LitE (IntegerL 1))) (VarE GHC.Num.+) (Just (LitE (IntegerL 2))))
 [DataD [] Foo [] Nothing [NormalC Foo []] []]
-ConP GHC.Tuple.() []
+ConP GHC.Tuple.() [] []
 AppT ListT (ConT GHC.Types.Int)
 InfixE Nothing (VarE GHC.Num.+) (Just (LitE (IntegerL 1)))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs
new file mode 100644
index 0000000000..7411ba07ee
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Existential.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo where
+  MkFoo :: forall a. a -> (a -> String) -> Foo
+
+foo :: Foo -> String
+foo (MkFoo @a x f) = f (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs
new file mode 100644
index 0000000000..7e207c312a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_ExistentialMulti.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo where
+  MkFoo :: forall a b. a -> (a -> String) -> b -> (b -> String) -> Foo
+
+foo :: Foo -> String
+foo (MkFoo @u @v x f y g) = f (x :: u) ++ g (y :: v)
+
+main = do
+  print (foo (MkFoo "hello" reverse True show))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs
new file mode 100644
index 0000000000..bba4c1df18
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_KindDependency.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+data Proxy (a :: k) = Proxy
+
+data Con k (a :: k) = Con (Proxy a)
+
+tyApp :: Con k a -> Proxy a
+tyApp (Con @kx @ax (x :: Proxy ax)) = x :: Proxy (ax :: kx)
+
+main = return ()
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs
new file mode 100644
index 0000000000..47812d994d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Mixed.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo b where
+  MkFoo :: forall b a. a -> (b -> a -> String) -> Foo b
+
+foo :: Foo b -> b -> String
+foo (MkFoo @b @a x f) u = f (u :: b) (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" (\x y -> reverse y ++ show x)) (6 :: Integer))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs
new file mode 100644
index 0000000000..aeaa4fcac3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_TH.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE TemplateHaskell #-}
+
+module Main where
+
+import Language.Haskell.TH
+
+apat :: Q Pat
+apat = [p| Just @[a] xs |]
+
+main = do
+  print ()
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs
new file mode 100644
index 0000000000..7a74ff8403
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Universal.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+foo :: Foo String -> String
+foo (MkFoo @a x f) = f (x :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs
new file mode 100644
index 0000000000..cccee20cb1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+import Data.Maybe
+
+data Foo a where
+  MkFoo :: a -> (String -> String) -> Foo a
+
+foo :: Foo (Int, [Char], Maybe String -> Bool) -> String
+foo (MkFoo @(u, [v], f w -> x) x f) = f (unwords [show @u 5, show @v 'c', show (fmap @f not (Just (True :: x))) :: w])
+
+main = do
+  print (foo (MkFoo (6,"hello",isJust) reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs
new file mode 100644
index 0000000000..f01b606799
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE KindSignatures #-}
+
+module Main where
+
+data Foo a b where
+  MkFoo :: forall b a. a -> (a -> b -> String) -> Foo a b
+
+foo :: Foo a b -> b -> String
+foo (MkFoo @c @d x f) t = f (x :: d) (t :: c)
+
+main = do
+  print (foo (MkFoo True (\x y -> show x ++ show y) :: Foo Bool Integer) (6 :: Integer))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs
new file mode 100644
index 0000000000..89fb88d5fe
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalMulti3.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+foo :: Foo String -> Foo String -> String
+foo (MkFoo @a x f) (MkFoo @b y g) = f (x :: a) ++ g (y :: b)
+
+main = do
+  print (foo (MkFoo "hello" reverse) (MkFoo "goodbye" reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs
new file mode 100644
index 0000000000..e7f5522776
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_UniversalNested.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: Maybe a -> (a -> String) -> Foo a
+
+foo :: Foo String -> String
+foo (MkFoo @a (Nothing @b) f) = "nothing"
+foo (MkFoo @a (Just @b x) f) = f ((x :: b) :: a)
+
+main = do
+  print (foo (MkFoo (Just "hello") reverse))
diff --git a/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs b/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs
new file mode 100644
index 0000000000..722a9b4d63
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TyAppPat_Wildcard.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+
+module Main where
+
+f :: Maybe Int -> Int
+f (Just @_ x) = x
+f Nothing = 0
+
+Just @_ x = Just "hello"
+
+Just @Int y = Just 5
+
+main = do
+  print x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3a36e77922..344b4394a9 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -737,3 +737,15 @@ test('InstanceGivenOverlap2', normal, compile, [''])
 test('LocalGivenEqs', normal, compile, [''])
 test('LocalGivenEqs2', normal, compile, [''])
 test('T18891', normal, compile, [''])
+
+test('TyAppPat_Existential', normal, compile, [''])
+test('TyAppPat_ExistentialMulti', normal, compile, [''])
+test('TyAppPat_KindDependency', normal, compile, [''])
+test('TyAppPat_Universal', normal, compile, [''])
+test('TyAppPat_Mixed', normal, compile, [''])
+test('TyAppPat_TH', normal, compile, [''])
+test('TyAppPat_UniversalMulti1', normal, compile, [''])
+test('TyAppPat_UniversalMulti2', normal, compile, [''])
+test('TyAppPat_UniversalMulti3', normal, compile, [''])
+test('TyAppPat_UniversalNested', normal, compile, [''])
+test('TyAppPat_Wildcard', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs
new file mode 100644
index 0000000000..d163874c8e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Some = forall a. Some a
+
+foo (Some @a x) = (x :: a)
+
+main = do
+  print (foo (Some (5 :: Integer)) :: Integer)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr
new file mode 100644
index 0000000000..06f7c3adca
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ExistentialEscape.stderr
@@ -0,0 +1,15 @@
+
+TyAppPat_ExistentialEscape.hs:9:20: error:
+    • Couldn't match expected type ‘p’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor: Some :: forall a. a -> Some,
+        in an equation for ‘foo’
+        at TyAppPat_ExistentialEscape.hs:9:6-14
+      ‘p’ is a rigid type variable bound by
+        the inferred type of foo :: Some -> p
+        at TyAppPat_ExistentialEscape.hs:9:1-26
+    • In the expression: x :: a
+      In an equation for ‘foo’: foo (Some @a x) = (x :: a)
+    • Relevant bindings include
+        x :: a (bound at TyAppPat_ExistentialEscape.hs:9:14)
+        foo :: Some -> p (bound at TyAppPat_ExistentialEscape.hs:9:1)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs
new file mode 100644
index 0000000000..4285a73572
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data T a = MkT a a
+
+foo (MkT x @a y) = (x :: a)
+
+main = do
+  print (foo (MkT True False))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr
new file mode 100644
index 0000000000..61ab78e86c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_MisplacedApplication.stderr
@@ -0,0 +1,3 @@
+
+TyAppPat_MisplacedApplication.hs:9:6: error:
+    Parse error in pattern: MkT x
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs
new file mode 100644
index 0000000000..db50abb7a5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a b where
+  MkFoo :: a -> (a -> String) -> b -> Foo a b
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Foo String String -> String
+foo (MkFoo @a @a x f y) = f (x ++ y :: a)
+
+main = do
+  print (foo (MkFoo "hello" reverse "goodbye"))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
new file mode 100644
index 0000000000..4b891df797
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiAppPat.stderr
@@ -0,0 +1,4 @@
+
+TyAppPat_NonlinearMultiAppPat.hs:12:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs
new file mode 100644
index 0000000000..557ebb1d97
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Maybe String -> Maybe String -> String
+foo (Nothing @a) (Nothing @a) = ("" :: a)
+foo (Just @a x) (Nothing @a) = (x :: a)
+foo (Nothing @a) (Just @a y) = (y :: a)
+foo (Just @a x) (Just @a y) = (x ++ y :: a)
+
+main = do
+  print (foo Nothing (Just "hello"))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
new file mode 100644
index 0000000000..48aeba149e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearMultiPat.stderr
@@ -0,0 +1,16 @@
+
+TyAppPat_NonlinearMultiPat.hs:9:19: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:10:18: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:11:19: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_NonlinearMultiPat.hs:12:18: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs
new file mode 100644
index 0000000000..f80e6d448c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Foo a where
+  MkFoo :: a -> (a -> String) -> Foo a
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: Foo (String, String) -> String
+foo (MkFoo @(a,a) (x,y) f) = f (x :: a, y :: a)
+
+main = do
+  print (foo (MkFoo ("hello", "goodbye") (\(x,y) -> reverse y ++ reverse x)))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
new file mode 100644
index 0000000000..b25bfcde34
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_NonlinearSinglePat.stderr
@@ -0,0 +1,3 @@
+
+TyAppPat_NonlinearSinglePat.hs:12:6: error:
+    Variable `a' would be bound multiple times by a type argument.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs
new file mode 100644
index 0000000000..7d6b8a47a5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+foo :: Maybe a -> a
+foo (Just @Int x) = x
+foo Nothing = 0
+
+main = do
+  print (foo (Just 5))
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr
new file mode 100644
index 0000000000..4d70de517c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_Nonmatching.stderr
@@ -0,0 +1,11 @@
+
+TyAppPat_Nonmatching.hs:8:6: error:
+    • Couldn't match expected type ‘a’ with actual type ‘Int’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall a. Maybe a -> a
+        at TyAppPat_Nonmatching.hs:7:1-19
+    • In the pattern: Just @Int x
+      In an equation for ‘foo’: foo (Just @Int x) = x
+    • Relevant bindings include
+        foo :: Maybe a -> a (bound at TyAppPat_Nonmatching.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs
new file mode 100644
index 0000000000..978e611501
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+x :: Integer
+Just @a x = Just (5 :: Integer)
+
+main = do
+  print x
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr
new file mode 100644
index 0000000000..e0d18596e0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBinding.stderr
@@ -0,0 +1,5 @@
+
+TyAppPat_PatternBinding.hs:8:1: error:
+    • Binding type variables is not allowed in pattern bindings
+    • In the pattern: Just @a x
+      In a pattern binding: Just @a x = Just (5 :: Integer)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs
new file mode 100644
index 0000000000..bd888b3bac
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+
+module Main where
+
+data Some = forall a. Some a
+
+Some @a x = Some (5 :: Integer)
+
+main = do
+  print (x :: a)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr
new file mode 100644
index 0000000000..9204f8016a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_PatternBindingExistential.stderr
@@ -0,0 +1,32 @@
+
+TyAppPat_PatternBindingExistential.hs:9:1: error:
+    • Binding type variables is not allowed in pattern bindings
+    • In the pattern: Some @a x
+      In a pattern binding: Some @a x = Some (5 :: Integer)
+
+TyAppPat_PatternBindingExistential.hs:9:9: error:
+    • Couldn't match expected type ‘p’ with actual type ‘a’
+      ‘a’ is a rigid type variable bound by
+        a pattern with constructor: Some :: forall a. a -> Some,
+        in a pattern binding
+        at TyAppPat_PatternBindingExistential.hs:9:1-9
+      ‘p’ is a rigid type variable bound by
+        the inferred type of x :: p
+        at TyAppPat_PatternBindingExistential.hs:9:1-31
+    • In the pattern: Some @a x
+      In a pattern binding: Some @a x = Some (5 :: Integer)
+
+TyAppPat_PatternBindingExistential.hs:12:3: error:
+    • Ambiguous type variable ‘a0’ arising from a use of ‘print’
+      prevents the constraint ‘(Show a0)’ from being solved.
+      Probable fix: use a type annotation to specify what ‘a0’ should be.
+      These potential instances exist:
+        instance Show Ordering -- Defined in ‘GHC.Show’
+        instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+        instance Show Integer -- Defined in ‘GHC.Show’
+        ...plus 22 others
+        ...plus 12 instances involving out-of-scope types
+        (use -fprint-potential-instances to see them all)
+    • In a stmt of a 'do' block: print (x :: a)
+      In the expression: do print (x :: a)
+      In an equation for ‘main’: main = do print (x :: a)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
new file mode 100644
index 0000000000..6906ed627b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Main where
+
+-- Shouldn't work because we don't accept multiple occurrences of a binding variable.
+foo :: forall a. Monoid a => Maybe a -> a
+foo (Nothing @a) = (mempty :: a)
+foo (Just @a x) = (x :: a)
+
+main = do
+  print (foo @String Nothing)
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
new file mode 100644
index 0000000000..5ce650e4be
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_ScopedTyVarConflict.stderr
@@ -0,0 +1,8 @@
+
+TyAppPat_ScopedTyVarConflict.hs:10:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
+
+TyAppPat_ScopedTyVarConflict.hs:11:6: error:
+    Type variable ‘a’ is already in scope.
+    Type applications in patterns must bind fresh variables, without shadowing.
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs
new file mode 100644
index 0000000000..03f44f052f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.hs
@@ -0,0 +1,5 @@
+module TyAppPat_TooMany where
+
+f :: Maybe Int -> Int
+f (Just @Int @Bool x) = x
+f Nothing = 10
diff --git a/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr
new file mode 100644
index 0000000000..87e9044919
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/TyAppPat_TooMany.stderr
@@ -0,0 +1,6 @@
+
+TyAppPat_TooMany.hs:4:4: error:
+    • Too many type arguments in constructor pattern for ‘Just’
+      Expected no more than 1; got 2
+    • In the pattern: Just @Int @Bool x
+      In an equation for ‘f’: f (Just @Int @Bool x) = x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 913d6d8029..3eff08d080 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -593,3 +593,13 @@ test('T10709', normal, compile_fail, [''])
 test('T10709b', normal, compile_fail, [''])
 test('GivenForallLoop', normal, compile_fail, [''])
 test('T18891a', normal, compile_fail, [''])
+test('TyAppPat_ExistentialEscape', normal, compile_fail, [''])
+test('TyAppPat_MisplacedApplication', normal, compile_fail, [''])
+test('TyAppPat_NonlinearMultiAppPat', normal, compile_fail, [''])
+test('TyAppPat_NonlinearMultiPat', normal, compile_fail, [''])
+test('TyAppPat_NonlinearSinglePat', normal, compile_fail, [''])
+test('TyAppPat_Nonmatching', normal, compile_fail, [''])
+test('TyAppPat_PatternBinding', normal, compile_fail, [''])
+test('TyAppPat_PatternBindingExistential', normal, compile_fail, [''])
+test('TyAppPat_ScopedTyVarConflict', normal, compile_fail, [''])
+test('TyAppPat_TooMany', normal, compile_fail, [''])