Fix scoping of pattern-synonym existentials

This patch fixes Trac #14998, where we eventually decided that
the existential type variables of the signature of a pattern
synonym should not scope over the pattern synonym.

See Note [Pattern synonym existentials do not scope] in TcPatSyn.

8 files changed, 56 insertions, 17 deletions

diff --git a/testsuite/tests/patsyn/should_fail/T11265.stderr b/testsuite/tests/patsyn/should_fail/T11265.stderr
index eda5d35a9d..7161c272b1 100644
--- a/testsuite/tests/patsyn/should_fail/T11265.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11265.stderr
@@ -1,6 +1,6 @@
 
 T11265.hs:6:12: error:
     • Pattern synonym ‘A’ cannot be used here
-        (Pattern synonyms cannot be promoted)
+        (pattern synonyms cannot be promoted)
     • In the first argument of ‘F’, namely ‘A’
       In the instance declaration for ‘F A’
diff --git a/testsuite/tests/patsyn/should_fail/T14498.hs b/testsuite/tests/patsyn/should_fail/T14498.hs
new file mode 100644
index 0000000000..0744310aee
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14498.hs
@@ -0,0 +1,32 @@
+{-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds #-}
+
+module T14498 where
+
+import Type.Reflection
+import Data.Kind
+
+data Dict c where Dict :: c => Dict c
+
+asTypeable :: TypeRep a -> Dict (Typeable a)
+asTypeable rep =
+  withTypeable rep
+    Dict
+
+pattern Typeable :: () => Typeable a => TypeRep a
+pattern Typeable <- (asTypeable -> Dict)
+  where Typeable = typeRep
+
+data N = O | S N
+
+type SN = (TypeRep :: N -> Type)
+
+pattern SO = (Typeable :: TypeRep (O::N))
+
+pattern SS ::
+     forall (t :: k').
+     ()
+  => forall (a :: kk -> k') (n :: kk).
+     (t ~ a n)
+  =>
+  TypeRep n -> TypeRep t
+pattern SS n <- (App (Typeable :: TypeRep (a ::kk -> k')) n)
diff --git a/testsuite/tests/patsyn/should_fail/T14498.stderr b/testsuite/tests/patsyn/should_fail/T14498.stderr
new file mode 100644
index 0000000000..668f9a1efc
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T14498.stderr
@@ -0,0 +1,8 @@
+
+T14498.hs:32:48: error:
+    • Pattern synonym existential ‘kk’ cannot be used here
+        (the existential variables of a pattern synonym
+         signature do not scope over the pattern)
+    • In the kind ‘kk -> k'’
+      In the first argument of ‘TypeRep’, namely ‘(a :: kk -> k')’
+      In the type ‘TypeRep (a :: kk -> k')’
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.stderr b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
index 04d9b31bf7..fff6efe286 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
@@ -1,6 +1,5 @@
 
 T9161-1.hs:6:14: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
-        (Pattern synonyms cannot be promoted)
-    • In the type signature:
-        wrongLift :: PATTERN
+        (pattern synonyms cannot be promoted)
+    • In the type signature: wrongLift :: PATTERN
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.stderr b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
index 409b922776..cc429313aa 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
@@ -1,7 +1,6 @@
 
 T9161-2.hs:8:20: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
-        (Pattern synonyms cannot be promoted)
+        (pattern synonyms cannot be promoted)
     • In the first argument of ‘Proxy’, namely ‘PATTERN’
-      In the type signature:
-        wrongLift :: Proxy PATTERN ()
+      In the type signature: wrongLift :: Proxy PATTERN ()
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 388e67b27b..4bf631f982 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -39,3 +39,4 @@ test('T13470', normal, compile_fail, [''])
 test('T14112', normal, compile_fail, [''])
 test('T14114', normal, compile_fail, [''])
 test('T14380', normal, compile_fail, [''])
+test('T14498', normal, compile_fail, [''])
diff --git a/testsuite/tests/polykinds/T5716.stderr b/testsuite/tests/polykinds/T5716.stderr
index d85166b0bb..0e3596da32 100644
--- a/testsuite/tests/polykinds/T5716.stderr
+++ b/testsuite/tests/polykinds/T5716.stderr
@@ -1,7 +1,7 @@
 
 T5716.hs:13:33: error:
-    Data constructor ‘U1’ cannot be used here
-      (Perhaps you intended to use TypeInType)
-    In the first argument of ‘I’, namely ‘(U1 DFInt)’
-    In the type ‘I (U1 DFInt)’
-    In the definition of data constructor ‘I1’
+    • Data constructor ‘U1’ cannot be used here
+        (perhaps you intended to use TypeInType)
+    • In the first argument of ‘I’, namely ‘(U1 DFInt)’
+      In the type ‘I (U1 DFInt)’
+      In the definition of data constructor ‘I1’
diff --git a/testsuite/tests/polykinds/T7433.stderr b/testsuite/tests/polykinds/T7433.stderr
index 1cd2ad2f29..4dce12a653 100644
--- a/testsuite/tests/polykinds/T7433.stderr
+++ b/testsuite/tests/polykinds/T7433.stderr
@@ -1,6 +1,6 @@
 
-T7433.hs:2:10:
-    Data constructor ‘Z’ cannot be used here
-      (Perhaps you intended to use DataKinds)
-    In the type ‘ 'Z’
-    In the type declaration for ‘T’
+T7433.hs:2:10: error:
+    • Data constructor ‘Z’ cannot be used here
+        (perhaps you intended to use DataKinds)
+    • In the type ‘ 'Z’
+      In the type declaration for ‘T’