Complete the fix for #13441 (pattern synonyms)

Do not attempt to typecheck both directions of an
implicitly-bidirectional pattern synonym simultanously,
as we were before.  Instead, the builder is typechecked
when we typecheck the code for the builder, which was
of course happening already, even in both bidirectional
cases.

See Note [Checking against a pattern signature], under
"Existential type variables".

5 files changed, 43 insertions, 0 deletions

diff --git a/testsuite/tests/patsyn/should_compile/T13441.hs b/testsuite/tests/patsyn/should_compile/T13441.hs
index d7a339f782..738017500d 100644
--- a/testsuite/tests/patsyn/should_compile/T13441.hs
+++ b/testsuite/tests/patsyn/should_compile/T13441.hs
@@ -21,9 +21,16 @@ type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
 
 type Vec n a = FList Identity (Replicate n a)
 
+-- Using explicitly-bidirectional pattern
 pattern (:>) :: forall n a. n ~ Length (Replicate n a)
              => forall m. n ~ Succ m
              => a -> Vec m a -> Vec n a
 pattern x :> xs <- Identity x :@ xs
   where
     x :> xs = Identity x :@ xs
+
+-- Using implicitly-bidirectional pattern
+pattern (:>>) :: forall n a. n ~ Length (Replicate n a)
+             => forall m. n ~ Succ m
+             => a -> Vec m a -> Vec n a
+pattern x :>> xs = Identity x :@ xs
diff --git a/testsuite/tests/patsyn/should_compile/T13441a.hs b/testsuite/tests/patsyn/should_compile/T13441a.hs
new file mode 100644
index 0000000000..77360946a2
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T13441a where
+
+data S where
+  MkS :: Eq a => [a] -> S
+
+-- Unidirectional pattern binding;
+-- the existential is more specific than needed
+-- c.f. T13441b
+pattern P :: () => Eq x => x -> S
+pattern P x <- MkS x
diff --git a/testsuite/tests/patsyn/should_compile/T13441b.hs b/testsuite/tests/patsyn/should_compile/T13441b.hs
new file mode 100644
index 0000000000..8f8d2ba5ca
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T13441a where
+
+data S where
+  MkS :: Eq a => [a] -> S
+
+-- Implicitly-bidirectional pattern binding;
+-- the existential is more specific than needed,
+-- and hence should be rejected
+-- c.f. T13441a
+pattern P :: () => Eq x => x -> S
+pattern P x = MkS x
diff --git a/testsuite/tests/patsyn/should_compile/T13441b.stderr b/testsuite/tests/patsyn/should_compile/T13441b.stderr
new file mode 100644
index 0000000000..4469086c82
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441b.stderr
@@ -0,0 +1,11 @@
+
+T13441b.hs:12:19: error:
+    • Couldn't match expected type ‘[a0]’ with actual type ‘x’
+      ‘x’ is a rigid type variable bound by
+        the signature for pattern synonym ‘P’ at T13441b.hs:12:1-19
+    • In the first argument of ‘MkS’, namely ‘x’
+      In the expression: MkS x
+      In an equation for ‘P’: P x = MkS x
+    • Relevant bindings include
+        x :: x (bound at T13441b.hs:12:19)
+        $bP :: x -> S (bound at T13441b.hs:12:9)
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 1f36424640..8fce7e987d 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -65,3 +65,5 @@ test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
 test('T12968', normal, compile, [''])
 test('T13349b', normal, compile, [''])
 test('T13441', normal, compile, [''])
+test('T13441a', normal, compile, [''])
+test('T13441b', normal, compile_fail, [''])