Add `PatSynSigSkol` and modify `PatSynCtxt`

As the type of a pattern synonym cannot in general be represented by a
value of type Type, we cannot use a value `SigSkol (PatSynCtxt n) (Check
ty)` to represent the signature of a pattern synonym (this causes
incorrect signatures to be printed in error messages). Therefore we now
represent it by a value `PatSynSigSkol n` (instead of incorrect
signatures we simply print no explicit signature).

Furthermore, we rename `PatSynCtxt` to `PatSynBuilderCtxt`, and use
`SigSkol (PatSynBuilderCtxt n) (Check ty)` to represent the type of a
bidirectional pattern synonym when used in an expression context.
Before, this type was represented by a value `SigSkol (PatSynCtxt n)
(Check ty)`, which caused incorrect error messages.

Also, in `mk_dict_err` of `typecheck\TcErrors.hs` we now distinguish
between all enclosing implications and "useful" enclosing implications,
for better error messages concerning pattern synonyms. See `Note [Useful
implications]`.

See the Phabricator page for examples.

Reviewers: mpickering, goldfire, simonpj, austin, bgamari

Reviewed By: bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1967

GHC Trac Issues: #11667

5 files changed, 80 insertions, 8 deletions

diff --git a/testsuite/tests/patsyn/should_fail/T10873.stderr b/testsuite/tests/patsyn/should_fail/T10873.stderr
index 766b2e0279..6eb925be30 100644
--- a/testsuite/tests/patsyn/should_fail/T10873.stderr
+++ b/testsuite/tests/patsyn/should_fail/T10873.stderr
@@ -12,13 +12,12 @@ T10873.hs:10:23: error:
     • Could not deduce (Show a)
         arising from the "provided" constraints claimed by
           the signature of ‘Pat2’
-      from the context: Enum a
-        bound by the type signature for pattern synonym ‘Pat2’:
-                   a -> T a
-        at T10873.hs:10:9-12
-      or from: Ord a
+      from the context: Ord a
         bound by a pattern with constructor:
                    MkT :: forall a. Ord a => a -> T a,
                  in a pattern synonym declaration
         at T10873.hs:10:19-23
+      In other words, a successful match on the pattern
+        MkT x
+      does not provide the constraint (Show a)
     • In the declaration for pattern synonym ‘Pat2’
diff --git a/testsuite/tests/patsyn/should_fail/T11039.stderr b/testsuite/tests/patsyn/should_fail/T11039.stderr
index 2c7c66327c..eea6257f58 100644
--- a/testsuite/tests/patsyn/should_fail/T11039.stderr
+++ b/testsuite/tests/patsyn/should_fail/T11039.stderr
@@ -2,9 +2,7 @@
 T11039.hs:8:15: error:
     • Couldn't match type ‘f’ with ‘A’
       ‘f’ is a rigid type variable bound by
-        the type signature for pattern synonym ‘Q’:
-          forall (f :: * -> *) a. a -> f a
-        at T11039.hs:7:14
+        the type signature of pattern synonym ‘Q’ at T11039.hs:7:14
       Expected type: f a
         Actual type: A a
     • In the pattern: A a
diff --git a/testsuite/tests/patsyn/should_fail/T11667.hs b/testsuite/tests/patsyn/should_fail/T11667.hs
new file mode 100644
index 0000000000..f2437fa8c5
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T11667.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE PatternSynonyms, GADTs #-}
+module T11667 where
+
+{-
+The following four pattern synonym declarations should give valid
+error messages
+-}
+
+-- Check if we mention no explicit type signature (or the correct
+-- signature "Eq a => Maybe a")
+pattern Pat1 :: Eq a => Maybe a
+pattern Pat1 <- Just 42
+
+-- Check if we mention no explicit type signature (or the correct
+-- signature "forall b. () => forall a. b ~ Bool => a -> b -> (b, T)")
+data T where MkT :: a -> T
+pattern Pat2 :: () => b ~ Bool => a -> b -> (b, T)
+pattern Pat2 x y = (y, MkT x)
+
+-- Check if we do not tell the user that we could not deduce (Show a)
+-- from the "required" context. Also, check if we do not give the
+-- possible fix that suggests to add (Show a) to the "required" context.
+pattern Pat3 :: Eq a => Show a => a -> Maybe a
+pattern Pat3 x <- Just x
+
+-- Check if we return a valid error message concerning the missing
+-- constraint (Num a) when the bidirectional pattern synonym is used
+-- in an expression context
+data S a where MkS :: (Num a, Show a) => a -> S a
+pattern Pat4 :: (Eq a) => (Show a) => S a
+pattern Pat4 = MkS 42
diff --git a/testsuite/tests/patsyn/should_fail/T11667.stderr b/testsuite/tests/patsyn/should_fail/T11667.stderr
new file mode 100644
index 0000000000..6befe1386c
--- /dev/null
+++ b/testsuite/tests/patsyn/should_fail/T11667.stderr
@@ -0,0 +1,43 @@
+
+T11667.hs:12:22: error:
+    • Could not deduce (Num a) arising from the literal ‘42’
+      from the context: Eq a
+        bound by the type signature of pattern synonym ‘Pat1’
+        at T11667.hs:12:9-12
+      Possible fix:
+        add (Num a) to the context of
+          the type signature of pattern synonym ‘Pat1’
+    • In the pattern: 42
+      In the pattern: Just 42
+      In the declaration for pattern synonym ‘Pat1’
+
+T11667.hs:18:28: error:
+    • Couldn't match type ‘b’ with ‘Bool’
+        arising from the "provided" constraints claimed by
+          the signature of ‘Pat2’
+      ‘b’ is a rigid type variable bound by
+        the type signature of pattern synonym ‘Pat2’ at T11667.hs:17:17
+    • In the declaration for pattern synonym ‘Pat2’
+    • Relevant bindings include y :: b (bound at T11667.hs:18:21)
+
+T11667.hs:24:24: error:
+    • No instance for (Show a)
+        arising from the "provided" constraints claimed by
+          the signature of ‘Pat3’
+      In other words, a successful match on the pattern
+        Just x
+      does not provide the constraint (Show a)
+    • In the declaration for pattern synonym ‘Pat3’
+
+T11667.hs:31:16: error:
+    • Could not deduce (Num a) arising from a use of ‘MkS’
+      from the context: (Eq a, Show a)
+        bound by the type signature for bidirectional pattern synonym ‘Pat4’
+                 when used in an expression context:
+                   (Eq a, Show a) => S a
+        at T11667.hs:31:1-21
+      Possible fix:
+        add (Num a) to the context of
+          the type signature of pattern synonym ‘Pat4’
+    • In the expression: MkS 42
+      In an equation for ‘$bPat4’: $bPat4 = MkS 42
diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T
index a9ba4479f0..658a5c0d96 100644
--- a/testsuite/tests/patsyn/should_fail/all.T
+++ b/testsuite/tests/patsyn/should_fail/all.T
@@ -30,3 +30,4 @@ test('export-ps-rec-sel', normal, compile_fail, [''])
 test('T11053', normal, compile, ['-fwarn-missing-pattern-synonym-signatures'])
 test('T10426', normal, compile_fail, [''])
 test('T11265', normal, compile_fail, [''])
+test('T11667', normal, compile_fail, [''])