Set GenSigCtxt for the argument part of tcSubType

The reason for this change is described in TcUnify
Note [Settting the argument context], and Trac #15438.

The only effect is on error messages, where it stops GHC
reporting an outright falsity (about the type signature for
a function) when it finds an errors in a higher-rank situation.

The testsuite changes in this patch illustrate the problem.

8 files changed, 59 insertions, 11 deletions

diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index dcc185cb27..2ed861c327 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -758,8 +758,9 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
       | not (isPredTy act_arg)
       , not (isPredTy exp_arg)
       = -- See Note [Co/contra-variance of subsumption checking]
-        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt act_res exp_res
-           ; arg_wrap <- tc_sub_tc_type eq_orig given_orig ctxt exp_arg act_arg
+        do { res_wrap <- tc_sub_type_ds eq_orig inst_orig  ctxt       act_res exp_res
+           ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg
+                         -- GenSigCtxt: See Note [Setting the argument context]
            ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) }
                -- arg_wrap :: exp_arg ~> act_arg
                -- res_wrap :: act-res ~> exp_res
@@ -808,6 +809,33 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
      -- use versions without synonyms expanded
     unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected
 
+{- Note [Settting the argument context]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider we are doing the ambiguity check for the (bogus)
+  f :: (forall a b. C b => a -> a) -> Int
+
+We'll call
+   tcSubType ((forall a b. C b => a->a) -> Int )
+             ((forall a b. C b => a->a) -> Int )
+
+with a UserTypeCtxt of (FunSigCtxt "f").  Then we'll do the co/contra thing
+on the argument type of the (->) -- and at that point we want to switch
+to a UserTypeCtxt of GenSigCtxt.  Why?
+
+* Error messages.  If we stick with FunSigCtxt we get errors like
+     * Could not deduce: C b
+       from the context: C b0
+        bound by the type signature for:
+            f :: forall a b. C b => a->a
+  But of course f does not have that type signature!
+  Example tests: T10508, T7220a, Simple14
+
+* Implications. We may decide to build an implication for the whole
+  ambiguity check, but we don't need one for each level within it,
+  and TcUnify.alwaysBuildImplication checks the UserTypeCtxt.
+  See Note [When to build an implication]
+-}
+
 -----------------
 -- needs both un-type-checked (for origins) and type-checked (for wrapping)
 -- expressions
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index 40d1d90fb7..4c61d95cc9 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -3,8 +3,8 @@ Simple14.hs:8:8: error:
     • Couldn't match type ‘z0’ with ‘z’
         ‘z0’ is untouchable
           inside the constraints: x ~ y
-          bound by the type signature for:
-                     eqE :: (x ~ y) => EQ_ z0 z0
+          bound by a type expected by the context:
+                     (x ~ y) => EQ_ z0 z0
           at Simple14.hs:8:8-39
       ‘z’ is a rigid type variable bound by
         the type signature for:
diff --git a/testsuite/tests/polykinds/T10503.stderr b/testsuite/tests/polykinds/T10503.stderr
index 731a14b117..2309cdaaae 100644
--- a/testsuite/tests/polykinds/T10503.stderr
+++ b/testsuite/tests/polykinds/T10503.stderr
@@ -2,8 +2,8 @@
 T10503.hs:8:6: error:
     • Could not deduce: k ~ *
       from the context: Proxy 'KProxy ~ Proxy 'KProxy
-        bound by the type signature for:
-                   h :: (Proxy 'KProxy ~ Proxy 'KProxy) => r
+        bound by a type expected by the context:
+                   (Proxy 'KProxy ~ Proxy 'KProxy) => r
         at T10503.hs:8:6-85
       ‘k’ is a rigid type variable bound by
         the type signature for:
diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr
index be80a79198..94e0c16f95 100644
--- a/testsuite/tests/polykinds/T9222.stderr
+++ b/testsuite/tests/polykinds/T9222.stderr
@@ -3,7 +3,7 @@ T9222.hs:14:3: error:
     • Couldn't match type ‘c0’ with ‘c’
         ‘c0’ is untouchable
           inside the constraints: a ~ '(b0, c0)
-          bound by the type of the constructor ‘Want’:
+          bound by a type expected by the context:
                      (a ~ '(b0, c0)) => Proxy b0
           at T9222.hs:14:3-43
       ‘c’ is a rigid type variable bound by
diff --git a/testsuite/tests/typecheck/should_compile/T7220a.stderr b/testsuite/tests/typecheck/should_compile/T7220a.stderr
index a1e865f131..2b311c1111 100644
--- a/testsuite/tests/typecheck/should_compile/T7220a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T7220a.stderr
@@ -2,13 +2,13 @@
 T7220a.hs:17:6: error:
     • Could not deduce (C a b)
       from the context: (C a0 b, TF b ~ Y)
-        bound by the type signature for:
-                   f :: forall b. (C a0 b, TF b ~ Y) => b
+        bound by a type expected by the context:
+                   forall b. (C a0 b, TF b ~ Y) => b
         at T7220a.hs:17:6-44
       Possible fix:
         add (C a b) to the context of
-          the type signature for:
-            f :: forall b. (C a0 b, TF b ~ Y) => b
+          a type expected by the context:
+            forall b. (C a0 b, TF b ~ Y) => b
     • In the ambiguity check for ‘f’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       In the type signature: f :: (forall b. (C a b, TF b ~ Y) => b) -> X
diff --git a/testsuite/tests/typecheck/should_fail/T15438.hs b/testsuite/tests/typecheck/should_fail/T15438.hs
new file mode 100644
index 0000000000..0f995389a0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15438.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE  MultiParamTypeClasses, RankNTypes #-}
+
+module T15438 where
+
+class C a b
+
+foo :: (forall a b. C a b => b -> b) -> Int
+foo = error "urk"
diff --git a/testsuite/tests/typecheck/should_fail/T15438.stderr b/testsuite/tests/typecheck/should_fail/T15438.stderr
new file mode 100644
index 0000000000..473d5dcc98
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15438.stderr
@@ -0,0 +1,11 @@
+
+T15438.hs:7:8: error:
+    • Could not deduce (C a0 b)
+      from the context: C a b
+        bound by a type expected by the context:
+                   forall a b. C a b => b -> b
+        at T15438.hs:7:8-43
+      The type variable ‘a0’ is ambiguous
+    • In the ambiguity check for ‘foo’
+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
+      In the type signature: foo :: (forall a b. C a b => b -> b) -> Int
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index b357b55d57..9a042ec22f 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -475,3 +475,4 @@ test('T14904a', normal, compile_fail, [''])
 test('T14904b', normal, compile_fail, [''])
 test('T15067', normal, compile_fail, [''])
 test('T15330', normal, compile_fail, [''])
+test('T15438', normal, compile_fail, [''])