[commit: ghc] master: Fix typechecking of kind signatures (30b029b)
git at git.haskell.org
git at git.haskell.org
Mon Jun 18 07:23:57 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/30b029bea9abe1f5f2855d9e7f0ae26a18cf049b/ghc
>---------------------------------------------------------------
commit 30b029bea9abe1f5f2855d9e7f0ae26a18cf049b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Sat Jun 16 23:50:02 2018 +0100
Fix typechecking of kind signatures
When typechecking a type like
Maybe (a :: <kind-sig>)
with a kind signature, we were using tc_lhs_kind to
typecheck the signature. But that's utterly wrong; we
need the signature to be fully solid (non unresolved
equalities) before using it. In the case of Trac #14904
we went on to instantiate the kind signature, when it
still had embedded unsolved constraints. This tripped
the level-checking assertion when unifying a variable.
The fix looks pretty easy to me: just call tcLHsKind
instead. I had to add KindSigCtxt to
>---------------------------------------------------------------
30b029bea9abe1f5f2855d9e7f0ae26a18cf049b
compiler/typecheck/TcHsType.hs | 6 +++++-
compiler/typecheck/TcType.hs | 2 ++
compiler/typecheck/TcValidity.hs | 3 +++
testsuite/tests/indexed-types/should_fail/T14904.hs | 8 ++++++++
.../T14904b.stderr => indexed-types/should_fail/T14904.stderr} | 2 +-
testsuite/tests/indexed-types/should_fail/all.T | 1 +
6 files changed, 20 insertions(+), 2 deletions(-)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 03d3866..90fa869 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -587,7 +587,11 @@ tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
[lhs, rhs] }
tc_infer_hs_type mode (HsKindSig _ ty sig)
- = do { sig' <- tc_lhs_kind (kindLevel mode) sig
+ = do { sig' <- tcLHsKindSig KindSigCtxt sig
+ -- We must typeckeck the kind signature, and solve all
+ -- its equalities etc; from this point on we may do
+ -- things like instantiate its foralls, so it needs
+ -- to be fully determined (Trac #149904)
; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
; ty' <- tc_lhs_type mode ty sig'
; return (ty', sig') }
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 21d030c..26fc9fe 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -594,6 +594,7 @@ data UserTypeCtxt
| InfSigCtxt Name -- Inferred type for function
| ExprSigCtxt -- Expression type signature
+ | KindSigCtxt -- Kind signature
| TypeAppCtxt -- Visible type application
| ConArgCtxt Name -- Data constructor argument
| TySynCtxt Name -- RHS of a type synonym decl
@@ -644,6 +645,7 @@ pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (pp
pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n)
pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt = text "an expression type signature"
+pprUserTypeCtxt KindSigCtxt = text "a kind signature"
pprUserTypeCtxt TypeAppCtxt = text "a type argument"
pprUserTypeCtxt (ConArgCtxt c) = text "the type of the constructor" <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = text "the RHS of the type synonym" <+> quotes (ppr c)
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 6d866f7..0dc5664 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -336,6 +336,7 @@ checkValidType ctxt ty
TySynCtxt _ -> rank0
ExprSigCtxt -> rank1
+ KindSigCtxt -> rank1
TypeAppCtxt | impred_flag -> ArbitraryRank
| otherwise -> tyConArgMonoType
-- Normally, ImpredicativeTypes is handled in check_arg_type,
@@ -932,6 +933,8 @@ okIPCtxt (DataTyCtxt {}) = True
okIPCtxt (PatSynCtxt {}) = True
okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int
-- Trac #11466
+
+okIPCtxt (KindSigCtxt {}) = False
okIPCtxt (ClassSCCtxt {}) = False
okIPCtxt (InstDeclCtxt {}) = False
okIPCtxt (SpecInstCtxt {}) = False
diff --git a/testsuite/tests/indexed-types/should_fail/T14904.hs b/testsuite/tests/indexed-types/should_fail/T14904.hs
new file mode 100644
index 0000000..db7f1f4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T14904.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType, TypeFamilies, RankNTypes #-}
+
+module T14904 where
+
+import Data.Kind
+
+type family F f :: Type where
+ F ((f :: forall a. g a) :: forall a. g a) = Int
diff --git a/testsuite/tests/typecheck/should_fail/T14904b.stderr b/testsuite/tests/indexed-types/should_fail/T14904.stderr
similarity index 91%
copy from testsuite/tests/typecheck/should_fail/T14904b.stderr
copy to testsuite/tests/indexed-types/should_fail/T14904.stderr
index fff6942..dd5506c 100644
--- a/testsuite/tests/typecheck/should_fail/T14904b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14904.stderr
@@ -1,5 +1,5 @@
-T14904b.hs:9:7: error:
+T14904.hs:8:8: error:
• Expected kind ‘forall (a :: k1). g a’, but ‘f’ has kind ‘k0’
• In the first argument of ‘F’, namely
‘((f :: forall a. g a) :: forall a. g a)’
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index ef5eee2..b877555 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -144,3 +144,4 @@ test('T14179', normal, compile_fail, [''])
test('T14246', normal, compile_fail, [''])
test('T14369', normal, compile_fail, [''])
test('T15172', normal, compile_fail, [''])
+test('T14904', normal, compile_fail, [''])
More information about the ghc-commits
mailing list