diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-25 09:55:36 +0100 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-07-25 11:21:19 +0100 |
commit | 12c0f03a66bcd978bda6472384ddc0348c5a1d7a (patch) | |
tree | fd567fd38decce85f1d13bf50e1f72e2689cba6b | |
parent | 6c19112ece09a098c71faac1f7a58dbb1e63ee71 (diff) | |
download | haskell-12c0f03a66bcd978bda6472384ddc0348c5a1d7a.tar.gz |
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.
-rw-r--r-- | compiler/typecheck/TcUnify.hs | 32 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/Simple14.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T10503.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T9222.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T7220a.stderr | 8 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15438.hs | 8 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T15438.stderr | 11 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 1 |
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, ['']) |