Fix #16517 by bumping the TcLevel for method sigswip/backport-MR951

There were actually two bugs fixed here:

1. candidateQTyVarsOfType needs to be careful that it does not
   try to zap metavariables from an outer scope as "naughty"
   quantification candidates. This commit adds a simple check
   to avoid doing so.

2. We weren't bumping the TcLevel in kcHsKindSig, which was used
   only for class method sigs. This mistake led to the acceptance
   of

     class C a where
       meth :: forall k. Proxy (a :: k) -> ()

   Note that k is *locally* quantified. This patch fixes the
   problem by using tcClassSigType, which correctly bumps the
   level. It's a bit inefficient because tcClassSigType does other
   work, too, but it would be tedious to repeat much of the code
   there with only a few changes. This version works well and is
   simple.

And, while updating comments, etc., I noticed that tcRnType was
missing a pushTcLevel, leading to #16767, which this patch also
fixes, by bumping the level. In the refactoring here, I also
use solveEqualities. This initially failed ghci/scripts/T15415,
but that was fixed by teaching solveEqualities to respect
-XPartialTypeSignatures.

This patch also cleans up some Notes around error generation that
came up in conversation.

Test case: typecheck/should_fail/T16517, ghci/scripts/T16767

(cherry picked from commit a22e51ea6f7a046c87d57ce30d143eef6abee9ff)

1 files changed, 22 insertions, 14 deletions

diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
index 8ceab3e931..ad5985e63a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -9,20 +9,6 @@ tcfail212.hs:10:14: error:
       Expected a type, but ‘Either Int’ has kind ‘* -> *’
     • In the type signature: f :: (Maybe, Either Int)
 
-tcfail212.hs:11:6: error:
-    • Couldn't match expected type ‘Maybe’
-                  with actual type ‘Maybe Integer’
-    • In the expression: Just 1
-      In the expression: (Just 1, Left 1)
-      In an equation for ‘f’: f = (Just 1, Left 1)
-
-tcfail212.hs:11:14: error:
-    • Couldn't match expected type ‘Either Int’
-                  with actual type ‘Either Integer b0’
-    • In the expression: Left 1
-      In the expression: (Just 1, Left 1)
-      In an equation for ‘f’: f = (Just 1, Left 1)
-
 tcfail212.hs:13:7: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
     • In the type signature: g :: (Int#, Int#)
@@ -30,3 +16,25 @@ tcfail212.hs:13:7: error:
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
     • In the type signature: g :: (Int#, Int#)
+
+tcfail212.hs:14:6: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        a :: *
+        Int# :: TYPE 'IntRep
+    • In the expression: 1#
+      In the expression: (1#, 2#)
+      In an equation for ‘g’: g = (1#, 2#)
+    • Relevant bindings include
+        g :: (a, b) (bound at tcfail212.hs:14:1)
+
+tcfail212.hs:14:10: error:
+    • Couldn't match a lifted type with an unlifted type
+      When matching types
+        b :: *
+        Int# :: TYPE 'IntRep
+    • In the expression: 2#
+      In the expression: (1#, 2#)
+      In an equation for ‘g’: g = (1#, 2#)
+    • Relevant bindings include
+        g :: (a, b) (bound at tcfail212.hs:14:1)