Support polymorphic kind recursion
authorSimon Peyton Jones <simonpj@microsoft.com>
Thu, 7 Jun 2012 11:09:22 +0000 (12:09 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 7 Jun 2012 11:09:22 +0000 (12:09 +0100)
This is (I hope) the last major patch for kind polymorphism.
The big new feature is polymorphic kind recursion when you
supply a complete kind signature for a type constructor.
(I've documented it in the user manual too.)

This fixes Trac #6137, #6093, #6049.

The patch also makes type/data families less polymorphic by default.
   data family T a
now defaults to T :: * -> *
If you want T :: forall k. k -> *, use
   data family T (a :: k)

This defaulting to * is done whenever there is a
"complete, user-specified kind signature", something that is
carefully defined in the user manual.

Hurrah!

compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcClassDcl.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcInstDcls.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcTyClsDecls.lhs
docs/users_guide/flags.xml
docs/users_guide/glasgow_exts.xml

index e6e0757..530d867 100644 (file)
@@ -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
index b971157..cde5eaa 100644 (file)
@@ -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
 %*                                                                     *
 %************************************************************************
index a380882..7f4eed8 100644 (file)
@@ -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
index bc217bb..920a702 100644 (file)
@@ -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)
index 95274f0..d16d838 100644 (file)
@@ -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.
+
 
 %************************************************************************
 %*                                                                      *
index d17d3e6..8f1bc76 100644 (file)
@@ -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
index 968be07..1bdc0bf 100644 (file)
@@ -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
index 3db2423..1cef0f7 100644 (file)
@@ -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), 
index b501961..be67da9 100644 (file)
           </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>
index 6681448..b65891a 100644 (file)
@@ -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>