Fix typechecking of kind signatures
authorSimon Peyton Jones <simonpj@microsoft.com>
Sat, 16 Jun 2018 22:50:02 +0000 (23:50 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 18 Jun 2018 07:23:17 +0000 (08:23 +0100)
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

compiler/typecheck/TcHsType.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/indexed-types/should_fail/T14904.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T14904.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/all.T

index 03d3866..90fa869 100644 (file)
@@ -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') }
index 21d030c..26fc9fe 100644 (file)
@@ -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)
index 6d866f7..0dc5664 100644 (file)
@@ -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 (file)
index 0000000..db7f1f4
--- /dev/null
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType, TypeFamilies, RankNTypes #-}\r
+\r
+module T14904 where\r
+\r
+import Data.Kind\r
+\r
+type family F f :: Type where\r
+   F ((f :: forall a. g a) :: forall a. g a) = Int\r
diff --git a/testsuite/tests/indexed-types/should_fail/T14904.stderr b/testsuite/tests/indexed-types/should_fail/T14904.stderr
new file mode 100644 (file)
index 0000000..dd5506c
--- /dev/null
@@ -0,0 +1,6 @@
+
+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)’
+      In the type family declaration for ‘F’
index ef5eee2..b877555 100644 (file)
@@ -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, [''])