Commit af8897ac authored by dreixel's avatar dreixel
Browse files

Fix kind checking of tuples

Makes tcrun043 work again.
parent 2639f405
...@@ -1206,9 +1206,7 @@ zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker ...@@ -1206,9 +1206,7 @@ zonkTvCollecting :: TcRef TyVarSet -> UnboundTyVarZonker
-- Works on both types and kinds -- Works on both types and kinds
zonkTvCollecting unbound_tv_set tv zonkTvCollecting unbound_tv_set tv
= do { poly_kinds <- xoptM Opt_PolyKinds = do { poly_kinds <- xoptM Opt_PolyKinds
; if isKiVar tv && not poly_kinds then ; if isKiVar tv && not poly_kinds then defaultKindVarToStar tv
do { defaultKindVarToStar tv
; return liftedTypeKind }
else do else do
{ tv' <- zonkQuantifiedTyVar tv { tv' <- zonkQuantifiedTyVar tv
; tv_set <- readMutVar unbound_tv_set ; tv_set <- readMutVar unbound_tv_set
......
...@@ -67,7 +67,7 @@ import NameSet ...@@ -67,7 +67,7 @@ import NameSet
import TysWiredIn import TysWiredIn
import BasicTypes import BasicTypes
import SrcLoc import SrcLoc
import DynFlags ( ExtensionFlag( Opt_ConstraintKinds, Opt_PolyKinds ) ) import DynFlags ( ExtensionFlag( Opt_PolyKinds ) )
import Util import Util
import UniqSupply import UniqSupply
import Outputable import Outputable
...@@ -375,31 +375,60 @@ kc_hs_type (HsKindSig ty sig_k) exp_kind = do ...@@ -375,31 +375,60 @@ kc_hs_type (HsKindSig ty sig_k) exp_kind = do
return (HsKindSig ty' sig_k) return (HsKindSig ty' sig_k)
-- See Note [Distinguishing tuple kinds] in HsTypes -- See Note [Distinguishing tuple kinds] in HsTypes
kc_hs_type (HsTupleTy HsBoxedOrConstraintTuple tys) exp_kind@(EK exp_k _ctxt) kc_hs_type ty@(HsTupleTy HsBoxedOrConstraintTuple tys) exp_kind@(EK exp_k _ctxt)
= do { fact_tup_ok <- xoptM Opt_ConstraintKinds | isConstraintOrLiftedKind exp_k -- (NB: not zonking, to avoid left-right bias)
; let (k, tupleType) = if fact_tup_ok && isConstraintKind exp_k = do { tys' <- kcArgs (ptext (sLit "a tuple")) tys exp_k
then (constraintKind, HsConstraintTuple) ; return $ if isConstraintKind exp_k
-- If it's not a constraint, then it has to be * then HsTupleTy HsConstraintTuple tys'
-- Unboxed tuples are a separate case else HsTupleTy HsBoxedTuple tys' }
else (liftedTypeKind, HsBoxedTuple) | otherwise
; kc_hs_tuple_type tys tupleType k exp_kind } -- It is not clear from the context if it's * or Constraint,
-- so we infer the kind from the arguments
kc_hs_type (HsTupleTy HsBoxedTuple tys) exp_kind = do { k <- newMetaKindVar
= kc_hs_tuple_type tys HsBoxedTuple liftedTypeKind exp_kind ; tys' <- kcArgs (ptext (sLit "a tuple")) tys k
; k' <- zonkTcKind k
kc_hs_type (HsTupleTy HsConstraintTuple tys) exp_kind ; if isConstraintKind k'
= kc_hs_tuple_type tys HsConstraintTuple constraintKind exp_kind then do { checkExpectedKind ty k' exp_kind
; return (HsTupleTy HsConstraintTuple tys') }
-- JPM merge with kc_hs_tuple_type ? -- If it's not clear from the arguments that it's Constraint, then
kc_hs_type ty@(HsTupleTy HsUnboxedTuple tys) exp_kind -- it must be *. Check the arguments again to give good error messages
= do { tys' <- kcArgs (ptext (sLit "an unboxed tuple")) tys argTypeKind -- in eg. `(Maybe, Maybe)`
; checkExpectedKindS ty ubxTupleKind exp_kind else do { tys'' <- kcArgs (ptext (sLit "a tuple")) tys liftedTypeKind
; return (HsTupleTy HsUnboxedTuple tys') } ; checkExpectedKind ty liftedTypeKind exp_kind
; return (HsTupleTy HsBoxedTuple tys'') } }
{-
Note that we will still fail to infer the correct kind in this case:
type T a = ((a,a), D a)
type family D :: Constraint -> Constraint
While kind checking T, we do not yet know the kind of D, so we will default the
kind of T to * -> *. It works if we annotate `a` with kind `Constraint`.
-}
kc_hs_type ty@(HsTupleTy tup_sort tys) exp_kind
= do { tys' <- kcArgs cxt_doc tys arg_kind
; checkExpectedKind ty out_kind exp_kind
; return (HsTupleTy tup_sort tys') }
where
arg_kind = case tup_sort of
HsBoxedTuple -> liftedTypeKind
HsUnboxedTuple -> argTypeKind
HsConstraintTuple -> constraintKind
_ -> panic "kc_hs_type arg_kind"
out_kind = case tup_sort of
HsUnboxedTuple -> ubxTupleKind
_ -> arg_kind
cxt_doc = case tup_sort of
HsBoxedTuple -> ptext (sLit "a tuple")
HsUnboxedTuple -> ptext (sLit "an unboxed tuple")
HsConstraintTuple -> ptext (sLit "a constraint tuple")
_ -> panic "kc_hs_type tup_sort"
kc_hs_type ty@(HsFunTy ty1 ty2) exp_kind@(EK _ ctxt) = do kc_hs_type ty@(HsFunTy ty1 ty2) exp_kind@(EK _ ctxt) = do
ty1' <- kc_lhs_type ty1 (EK argTypeKind ctxt) ty1' <- kc_lhs_type ty1 (EK argTypeKind ctxt)
ty2' <- kc_lhs_type ty2 (EK openTypeKind ctxt) ty2' <- kc_lhs_type ty2 (EK openTypeKind ctxt)
checkExpectedKindS ty liftedTypeKind exp_kind checkExpectedKind ty liftedTypeKind exp_kind
return (HsFunTy ty1' ty2') return (HsFunTy ty1' ty2')
kc_hs_type ty@(HsOpTy ty1 (_, l_op@(L loc op)) ty2) exp_kind = do kc_hs_type ty@(HsOpTy ty1 (_, l_op@(L loc op)) ty2) exp_kind = do
...@@ -421,7 +450,7 @@ kc_hs_type ipTy@(HsIParamTy n ty) exp_kind = do ...@@ -421,7 +450,7 @@ kc_hs_type ipTy@(HsIParamTy n ty) exp_kind = do
ty' <- kc_lhs_type ty ty' <- kc_lhs_type ty
(EK liftedTypeKind (EK liftedTypeKind
(ptext (sLit "The type argument of the implicit parameter had"))) (ptext (sLit "The type argument of the implicit parameter had")))
checkExpectedKindS ipTy constraintKind exp_kind checkExpectedKind ipTy constraintKind exp_kind
return (HsIParamTy n ty') return (HsIParamTy n ty')
kc_hs_type ty@(HsEqTy ty1 ty2) exp_kind = do kc_hs_type ty@(HsEqTy ty1 ty2) exp_kind = do
...@@ -429,7 +458,7 @@ kc_hs_type ty@(HsEqTy ty1 ty2) exp_kind = do ...@@ -429,7 +458,7 @@ kc_hs_type ty@(HsEqTy ty1 ty2) exp_kind = do
(ty2', kind2) <- kc_lhs_type_fresh ty2 (ty2', kind2) <- kc_lhs_type_fresh ty2
checkExpectedKind ty2 kind2 checkExpectedKind ty2 kind2
(EK kind1 (ptext (sLit "The left argument of the equality predicate had"))) (EK kind1 (ptext (sLit "The left argument of the equality predicate had")))
checkExpectedKindS ty constraintKind exp_kind checkExpectedKind ty constraintKind exp_kind
return (HsEqTy ty1' ty2') return (HsEqTy ty1' ty2')
kc_hs_type (HsCoreTy ty) exp_kind = do kc_hs_type (HsCoreTy ty) exp_kind = do
...@@ -467,7 +496,7 @@ kc_hs_type ty@(HsRecTy _) _exp_kind ...@@ -467,7 +496,7 @@ kc_hs_type ty@(HsRecTy _) _exp_kind
#ifdef GHCI /* Only if bootstrapped */ #ifdef GHCI /* Only if bootstrapped */
kc_hs_type (HsSpliceTy sp fvs _) exp_kind = do kc_hs_type (HsSpliceTy sp fvs _) exp_kind = do
(ty, k) <- kcSpliceType sp fvs (ty, k) <- kcSpliceType sp fvs
checkExpectedKindS ty k exp_kind checkExpectedKind ty k exp_kind
return ty return ty
#else #else
kc_hs_type ty@(HsSpliceTy {}) _exp_kind = kc_hs_type ty@(HsSpliceTy {}) _exp_kind =
...@@ -485,27 +514,19 @@ kc_hs_type (HsDocTy ty _) exp_kind ...@@ -485,27 +514,19 @@ kc_hs_type (HsDocTy ty _) exp_kind
kc_hs_type ty@(HsExplicitListTy _k tys) exp_kind kc_hs_type ty@(HsExplicitListTy _k tys) exp_kind
= do { ty_k_s <- mapM kc_lhs_type_fresh tys = do { ty_k_s <- mapM kc_lhs_type_fresh tys
; kind <- unifyKinds (ptext (sLit "In a promoted list")) ty_k_s ; kind <- unifyKinds (ptext (sLit "In a promoted list")) ty_k_s
; checkExpectedKindS ty (mkListTy kind) exp_kind ; checkExpectedKind ty (mkListTy kind) exp_kind
; return (HsExplicitListTy kind (map fst ty_k_s)) } ; return (HsExplicitListTy kind (map fst ty_k_s)) }
kc_hs_type ty@(HsExplicitTupleTy _ tys) exp_kind = do kc_hs_type ty@(HsExplicitTupleTy _ tys) exp_kind = do
ty_k_s <- mapM kc_lhs_type_fresh tys ty_k_s <- mapM kc_lhs_type_fresh tys
let tupleKi = mkTyConApp (tupleTyCon BoxedTuple (length tys)) (map snd ty_k_s) let tupleKi = mkTyConApp (tupleTyCon BoxedTuple (length tys)) (map snd ty_k_s)
checkExpectedKindS ty tupleKi exp_kind checkExpectedKind ty tupleKi exp_kind
return (HsExplicitTupleTy (map snd ty_k_s) (map fst ty_k_s)) return (HsExplicitTupleTy (map snd ty_k_s) (map fst ty_k_s))
kc_hs_type (HsWrapTy {}) _exp_kind = kc_hs_type (HsWrapTy {}) _exp_kind =
panic "kc_hs_type HsWrapTy" -- We kind checked something twice panic "kc_hs_type HsWrapTy" -- We kind checked something twice
--------------------------- ---------------------------
kc_hs_tuple_type :: [LHsType Name] -> HsTupleSort -> Kind -> ExpKind
-> TcM (HsType Name)
kc_hs_tuple_type tys tuple_type kind exp_kind
= do { tys' <- kcArgs (ptext (sLit "a tuple")) tys kind
; let hsTupleTy = HsTupleTy tuple_type tys'
; checkExpectedKindS hsTupleTy kind exp_kind
; return hsTupleTy }
kcApps :: Outputable a kcApps :: Outputable a
=> a => a
-> TcKind -- Function kind -> TcKind -- Function kind
...@@ -523,7 +544,7 @@ kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name] ...@@ -523,7 +544,7 @@ kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
kcCheckApps the_fun fun_kind args ty exp_kind kcCheckApps the_fun fun_kind args ty exp_kind
= do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
; args_w_kinds' <- kc_lhs_types args_w_kinds ; args_w_kinds' <- kc_lhs_types args_w_kinds
; checkExpectedKindS ty res_kind exp_kind ; checkExpectedKind ty res_kind exp_kind
; return args_w_kinds' } ; return args_w_kinds' }
...@@ -1242,18 +1263,6 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt) = do ...@@ -1242,18 +1263,6 @@ checkExpectedKind ty act_kind ek@(EK exp_kind ek_ctxt) = do
ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)] ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
failWithTcM (env2, err $$ more_info) failWithTcM (env2, err $$ more_info)
-- We infer the kind of the type, and then complain if it's not right.
-- But we don't want to complain about
-- (ty) or !(ty) or forall a. ty
-- when the real difficulty is with the 'ty' part.
checkExpectedKindS :: HsType Name -> TcKind -> ExpKind -> TcM ()
checkExpectedKindS ty = checkExpectedKind (strip ty)
where
strip (HsParTy (L _ ty)) = strip ty
strip (HsBangTy _ (L _ ty)) = strip ty
strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
strip ty = ty
\end{code} \end{code}
%************************************************************************ %************************************************************************
......
...@@ -576,11 +576,12 @@ zonkTcPredType = zonkTcType ...@@ -576,11 +576,12 @@ zonkTcPredType = zonkTcType
are used at the end of type checking are used at the end of type checking
\begin{code} \begin{code}
defaultKindVarToStar :: TcTyVar -> TcM () defaultKindVarToStar :: TcTyVar -> TcM Kind
-- We have a meta-kind: unify it with '*' -- We have a meta-kind: unify it with '*'
defaultKindVarToStar kv defaultKindVarToStar kv
= ASSERT ( isKiVar kv && isMetaTyVar kv ) = do { ASSERT ( isKiVar kv && isMetaTyVar kv )
writeMetaTyVar kv liftedTypeKind writeMetaTyVar kv liftedTypeKind
; return liftedTypeKind }
zonkQuantifiedTyVars :: TcTyVarSet -> TcM [TcTyVar] zonkQuantifiedTyVars :: TcTyVarSet -> TcM [TcTyVar]
-- Precondition: a kind variable occurs before a type -- Precondition: a kind variable occurs before a type
...@@ -907,11 +908,12 @@ expectedKindInCtxt _ = Just argTypeKind ...@@ -907,11 +908,12 @@ expectedKindInCtxt _ = Just argTypeKind
checkValidType :: UserTypeCtxt -> Type -> TcM () checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context -- Checks that the type is valid for the given context
checkValidType ctxt ty = do checkValidType ctxt ty = do
traceTc "checkValidType" (ppr ty) traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
unboxed <- xoptM Opt_UnboxedTuples unboxed <- xoptM Opt_UnboxedTuples
rank2 <- xoptM Opt_Rank2Types rank2 <- xoptM Opt_Rank2Types
rankn <- xoptM Opt_RankNTypes rankn <- xoptM Opt_RankNTypes
polycomp <- xoptM Opt_PolymorphicComponents polycomp <- xoptM Opt_PolymorphicComponents
constraintKinds <- xoptM Opt_ConstraintKinds
let let
gen_rank n | rankn = ArbitraryRank gen_rank n | rankn = ArbitraryRank
| rank2 = Rank 2 | rank2 = Rank 2
...@@ -960,10 +962,12 @@ checkValidType ctxt ty = do ...@@ -960,10 +962,12 @@ checkValidType ctxt ty = do
-- Check that the thing has kind Type, and is lifted if necessary -- Check that the thing has kind Type, and is lifted if necessary
-- Do this second, because we can't usefully take the kind of an -- Do this second, because we can't usefully take the kind of an
-- ill-formed type such as (a~Int) -- ill-formed type such as (a~Int)
traceTc "checkValidType kind_ok ctxt" (ppr kind_ok $$ pprUserTypeCtxt ctxt)
checkTc kind_ok (kindErr actual_kind) checkTc kind_ok (kindErr actual_kind)
traceTc "checkValidType done" (ppr ty) -- Check that the thing does not have kind Constraint,
-- if -XConstraintKinds isn't enabled
unless constraintKinds
$ checkTc (not (isConstraintKind actual_kind)) (predTupleErr ty)
checkValidMonoType :: Type -> TcM () checkValidMonoType :: Type -> TcM ()
checkValidMonoType ty = check_mono_type MustBeMonoType ty checkValidMonoType ty = check_mono_type MustBeMonoType ty
......
...@@ -35,7 +35,8 @@ module Kind ( ...@@ -35,7 +35,8 @@ module Kind (
-- ** Predicates on Kinds -- ** Predicates on Kinds
isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind,
isUbxTupleKind, isArgTypeKind, isConstraintKind, isKind, isUbxTupleKind, isArgTypeKind, isConstraintKind,
isConstraintOrLiftedKind, isKind,
isSuperKind, noHashInKind, isSuperKind, noHashInKind,
isLiftedTypeKindCon, isConstraintKindCon, isLiftedTypeKindCon, isConstraintKindCon,
isAnyKind, isAnyKindCon, isAnyKind, isAnyKindCon,
...@@ -138,7 +139,7 @@ synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyV ...@@ -138,7 +139,7 @@ synTyConResKind tycon = kindAppResult (tyConKind tycon) (map mkTyVarTy (tyConTyV
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's -- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind, isUbxTupleKind, isOpenTypeKind, isArgTypeKind, isUnliftedTypeKind,
isConstraintKind, isAnyKind :: Kind -> Bool isConstraintKind, isAnyKind, isConstraintOrLiftedKind :: Kind -> Bool
isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon, isOpenTypeKindCon, isUbxTupleKindCon, isArgTypeKindCon,
isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon, isUnliftedTypeKindCon, isSubArgTypeKindCon, tcIsSubArgTypeKindCon,
...@@ -175,6 +176,9 @@ isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey ...@@ -175,6 +176,9 @@ isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
isConstraintKind (TyConApp tc _) = isConstraintKindCon tc isConstraintKind (TyConApp tc _) = isConstraintKindCon tc
isConstraintKind _ = False isConstraintKind _ = False
isConstraintOrLiftedKind (TyConApp tc _)
= isConstraintKindCon tc || isLiftedTypeKindCon tc
isConstraintOrLiftedKind _ = False
-- Subkinding -- Subkinding
-- The tc variants are used during type-checking, where we don't want the -- The tc variants are used during type-checking, where we don't want the
...@@ -288,8 +292,8 @@ defaultKind :: Kind -> Kind ...@@ -288,8 +292,8 @@ defaultKind :: Kind -> Kind
-- and the calling conventions differ. -- and the calling conventions differ.
-- This defaulting is done in TcMType.zonkTcTyVarBndr. -- This defaulting is done in TcMType.zonkTcTyVarBndr.
defaultKind k defaultKind k
| isSubOpenTypeKind k = liftedTypeKind | tcIsSubOpenTypeKind k = liftedTypeKind
| otherwise = k | otherwise = k
splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar]) splitKiTyVars :: [TyVar] -> ([KindVar], [TyVar])
-- Precondition: kind variables should precede type variables -- Precondition: kind variables should precede type variables
......
...@@ -824,14 +824,18 @@ Make PredTypes ...@@ -824,14 +824,18 @@ Make PredTypes
mkEqPred :: (Type, Type) -> PredType mkEqPred :: (Type, Type) -> PredType
mkEqPred (ty1, ty2) mkEqPred (ty1, ty2)
-- IA0_TODO: The caller should give the kind. -- IA0_TODO: The caller should give the kind.
= TyConApp eqTyCon [k, ty1, ty2] = WARN ( not (k `eqKind` defaultKind k), ppr (k, ty1, ty2) )
TyConApp eqTyCon [k, ty1, ty2]
where k = defaultKind (typeKind ty1) where k = defaultKind (typeKind ty1)
-- where k = typeKind ty1
mkPrimEqType :: (Type, Type) -> Type mkPrimEqType :: (Type, Type) -> Type
mkPrimEqType (ty1, ty2) mkPrimEqType (ty1, ty2)
-- IA0_TODO: The caller should give the kind. -- IA0_TODO: The caller should give the kind.
= TyConApp eqPrimTyCon [k, ty1, ty2] = WARN ( not (k `eqKind` defaultKind k), ppr (k, ty1, ty2) )
TyConApp eqPrimTyCon [k, ty1, ty2]
where k = defaultKind (typeKind ty1) where k = defaultKind (typeKind ty1)
-- where k = typeKind ty1
\end{code} \end{code}
--------------------- Implicit parameters --------------------------------- --------------------- Implicit parameters ---------------------------------
......
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