-- Kind checking
kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
- kcCheckHsType, kcHsContext, kcHsType,
+ kcLHsType, kcCheckLHsType, kcHsContext,
-- Typechecking kinded types
tcHsKindedContext, tcHsKindedType, tcHsBangType,
tcTyVarBndrs, dsHsType, tcLHsConResTy,
- tcDataKindSig,
+ tcDataKindSig, ExpKind(..), EkCtxt(..),
-- Pattern type signatures
tcHsPatSigType, tcPatSig
import TcType
import {- Kind parts of -} Type
import Var
+import Coercion
import TyCon
import Class
import Name
import SrcLoc
import UniqSupply
import Outputable
+import FastString
+
+import Control.Monad
\end{code}
do { kinded_ty <- kcTypeType hs_ty
; ty <- tcHsKindedType kinded_ty
; checkValidType ctxt ty
- ; returnM ty }
+ ; return ty }
tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
-- Typecheck an instance head. We can't use
; return (tvs, ty) } }
-- Used for the deriving(...) items
-tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
-tcHsDeriv = addLocM (tc_hs_deriv [])
+tcHsDeriv :: HsType Name -> TcM ([TyVar], Class, [Type])
+tcHsDeriv = tc_hs_deriv []
+tc_hs_deriv :: [LHsTyVarBndr Name] -> HsType Name
+ -> TcM ([TyVar], Class, [Type])
tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
= kcHsTyVars tv_names $ \ tv_names' ->
do { cls_kind <- kcClass cls_name
- ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
+ ; (tys, _res_kind) <- kcApps cls_name cls_kind hs_tys
; tcTyVarBndrs tv_names' $ \ tyvars ->
do { arg_tys <- dsHsTypes tys
; cls <- tcLookupClass cls_name
tc_hs_deriv (tv_names1 ++ tv_names2) ty
tc_hs_deriv _ other
- = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
+ = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr other)
\end{code}
These functions are used during knot-tying in
\begin{code}
kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
-- Used for type signatures
-kcHsSigType ty = kcTypeType ty
-kcHsLiftedSigType ty = kcLiftedType ty
+kcHsSigType ty = addKcTypeCtxt ty $ kcTypeType ty
+kcHsLiftedSigType ty = addKcTypeCtxt ty $ kcLiftedType ty
tcHsKindedType :: LHsType Name -> TcM Type
-- Don't do kind checking, nor validity checking.
tcHsBangType :: LHsType Name -> TcM Type
-- Permit a bang, but discard it
-tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
-tcHsBangType ty = tcHsKindedType ty
+tcHsBangType (L _ (HsBangTy _ ty)) = tcHsKindedType ty
+tcHsBangType ty = tcHsKindedType ty
tcHsKindedContext :: LHsContext Name -> TcM ThetaType
-- Used when we are expecting a ClassContext (i.e. no implicit params)
-- Does not do validity checking, like tcHsKindedType
-tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
+tcHsKindedContext hs_theta = addLocM (mapM dsHsLPred) hs_theta
\end{code}
---------------------------
kcLiftedType :: LHsType Name -> TcM (LHsType Name)
-- The type ty must be a *lifted* *type*
-kcLiftedType ty = kcCheckHsType ty liftedTypeKind
+kcLiftedType ty = kc_check_lhs_type ty ekLifted
---------------------------
kcTypeType :: LHsType Name -> TcM (LHsType Name)
-- The type ty must be a *type*, but it can be lifted or
-- unlifted or an unboxed tuple.
-kcTypeType ty = kcCheckHsType ty openTypeKind
+kcTypeType ty = kc_check_lhs_type ty ekOpen
---------------------------
-kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
+kcCheckLHsType :: LHsType Name -> ExpKind -> TcM (LHsType Name)
+kcCheckLHsType ty kind = addKcTypeCtxt ty $ kc_check_lhs_type ty kind
+
+
+kc_check_lhs_type :: LHsType Name -> ExpKind -> TcM (LHsType Name)
-- Check that the type has the specified kind
-- Be sure to use checkExpectedKind, rather than simply unifying
-- with OpenTypeKind, because it gives better error messages
-kcCheckHsType (L span ty) exp_kind
- = setSrcSpan span $
- do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
+kc_check_lhs_type (L span ty) exp_kind
+ = setSrcSpan span $
+ do { ty' <- kc_check_hs_type ty exp_kind
+ ; return (L span ty') }
+
+kc_check_lhs_types :: [(LHsType Name, ExpKind)] -> TcM [LHsType Name]
+kc_check_lhs_types tys_w_kinds
+ = mapM kc_arg tys_w_kinds
+ where
+ kc_arg (arg, arg_kind) = kc_check_lhs_type arg arg_kind
+
+
+---------------------------
+kc_check_hs_type :: HsType Name -> ExpKind -> TcM (HsType Name)
+
+-- First some special cases for better error messages
+-- when we know the expected kind
+kc_check_hs_type (HsParTy ty) exp_kind
+ = do { ty' <- kc_check_lhs_type ty exp_kind; return (HsParTy ty') }
+
+kc_check_hs_type ty@(HsAppTy ty1 ty2) exp_kind
+ = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
+ ; (fun_ty', fun_kind) <- kc_lhs_type fun_ty
+ ; arg_tys' <- kcCheckApps fun_ty fun_kind arg_tys ty exp_kind
+ ; return (mkHsAppTys fun_ty' arg_tys') }
+
+kc_check_hs_type ty@(HsPredTy (HsClassP cls tys)) exp_kind
+ = do { cls_kind <- kcClass cls
+ ; tys' <- kcCheckApps cls cls_kind tys ty exp_kind
+ ; return (HsPredTy (HsClassP cls tys')) }
+
+-- This is the general case: infer the kind and compare
+kc_check_hs_type ty exp_kind
+ = do { (ty', act_kind) <- kc_hs_type ty
-- Add the context round the inner check only
-- because checkExpectedKind already mentions
-- 'ty' by name in any error message
; checkExpectedKind (strip ty) act_kind exp_kind
- ; return (L span ty') }
+ ; return ty' }
where
- -- Wrap a context around only if we want to show that contexts.
- add_ctxt (HsPredTy p) thing = thing
- -- Omit invisble ones and ones user's won't grok (HsPred p).
- add_ctxt (HsForAllTy _ _ (L _ []) _) thing = thing
- -- Omit wrapping if the theta-part is empty
- -- Reason: the recursive call to kcLiftedType, in the ForAllTy
- -- case of kc_hs_type, will do the wrapping instead
- -- and we don't want to duplicate
- add_ctxt other_ty thing = addErrCtxt (typeCtxt other_ty) thing
-
-- 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
strip (HsBangTy _ (L _ ty)) = strip ty
strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
strip ty = ty
+
\end{code}
Here comes the main function
\begin{code}
-kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
-kcHsType ty = wrapLocFstM kc_hs_type ty
--- kcHsType *returns* the kind of the type, rather than taking an expected
+kcLHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
+-- Called from outside: set the context
+kcLHsType ty = addKcTypeCtxt ty (kc_lhs_type ty)
+
+kc_lhs_type :: LHsType Name -> TcM (LHsType Name, TcKind)
+kc_lhs_type (L span ty)
+ = setSrcSpan span $
+ do { (ty', kind) <- kc_hs_type ty
+ ; return (L span ty', kind) }
+
+-- kc_hs_type *returns* the kind of the type, rather than taking an expected
-- kind as argument as tcExpr does.
-- Reasons:
-- (a) the kind of (->) is
--
-- The translated type has explicitly-kinded type-variable binders
-kc_hs_type (HsParTy ty)
- = kcHsType ty `thenM` \ (ty', kind) ->
- returnM (HsParTy ty', kind)
+kc_hs_type :: HsType Name -> TcM (HsType Name, TcKind)
+kc_hs_type (HsParTy ty) = do
+ (ty', kind) <- kc_lhs_type ty
+ return (HsParTy ty', kind)
-kc_hs_type (HsTyVar name)
- = kcTyVar name `thenM` \ kind ->
- returnM (HsTyVar name, kind)
+kc_hs_type (HsTyVar name) = do
+ kind <- kcTyVar name
+ return (HsTyVar name, kind)
-kc_hs_type (HsListTy ty)
- = kcLiftedType ty `thenM` \ ty' ->
- returnM (HsListTy ty', liftedTypeKind)
+kc_hs_type (HsListTy ty) = do
+ ty' <- kcLiftedType ty
+ return (HsListTy ty', liftedTypeKind)
-kc_hs_type (HsPArrTy ty)
- = kcLiftedType ty `thenM` \ ty' ->
- returnM (HsPArrTy ty', liftedTypeKind)
+kc_hs_type (HsPArrTy ty) = do
+ ty' <- kcLiftedType ty
+ return (HsPArrTy ty', liftedTypeKind)
kc_hs_type (HsNumTy n)
- = returnM (HsNumTy n, liftedTypeKind)
-
-kc_hs_type (HsKindSig ty k)
- = kcCheckHsType ty k `thenM` \ ty' ->
- returnM (HsKindSig ty' k, k)
-
-kc_hs_type (HsTupleTy Boxed tys)
- = mappM kcLiftedType tys `thenM` \ tys' ->
- returnM (HsTupleTy Boxed tys', liftedTypeKind)
-
-kc_hs_type (HsTupleTy Unboxed tys)
- = mappM kcTypeType tys `thenM` \ tys' ->
- returnM (HsTupleTy Unboxed tys', ubxTupleKind)
-
-kc_hs_type (HsFunTy ty1 ty2)
- = kcCheckHsType ty1 argTypeKind `thenM` \ ty1' ->
- kcTypeType ty2 `thenM` \ ty2' ->
- returnM (HsFunTy ty1' ty2', liftedTypeKind)
-
-kc_hs_type ty@(HsOpTy ty1 op ty2)
- = addLocM kcTyVar op `thenM` \ op_kind ->
- kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
- returnM (HsOpTy ty1' op ty2', res_kind)
-
-kc_hs_type ty@(HsAppTy ty1 ty2)
- = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
- kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
- returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
+ = return (HsNumTy n, liftedTypeKind)
+
+kc_hs_type (HsKindSig ty k) = do
+ ty' <- kc_check_lhs_type ty (EK k EkKindSig)
+ return (HsKindSig ty' k, k)
+
+kc_hs_type (HsTupleTy Boxed tys) = do
+ tys' <- mapM kcLiftedType tys
+ return (HsTupleTy Boxed tys', liftedTypeKind)
+
+kc_hs_type (HsTupleTy Unboxed tys) = do
+ tys' <- mapM kcTypeType tys
+ return (HsTupleTy Unboxed tys', ubxTupleKind)
+
+kc_hs_type (HsFunTy ty1 ty2) = do
+ ty1' <- kc_check_lhs_type ty1 (EK argTypeKind EkUnk)
+ ty2' <- kcTypeType ty2
+ return (HsFunTy ty1' ty2', liftedTypeKind)
+
+kc_hs_type (HsOpTy ty1 op ty2) = do
+ op_kind <- addLocM kcTyVar op
+ ([ty1',ty2'], res_kind) <- kcApps op op_kind [ty1,ty2]
+ return (HsOpTy ty1' op ty2', res_kind)
+
+kc_hs_type (HsAppTy ty1 ty2) = do
+ (fun_ty', fun_kind) <- kc_lhs_type fun_ty
+ (arg_tys', res_kind) <- kcApps fun_ty fun_kind arg_tys
+ return (mkHsAppTys fun_ty' arg_tys', res_kind)
where
- (fun_ty, arg_tys) = split ty1 [ty2]
- split (L _ (HsAppTy f a)) as = split f (a:as)
- split f as = (f,as)
- mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
- -- the application; they are never used
-
-kc_hs_type (HsPredTy pred)
- = kcHsPred pred `thenM` \ pred' ->
- returnM (HsPredTy pred', liftedTypeKind)
+ (fun_ty, arg_tys) = splitHsAppTys ty1 ty2
+
+kc_hs_type (HsPredTy (HsEqualP _ _))
+ = wrongEqualityErr
+
+kc_hs_type (HsPredTy pred) = do
+ pred' <- kcHsPred pred
+ return (HsPredTy pred', liftedTypeKind)
kc_hs_type (HsForAllTy exp tv_names context ty)
- = kcHsTyVars tv_names $ \ tv_names' ->
+ = kcHsTyVars tv_names $ \ tv_names' ->
do { ctxt' <- kcHsContext context
; ty' <- kcLiftedType ty
-- The body of a forall is usually a type, but in principle
; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
-kc_hs_type (HsBangTy b ty)
- = do { (ty', kind) <- kcHsType ty
- ; return (HsBangTy b ty', kind) }
+kc_hs_type (HsBangTy b ty) = do
+ (ty', kind) <- kc_lhs_type ty
+ return (HsBangTy b ty', kind)
kc_hs_type ty@(HsSpliceTy _)
- = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
+ = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
-- remove the doc nodes here, no need to worry about the location since
-- its the same for a doc node and it's child type node
= kc_hs_type (unLoc ty)
---------------------------
-kcApps :: TcKind -- Function kind
- -> SDoc -- Function
+kcApps :: Outputable a
+ => a
+ -> TcKind -- Function kind
-> [LHsType Name] -- Arg types
-> TcM ([LHsType Name], TcKind) -- Kind-checked args
-kcApps fun_kind ppr_fun args
- = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
- zipWithM kc_arg args arg_kinds `thenM` \ args' ->
- returnM (args', res_kind)
+kcApps the_fun fun_kind args
+ = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
+ ; args' <- kc_check_lhs_types args_w_kinds
+ ; return (args', res_kind) }
+
+kcCheckApps :: Outputable a => a -> TcKind -> [LHsType Name]
+ -> HsType Name -- The type being checked (for err messages only)
+ -> ExpKind -- Expected kind
+ -> TcM [LHsType Name]
+kcCheckApps the_fun fun_kind args ty exp_kind
+ = do { (args_w_kinds, res_kind) <- splitFunKind (ppr the_fun) 1 fun_kind args
+ ; checkExpectedKind ty res_kind exp_kind
+ -- Check the result kind *before* checking argument kinds
+ -- This improves error message; Trac #2994
+ ; kc_check_lhs_types args_w_kinds }
+
+splitHsAppTys :: LHsType Name -> LHsType Name -> (LHsType Name, [LHsType Name])
+splitHsAppTys fun_ty arg_ty = split fun_ty [arg_ty]
where
- split_fk fk 0 = returnM ([], fk)
- split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
- case mb_fk of
- Nothing -> failWithTc too_many_args
- Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
- returnM (ak:aks, rk)
+ split (L _ (HsAppTy f a)) as = split f (a:as)
+ split f as = (f,as)
- kc_arg arg arg_kind = kcCheckHsType arg arg_kind
+mkHsAppTys :: LHsType Name -> [LHsType Name] -> HsType Name
+mkHsAppTys fun_ty [] = pprPanic "mkHsAppTys" (ppr fun_ty)
+mkHsAppTys fun_ty (arg_ty:arg_tys)
+ = foldl mk_app (HsAppTy fun_ty arg_ty) arg_tys
+ where
+ mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
+ -- the application; they are
+ -- never used
- too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
- ptext SLIT("is applied to too many type arguments")
+---------------------------
+splitFunKind :: SDoc -> Int -> TcKind -> [b] -> TcM ([(b,ExpKind)], TcKind)
+splitFunKind _ _ fk [] = return ([], fk)
+splitFunKind the_fun arg_no fk (arg:args)
+ = do { mb_fk <- unifyFunKind fk
+ ; case mb_fk of
+ Nothing -> failWithTc too_many_args
+ Just (ak,fk') -> do { (aks, rk) <- splitFunKind the_fun (arg_no+1) fk' args
+ ; return ((arg, EK ak (EkArg the_fun arg_no)):aks, rk) } }
+ where
+ too_many_args = quotes the_fun <+>
+ ptext (sLit "is applied to too many type arguments")
---------------------------
kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
-kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
+kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
kcHsLPred = wrapLocM kcHsPred
kcHsPred :: HsPred Name -> TcM (HsPred Name)
-kcHsPred pred -- Checks that the result is of kind liftedType
- = kc_pred pred `thenM` \ (pred', kind) ->
- checkExpectedKind pred kind liftedTypeKind `thenM_`
- returnM pred'
+kcHsPred pred = do -- Checks that the result is of kind liftedType
+ (pred', kind) <- kc_pred pred
+ checkExpectedKind pred kind ekLifted
+ return pred'
---------------------------
kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
-- Does *not* check for a saturated
-- application (reason: used from TcDeriv)
-kc_pred pred@(HsIParam name ty)
- = do { (ty', kind) <- kcHsType ty
- ; returnM (HsIParam name ty', kind)
+kc_pred (HsIParam name ty)
+ = do { (ty', kind) <- kc_lhs_type ty
+ ; return (HsIParam name ty', kind)
}
-kc_pred pred@(HsClassP cls tys)
+kc_pred (HsClassP cls tys)
= do { kind <- kcClass cls
- ; (tys', res_kind) <- kcApps kind (ppr cls) tys
- ; returnM (HsClassP cls tys', res_kind)
+ ; (tys', res_kind) <- kcApps cls kind tys
+ ; return (HsClassP cls tys', res_kind)
}
-kc_pred pred@(HsEqualP ty1 ty2)
- = do { (ty1', kind1) <- kcHsType ty1
- ; checkExpectedKind ty1 kind1 liftedTypeKind
- ; (ty2', kind2) <- kcHsType ty2
- ; checkExpectedKind ty2 kind2 liftedTypeKind
- ; returnM (HsEqualP ty1 ty2, liftedTypeKind)
+kc_pred (HsEqualP ty1 ty2)
+ = do { (ty1', kind1) <- kc_lhs_type ty1
+-- ; checkExpectedKind ty1 kind1 liftedTypeKind
+ ; (ty2', kind2) <- kc_lhs_type ty2
+-- ; checkExpectedKind ty2 kind2 liftedTypeKind
+ ; checkExpectedKind ty2 kind2 (EK kind1 EkEqPred)
+ ; return (HsEqualP ty1' ty2', liftedTypeKind)
}
---------------------------
kcTyVar :: Name -> TcM TcKind
-kcTyVar name -- Could be a tyvar or a tycon
- = traceTc (text "lk1" <+> ppr name) `thenM_`
- tcLookup name `thenM` \ thing ->
- traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
+kcTyVar name = do -- Could be a tyvar or a tycon
+ traceTc (text "lk1" <+> ppr name)
+ thing <- tcLookup name
+ traceTc (text "lk2" <+> ppr name <+> ppr thing)
case thing of
- ATyVar _ ty -> returnM (typeKind ty)
- AThing kind -> returnM kind
- AGlobal (ATyCon tc) -> returnM (tyConKind tc)
- other -> wrongThingErr "type" thing name
+ ATyVar _ ty -> return (typeKind ty)
+ AThing kind -> return kind
+ AGlobal (ATyCon tc) -> return (tyConKind tc)
+ _ -> wrongThingErr "type" thing name
kcClass :: Name -> TcM TcKind
-kcClass cls -- Must be a class
- = tcLookup cls `thenM` \ thing ->
+kcClass cls = do -- Must be a class
+ thing <- tcLookup cls
case thing of
- AThing kind -> returnM kind
- AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
- other -> wrongThingErr "class" thing cls
+ AThing kind -> return kind
+ AGlobal (AClass cls) -> return (tyConKind (classTyCon cls))
+ _ -> wrongThingErr "class" thing cls
\end{code}
-- All HsTyVarBndrs in the intput type are kind-annotated
dsHsType ty = ds_type (unLoc ty)
-ds_type ty@(HsTyVar name)
+ds_type :: HsType Name -> TcM Type
+ds_type ty@(HsTyVar _)
= ds_app ty []
ds_type (HsParTy ty) -- Remove the parentheses markers
= dsHsType ty
ds_type ty@(HsBangTy _ _) -- No bangs should be here
- = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
+ = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
-ds_type (HsKindSig ty k)
+ds_type (HsKindSig ty _)
= dsHsType ty -- Kind checking done already
-ds_type (HsListTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
- checkWiredInTyCon listTyCon `thenM_`
- returnM (mkListTy tau_ty)
+ds_type (HsListTy ty) = do
+ tau_ty <- dsHsType ty
+ checkWiredInTyCon listTyCon
+ return (mkListTy tau_ty)
-ds_type (HsPArrTy ty)
- = dsHsType ty `thenM` \ tau_ty ->
- checkWiredInTyCon parrTyCon `thenM_`
- returnM (mkPArrTy tau_ty)
+ds_type (HsPArrTy ty) = do
+ tau_ty <- dsHsType ty
+ checkWiredInTyCon parrTyCon
+ return (mkPArrTy tau_ty)
-ds_type (HsTupleTy boxity tys)
- = dsHsTypes tys `thenM` \ tau_tys ->
- checkWiredInTyCon tycon `thenM_`
- returnM (mkTyConApp tycon tau_tys)
+ds_type (HsTupleTy boxity tys) = do
+ tau_tys <- dsHsTypes tys
+ checkWiredInTyCon tycon
+ return (mkTyConApp tycon tau_tys)
where
tycon = tupleTyCon boxity (length tys)
-ds_type (HsFunTy ty1 ty2)
- = dsHsType ty1 `thenM` \ tau_ty1 ->
- dsHsType ty2 `thenM` \ tau_ty2 ->
- returnM (mkFunTy tau_ty1 tau_ty2)
+ds_type (HsFunTy ty1 ty2) = do
+ tau_ty1 <- dsHsType ty1
+ tau_ty2 <- dsHsType ty2
+ return (mkFunTy tau_ty1 tau_ty2)
-ds_type (HsOpTy ty1 (L span op) ty2)
- = dsHsType ty1 `thenM` \ tau_ty1 ->
- dsHsType ty2 `thenM` \ tau_ty2 ->
+ds_type (HsOpTy ty1 (L span op) ty2) = do
+ tau_ty1 <- dsHsType ty1
+ tau_ty2 <- dsHsType ty2
setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
ds_type (HsNumTy n)
- = ASSERT(n==1)
- tcLookupTyCon genUnitTyConName `thenM` \ tc ->
- returnM (mkTyConApp tc [])
+ = ASSERT(n==1) do
+ tc <- tcLookupTyCon genUnitTyConName
+ return (mkTyConApp tc [])
ds_type ty@(HsAppTy _ _)
= ds_app ty []
-ds_type (HsPredTy pred)
- = dsHsPred pred `thenM` \ pred' ->
- returnM (mkPredTy pred')
+ds_type (HsPredTy pred) = do
+ pred' <- dsHsPred pred
+ return (mkPredTy pred')
-ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
- = tcTyVarBndrs tv_names $ \ tyvars ->
- mappM dsHsLPred (unLoc ctxt) `thenM` \ theta ->
- dsHsType ty `thenM` \ tau ->
- returnM (mkSigmaTy tyvars theta tau)
+ds_type (HsForAllTy _ tv_names ctxt ty)
+ = tcTyVarBndrs tv_names $ \ tyvars -> do
+ theta <- mapM dsHsLPred (unLoc ctxt)
+ tau <- dsHsType ty
+ return (mkSigmaTy tyvars theta tau)
ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
ds_type (HsDocTy ty _) -- Remove the doc comment
= dsHsType ty
-dsHsTypes arg_tys = mappM dsHsType arg_tys
+dsHsTypes :: [LHsType Name] -> TcM [Type]
+dsHsTypes arg_tys = mapM dsHsType arg_tys
\end{code}
Help functions for type applications
ds_app (HsAppTy ty1 ty2) tys
= ds_app (unLoc ty1) (ty2:tys)
-ds_app ty tys
- = dsHsTypes tys `thenM` \ arg_tys ->
+ds_app ty tys = do
+ arg_tys <- dsHsTypes tys
case ty of
HsTyVar fun -> ds_var_app fun arg_tys
- other -> ds_type ty `thenM` \ fun_ty ->
- returnM (mkAppTys fun_ty arg_tys)
+ _ -> do fun_ty <- ds_type ty
+ return (mkAppTys fun_ty arg_tys)
ds_var_app :: Name -> [Type] -> TcM Type
-ds_var_app name arg_tys
- = tcLookup name `thenM` \ thing ->
+ds_var_app name arg_tys = do
+ thing <- tcLookup name
case thing of
- ATyVar _ ty -> returnM (mkAppTys ty arg_tys)
- AGlobal (ATyCon tc) -> returnM (mkTyConApp tc arg_tys)
- other -> wrongThingErr "type" thing name
+ ATyVar _ ty -> return (mkAppTys ty arg_tys)
+ AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
+ _ -> wrongThingErr "type" thing name
\end{code}
dsHsLPred :: LHsPred Name -> TcM PredType
dsHsLPred pred = dsHsPred (unLoc pred)
-dsHsPred pred@(HsClassP class_name tys)
+dsHsPred :: HsPred Name -> TcM PredType
+dsHsPred (HsClassP class_name tys)
= do { arg_tys <- dsHsTypes tys
; clas <- tcLookupClass class_name
- ; returnM (ClassP clas arg_tys)
+ ; return (ClassP clas arg_tys)
}
-dsHsPred pred@(HsEqualP ty1 ty2)
+dsHsPred (HsEqualP ty1 ty2)
= do { arg_ty1 <- dsHsType ty1
; arg_ty2 <- dsHsType ty2
- ; returnM (EqPred arg_ty1 arg_ty2)
+ ; return (EqPred arg_ty1 arg_ty2)
}
dsHsPred (HsIParam name ty)
= do { arg_ty <- dsHsType ty
- ; returnM (IParam name arg_ty)
+ ; return (IParam name arg_ty)
}
\end{code}
\begin{code}
tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
-tcLHsConResTy res_ty
- = addErrCtxt (gadtResCtxt res_ty) $
- case get_largs res_ty [] of
+tcLHsConResTy (L span res_ty)
+ = setSrcSpan span $
+ case get_args res_ty [] of
(HsTyVar tc_name, args)
-> do { args' <- mapM dsHsType args
; thing <- tcLookup tc_name
; case thing of
AGlobal (ATyCon tc) -> return (tc, args')
- other -> failWithTc (badGadtDecl res_ty) }
- other -> failWithTc (badGadtDecl res_ty)
+ _ -> failWithTc (badGadtDecl res_ty) }
+ _ -> failWithTc (badGadtDecl res_ty)
where
-- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
-- because that causes a black hole, and for good reason. Building
-- the type means expanding type synonyms, and we can't do that
-- inside the "knot". So we have to work by steam.
- get_largs (L _ ty) args = get_args ty args
- get_args (HsAppTy fun arg) args = get_largs fun (arg:args)
- get_args (HsParTy ty) args = get_largs ty args
- get_args (HsOpTy ty1 (L span tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
- get_args ty args = (ty, args)
-
-gadtResCtxt ty
- = hang (ptext SLIT("In the result type of a data constructor:"))
- 2 (ppr ty)
+ get_args (HsAppTy (L _ fun) arg) args = get_args fun (arg:args)
+ get_args (HsParTy (L _ ty)) args = get_args ty args
+ get_args (HsOpTy ty1 (L _ tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
+ get_args ty args = (ty, args)
+
+badGadtDecl :: HsType Name -> SDoc
badGadtDecl ty
- = hang (ptext SLIT("Malformed constructor result type:"))
+ = hang (ptext (sLit "Malformed constructor result type:"))
2 (ppr ty)
-typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
+addKcTypeCtxt :: LHsType Name -> TcM a -> TcM a
+ -- Wrap a context around only if we want to show that contexts.
+addKcTypeCtxt (L _ (HsPredTy _)) thing = thing
+ -- Omit invisble ones and ones user's won't grok (HsPred p).
+addKcTypeCtxt (L _ other_ty) thing = addErrCtxt (typeCtxt other_ty) thing
+
+typeCtxt :: HsType Name -> SDoc
+typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
\end{code}
%************************************************************************
-> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
-- They scope over the thing inside
-> TcM r
-kcHsTyVars tvs thing_inside
- = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
+kcHsTyVars tvs thing_inside = do
+ bndrs <- mapM (wrapLocM kcHsTyVar) tvs
tcExtendKindEnvTvs bndrs (thing_inside bndrs)
kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
-- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
-kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
- returnM (KindedTyVar name kind)
-kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
+kcHsTyVar (UserTyVar name) = KindedTyVar name <$> newKindVar
+kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
------------------
tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
-> TcM r
-- Used when type-checking types/classes/type-decls
-- Brings into scope immutable TyVars, not mutable ones that require later zonking
-tcTyVarBndrs bndrs thing_inside
- = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
+tcTyVarBndrs bndrs thing_inside = do
+ tyvars <- mapM (zonk . unLoc) bndrs
tcExtendTyVarEnv tyvars (thing_inside tyvars)
where
zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
; return (mkTyVar name kind') }
- zonk (UserTyVar name) = WARN( True, ptext SLIT("Un-kinded tyvar") <+> ppr name )
+ zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
return (mkTyVar name liftedTypeKind)
-----------------------------------
= do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
; span <- getSrcSpanM
; us <- newUniqueSupply
- ; let loc = srcSpanStart span
- uniqs = uniqsFromSupply us
- ; return [ mk_tv loc uniq str kind
- | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
+ ; let uniqs = uniqsFromSupply us
+ ; return [ mk_tv span uniq str kind
+ | ((kind, str), uniq) <- arg_kinds `zip` dnames `zip` uniqs ] }
where
(arg_kinds, res_kind) = splitKindFunTys kind
mk_tv loc uniq str kind = mkTyVar name kind
where
name = mkInternalName uniq occ loc
occ = mkOccName tvName str
+
+ dnames = map ('$' :) names -- Note [Avoid name clashes for associated data types]
- names :: [String] -- a,b,c...aa,ab,ac etc
+ names :: [String]
names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
badKindSig :: Kind -> SDoc
badKindSig kind
- = hang (ptext SLIT("Kind signature on data type declaration has non-* return kind"))
+ = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
2 (ppr kind)
\end{code}
+Note [Avoid name clashes for associated data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider class C a b where
+ data D b :: * -> *
+When typechecking the decl for D, we'll invent an extra type variable for D,
+to fill out its kind. We *don't* want this type variable to be 'a', because
+in an .hi file we'd get
+ class C a b where
+ data D b a
+which makes it look as if there are *two* type indices. But there aren't!
+So we use $a instead, which cannot clash with a user-written type variable.
+Remember that type variable binders in interface files are just FastStrings,
+not proper Names.
+
+(The tidying phase can't help here because we don't tidy TyCons. Another
+alternative would be to record the number of indexing parameters in the
+interface file.)
+
%************************************************************************
%* *
-> LHsType Name
-> BoxySigmaType
-> TcM (TcType, -- The type to use for "inside" the signature
- [(Name,TcType)]) -- The new bit of type environment, binding
+ [(Name, TcType)], -- The new bit of type environment, binding
-- the scoped type variables
+ CoercionI) -- Coercion due to unification with actual ty
tcPatSig ctxt sig res_ty
= do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
; if null sig_tvs then do {
-- The type signature binds no type variables,
-- and hence is rigid, so use it to zap the res_ty
- boxyUnify sig_ty res_ty
- ; return (sig_ty, [])
+ coi <- boxyUnify sig_ty res_ty
+ ; return (sig_ty, [], coi)
} else do {
-- Type signature binds at least one scoped type variable
-- So we just have an ASSERT here
; let in_pat_bind = case ctxt of
BindPatSigCtxt -> True
- other -> False
+ _ -> False
; ASSERT( not in_pat_bind || null sig_tvs ) return ()
-- Check that pat_ty is rigid
-- unifying, and reading out the results.
-- This is a strictly local operation.
; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
- ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
+ ; coi <- boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty)
+ res_ty
; sig_tv_tys <- mapM readFilledBox box_tvs
-- Check that each is bound to a distinct type variable,
; check binds_in_scope tv_binds
-- Phew!
- ; return (res_ty, tv_binds)
+ ; return (res_ty, tv_binds, coi)
} }
where
- check in_scope [] = return ()
+ check _ [] = return ()
check in_scope ((n,ty):rest) = do { check_one in_scope n ty
; check ((n,ty):in_scope) rest }
%************************************************************************
+%* *
+ Checking kinds
+%* *
+%************************************************************************
+
+We would like to get a decent error message from
+ (a) Under-applied type constructors
+ f :: (Maybe, Maybe)
+ (b) Over-applied type constructors
+ f :: Int x -> Int x
+
+\begin{code}
+-- The ExpKind datatype means "expected kind" and contains
+-- some info about just why that kind is expected, to improve
+-- the error message on a mis-match
+data ExpKind = EK TcKind EkCtxt
+data EkCtxt = EkUnk -- Unknown context
+ | EkEqPred -- Second argument of an equality predicate
+ | EkKindSig -- Kind signature
+ | EkArg SDoc Int -- Function, arg posn, expected kind
+
+
+ekLifted, ekOpen :: ExpKind
+ekLifted = EK liftedTypeKind EkUnk
+ekOpen = EK openTypeKind EkUnk
+
+checkExpectedKind :: Outputable a => a -> TcKind -> ExpKind -> TcM ()
+-- A fancy wrapper for 'unifyKind', which tries
+-- to give decent error messages.
+-- (checkExpectedKind ty act_kind exp_kind)
+-- checks that the actual kind act_kind is compatible
+-- with the expected kind exp_kind
+-- The first argument, ty, is used only in the error message generation
+checkExpectedKind ty act_kind (EK exp_kind ek_ctxt)
+ | act_kind `isSubKind` exp_kind -- Short cut for a very common case
+ = return ()
+ | otherwise = do
+ (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind)
+ case mb_r of
+ Just _ -> return () -- Unification succeeded
+ Nothing -> do
+
+ -- So there's definitely an error
+ -- Now to find out what sort
+ exp_kind <- zonkTcKind exp_kind
+ act_kind <- zonkTcKind act_kind
+
+ env0 <- tcInitTidyEnv
+ let (exp_as, _) = splitKindFunTys exp_kind
+ (act_as, _) = splitKindFunTys act_kind
+ n_exp_as = length exp_as
+ n_act_as = length act_as
+
+ (env1, tidy_exp_kind) = tidyKind env0 exp_kind
+ (env2, tidy_act_kind) = tidyKind env1 act_kind
+
+ err | n_exp_as < n_act_as -- E.g. [Maybe]
+ = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments")
+
+ -- Now n_exp_as >= n_act_as. In the next two cases,
+ -- n_exp_as == 0, and hence so is n_act_as
+ | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
+ = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty)
+ <+> ptext (sLit "is unlifted")
+
+ | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
+ = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty)
+ <+> ptext (sLit "is lifted")
+
+ | otherwise -- E.g. Monad [Int]
+ = ptext (sLit "Kind mis-match")
+
+ more_info = sep [ expected_herald ek_ctxt <+> ptext (sLit "kind")
+ <+> quotes (pprKind tidy_exp_kind) <> comma,
+ ptext (sLit "but") <+> quotes (ppr ty) <+>
+ ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)]
+
+ expected_herald EkUnk = ptext (sLit "Expected")
+ expected_herald EkKindSig = ptext (sLit "An enclosing kind signature specified")
+ expected_herald EkEqPred = ptext (sLit "The left argument of the equality predicate had")
+ expected_herald (EkArg fun arg_no)
+ = ptext (sLit "The") <+> speakNth arg_no <+> ptext (sLit "argument of")
+ <+> quotes fun <+> ptext (sLit ("should have"))
+
+ failWithTcM (env2, err $$ more_info)
+\end{code}
+
+%************************************************************************
%* *
Scoped type variables
%* *
\begin{code}
pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = vcat [ ptext SLIT("In") <+> pprUserTypeCtxt ctxt <> colon,
+pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
nest 2 (pp_sig ctxt) ]
where
pp_sig (FunSigCtxt n) = pp_n_colon n
pp_sig (ConArgCtxt n) = pp_n_colon n
pp_sig (ForSigCtxt n) = pp_n_colon n
- pp_sig other = ppr (unLoc hs_ty)
+ pp_sig _ = ppr (unLoc hs_ty)
pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
-
+wobblyPatSig :: [Var] -> SDoc
wobblyPatSig sig_tvs
- = hang (ptext SLIT("A pattern type signature cannot bind scoped type variables")
+ = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables")
<+> pprQuotedList sig_tvs)
- 2 (ptext SLIT("unless the pattern has a rigid type context"))
+ 2 (ptext (sLit "unless the pattern has a rigid type context"))
+scopedNonVar :: Name -> Type -> SDoc
scopedNonVar n ty
- = vcat [sep [ptext SLIT("The scoped type variable") <+> quotes (ppr n),
- nest 2 (ptext SLIT("is bound to the type") <+> quotes (ppr ty))],
- nest 2 (ptext SLIT("You can only bind scoped type variables to type variables"))]
-
-dupInScope n n' ty
- = hang (ptext SLIT("The scoped type variables") <+> quotes (ppr n) <+> ptext SLIT("and") <+> quotes (ppr n'))
- 2 (vcat [ptext SLIT("are bound to the same type (variable)"),
- ptext SLIT("Distinct scoped type variables must be distinct")])
+ = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
+ nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
+ nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
+
+dupInScope :: Name -> Name -> Type -> SDoc
+dupInScope n n' _
+ = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
+ 2 (vcat [ptext (sLit "are bound to the same type (variable)"),
+ ptext (sLit "Distinct scoped type variables must be distinct")])
+
+wrongEqualityErr :: TcM (HsType Name, TcKind)
+wrongEqualityErr
+ = failWithTc (text "Equality predicate used as a type")
\end{code}
projects / ghc-hetmet.git / blobdiff