diff options
| -rw-r--r-- | compiler/typecheck/TcBinds.lhs | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcClassDcl.lhs | 49 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.lhs | 50 | ||||
| -rw-r--r-- | compiler/typecheck/TcInstDcls.lhs | 106 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnDriver.lhs | 66 | ||||
| -rw-r--r-- | compiler/typecheck/TcRnTypes.lhs | 31 | ||||
| -rw-r--r-- | compiler/typecheck/TcSplice.lhs | 3 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.lhs | 204 | ||||
| -rw-r--r-- | docs/users_guide/flags.xml | 5 | ||||
| -rw-r--r-- | docs/users_guide/glasgow_exts.xml | 228 |
10 files changed, 400 insertions, 345 deletions
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index e6e07576d2..530d867b20 100644 --- a/compiler/typecheck/TcBinds.lhs +++ b/compiler/typecheck/TcBinds.lhs @@ -1210,8 +1210,7 @@ decideGeneralisationPlan dflags type_env bndr_names lbinds sig_fn ATcId { tct_closed = cl } -> isTopLevel cl -- This is the key line ATyVar {} -> False -- In-scope type variables AGlobal {} -> True -- are not closed! - AThing {} -> pprPanic "is_closed_id" (ppr name) - ANothing {} -> pprPanic "is_closed_id" (ppr name) + _ -> pprPanic "is_closed_id" (ppr name) | otherwise = WARN( isInternalName name, ppr name ) True -- The free-var set for a top level binding mentions diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs index b9711576c4..cde5eaa613 100644 --- a/compiler/typecheck/TcClassDcl.lhs +++ b/compiler/typecheck/TcClassDcl.lhs @@ -15,7 +15,6 @@ Typechecking class declarations module TcClassDcl ( tcClassSigs, tcClassDecl2, findMethodBind, instantiateMethod, tcInstanceMethodBody, - mkGenericDefMethBind, HsSigFun, mkHsSigFun, lookupHsSig, emptyHsSigs, tcAddDeclCtxt, badMethodErr ) where @@ -41,8 +40,6 @@ import NameEnv import NameSet import Var import Outputable -import DynFlags -import ErrUtils import SrcLoc import Maybes import BasicTypes @@ -349,52 +346,6 @@ This makes the error messages right. %************************************************************************ %* * - Extracting generic instance declaration from class declarations -%* * -%************************************************************************ - -@getGenericInstances@ extracts the generic instance declarations from a class -declaration. For exmaple - - class C a where - op :: a -> a - - op{ x+y } (Inl v) = ... - op{ x+y } (Inr v) = ... - op{ x*y } (v :*: w) = ... - op{ 1 } Unit = ... - -gives rise to the instance declarations - - instance C (x+y) where - op (Inl v) = ... - op (Inr v) = ... - - instance C (x*y) where - op (v :*: w) = ... - - instance C 1 where - op Unit = ... - -\begin{code} -mkGenericDefMethBind :: Class -> [Type] -> Id -> Name -> TcM (LHsBind Name) -mkGenericDefMethBind clas inst_tys sel_id dm_name - = -- A generic default method - -- If the method is defined generically, we only have to call the - -- dm_name. - do { dflags <- getDynFlags - ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Filling in method body" - (vcat [ppr clas <+> ppr inst_tys, - nest 2 (ppr sel_id <+> equals <+> ppr rhs)])) - - ; return (noLoc $ mkTopFunBind (noLoc (idName sel_id)) - [mkSimpleMatch [] rhs]) } - where - rhs = nlHsVar dm_name -\end{code} - -%************************************************************************ -%* * Error messages %* * %************************************************************************ diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index a3808822f6..7f4eed87ce 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -19,18 +19,18 @@ module TcHsType ( -- Type checking type and class decls kcTyClTyVars, tcTyClTyVars, - tcHsConArgType, tcDataKindSig, + tcHsArgType, tcHsConArgType, tcDataKindSig, tcClassSigType, -- Kind-checking types -- No kind generalisation, no checkValidType - tcHsTyVarBndrs, + kcHsTyVarBndrs, tcHsTyVarBndrs, tcHsLiftedType, tcLHsType, tcCheckLHsType, tcHsContext, tcInferApps, tcHsArgTys, ExpKind(..), ekConstraint, expArgKind, checkExpectedKind, - kindGeneralize, + bindScopedKindVars, kindGeneralize, -- Sort-checking kinds tcLHsKind, @@ -577,12 +577,16 @@ tcTyVar name -- Could be a tyvar, a tycon, or a datacon ty = dataConUserType dc tc = buildPromotedDataCon dc - ANothing -> failWithTc (ptext (sLit "Promoted kind") <+> - quotes (ppr name) <+> - ptext (sLit "used in a mutually recursive group")) + AFamDataCon -> bad_promote (ptext (sLit "it comes from a data family instance")) + ARecDataCon -> bad_promote (ptext (sLit "it is defined and used in the same recursive group")) _ -> wrongThingErr "type" thing name } where + bad_promote reason + = failWithTc (hang (ptext (sLit "You can't use data constructor") <+> quotes (ppr name) + <+> ptext (sLit "here")) + 2 (parens reason)) + get_loopy_tc name = do { env <- getGblEnv ; case lookupNameEnv (tcg_type_env env) name of @@ -783,19 +787,42 @@ then we'd also need since we only have BOX for a super kind) \begin{code} -bindScopedKindVars :: [Name] -> TcM a -> TcM a +bindScopedKindVars :: [Name] -> ([KindVar] -> TcM a) -> TcM a -- Given some tyvar binders like [a (b :: k -> *) (c :: k)] -- bind each scoped kind variable (k in this case) to a fresh -- kind skolem variable -bindScopedKindVars kvs thing_inside - = tcExtendTyVarEnv (map mkKindSigVar kvs) thing_inside +bindScopedKindVars kv_ns thing_inside + = tcExtendTyVarEnv kvs (thing_inside kvs) + where + kvs = map mkKindSigVar kv_ns + +kcHsTyVarBndrs :: Bool -- Default UserTyVar to * + -> LHsTyVarBndrs Name + -> ([TcKind] -> TcM r) + -> TcM r +kcHsTyVarBndrs default_to_star (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside + = bindScopedKindVars kvs $ \ _ -> + do { nks <- mapM (kc_hs_tv . unLoc) hs_tvs + ; tcExtendKindEnv nks (thing_inside (map snd nks)) } + where + kc_hs_tv :: HsTyVarBndr Name -> TcM (Name, TcKind) + kc_hs_tv (UserTyVar n) + = do { mb_thing <- tcLookupLcl_maybe n + ; kind <- case mb_thing of + Just (AThing k) -> return k + _ | default_to_star -> return liftedTypeKind + | otherwise -> newMetaKindVar + ; return (n, kind) } + kc_hs_tv (KindedTyVar n k) + = do { kind <- tcLHsKind k + ; return (n, kind) } tcHsTyVarBndrs :: LHsTyVarBndrs Name -> ([TyVar] -> TcM r) -> TcM r -- Bind the type variables to skolems, each with a meta-kind variable kind tcHsTyVarBndrs (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside - = bindScopedKindVars kvs $ + = bindScopedKindVars kvs $ \ _ -> do { tvs <- mapM tcHsTyVarBndr hs_tvs ; traceTc "tcHsTyVarBndrs" (ppr hs_tvs $$ ppr tvs) ; tcExtendTyVarEnv tvs (thing_inside tvs) } @@ -904,7 +931,7 @@ kcTyClTyVars :: Name -> LHsTyVarBndrs Name -> (TcKind -> TcM a) -> TcM a -- Used for the type variables of a type or class decl, -- when doing the initial kind-check. kcTyClTyVars name (HsQTvs { hsq_kvs = kvs, hsq_tvs = hs_tvs }) thing_inside - = bindScopedKindVars kvs $ + = bindScopedKindVars kvs $ \ _ -> do { tc_kind <- kcLookupKind name ; let (arg_ks, res_k) = splitKindFunTysN (length hs_tvs) tc_kind -- There should be enough arrows, because @@ -1354,7 +1381,6 @@ tc_kind_var_app name arg_kis = do { (_errs, mb_thing) <- tryTc (tcLookup name) ; case mb_thing of Just (AGlobal (ATyCon tc)) - | isAlgTyCon tc || isTupleTyCon tc -> do { data_kinds <- xoptM Opt_DataKinds ; unless data_kinds $ addErr (dataKindsErr name) ; case isPromotableTyCon tc of diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs index bc217bb041..920a702059 100644 --- a/compiler/typecheck/TcInstDcls.lhs +++ b/compiler/typecheck/TcInstDcls.lhs @@ -19,8 +19,12 @@ module TcInstDcls ( tcInstDecls1, tcInstDecls2 ) where import HsSyn import TcBinds -import TcTyClsDecls -import TcClassDcl +import TcTyClsDecls( tcAddImplicits, tcAddFamInstCtxt, tcSynFamInstDecl, + wrongKindOfFamily, tcFamTyPats, kcTyDefn, dataDeclChecks, + tcConDecls, checkValidTyCon, badATErr, wrongATArgErr ) +import TcClassDcl( tcClassDecl2, + HsSigFun, lookupHsSig, mkHsSigFun, emptyHsSigs, + findMethodBind, instantiateMethod, tcInstanceMethodBody ) import TcPat ( addInlinePrags ) import TcRnMonad import TcMType @@ -51,15 +55,14 @@ import PrelNames ( typeableClassNames ) import Bag import BasicTypes import DynFlags +import ErrUtils import FastString import Id import MkId import Name import NameSet -import NameEnv import Outputable import SrcLoc -import Digraph( SCC(..) ) import Util import Control.Monad @@ -373,8 +376,12 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls -- round) -- Do class and family instance declarations - ; (gbl_env, local_infos) <- tcLocalInstDecls (calcInstDeclCycles inst_decls) - ; setGblEnv gbl_env $ + ; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls + ; let (local_infos_s, fam_insts_s) = unzip stuff + local_infos = concat local_infos_s + fam_insts = concat fam_insts_s + ; addClsInsts local_infos $ + addFamInsts fam_insts $ do { -- Compute instances from "deriving" clauses; -- This stuff computes a context for the derived instance @@ -389,7 +396,8 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls ; th_stage <- getStage -- See Note [Deriving inside TH brackets ] ; (gbl_env, deriv_inst_info, deriv_binds) <- if isBrackStage th_stage - then return (gbl_env, emptyBag, emptyValBindsOut) + then do { gbl_env <- getGblEnv + ; return (gbl_env, emptyBag, emptyValBindsOut) } else tcDeriving tycl_decls inst_decls deriv_decls @@ -414,20 +422,6 @@ tcInstDecls1 tycl_decls inst_decls deriv_decls typInstErr = ptext $ sLit $ "Can't create hand written instances of Typeable in Safe" ++ " Haskell! Can only derive them" -tcLocalInstDecls :: [SCC (LInstDecl Name)] -> TcM (TcGblEnv, [InstInfo Name]) -tcLocalInstDecls [] - = do { gbl_env <- getGblEnv - ; return (gbl_env, []) } -tcLocalInstDecls (AcyclicSCC inst_decl : sccs) - = do { (inst_infos, fam_insts) <- recoverM (return ([], [])) $ - tcLocalInstDecl inst_decl - ; (gbl_env, more_infos) <- addClsInsts inst_infos $ - addFamInsts fam_insts $ - tcLocalInstDecls sccs - ; return (gbl_env, inst_infos ++ more_infos) } -tcLocalInstDecls (CyclicSCC inst_decls : _) - = do { cyclicDeclErr inst_decls; failM } - addClsInsts :: [InstInfo Name] -> TcM a -> TcM a addClsInsts infos thing_inside = tcExtendLocalInstEnv (map iSpec infos) thing_inside @@ -464,59 +458,6 @@ bindings.) This will become moot when we shift to the new TH plan, so the brutal solution will do. -Note [Instance declaration cycles] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -With -XDataKinds we can get this - data instance Foo [a] = MkFoo (MkFoo a) -where the constructor MkFoo is used in a type before it is -defined. Here is a more complicated situation, involving an -associated type and mutual recursion - - data instance T [a] = MkT (MkS a) - - instance C [a] where - data S [a] = MkS (MkT a) - -When type checking ordinary data type decls we detect this staging -problem in the kind-inference phase, but there *is* no kind inference -phase here. - -So intead we extract the strongly connected components and look for -cycles. - - -\begin{code} -calcInstDeclCycles :: [LInstDecl Name] -> [SCC (LInstDecl Name)] --- see Note [Instance declaration cycles] -calcInstDeclCycles decls - = depAnal get_defs get_uses decls - where - -- get_defs extracts the *constructor* bindings of the declaration - get_defs :: LInstDecl Name -> [Name] - get_defs (L _ (FamInstD { lid_inst = fid })) = get_fi_defs fid - get_defs (L _ (ClsInstD { cid_fam_insts = fids })) = concatMap (get_fi_defs . unLoc) fids - - get_fi_defs :: FamInstDecl Name -> [Name] - get_fi_defs (FamInstDecl { fid_defn = TyData { td_cons = cons } }) - = map (unLoc . con_name . unLoc) cons - get_fi_defs (FamInstDecl {}) = [] - - -- get_uses extracts the *tycon or constructor* uses of the declaration - get_uses :: LInstDecl Name -> [Name] - get_uses (L _ (FamInstD { lid_inst = fid })) = nameSetToList (fid_fvs fid) - get_uses (L _ (ClsInstD { cid_fam_insts = fids })) - = nameSetToList (foldr (unionNameSets . fid_fvs . unLoc) emptyNameSet fids) - -cyclicDeclErr :: Outputable d => [Located d] -> TcRn () -cyclicDeclErr inst_decls - = setSrcSpan (getLoc (head sorted_decls)) $ - addErr (sep [ptext (sLit "Cycle in type declarations: data constructor used (in a type) before it is defined"), - nest 2 (vcat (map ppr_decl sorted_decls))]) - where - sorted_decls = sortLocated inst_decls - ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl -\end{code} - \begin{code} tcLocalInstDecl :: LInstDecl Name -> TcM ([InstInfo Name], [FamInst]) @@ -878,7 +819,6 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) loc = getSrcSpan dfun_id ------------------------------ ----------------------- mkMethIds :: HsSigFun -> Class -> [TcTyVar] -> [EvVar] -> [TcType] -> Id -> TcM (TcId, TcSigInfo) mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id @@ -1275,6 +1215,22 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys (_, local_meth_ty) = tcSplitPredFunTy_maybe sel_rho `orElse` pprPanic "tcInstanceMethods" (ppr sel_id) +------------------ +mkGenericDefMethBind :: Class -> [Type] -> Id -> Name -> TcM (LHsBind Name) +mkGenericDefMethBind clas inst_tys sel_id dm_name + = -- A generic default method + -- If the method is defined generically, we only have to call the + -- dm_name. + do { dflags <- getDynFlags + ; liftIO (dumpIfSet_dyn dflags Opt_D_dump_deriv "Filling in method body" + (vcat [ppr clas <+> ppr inst_tys, + nest 2 (ppr sel_id <+> equals <+> ppr rhs)])) + + ; return (noLoc $ mkTopFunBind (noLoc (idName sel_id)) + [mkSimpleMatch [] rhs]) } + where + rhs = nlHsVar dm_name + ---------------------- wrapId :: HsWrapper -> id -> HsExpr id wrapId wrapper id = mkHsWrap wrapper (HsVar id) diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs index 95274f0814..d16d838286 100644 --- a/compiler/typecheck/TcRnDriver.lhs +++ b/compiler/typecheck/TcRnDriver.lhs @@ -551,17 +551,10 @@ tcRnHsBootDecls decls ; mapM_ (badBootDecl "rule") rule_decls ; mapM_ (badBootDecl "vect") vect_decls - -- Typecheck type/class decls + -- Typecheck type/class/isntance decls ; traceTc "Tc2 (boot)" empty - ; tcg_env <- tcTyAndClassDecls emptyModDetails tycl_decls - ; setGblEnv tcg_env $ do { - - -- Typecheck instance decls - -- Family instance declarations are rejected here - ; traceTc "Tc3" empty ; (tcg_env, inst_infos, _deriv_binds) - <- tcInstDecls1 (concat tycl_decls) inst_decls deriv_decls - + <- tcTyClsInstDecls emptyModDetails tycl_decls inst_decls deriv_decls ; setGblEnv tcg_env $ do { -- Typecheck value declarations @@ -583,7 +576,7 @@ tcRnHsBootDecls decls } ; setGlobalTypeEnv gbl_env type_env2 - }}} + }} ; traceTc "boot" (ppr lie); return gbl_env } badBootDecl :: String -> Located decl -> TcM () @@ -897,14 +890,11 @@ tcTopSrcDecls boot_details -- The latter come in via tycl_decls traceTc "Tc2 (src)" empty ; - tcg_env <- tcTyAndClassDecls boot_details tycl_decls ; - setGblEnv tcg_env $ do { - -- Source-language instances, including derivings, -- and import the supporting declarations traceTc "Tc3" empty ; (tcg_env, inst_infos, deriv_binds) - <- tcInstDecls1 (concat tycl_decls) inst_decls deriv_decls; + <- tcTyClsInstDecls boot_details tycl_decls inst_decls deriv_decls ; setGblEnv tcg_env $ do { -- Foreign import declarations next. @@ -964,9 +954,55 @@ tcTopSrcDecls boot_details , tcg_fords = tcg_fords tcg_env ++ foe_decls ++ fi_decls } } ; return (tcg_env', tcl_env) - }}}}}}} + }}}}}} + +--------------------------- +tcTyClsInstDecls :: ModDetails + -> [TyClGroup Name] + -> [LInstDecl Name] + -> [LDerivDecl Name] + -> TcM (TcGblEnv, -- The full inst env + [InstInfo Name], -- Source-code instance decls to process; + -- contains all dfuns for this module + HsValBinds Name) -- Supporting bindings for derived instances + +tcTyClsInstDecls boot_details tycl_decls inst_decls deriv_decls + = tcExtendTcTyThingEnv [(con, AFamDataCon) | lid <- inst_decls + , con <- get_cons lid ] $ + -- Note [AFamDataCon: not promoting data family constructors] + do { tcg_env <- tcTyAndClassDecls boot_details tycl_decls ; + ; setGblEnv tcg_env $ + tcInstDecls1 (concat tycl_decls) inst_decls deriv_decls } + where + -- get_cons extracts the *constructor* bindings of the declaration + get_cons :: LInstDecl Name -> [Name] + get_cons (L _ (FamInstD { lid_inst = fid })) = get_fi_cons fid + get_cons (L _ (ClsInstD { cid_fam_insts = fids })) = concatMap (get_fi_cons . unLoc) fids + + get_fi_cons :: FamInstDecl Name -> [Name] + get_fi_cons (FamInstDecl { fid_defn = TyData { td_cons = cons } }) + = map (unLoc . con_name . unLoc) cons + get_fi_cons (FamInstDecl {}) = [] \end{code} +Note [AFamDataCon: not promoting data family constructors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + data family T a + data instance T Int = MkT + data Proxy (a :: k) + data S = MkS (Proxy 'MkT) + +Is it ok to use the promoted data family instance constructor 'MkT' in +the data declaration for S? No, we don't allow this. It *might* make +sense, but at least it would mean that we'd have to interleave +typechecking instances and data types, whereas at present we do data +types *then* instances. + +So to check for this we put in the TcLclEnv a binding for all the family +constructors, bound to AFamDataCon, so that if we trip over 'MkT' when +type checking 'S' we'll produce a decent error message. + %************************************************************************ %* * diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs index d17d3e6a10..8f1bc76222 100644 --- a/compiler/typecheck/TcRnTypes.lhs +++ b/compiler/typecheck/TcRnTypes.lhs @@ -578,27 +578,11 @@ data TcTyThing -- Can be a mono-kind or a poly-kind; in TcTyClsDcls see -- Note [Type checking recursive type and class declarations] - | ANothing -- see Note [ANothing] - -{- -Note [ANothing] -~~~~~~~~~~~~~~~ - -We don't want to allow promotion in a strongly connected component -when kind checking. - -Consider: - data T f = K (f (K Any)) - -When kind checking the `data T' declaration the local env contains the -mappings: - T -> AThing <some initial kind> - K -> ANothing - -ANothing is only used for DataCons, and only used during type checking -in tcTyClGroup. --} + | AFamDataCon -- Data constructor for a data family + -- See Note [AFamDataCon: not promoting data family constructors] in TcRnDriver + | ARecDataCon -- Data constructor in a reuursive loop + -- See Note [ARecDataCon: recusion and promoting data constructors] in TcTyClsDecls instance Outputable TcTyThing where -- Debugging only ppr (AGlobal g) = pprTyThing g @@ -609,16 +593,19 @@ instance Outputable TcTyThing where -- Debugging only <+> ppr (tct_level elt)) ppr (ATyVar tv _) = text "Type variable" <+> quotes (ppr tv) ppr (AThing k) = text "AThing" <+> ppr k - ppr ANothing = text "ANothing" + ppr AFamDataCon = text "AFamDataCon" + ppr ARecDataCon = text "ARecDataCon" pprTcTyThingCategory :: TcTyThing -> SDoc pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing pprTcTyThingCategory (ATyVar {}) = ptext (sLit "Type variable") pprTcTyThingCategory (ATcId {}) = ptext (sLit "Local identifier") pprTcTyThingCategory (AThing {}) = ptext (sLit "Kinded thing") -pprTcTyThingCategory ANothing = ptext (sLit "Opaque thing") +pprTcTyThingCategory AFamDataCon = ptext (sLit "Family data con") +pprTcTyThingCategory ARecDataCon = ptext (sLit "Recursive data con") \end{code} + Note [Bindings with closed types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs index 968be0765e..1bdc0bf5a5 100644 --- a/compiler/typecheck/TcSplice.lhs +++ b/compiler/typecheck/TcSplice.lhs @@ -1188,8 +1188,7 @@ reifyThing (ATyVar tv tv1) ; ty2 <- reifyType ty1 ; return (TH.TyVarI (reifyName tv) ty2) } -reifyThing (AThing {}) = panic "reifyThing AThing" -reifyThing ANothing = panic "reifyThing ANothing" +reifyThing thing = pprPanic "reifyThing" (pprTcTyThingCategory thing) ------------------------------ reifyAxiom :: CoAxiom -> TcM TH.Info diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 3db2423999..1cef0f734b 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -104,7 +104,7 @@ tcTyAndClassDecls :: ModDetails tcTyAndClassDecls boot_details tyclds_s = checkNoErrs $ -- The code recovers internally, but if anything gave rise to -- an error we'd better stop now, to avoid a cascade - fold_env tyclds_s -- type check each group in dependency order folding the global env + fold_env tyclds_s -- Type check each group in dependency order folding the global env where fold_env :: [TyClGroup Name] -> TcM TcGblEnv fold_env [] = getGblEnv @@ -268,8 +268,9 @@ kcTyClGroup decls -- Step 1: Bind kind variables for non-synonyms ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls - ; initial_kinds <- concatMapM getInitialKinds non_syn_decls + ; initial_kinds <- getInitialKinds TopLevel non_syn_decls + ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds) ; tcl_env <- tcExtendTcTyThingEnv initial_kinds $ do do { -- Step 2: kind-check the synonyms, and extend envt tcl_env <- kcSynDecls (calcSynCycles syn_decls) @@ -288,6 +289,7 @@ kcTyClGroup decls where generalise :: TcTypeEnv -> Name -> TcM (Name, Kind) + -- For polymorphic things this is a no-op generalise kind_env name = do { traceTc "Generalise type of" (ppr name) ; let kc_kind = case lookupNameEnv kind_env name of @@ -297,7 +299,10 @@ kcTyClGroup decls ; kc_kind' <- zonkTcKind kc_kind ; return (name, mkForAllTys kvs kc_kind') } -getInitialKinds :: LTyClDecl Name -> TcM [(Name, TcTyThing)] +getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)] +getInitialKinds top_lvl = concatMapM (addLocM (getInitialKind top_lvl)) + +getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)] -- Allocate a fresh kind variable for each TyCon and Class -- For each tycon, return (tc, AThing k) -- where k is the kind of tc, derived from the LHS @@ -311,35 +316,54 @@ getInitialKinds :: LTyClDecl Name -> TcM [(Name, TcTyThing)] -- -- No family instances are passed to getInitialKinds -getInitialKinds (L _ decl) - = do { arg_kinds <- mapM (\_ -> newMetaKindVar) (get_tvs decl) - ; res_kind <- get_res_kind decl - ; let main_pair = (tcdName decl, AThing (mkArrowKinds arg_kinds res_kind)) - ; inner_pairs <- get_inner_kinds decl - ; return (main_pair : inner_pairs) } - where - get_inner_kinds :: TyClDecl Name -> TcM [(Name,TcTyThing)] - get_inner_kinds (TyDecl { tcdTyDefn = TyData { td_cons = cons } }) - = return [ (unLoc (con_name con), ANothing) | L _ con <- cons ] - get_inner_kinds (ClassDecl { tcdATs = ats }) - = concatMapM getInitialKinds ats - get_inner_kinds _ - = return [] - - get_res_kind (ClassDecl {}) = return constraintKind - get_res_kind (TyDecl { tcdTyDefn = TyData { td_kindSig = Nothing } }) - = return liftedTypeKind - get_res_kind _ = newMetaKindVar - -- Warning: you might be tempted to return * for all data decls - -- but on GADT-style declarations we allow a kind signature - -- data T :: *->* where { ... } - -- with *no* tvs in the HsTyDefn - - get_tvs (TyFamily {tcdTyVars = tvs}) = hsQTvBndrs tvs - get_tvs (ClassDecl {tcdTyVars = tvs}) = hsQTvBndrs tvs - get_tvs (TyDecl {tcdTyVars = tvs}) = hsQTvBndrs tvs - get_tvs (ForeignType {}) = [] +getInitialKind top_lvl (TyFamily { tcdLName = L _ name, tcdTyVars = ktvs, tcdKindSig = ksig }) + | isTopLevel top_lvl + = kcHsTyVarBndrs True ktvs $ \ arg_kinds -> + do { res_k <- case ksig of + Just k -> tcLHsKind k + Nothing -> return liftedTypeKind + ; let body_kind = mkArrowKinds arg_kinds res_k + kvs = varSetElems (tyVarsOfType body_kind) + ; return [ (name, AThing (mkForAllTys kvs body_kind)) ] } + + | otherwise + = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> + do { res_k <- case ksig of + Just k -> tcLHsKind k + Nothing -> newMetaKindVar + ; return [ (name, AThing (mkArrowKinds arg_kinds res_k)) ] } + +getInitialKind _ (ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) + = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> + do { inner_prs <- getInitialKinds NotTopLevel ats + ; let main_pr = (name, AThing (mkArrowKinds arg_kinds constraintKind)) + ; return (main_pr : inner_prs) } + +getInitialKind top_lvl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdTyDefn = defn }) + | TyData { td_kindSig = Just ksig, td_cons = cons } <- defn + = ASSERT( isTopLevel top_lvl ) + kcHsTyVarBndrs True ktvs $ \ arg_kinds -> + do { res_k <- tcLHsKind ksig + ; let body_kind = mkArrowKinds arg_kinds res_k + kvs = varSetElems (tyVarsOfType body_kind) + main_pr = (name, AThing (mkForAllTys kvs body_kind)) + inner_prs = [(unLoc (con_name con), ARecDataCon) | L _ con <- cons ] + -- See Note [ARecDataCon: Recusion and promoting data constructors] + ; return (main_pr : inner_prs) } + | TyData { td_cons = cons } <- defn + = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> + do { let main_pr = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind)) + inner_prs = [(unLoc (con_name con), ARecDataCon) | L _ con <- cons ] + -- See Note [ARecDataCon: Recusion and promoting data constructors] + ; return (main_pr : inner_prs) } + + | otherwise = pprPanic "getInitialKind" (ppr decl) + +getInitialKind _ (ForeignType { tcdLName = L _ name }) + = return [(name, AThing liftedTypeKind)] + + ---------------- kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv -- Kind bindings kcSynDecls [] = getLclEnv @@ -347,7 +371,6 @@ kcSynDecls (group : groups) = do { nk <- kcSynDecl1 group ; tcExtendKindEnv [nk] (kcSynDecls groups) } ----------------- kcSynDecl1 :: SCC (LTyClDecl Name) -> TcM (Name,TcKind) -- Kind bindings kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl @@ -358,15 +381,14 @@ kcSynDecl1 (CyclicSCC decls) = do { recSynErr decls; failM } kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind) kcSynDecl decl@(TyDecl { tcdTyVars = hs_tvs, tcdLName = L _ name , tcdTyDefn = TySynonym { td_synRhs = rhs } }) - -- Vanilla type synonyoms only, not family instances -- Returns a possibly-unzonked kind = tcAddDeclCtxt decl $ - tcHsTyVarBndrs hs_tvs $ \ k_tvs -> + kcHsTyVarBndrs False hs_tvs $ \ ks -> do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs) - <+> brackets (ppr k_tvs)) + <+> brackets (ppr ks)) ; (_, rhs_kind) <- tcLHsType rhs ; traceTc "kcd2" (ppr name) - ; let tc_kind = foldr (mkArrowKind . tyVarKind) rhs_kind k_tvs + ; let tc_kind = mkArrowKinds ks rhs_kind ; return (name, tc_kind) } kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl) @@ -379,14 +401,21 @@ kcLTyClDecl (L loc decl) kcTyClDecl :: TyClDecl Name -> TcM () -- This function is used solely for its side effect on kind variables -kcTyClDecl (TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = defn }) - = kcTyClTyVars name hs_tvs $ \ res_k -> kcTyDefn defn res_k +kcTyClDecl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = defn }) + | TyData { td_cons = cons, td_kindSig = Just _ } <- defn + = mapM_ (wrapLocM kcConDecl) cons -- Ignore the td_ctxt; heavily deprecated and inconvenient + + | TyData { td_ctxt = ctxt, td_cons = cons } <- defn + = kcTyClTyVars name hs_tvs $ \ _res_k -> + do { _ <- tcHsContext ctxt + ; mapM_ (wrapLocM kcConDecl) cons } + + | otherwise = pprPanic "kcTyClDecl" (ppr decl) kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs , tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats}) - = kcTyClTyVars name hs_tvs $ \ res_k -> + = kcTyClTyVars name hs_tvs $ \ _res_k -> do { _ <- tcHsContext ctxt - ; _ <- unifyKind res_k constraintKind ; mapM_ (wrapLocM kcTyClDecl) ats ; mapM_ (wrapLocM kc_sig) sigs } where @@ -394,53 +423,37 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty) kc_sig _ = return () -kcTyClDecl (ForeignType {}) = return () - -kcTyClDecl (TyFamily { tcdLName = L _ name, tcdTyVars = hs_tvs - , tcdKindSig = mb_kind}) - = kcTyClTyVars name hs_tvs $ \res_k -> kcResultKind mb_kind res_k - -------------------- --- Kind check a data declaration, assuming that we already extended the --- kind environment with the type variables of the left-hand side (these --- kinded type variables are also passed as the second parameter). -kcTyDefn :: HsTyDefn Name -> Kind -> TcM () -kcTyDefn (TyData { td_ND = new_or_data, td_ctxt = ctxt - , td_cons = cons, td_kindSig = mb_kind }) res_k - = do { traceTc "kcTyDefn1" (ppr cons) - ; _ <- tcHsContext ctxt --- ; let h98_syntax = consUseH98Syntax cons --- ; when h98_syntax $ mapM_ (wrapLocM (kcConDecl new_or_data)) cons - ; mapM_ (wrapLocM (kcConDecl new_or_data)) cons - ; traceTc "kcTyDefn2" (ppr cons) - ; kcResultKind mb_kind res_k - ; traceTc "kcTyDefn3" (ppr cons) - } -kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k - = discardResult (tcCheckLHsType rhs_ty res_k) +kcTyClDecl (ForeignType {}) = return () +kcTyClDecl (TyFamily {}) = return () ------------------- -kcConDecl :: NewOrData -> ConDecl Name -> TcM () -kcConDecl new_or_data (ConDecl { con_name = name, con_qvars = ex_tvs - , con_cxt = ex_ctxt, con_details = details, con_res = res }) +kcConDecl :: ConDecl Name -> TcM () +kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs + , con_cxt = ex_ctxt, con_details = details, con_res = res }) = addErrCtxt (dataConCtxt name) $ - tcHsTyVarBndrs ex_tvs $ \ _ -> + kcHsTyVarBndrs False ex_tvs $ \ _ -> do { _ <- tcHsContext ex_ctxt - ; mapM_ (tcHsConArgType new_or_data) (hsConDeclArgTys details) + ; mapM_ (tcHsArgType . getBangType) (hsConDeclArgTys details) ; _ <- tcConRes res ; return () } - ------------------- -kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM () -kcResultKind Nothing res_k - = discardResult (unifyKind res_k liftedTypeKind) - -- type family F a - -- defaults to type family F a :: * -kcResultKind (Just k ) res_k - = do { k' <- tcLHsKind k - ; discardResult (unifyKind k' res_k) } \end{code} +Note [ARecDataCon: Recusion and promoting data constructors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We don't want to allow promotion in a strongly connected component +when kind checking. + +Consider: + data T f = K (f (K Any)) + +When kind checking the `data T' declaration the local env contains the +mappings: + T -> AThing <some initial kind> + K -> ARecDataCon + +ANothing is only used for DataCons, and only used during type checking +in tcTyClGroup. + %************************************************************************ %* * @@ -713,6 +726,27 @@ tcSynFamInstDecl fam_tc tcSynFamInstDecl _ decl = pprPanic "tcSynFamInstDecl" (ppr decl) +kcTyDefn :: HsTyDefn Name -> TcKind -> TcM () +-- Used for 'data instance' and 'type instance' only +-- Ordinary 'data' and 'type' are handed by kcTyClDec and kcSynDecls resp +kcTyDefn (TyData { td_ctxt = ctxt, td_cons = cons, td_kindSig = mb_kind }) res_k + = do { _ <- tcHsContext ctxt + ; mapM_ (wrapLocM kcConDecl) cons + ; kcResultKind mb_kind res_k } + +kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k + = discardResult (tcCheckLHsType rhs_ty res_k) + +------------------ +kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM () +kcResultKind Nothing res_k + = discardResult (unifyKind res_k liftedTypeKind) + -- type family F a + -- defaults to type family F a :: * +kcResultKind (Just k ) res_k + = do { k' <- tcLHsKind k + ; discardResult (unifyKind k' res_k) } + ------------------------- -- Kind check type patterns and kind annotate the embedded type variables. -- type instance F [a] = rhs @@ -1343,10 +1377,8 @@ checkValidDataCon tc con ; mapM_ check_bang (dataConStrictMarks con `zip` [1..]) - ; ASSERT2( not (any (isKindVar . fst) (dataConEqSpec con)), - ppr con $$ ppr (dataConEqSpec con) ) - -- We don't support kind equalities, and shoud not be any - return () + ; checkTc (not (any (isKindVar . fst) (dataConEqSpec con))) + (badGadtKindCon con) ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con)) } @@ -1754,6 +1786,12 @@ badDataConTyCon data_con res_ty_tmpl actual_res_ty ptext (sLit "returns type") <+> quotes (ppr actual_res_ty)) 2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl)) +badGadtKindCon :: DataCon -> SDoc +badGadtKindCon data_con + = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) + <+> ptext (sLit "cannot be GADT-like in its *kind* arguments")) + 2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con)) + badATErr :: Name -> Name -> SDoc badATErr clas op = hsep [ptext (sLit "Class"), quotes (ppr clas), diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml index b501961b4e..be67da9f3b 100644 --- a/docs/users_guide/flags.xml +++ b/docs/users_guide/flags.xml @@ -834,13 +834,14 @@ </row> <row> <entry><option>-XDataKinds</option></entry> - <entry>Enable <link linkend="kind-polymorphism-and-promotion">datatype promotion</link>.</entry> + <entry>Enable <link linkend="promotion">datatype promotion</link>.</entry> <entry>dynamic</entry> <entry><option>-XNoDataKinds</option></entry> </row> <row> <entry><option>-XPolyKinds</option></entry> - <entry>Enable <link linkend="kind-polymorphism-and-promotion">kind polymorphism</link>.</entry> + <entry>Enable <link linkend="kind-polymorphism">kind polymorphism</link>. + Implies <option>-XKindSignatures</option>.</entry> <entry>dynamic</entry> <entry><option>-XNoPolyKinds</option></entry> </row> diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 6681448c2c..b65891a108 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -5154,60 +5154,19 @@ instance Show v => Show (GMap () v) where ... </sect1> -<sect1 id="kind-polymorphism-and-promotion"> -<title>Kind polymorphism and promotion</title> - -<para> -Standard Haskell has a rich type language. Types classify terms and serve to -avoid many common programming mistakes. The kind language, however, is -relatively simple, distinguishing only lifted types (kind <literal>*</literal>), -type constructors (eg. kind <literal>* -> * -> *</literal>), and unlifted -types (<xref linkend="glasgow-unboxed"/>). In particular when using advanced -type system features, such as type families (<xref linkend="type-families"/>) -or GADTs (<xref linkend="gadt"/>), this simple kind system is insufficient, -and fails to prevent simple errors. Consider the example of type-level natural -numbers, and length-indexed vectors: -<programlisting> -data Ze -data Su n - -data Vec :: * -> * -> * where - Nil :: Vec a Ze - Cons :: a -> Vec a n -> Vec a (Su n) -</programlisting> -The kind of <literal>Vec</literal> is <literal>* -> * -> *</literal>. This means -that eg. <literal>Vec Int Char</literal> is a well-kinded type, even though this -is not what we intend when defining length-indexed vectors. -</para> - -<para> -With the flags <option>-XPolyKinds</option> and <option>-XDataKinds</option>, -users get access to a richer kind language. -<option>-XPolyKinds</option> enables kind polymorphism, while -<option>-XDataKinds</option> enables user defined kinds through datatype -promotion. With <option>-XDataKinds</option>, the example above can then be -rewritten to: -<programlisting> -data Nat = Ze | Su Nat - -data Vec :: * -> Nat -> * where - Nil :: Vec a Ze - Cons :: a -> Vec a n -> Vec a (Su n) -</programlisting> -With the improved kind of <literal>Vec</literal>, things like -<literal>Vec Int Char</literal> are now ill-kinded, and GHC will report an -error. -</para> +<sect1 id="kind-polymorphism"> +<title>Kind polymorphism</title> <para> -In this section we show a few examples of how to make use of the new kind -system. This extension is described in more detail in the paper +This section describes <emphasis>kind polymorphism</emphasis>, and extension +enabled by <option>-XPolyKinds</option>. +It is described in more detail in the paper <ulink url="http://dreixel.net/research/pdf/ghp.pdf">Giving Haskell a Promotion</ulink>, which appeared at TLDI 2012. </para> -<sect2 id="kind-polymorphism"> -<title>Kind polymorphism</title> +<sect2> <title>Overview of kind polymorphism</title> + <para> Currently there is a lot of code duplication in the way Typeable is implemented (<xref linkend="deriving-typeable"/>): @@ -5240,34 +5199,148 @@ Note that the datatype <literal>Proxy</literal> has kind <literal>Typeable</literal> class has kind <literal>forall k. k -> Constraint</literal>. </para> +</sect2> + +<sect2> <title>Overview</title> + +<para> +Generally speaking, with <option>-XPolyKinds</option>, GHC will infer a polymorphic +kind for un-decorated whenever possible. For example: +<programlisting> +data T m a = MkT (m a) +-- GHC infers kind T :: forall k. (k -> *) -> k -> * +</programlisting> +Just as in the world of terms, you can restrict polymorphism using a signature +(<option>-XPolyKinds</option> implies <option>-XKindSignatures</option>): +<programlisting> +data T m (a :: *) = MkT (m a) +-- GHC now infers kind T :: (* -> *) -> * -> * +</programlisting> +There is no "forall" for kind variables. Instead, you can simply mention a kind +variable in a kind signature, thus: +<programlisting> +data T (m :: k -> *) a = MkT (m a) +-- GHC now infers kind T :: forall k. (k -> *) -> k -> * +</programlisting> +</para> +</sect2> + +<sect2> <title>Polymorphic kind recursion and complete kind signatures</title> + +<para> +Just as in type inference, kind inference for recursive types can only use <emphasis>monomorphic</emphasis> recursion. +Consider this (contrived) example: +<programlisting> +data T m a = MkT (m a) (T Maybe (m a)) +-- GHC infers kind T :: (* -> *) -> * -> * +</programlisting> +The recursive use of <literal>T</literal> forced the second argument to have kind <literal>*</literal>. +However, just as in type inference, you can achieve polymorphic recursion by giving a +<emphasis>complete kind signature</emphasis> for <literal>T</literal>. The way to give +a complete kind signature for a data type is to use a GADT-style declaration with an +explicit kind signature thus: +<programlisting> +data T :: (k -> *) -> k -> * where + MkT :: m a -> T Maybe (m a) -> T m a +</programlisting> +The complete user-supplied kind signature specifies the polymorphic kind for <literal>T</literal>, +and this signature is used for all the calls to <literal>T</literal> including the recursive ones. +In particular, the recursive use of <literal>T</literal> is at kind <literal>*</literal>. +</para> <para> -There are some restrictions in the current implementation: +What exactly is considered to be a "complete user-supplied kind signature" for a type constructor? +These are the forms: <itemizedlist> - <listitem><para>You cannot (yet) explicitly abstract over kinds, or mention - kind variables. So the following are all rejected: +<listitem><para> +A GADT-style data type declaration, with an explicit "<literal>::</literal>" in the header. +For example: <programlisting> -data D1 (t :: k) +data T1 :: (k -> *) -> k -> * where ... -- Yes T1 :: forall k. (k->*) -> k -> * +data T2 (a :: k -> *) :: k -> * where ... -- Yes T2 :: forall k. (k->*) -> k -> * +data T3 (a :: k -> *) (b :: k) :: * where ... -- Yes T3 :: forall k. (k->*) -> k -> * +data T4 a (b :: k) :: * where ... -- YES T4 :: forall k. * -> k -> * -data D2 :: k -> * +data T5 a b where ... -- NO kind is inferred +data T4 (a :: k -> *) (b :: k) where ... -- NO kind is inferred +</programlisting> +It makes no difference where you put the "<literal>::</literal>" but it must be there. +You cannot give a complete kind signature using a Haskell-98-style data type declaration; +you must use GADT syntax. +</para></listitem> -data D3 (k :: BOX) -</programlisting></para> - </listitem> - <listitem><para>The return kind of a type family is always defaulted to - <literal>*</literal>. So the following is rejected: +<listitem><para> +A type or data family declaration <emphasis>always</emphasis> have a +complete user-specified kind signature; no "<literal>::</literal>" is required: <programlisting> -type family F a -type instance F Int = Maybe -</programlisting></para> - </listitem> +data family D1 a -- D1 :: * -> * +data family D2 (a :: k) -- D2 :: forall k. k -> * +data family D3 (a :: k) :: * -- D3 :: forall k. k -> * +type family S1 a :: k -> * -- S1 :: forall k. * -> k -> * +</programlisting> +</para></listitem> </itemizedlist> +In a complete user-specified kind signature, any un-decorated type variable to the +left of the "<literal>::</literal>" is considered to have kind "<literal>*</literal>". +If you want kind polymorphism, specify a kind variable. </para> </sect2> +</sect1> -<sect2 id="promotion"> +<sect1 id="promotion"> <title>Datatype promotion</title> + +<para> +This section describes <emphasis>data type promotion</emphasis>, an extension +to the kind system that complements kind polymorphism. It is enabled by <option>-XDataKinds</option>, +and described in more detail in the paper +<ulink url="http://dreixel.net/research/pdf/ghp.pdf">Giving Haskell a +Promotion</ulink>, which appeared at TLDI 2012. +</para> + +<sect2> <title>Motivation</title> + +<para> +Standard Haskell has a rich type language. Types classify terms and serve to +avoid many common programming mistakes. The kind language, however, is +relatively simple, distinguishing only lifted types (kind <literal>*</literal>), +type constructors (eg. kind <literal>* -> * -> *</literal>), and unlifted +types (<xref linkend="glasgow-unboxed"/>). In particular when using advanced +type system features, such as type families (<xref linkend="type-families"/>) +or GADTs (<xref linkend="gadt"/>), this simple kind system is insufficient, +and fails to prevent simple errors. Consider the example of type-level natural +numbers, and length-indexed vectors: +<programlisting> +data Ze +data Su n + +data Vec :: * -> * -> * where + Nil :: Vec a Ze + Cons :: a -> Vec a n -> Vec a (Su n) +</programlisting> +The kind of <literal>Vec</literal> is <literal>* -> * -> *</literal>. This means +that eg. <literal>Vec Int Char</literal> is a well-kinded type, even though this +is not what we intend when defining length-indexed vectors. +</para> + +<para> +With <option>-XDataKinds</option>, the example above can then be +rewritten to: +<programlisting> +data Nat = Ze | Su Nat + +data Vec :: * -> Nat -> * where + Nil :: Vec a Ze + Cons :: a -> Vec a n -> Vec a (Su n) +</programlisting> +With the improved kind of <literal>Vec</literal>, things like +<literal>Vec Int Char</literal> are now ill-kinded, and GHC will report an +error. +</para> +</sect2> + +<sect2><title>Overview</title> <para> With <option>-XDataKinds</option>, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors. @@ -5315,10 +5388,13 @@ The following restrictions apply to promotion: <listitem><para>We do not promote datatypes whose constructors are kind polymorphic, involve constraints, or use existential quantification. </para></listitem> + <listitem><para>We do not promote data family instances (<xref linkend="data-families"/>). + </para></listitem> </itemizedlist> </para> +</sect2> -<sect3 id="promotion-syntax"> +<sect2 id="promotion-syntax"> <title>Distinguishing between types and constructors</title> <para> Since constructors and types share the same namespace, with promotion you can @@ -5343,9 +5419,9 @@ ambiguous, we do not allow quotes in kind names. <para>Just as in the case of Template Haskell (<xref linkend="th-syntax"/>), there is no way to quote a data constructor or type constructor whose second character is a single quote.</para> -</sect3> +</sect2> -<sect3 id="promoted-lists-and-tuples"> +<sect2 id="promoted-lists-and-tuples"> <title>Promoted lists and tuples types</title> <para> Haskell's list and tuple types are natively promoted to kinds, and enjoy the @@ -5360,9 +5436,9 @@ data Tuple :: (*,*) -> * where </programlisting> Note that this requires <option>-XTypeOperators</option>. </para> -</sect3> +</sect2> -<sect3 id="promoted-literals"> +<sect2 id="promoted-literals"> <title>Promoted Literals</title> <para> Numeric and string literals are prmoted to the type level, giving convenient @@ -5404,25 +5480,11 @@ instance Has Point "y" Int where from (Point _ y) _ = y example = from (Point 1 2) (Get :: Label "x") </programlisting> </para> -</sect3> - - - -</sect2> - -<sect2 id="kind-polymorphism-limitations"> -<title>Shortcomings of the current implementation</title> -<para> -For the release on GHC 7.4 we focused on getting the new kind-polymorphic core -to work with all existing programs (which do not make use of kind polymorphism). -Many things already work properly with <option>-XPolyKinds</option>, but we -expect that some things will not work. If you run into trouble, please -<link linkend="bug-reporting">report a bug</link>! -</para> </sect2> </sect1> + <sect1 id="equality-constraints"> <title>Equality constraints</title> <para> |