Fix validity checking for inferred types

GHC is suposed to uphold the principle that an /inferred/ type
for a let-binding should obey the rules for that module.  E.g.
we should only accept an inferred higher rank type if we have
RankNTypes on.

But we were failing to check this: TcValidity.checkValidType
allowed arbitrary rank for inferred types.

This patch fixes the bug.  It might in principle cause some breakage,
but if so that's good: the user should add RankNTypes and/or a
manual signature.  (And almost every package has explicit user
signatures for all top-level things anyway.)  Let's see.

Fixes #17213.

Metric Decrease:
    T10370

5 files changed, 21 insertions, 2 deletions

diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 307ec6d0c5..b622480b3e 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -356,7 +356,9 @@ checkValidType ctxt ty
                     -- So we do this check here.
 
                  FunSigCtxt {}  -> rank1
-                 InfSigCtxt _   -> ArbitraryRank        -- Inferred type
+                 InfSigCtxt {}  -> rank1 -- Inferred types should obey the
+                                         -- same rules as declared ones
+
                  ConArgCtxt _   -> rank1 -- We are given the type of the entire
                                          -- constructor, hence rank 1
                  PatSynCtxt _   -> rank1
@@ -676,7 +678,7 @@ check_type ve (CastTy ty _) = check_type ve ty
 check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
                           , ve_rank = rank, ve_expand = expand }) ty
   | not (null tvbs && null theta)
-  = do  { traceTc "check_type" (ppr ty $$ ppr (forAllAllowed rank))
+  = do  { traceTc "check_type" (ppr ty $$ ppr rank)
         ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty)
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
diff --git a/testsuite/tests/typecheck/should_fail/T17213.hs b/testsuite/tests/typecheck/should_fail/T17213.hs
new file mode 100644
index 0000000000..e9c093c903
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17213.hs
@@ -0,0 +1,5 @@
+module T17213 where
+
+import T17213a
+
+g = foo
diff --git a/testsuite/tests/typecheck/should_fail/T17213.stderr b/testsuite/tests/typecheck/should_fail/T17213.stderr
new file mode 100644
index 0000000000..1172992660
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17213.stderr
@@ -0,0 +1,6 @@
+
+T17213.hs:5:1: error:
+    • Illegal polymorphic type: forall a. a -> a
+      Perhaps you intended to use RankNTypes
+    • When checking the inferred type
+        g :: (forall a. a -> a) -> Int
diff --git a/testsuite/tests/typecheck/should_fail/T17213a.hs b/testsuite/tests/typecheck/should_fail/T17213a.hs
new file mode 100644
index 0000000000..48537600d5
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T17213a.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE RankNTypes #-}
+module T17213a where
+
+foo :: (forall a. a->a)-> Int
+foo x = error "ukr"
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4ccde2163f..6b66d41975 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -543,3 +543,4 @@ test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
 test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
 test('T13834', normal, compile_fail, [''])
 test('T17077', normal, compile_fail, [''])
+test('T17213', [extra_files(['T17213a.hs'])], multimod_compile_fail, ['T17213', '-v0'])