Commit 12c0f03a authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 6c19112e
......@@ -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
......
......@@ -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:
......
......@@ -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:
......
......@@ -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
......
......@@ -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
{-# LANGUAGE MultiParamTypeClasses, RankNTypes #-}
module T15438 where
class C a b
foo :: (forall a b. C a b => b -> b) -> Int
foo = error "urk"
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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment