Implement type applications in patterns

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

33 files changed, 411 insertions, 0 deletions

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, [''])