Fix explicitly-bidirectional pattern synonyms

This partly fixes Trac #13441, at least for the explicitly
bidirectional case.

See Note [Checking against a pattern signature], the part about
"Existential type variables".

Alas, the implicitly-bidirectional case is still not quite right, but
at least there is a workaround by making it explicitly bidirectional.

2 files changed, 30 insertions, 0 deletions

diff --git a/testsuite/tests/patsyn/should_compile/T13441.hs b/testsuite/tests/patsyn/should_compile/T13441.hs
new file mode 100644
index 0000000000..d7a339f782
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T13441.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds,
+             GADTs, TypeOperators, TypeFamilies #-}
+
+module T13441 where
+
+import Data.Functor.Identity
+
+data FList f xs where
+  FNil :: FList f '[]
+  (:@) :: f x -> FList f xs -> FList f (x ': xs)
+
+data Nat = Zero | Succ Nat
+
+type family Length (xs :: [k]) :: Nat where
+  Length '[]       = Zero
+  Length (_ ': xs) = Succ (Length xs)
+
+type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
+  Replicate Zero     _ = '[]
+  Replicate (Succ n) x = x ': Replicate n x
+
+type Vec n a = FList Identity (Replicate n a)
+
+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
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index 87de2f00bb..1f36424640 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -64,3 +64,4 @@ test('T12698', normal, compile, [''])
 test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
 test('T12968', normal, compile, [''])
 test('T13349b', normal, compile, [''])
+test('T13441', normal, compile, [''])