Fail fast on pattern synonyms

We were recovering too eagerly from errors in pattern-synonym
type inference, leading to a cascade of confusing follow up errors
(Trac #15685, #15692).

The underlying issue is that a pattern synonym should have a closed,
fixed type, with no unification variables in it.  But it wasn't!

Fixing this made me change the interface to simplifyInfer slightly.
Instead of /emitting/ a residual implication constraint, it
now /returns/ it, so that the caller can decide what to do.

5 files changed, 47 insertions, 0 deletions

diff --git a/testsuite/tests/patsyn/should_fail/T15685.hs b/testsuite/tests/patsyn/should_fail/T15685.hs
new file mode 100644
index 0000000000..6bb84c06e5
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15685.hs
@@ -0,0 +1,13 @@
+{-# Language DataKinds, TypeOperators, PolyKinds, GADTs, PatternSynonyms #-}
+
+module T15685 where
+
+import Data.Kind
+
+data NS f as where
+ Here :: f a -> NS f (a:as)
+
+data NP :: (k -> Type) -> ([k] -> Type) where
+ Nil :: NP f '[]
+
+pattern HereNil = Here Nil
diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr
new file mode 100644
index 0000000000..13fc5a81ec
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15685.stderr
@@ -0,0 +1,10 @@
+
+T15685.hs:13:24: error:
+    • Kind mismatch: cannot unify (f :: a -> *) with:
+        NP a0 :: [k0] -> *
+      Their kinds differ.
+      Expected type: f a1
+        Actual type: NP a0 b0
+    • In the pattern: Nil
+      In the pattern: Here Nil
+      In the declaration for pattern synonym ‘HereNil’
diff --git a/testsuite/tests/patsyn/should_fail/T15692.hs b/testsuite/tests/patsyn/should_fail/T15692.hs
new file mode 100644
index 0000000000..68c4aea385
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15692.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# OPTIONS_GHC -fdefer-type-errors #-}
+module T15692 where
+
+data F x where
+  FS :: F (f a) -> F a
+
+pattern FS' = FS False
diff --git a/testsuite/tests/patsyn/should_fail/T15692.stderr b/testsuite/tests/patsyn/should_fail/T15692.stderr
new file mode 100644
index 0000000000..42de53beec
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T15692.stderr
@@ -0,0 +1,13 @@
+
+T15692.hs:9:18: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘F (f x)’ with actual type ‘Bool’
+    • In the pattern: False
+      In the pattern: FS False
+      In the declaration for pattern synonym ‘FS'’
+
+T15692.hs:9:18: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • Couldn't match expected type ‘F (f0 x)’ with actual type ‘Bool’
+    • In the first argument of ‘FS’, namely ‘False’
+      In the expression: FS False
+      In an equation for ‘FS'’: FS' = FS False
+    • Relevant bindings include $bFS' :: F x (bound at T15692.hs:9:9)
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index 81e664445a..e726eaa1f2 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -44,3 +44,5 @@ test('T14498', normal, compile_fail, [''])
 test('T14552', normal, compile_fail, [''])
 test('T14507', normal, compile_fail, ['-dsuppress-uniques'])
 test('T15289', normal, compile_fail, [''])
+test('T15685', normal, compile_fail, [''])
+test('T15692', normal, compile, [''])   # It has -fdefer-type-errors inside