Commit 30b029be authored by Simon Peyton Jones's avatar Simon Peyton Jones

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
parent 850ae8c5
......@@ -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') }
......
......@@ -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)
......
......@@ -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
......
{-# 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
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’
......@@ -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, [''])
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