Improve partial signatures

This MR fixes #23223. The changes are in two places:

* GHC.Tc.Bind.checkMonomorphismRestriction
  See the new `Note [When the MR applies]`
  We now no longer stupidly attempt to apply the MR when the user
  specifies a context, e.g.   f :: Eq a => _ -> _

* GHC.Tc.Solver.decideQuantification
  See rewritten `Note [Constraints in partial type signatures]`

Fixing this bug apparently breaks three tests:

* partial-sigs/should_compile/T11192
* partial-sigs/should_fail/Defaulting1MROff
* partial-sigs/should_fail/T11122

However they are all symptoms of #23232, so I'm marking them as
expect_broken(23232).

I feel happy about this MR. Nice.

7 files changed, 44 insertions, 34 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 37f5ad522b..ff45dc06fc 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -14,41 +14,17 @@ T10403.hs:16:12: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
     • In the type signature: h1 :: _ => _
 
 T10403.hs:20:7: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’
-        standing for ‘(a1 -> a2) -> f0 a1 -> H f0’
-      Where: ‘f0’ is an ambiguous type variable
-             ‘a2’, ‘a1’ are rigid type variables bound by
-               the inferred type of h2 :: (a1 -> a2) -> f0 a1 -> H f0
+    • Found type wildcard ‘_’ standing for ‘(a1 -> a2) -> f a1 -> H f’
+      Where: ‘a2’, ‘a1’, ‘f’ are rigid type variables bound by
+               the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
                at T10403.hs:23:1-41
     • In the type signature: h2 :: _
 
 T10403.hs:23:15: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
-    • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’
-      prevents the constraint ‘(Functor f0)’ from being solved.
-      Relevant bindings include
-        b :: f0 a1 (bound at T10403.hs:23:6)
-        h2 :: (a1 -> a2) -> f0 a1 -> H f0 (bound at T10403.hs:23:1)
-      Probable fix: use a type annotation to specify what ‘f0’ should be.
-      Potentially matching instances:
-        instance Functor IO -- Defined in ‘GHC.Base’
-        instance Functor (B t) -- Defined at T10403.hs:11:10
-        ...plus 8 others
-        ...plus one instance involving out-of-scope types
-        (use -fprint-potential-instances to see them all)
+    • No instance for ‘Functor f’ arising from a use of ‘fmap’
+      Possible fix:
+        add (Functor f) to the context of
+          the inferred type of h2 :: (a1 -> a2) -> f a1 -> H f
     • In the second argument of ‘(.)’, namely ‘fmap (const ())’
       In the expression: (H . fmap (const ())) (fmap f b)
       In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b)
-
-T10403.hs:29:8: warning: [GHC-46956] [-Wdeferred-type-errors (in -Wdefault)]
-    • Couldn't match type ‘f0’ with ‘B t’
-      Expected: H (B t)
-        Actual: H f0
-    • because type variable ‘t’ would escape its scope
-    This (rigid, skolem) type variable is bound by
-      the type signature for:
-        app2 :: forall t. H (B t)
-      at T10403.hs:28:1-15
-    • In the expression: h2 (H . I) (B ())
-      In an equation for ‘app2’: app2 = h2 (H . I) (B ())
-    • Relevant bindings include
-        app2 :: H (B t) (bound at T10403.hs:29:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/T19106.hs b/testsuite/tests/partial-sigs/should_compile/T19106.hs
index 02f36744a0..9ed7cb058d 100644
--- a/testsuite/tests/partial-sigs/should_compile/T19106.hs
+++ b/testsuite/tests/partial-sigs/should_compile/T19106.hs
@@ -3,6 +3,13 @@
 
 module T19106 where
 
+-- This is a very subtle program:
+-- From the body of the function we get [W] Show a
+-- That can be satisfied only from the /combination/ of
+--    [G] a ~ [b]       from type sig
+--    [G] G a           from pattern match (MkT x)
+--    The type instance G [b] = Show b
+
 f :: (a ~ [b]) => T a -> _ -> String
 f (MkT x) _ = show x
 
diff --git a/testsuite/tests/partial-sigs/should_compile/T20076.hs b/testsuite/tests/partial-sigs/should_compile/T20076.hs
new file mode 100644
index 0000000000..9d53d030a4
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T20076.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE FlexibleContexts, PartialTypeSignatures #-}
+
+module Bug where
+
+f :: Eq [a] => a -> _
+f x = [x] == [x]
+
+-- See Note [Constraints in partial type signatures] in
+-- GHC.Tc.Solver, in particular the bullet about (P2).
\ No newline at end of file
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 935d62231c..d421491b5a 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -71,7 +71,7 @@ test('T10519', normal, compile, [''])
 test('T10463', normal, compile, [''])
 test('ExprSigLocal', normal, compile, [''])
 test('T11016', normal, compile, [''])
-test('T11192', normal, compile, [''])
+test('T11192', expect_broken(23232), compile, [''])
 test('SuperCls', normal, compile, [''])
 test('T12033', normal, compile, [''])
 test('T11339a', normal, compile, [''])
@@ -107,3 +107,4 @@ test('InstanceGivenOverlap3', expect_broken(20076), compile, [''])
 test('T21667', normal, compile, [''])
 test('T22065', normal, compile, [''])
 test('T16152', normal, compile, [''])
+test('T20076', expect_broken(20076), compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T23223.hs b/testsuite/tests/partial-sigs/should_fail/T23223.hs
new file mode 100644
index 0000000000..79ccf61fcd
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T23223.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+module Foo where
+
+f :: (Show a) => a -> _ -> Bool
+f x y = x>x
diff --git a/testsuite/tests/partial-sigs/should_fail/T23223.stderr b/testsuite/tests/partial-sigs/should_fail/T23223.stderr
new file mode 100644
index 0000000000..06c0262dc8
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T23223.stderr
@@ -0,0 +1,11 @@
+
+T23223.hs:5:10: error: [GHC-39999]
+    • Could not deduce ‘Ord a’ arising from a use of ‘>’
+      from the context: Show a
+        bound by the inferred type of f :: Show a => a -> w -> Bool
+        at T23223.hs:5:1-11
+      Possible fix:
+        add (Ord a) to the context of
+          the inferred type of f :: Show a => a -> w -> Bool
+    • In the expression: x > x
+      In an equation for ‘f’: f x y = x > x
diff --git a/testsuite/tests/partial-sigs/should_fail/all.T b/testsuite/tests/partial-sigs/should_fail/all.T
index 949f449452..01baa58d1f 100644
--- a/testsuite/tests/partial-sigs/should_fail/all.T
+++ b/testsuite/tests/partial-sigs/should_fail/all.T
@@ -1,6 +1,6 @@
 test('AnnotatedConstraint', normal, compile_fail, [''])
 test('AnnotatedConstraintNotForgotten', normal, compile_fail, [''])
-test('Defaulting1MROff', normal, compile, [''])
+test('Defaulting1MROff', expect_broken(23232), compile, [''])
 test('ExtraConstraintsWildcardInExpressionSignature', normal, compile, [''])
 test('ExtraConstraintsWildcardInPatternSignature', normal, compile_fail, [''])
 test('ExtraConstraintsWildcardInPatternSplice', [req_interp, normal], compile_fail, [''])
@@ -58,7 +58,7 @@ test('WildcardInTypeSynonymRHS', normal, compile_fail, [''])
 test('T10615', normal, compile_fail, [''])
 test('T10045', normal, compile_fail, [''])
 test('T10999', normalise_fun(normalise_errmsg), compile_fail, [''])
-test('T11122', normal, compile, [''])
+test('T11122', expect_broken(23232), compile, [''])
 test('T11515', normal, compile_fail, [''])
 test('T11976', normal, compile_fail, [''])
 test('PatBind3', normal, compile_fail, [''])
@@ -72,3 +72,4 @@ test('T14449', normal, compile_fail, [''])
 test('T14479', normal, compile_fail, [''])
 test('T14584', normal, compile, [''])
 test('T14584a', normal, compile, [''])
+test('T23223', normal, compile_fail, [''])