[commit: ghc] master: Set GenSigCtxt for the argument part of tcSubType (12c0f03)
git at git.haskell.org
git at git.haskell.org
Wed Jul 25 11:25:58 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/12c0f03a66bcd978bda6472384ddc0348c5a1d7a/ghc
>---------------------------------------------------------------
commit 12c0f03a66bcd978bda6472384ddc0348c5a1d7a
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Wed Jul 25 09:55:36 2018 +0100
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.
>---------------------------------------------------------------
12c0f03a66bcd978bda6472384ddc0348c5a1d7a
compiler/typecheck/TcUnify.hs | 32 ++++++++++++++++++++--
.../indexed-types/should_compile/Simple14.stderr | 4 +--
testsuite/tests/polykinds/T10503.stderr | 4 +--
testsuite/tests/polykinds/T9222.stderr | 2 +-
.../tests/typecheck/should_compile/T7220a.stderr | 8 +++---
testsuite/tests/typecheck/should_fail/T15438.hs | 8 ++++++
.../tests/typecheck/should_fail/T15438.stderr | 11 ++++++++
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 dcc185c..2ed861c 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 40d1d90..4c61d95 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 731a14b..2309cda 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 be80a79..94e0c16 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 a1e865f..2b311c1 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 0000000..0f99538
--- /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 0000000..473d5dc
--- /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 b357b55..9a042ec 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, [''])
More information about the ghc-commits
mailing list