Re-quantify when generalising over rewrite rule types

Previously, `tcRules` would check for naughty quantification
candidates (see `Note [Naughty quantification candidates]` in
`TcMType`) when generalising over the type of a rewrite rule. This
caused sensible-looking rewrite rules (like those in #17710) to be
rejected. A more permissing (and easier-to-implement) approach is to
do what is described in `Note [Generalising in tcTyFamInstEqnGuts]`
in `TcTyClsDecls`: just re-quantify all the type variable binders,
regardless of the order in which the user specified them. After all,
the notion of type variable specificity has no real meaning in
rewrite rules, since one cannot "visibly apply" a rewrite rule.
I have written up this wisdom in
`Note [Re-quantify type variables in rules]` in `TcRules`.

As a result of this patch, compiling the `ExplicitForAllRules1` test
case now generates one fewer warning than it used to. As far as I can
tell, this is benign, since the thing that the disappearing warning
talked about was also mentioned in an entirely separate warning.

Fixes #17710.

3 files changed, 16 insertions, 10 deletions

diff --git a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
index a233fb4f50..0a575c9bb3 100644
--- a/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
+++ b/testsuite/tests/rename/should_compile/ExplicitForAllRules1.stderr
@@ -1,14 +1,4 @@
 
-ExplicitForAllRules1.hs:49:11: warning:
-    Forall'd type variable ‘k’ is not bound in RULE lhs
-      Orig bndrs: [k, a, b, x]
-      Orig lhs: id' @a x
-      optimised lhs: id' @a x
-    Forall'd type variable ‘b’ is not bound in RULE lhs
-      Orig bndrs: [k, a, b, x]
-      Orig lhs: id' @a x
-      optimised lhs: id' @a x
-
 ExplicitForAllRules1.hs:49:31: warning: [-Wunused-foralls (in -Wextra)]
     Unused quantified type variable ‘b’
     in the rule "example7"
diff --git a/testsuite/tests/typecheck/should_compile/T17710.hs b/testsuite/tests/typecheck/should_compile/T17710.hs
new file mode 100644
index 0000000000..f30370c201
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17710.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T17710 where
+
+import Data.Proxy
+
+foo :: forall k (a :: k) (b :: k). Proxy a -> Proxy b
+foo x = Proxy
+{-# INLINABLE [1] foo #-}
+{-# RULES "foo" forall (x :: Proxy (a :: k)). foo x = Proxy #-}
+
+bar :: forall k (b :: k). (forall (a :: k). Proxy a -> Proxy a) -> Proxy b
+bar g = g Proxy
+{-# INLINABLE [1] bar #-}
+{-# RULES "bar" forall (g :: forall (a :: k). Proxy a -> Proxy a). bar g = g Proxy #-}
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 467f7ea192..d8b309dda6 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -697,5 +697,6 @@ test('T17566', [extra_files(['T17566a.hs'])], makefile_test, [])
 test('T12760', unless(compiler_debugged(), skip), compile, ['-O'])
 test('T13142', normal, compile, ['-O2'])
 test('T12926', reqlib('vector'), compile, ['-O2'])
+test('T17710', normal, compile, [''])
 test('T17792', normal, compile, [''])
 test('T17024', normal, compile, [''])