Correct order of existentials in pattern synonyms

Trac #12698 exposed a nasty bug in the typechecking for
pattern synonmys: the existential type variables weren't
being put in properly-scoped order.

For some reason TcPatSyn.tcCollectEx was colleting them as a
set, not as a list!  Easily fixed.

2 files changed, 63 insertions, 0 deletions

diff --git a/testsuite/tests/patsyn/should_compile/T12698.hs b/testsuite/tests/patsyn/should_compile/T12698.hs
new file mode 100644
index 0000000000..6ba45e4e85
--- /dev/null
+++ b/testsuite/tests/patsyn/should_compile/T12698.hs
@@ -0,0 +1,62 @@
+{-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds,
+             TypeInType, StandaloneDeriving, GADTs, RebindableSyntax,
+             RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-}
+
+module T12698 where
+
+import GHC.Types
+import Prelude hiding ( fromInteger )
+import Data.Type.Equality
+import Data.Kind
+import qualified Prelude
+
+class Ty (a :: k) where ty :: T a
+instance Ty Int where ty = TI
+instance Ty Bool where ty = TB
+instance Ty a => Ty [a] where ty = TA TL ty
+instance Ty [] where ty = TL
+instance Ty (,) where ty = TP
+
+data AppResult (t :: k) where
+  App :: T a -> T b -> AppResult (a b)
+
+data T :: forall k. k -> Type where
+  TI :: T Int
+  TB :: T Bool
+  TL :: T []
+  TP :: T (,)
+  TA :: T f -> T x -> T (f x)
+deriving instance Show (T a)
+
+splitApp :: T a -> Maybe (AppResult a)
+splitApp = \case
+  TI -> Nothing
+  TB -> Nothing
+  TL -> Nothing
+  TP -> Nothing
+  TA f x -> Just (App f x)
+
+data (a :: k1) :~~: (b :: k2) where
+  HRefl :: a :~~: a
+
+eqT :: T a -> T b -> Maybe (a :~~: b)
+eqT a b =
+  case (a, b) of
+    (TI, TI) -> Just HRefl
+    (TB, TB) -> Just HRefl
+    (TL, TL) -> Just HRefl
+    (TP, TP) -> Just HRefl
+
+pattern List :: () => [] ~~ b => T b
+pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl)
+  where List = ty
+
+pattern Int :: () => Int ~~ b => T b
+pattern Int <- (eqT (ty @Type @Int) -> Just HRefl)
+  where Int = ty
+
+pattern (:<->:) :: () => fx ~ f x => T f -> T x -> T fx
+pattern f :<->: x <- (splitApp -> Just (App f x))
+  where f :<->: x = TA f x
+
+pattern Foo <- List :<->: Int
diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T
index d26fc84bec..4426c74733 100644
--- a/testsuite/tests/patsyn/should_compile/all.T
+++ b/testsuite/tests/patsyn/should_compile/all.T
@@ -60,3 +60,4 @@ test('T12108', normal, compile, [''])
 test('T12484', normal, compile, [''])
 test('T11987', normal, multimod_compile, ['T11987', '-v0'])
 test('T12615', normal, compile, [''])
+test('T12698', normal, compile, [''])