Support polymorphic kind recursion

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!

8 files changed, 252 insertions, 260 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),