Basic set up for global family instance environment
[ghc-hetmet.git] / compiler / typecheck / TcTyClsDecls.lhs
index 1a9d4c0..3c25a7f 100644 (file)
@@ -5,17 +5,19 @@
 
 \begin{code}
 module TcTyClsDecls (
-       tcTyAndClassDecls
+       tcTyAndClassDecls, tcIdxTyInstDecl
     ) where
 
 #include "HsVersions.h"
 
 import HsSyn           ( TyClDecl(..),  HsConDetails(..), HsTyVarBndr(..),
-                         ConDecl(..),   Sig(..), , NewOrData(..), ResType(..),
-                         tyClDeclTyVars, isSynDecl, hsConArgs,
-                         LTyClDecl, tcdName, hsTyVarName, LHsTyVarBndr
+                         ConDecl(..),   Sig(..), NewOrData(..), ResType(..),
+                         tyClDeclTyVars, isSynDecl, isClassDecl, isIdxTyDecl,
+                         isKindSigDecl, hsConArgs, LTyClDecl, tcdName,
+                         hsTyVarName, LHsTyVarBndr, LHsType, HsType(..),
+                         mkHsAppTy
                        )
-import HsTypes          ( HsBang(..), getBangStrictness )
+import HsTypes          ( HsBang(..), getBangStrictness, hsLTyVarNames )
 import BasicTypes      ( RecFlag(..), StrictnessMark(..) )
 import HscTypes                ( implicitTyThings, ModDetails )
 import BuildTyCl       ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
@@ -23,46 +25,54 @@ import BuildTyCl    ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
 import TcRnMonad
 import TcEnv           ( TyThing(..), 
                          tcLookupLocated, tcLookupLocatedGlobal, 
-                         tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
-                         tcExtendRecEnv, tcLookupTyVar )
-import TcTyDecls       ( calcTyConArgVrcs, calcRecFlags, calcClassCycles, calcSynCycles )
+                         tcExtendGlobalEnv, tcExtendKindEnv,
+                         tcExtendKindEnvTvs, newFamInstTyConName,
+                         tcExtendRecEnv, tcLookupTyVar, tcLookupLocatedTyCon )
+import TcTyDecls       ( calcRecFlags, calcClassCycles, calcSynCycles )
 import TcClassDcl      ( tcClassSigs, tcAddDeclCtxt )
 import TcHsType                ( kcHsTyVars, kcHsLiftedSigType, kcHsType, 
                          kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
-                         kcHsSigType, tcHsBangType, tcLHsConResTy, tcDataKindSig )
+                         kcHsSigType, tcHsBangType, tcLHsConResTy,
+                         tcDataKindSig, kcCheckHsType )
 import TcMType         ( newKindVar, checkValidTheta, checkValidType, 
                          -- checkFreeness, 
                          UserTypeCtxt(..), SourceTyCtxt(..) ) 
-import TcType          ( TcKind, TcType, tyVarsOfType, mkPhiTy,
+import TcType          ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
                          mkArrowKind, liftedTypeKind, mkTyVarTys, 
                          tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type            ( splitTyConApp_maybe, 
+import Type            ( PredType(..), splitTyConApp_maybe, mkTyVarTy,
+                          newTyConInstRhs, isLiftedTypeKind, Kind
                          -- pprParendType, pprThetaArrow
                        )
-import Kind            ( mkArrowKinds, splitKindFunTys )
 import Generics                ( validGenericMethodType, canDoGenerics )
 import Class           ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
-import TyCon           ( TyCon, ArgVrcs, AlgTyConRhs( AbstractTyCon ),
-                         tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
-                         tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName )
-import DataCon         ( DataCon, dataConWrapId, dataConName, 
-                         dataConFieldLabels, dataConTyCon,
-                         dataConTyVars, dataConFieldType, dataConResTys )
+import TyCon           ( TyCon, AlgTyConRhs( AbstractTyCon, OpenDataTyCon, 
+                                             OpenNewTyCon ), 
+                         SynTyConRhs( OpenSynTyCon, SynonymTyCon ),
+                         tyConDataCons, mkForeignTyCon, isProductTyCon,
+                         isRecursiveTyCon, isOpenTyCon,
+                         tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName,
+                          isNewTyCon, isDataTyCon, tyConKind, 
+                         setTyConArgPoss )
+import DataCon         ( DataCon, dataConUserType, dataConName, 
+                         dataConFieldLabels, dataConTyCon, dataConAllTyVars,
+                         dataConFieldType, dataConResTys )
 import Var             ( TyVar, idType, idName )
 import VarSet          ( elemVarSet, mkVarSet )
 import Name            ( Name, getSrcLoc )
 import Outputable
-import Maybe           ( isJust )
+import Maybe           ( isJust, fromJust, isNothing, catMaybes )
 import Maybes          ( expectJust )
+import Monad           ( unless )
 import Unify           ( tcMatchTys, tcMatchTyX )
 import Util            ( zipLazy, isSingleton, notNull, sortLe )
-import List            ( partition )
-import SrcLoc          ( Located(..), unLoc, getLoc, srcLocSpan )
-import ListSetOps      ( equivClasses )
-import List            ( delete )
+import List            ( partition, elemIndex )
+import SrcLoc          ( Located(..), unLoc, getLoc, srcLocSpan, 
+                         srcSpanStart )
+import ListSetOps      ( equivClasses, minusList )
 import Digraph         ( SCC(..) )
 import DynFlags                ( DynFlag( Opt_GlasgowExts, Opt_Generics, 
-                                       Opt_UnboxStrictFields ) )
+                                  Opt_UnboxStrictFields, Opt_IndexedTypes ) )
 \end{code}
 
 
@@ -111,46 +121,87 @@ Step 7:           checkValidTyCl
        to check all the side conditions on validity.  We could not
        do this before because we were in a mutually recursive knot.
 
-
+Identification of recursive TyCons
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
-@TyThing@s.  @rec_vrcs@ is a finite map from @Name@s to @ArgVrcs@s.
+@TyThing@s.
+
+Identifying a TyCon as recursive serves two purposes
+
+1.  Avoid infinite types.  Non-recursive newtypes are treated as
+"transparent", like type synonyms, after the type checker.  If we did
+this for all newtypes, we'd get infinite types.  So we figure out for
+each newtype whether it is "recursive", and add a coercion if so.  In
+effect, we are trying to "cut the loops" by identifying a loop-breaker.
+
+2.  Avoid infinite unboxing.  This is nothing to do with newtypes.
+Suppose we have
+        data T = MkT Int T
+        f (MkT x t) = f t
+Well, this function diverges, but we don't want the strictness analyser
+to diverge.  But the strictness analyser will diverge because it looks
+deeper and deeper into the structure of T.   (I believe there are
+examples where the function does something sane, and the strictness
+analyser still diverges, but I can't see one now.)
+
+Now, concerning (1), the FC2 branch currently adds a coercion for ALL
+newtypes.  I did this as an experiment, to try to expose cases in which
+the coercions got in the way of optimisations.  If it turns out that we
+can indeed always use a coercion, then we don't risk recursive types,
+and don't need to figure out what the loop breakers are.
+
+For newtype *families* though, we will always have a coercion, so they
+are always loop breakers!  So you can easily adjust the current
+algorithm by simply treating all newtype families as loop breakers (and
+indeed type families).  I think.
 
 \begin{code}
 tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
                   -> TcM TcGblEnv      -- Input env extended by types and classes 
                                        -- and their implicit Ids,DataCons
-tcTyAndClassDecls boot_details decls
-  = do {       -- First check for cyclic type synonysm or classes
+tcTyAndClassDecls boot_details allDecls
+  = do {       -- Omit instances of indexed types; they are handled together
+               -- with the *heads* of class instances
+        ; let decls = filter (not . isIdxTyDecl . unLoc) allDecls
+
+               -- First check for cyclic type synonysm or classes
                -- See notes with checkCycleErrs
-         checkCycleErrs decls
+       ; checkCycleErrs decls
        ; mod <- getModule
        ; traceTc (text "tcTyAndCl" <+> ppr mod)
        ; (syn_tycons, alg_tyclss) <- fixM (\ ~(rec_syn_tycons, rec_alg_tyclss) ->
-         do    { let { -- Calculate variances and rec-flag
-                     ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc) decls }
-
+         do    { let { -- Seperate ordinary synonyms from all other type and
+                       -- class declarations and add all associated type
+                       -- declarations from type classes.  The latter is
+                       -- required so that the temporary environment for the
+                       -- knot includes all associated family declarations.
+                     ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
+                                                  decls
+                     ; alg_at_decls           = concatMap addATs alg_decls
+                     }
                        -- Extend the global env with the knot-tied results
                        -- for data types and classes
                        -- 
-                       -- We must populate the environment with the loop-tied T's right
-                       -- away, because the kind checker may "fault in" some type 
-                       -- constructors that recursively mention T
-               ; let { gbl_things = mkGlobalThings alg_decls rec_alg_tyclss }
+                       -- We must populate the environment with the loop-tied
+                       -- T's right away, because the kind checker may "fault
+                       -- in" some type  constructors that recursively
+                       -- mention T
+               ; let gbl_things = mkGlobalThings alg_at_decls rec_alg_tyclss
                ; tcExtendRecEnv gbl_things $ do
 
                        -- Kind-check the declarations
                { (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls
 
-               ; let { calc_vrcs = calcTyConArgVrcs (rec_syn_tycons ++ rec_alg_tyclss)
+               ; let { -- Calculate rec-flag
                      ; calc_rec  = calcRecFlags boot_details rec_alg_tyclss
-                     ; tc_decl   = addLocM (tcTyClDecl calc_vrcs calc_rec) }
+                     ; tc_decl   = addLocM (tcTyClDecl calc_rec) }
                        -- Type-check the type synonyms, and extend the envt
-               ; syn_tycons <- tcSynDecls calc_vrcs kc_syn_decls
+               ; syn_tycons <- tcSynDecls kc_syn_decls
                ; tcExtendGlobalEnv syn_tycons $ do
 
                        -- Type-check the data types and classes
                { alg_tyclss <- mappM tc_decl kc_alg_decls
-               ; return (syn_tycons, alg_tyclss)
+               ; return (syn_tycons, concat alg_tyclss)
            }}})
        -- Finished with knot-tying now
        -- Extend the environment with the finished things
@@ -164,10 +215,22 @@ tcTyAndClassDecls boot_details decls
        -- Add the implicit things;
        -- we want them in the environment because 
        -- they may be mentioned in interface files
+       -- NB: All associated types and their implicit things will be added a
+       --     second time here.  This doesn't matter as the definitions are
+       --     the same.
        ; let { implicit_things = concatMap implicitTyThings alg_tyclss }
-       ; traceTc ((text "Adding" <+> ppr alg_tyclss) $$ (text "and" <+> ppr implicit_things))
+       ; traceTc ((text "Adding" <+> ppr alg_tyclss) 
+                  $$ (text "and" <+> ppr implicit_things))
        ; tcExtendGlobalEnv implicit_things getGblEnv
     }}
+  where
+    -- Pull associated types out of class declarations, to tie them into the
+    -- knot above.  
+    -- NB: We put them in the same place in the list as `tcTyClDecl' will
+    --    eventually put the matching `TyThing's.  That's crucial; otherwise,
+    --    the two argument lists of `mkGlobalThings' don't match up.
+    addATs decl@(L _ (ClassDecl {tcdATs = ats})) = decl : ats
+    addATs decl                                         = [decl]
 
 mkGlobalThings :: [LTyClDecl Name]     -- The decls
               -> [TyThing]             -- Knot-tied, in 1-1 correspondence with the decls
@@ -186,6 +249,144 @@ mkGlobalThings decls things
 
 %************************************************************************
 %*                                                                     *
+\subsection{Type checking instances of indexed types}
+%*                                                                     *
+%************************************************************************
+
+Instances of indexed types are somewhat of a hybrid.  They are processed
+together with class instance heads, but can contain data constructors and hence
+they share a lot of kinding and type checking code with ordinary algebraic
+data types (and GADTs).
+
+\begin{code}
+tcIdxTyInstDecl :: LTyClDecl Name -> TcM (Maybe TyThing)   -- Nothing if error
+tcIdxTyInstDecl (L loc decl)
+  =    -- Prime error recovery, set source location
+    recoverM (returnM Nothing)                 $
+    setSrcSpan loc                             $
+    tcAddDeclCtxt decl                         $
+    do { -- indexed data types require -findexed-types and can't be in an
+        -- hs-boot file
+       ; gla_exts <- doptM Opt_IndexedTypes
+       ; is_boot  <- tcIsHsBoot          -- Are we compiling an hs-boot file?
+       ; checkTc gla_exts      $ badIdxTyDecl (tcdLName decl)
+       ; checkTc (not is_boot) $ badBootTyIdxDeclErr
+
+        -- perform kind and type checking
+       ; tcIdxTyInstDecl1 decl
+       }
+
+tcIdxTyInstDecl1 :: TyClDecl Name -> TcM (Maybe TyThing)   -- Nothing if error
+
+tcIdxTyInstDecl1 (decl@TySynonym {})
+  = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+    do { -- check that the family declaration is for a synonym
+        unless (isSynTyCon family) $
+          addErr (wrongKindOfFamily family)
+
+       ; -- (1) kind check the right hand side of the type equation
+       ; k_rhs <- kcCheckHsType (tcdSynRhs decl) resKind
+
+         -- (2) type check type equation
+       ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
+       ; t_typats <- mappM tcHsKindedType k_typats
+       ; t_rhs    <- tcHsKindedType k_rhs
+
+         -- !!!of the form: forall t_tvs. (tcdLName decl) t_typats = t_rhs
+       ; return Nothing     -- !!!TODO: need TyThing for indexed synonym
+       }}
+      
+tcIdxTyInstDecl1 (decl@TyData {tcdND = new_or_data, tcdLName = L loc tc_name,
+                              tcdCons = cons})
+  = kcIdxTyPats decl $ \k_tvs k_typats resKind family ->
+    do { -- check that the family declaration is for the right kind
+        unless (new_or_data == NewType  && isNewTyCon  family ||
+                new_or_data == DataType && isDataTyCon family) $
+          addErr (wrongKindOfFamily family)
+
+       ; -- (1) kind check the data declaration as usual
+       ; k_decl <- kcDataDecl decl k_tvs
+       ; let k_ctxt = tcdCtxt k_decl
+            k_cons = tcdCons k_decl
+
+         -- result kind must be '*' (otherwise, we have too few patterns)
+       ; checkTc (isLiftedTypeKind resKind) $ tooFewParmsErr tc_name
+
+         -- (2) type check indexed data type declaration
+       ; tcTyVarBndrs k_tvs $ \t_tvs -> do {  -- turn kinded into proper tyvars
+       ; unbox_strict <- doptM Opt_UnboxStrictFields
+
+        -- Check that we don't use GADT syntax for indexed types
+       ; checkTc h98_syntax (badGadtIdxTyDecl tc_name)
+
+        -- Check that a newtype has exactly one constructor
+       ; checkTc (new_or_data == DataType || isSingleton k_cons) $
+          newtypeConError tc_name (length k_cons)
+
+       ; t_typats     <- mappM tcHsKindedType k_typats
+       ; stupid_theta <- tcHsKindedContext k_ctxt
+
+       ; rep_tc_name <- newFamInstTyConName tc_name (srcSpanStart loc)
+       ; tycon <- fixM (\ tycon -> do 
+            { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data 
+                                             tycon t_tvs))
+                                 k_cons
+            ; tc_rhs <-
+                case new_or_data of
+                  DataType -> return (mkDataTyConRhs data_cons)
+                  NewType  -> ASSERT( isSingleton data_cons )
+                              mkNewTyConRhs tc_name tycon (head data_cons)
+            ; buildAlgTyCon rep_tc_name t_tvs stupid_theta tc_rhs Recursive
+                            False h98_syntax (Just (family, t_typats))
+                 -- We always assume that indexed types are recursive.  Why?
+                 -- (1) Due to their open nature, we can never be sure that a
+                 -- further instance might not introduce a new recursive
+                 -- dependency.  (2) They are always valid loop breakers as
+                 -- they involve a coercion.
+            })
+
+         -- construct result
+       ; return $ Just (ATyCon tycon)
+       }}
+       where
+        h98_syntax = case cons of      -- All constructors have same shape
+                       L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
+                       other -> True
+
+-- Kind checking of indexed types
+-- -
+
+-- Kind check type patterns and kind annotate the embedded type variables.
+--
+-- * Here we check that a type instance matches its kind signature, but we do
+--   not check whether there is a pattern for each type index; the latter
+--   check is only required for type functions.
+--
+kcIdxTyPats :: TyClDecl Name
+           -> ([LHsTyVarBndr Name] -> [LHsType Name] -> Kind -> TyCon -> TcM a)
+              -- ^^kinded tvs         ^^kinded ty pats  ^^res kind
+           -> TcM a
+kcIdxTyPats decl thing_inside
+  = kcHsTyVars (tcdTyVars decl) $ \tvs -> 
+    do { family <- tcLookupLocatedTyCon (tcdLName decl)
+       ; let { (kinds, resKind) = splitKindFunTys (tyConKind family)
+            ; hs_typats        = fromJust $ tcdTyPats decl }
+
+         -- we may not have more parameters than the kind indicates
+       ; checkTc (length kinds >= length hs_typats) $
+          tooManyParmsErr (tcdLName decl)
+
+         -- type functions can have a higher-kinded result
+       ; let resultKind = mkArrowKinds (drop (length hs_typats) kinds) resKind
+       ; typats <- zipWithM kcCheckHsType hs_typats kinds
+       ; thing_inside tvs typats resultKind family
+       }
+  where
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
                Kind checking
 %*                                                                     *
 %************************************************************************
@@ -212,11 +413,24 @@ So we must infer their kinds from their right-hand sides *first* and then
 use them, whereas for the mutually recursive data types D we bring into
 scope kind bindings D -> k, where k is a kind variable, and do inference.
 
+Indexed Types
+~~~~~~~~~~~~~
+This treatment of type synonyms only applies to Haskell 98-style synonyms.
+General type functions can be recursive, and hence, appear in `alg_decls'.
+
+The kind of an indexed type is solely determinded by its kind signature;
+hence, only kind signatures participate in the construction of the initial
+kind environment (as constructed by `getInitialKind').  In fact, we ignore
+instances of indexed types altogether in the following.  However, we need to
+include the kind signatures of associated types into the construction of the
+initial kind environment.  (This is handled by `allDecls').
+
 \begin{code}
 kcTyClDecls syn_decls alg_decls
-  = do {       -- First extend the kind env with each data 
-               -- type and class, mapping them to a type variable
-         alg_kinds <- mappM getInitialKind alg_decls
+  = do {       -- First extend the kind env with each data type, class, and
+               -- indexed type, mapping them to a type variable
+          let initialKindDecls = concat [allDecls decl | L _ decl <- alg_decls]
+       ; alg_kinds <- mappM getInitialKind initialKindDecls
        ; tcExtendKindEnv alg_kinds $ do
 
                -- Now kind-check the type synonyms, in dependency order
@@ -228,18 +442,29 @@ kcTyClDecls syn_decls alg_decls
        { (kc_syn_decls, syn_kinds) <- kcSynDecls (calcSynCycles syn_decls)
        ; tcExtendKindEnv syn_kinds $  do
 
-               -- Now kind-check the data type and class declarations, 
-               -- returning kind-annotated decls
-       { kc_alg_decls <- mappM (wrapLocM kcTyClDecl) alg_decls
+               -- Now kind-check the data type, class, and kind signatures,
+               -- returning kind-annotated decls; we don't kind-check
+               -- instances of indexed types yet, but leave this to
+               -- `tcInstDecls1'
+       { kc_alg_decls <- mappM (wrapLocM kcTyClDecl) 
+                           (filter (not . isIdxTyDecl . unLoc) alg_decls)
 
        ; return (kc_syn_decls, kc_alg_decls) }}}
+  where
+    -- get all declarations relevant for determining the initial kind
+    -- environment
+    allDecls (decl@ClassDecl {tcdATs = ats}) = decl : [ at 
+                                                     | L _ at <- ats
+                                                     , isKindSigDecl at]
+    allDecls decl | isIdxTyDecl decl         = []
+                 | otherwise                = [decl]
 
 ------------------------------------------------------------------------
-getInitialKind :: LTyClDecl Name -> TcM (Name, TcKind)
--- Only for data type and class declarations
--- Get as much info as possible from the data or class decl,
+getInitialKind :: TyClDecl Name -> TcM (Name, TcKind)
+-- Only for data type, class, and indexed type declarations
+-- Get as much info as possible from the data, class, or indexed type decl,
 -- so as to maximise usefulness of error messages
-getInitialKind (L _ decl)
+getInitialKind decl
   = do         { arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
        ; res_kind  <- mk_res_kind decl
        ; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
@@ -247,8 +472,10 @@ getInitialKind (L _ decl)
     mk_arg_kind (UserTyVar _)        = newKindVar
     mk_arg_kind (KindedTyVar _ kind) = return kind
 
-    mk_res_kind (TyData { tcdKindSig = Just kind }) = return kind
-       -- On GADT-style declarations we allow a kind signature
+    mk_res_kind (TyFunction { tcdKind    = kind      }) = return kind
+    mk_res_kind (TyData     { tcdKindSig = Just kind }) = return kind
+       -- On GADT-style and data signature declarations we allow a kind 
+       -- signature
        --      data T :: *->* where { ... }
     mk_res_kind other = return liftedTypeKind
 
@@ -289,44 +516,23 @@ kindedTyVarKind (L _ (KindedTyVar _ k)) = k
 kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
        -- Not used for type synonyms (see kcSynDecl)
 
-kcTyClDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
-  = kcTyClDeclBody decl        $ \ tvs' ->
-    do { ctxt' <- kcHsContext ctxt     
-       ; cons' <- mappM (wrapLocM kc_con_decl) cons
-       ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdCons = cons'}) }
-  where
-    kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res) = do
-      kcHsTyVars ex_tvs $ \ex_tvs' -> do
-        ex_ctxt' <- kcHsContext ex_ctxt
-        details' <- kc_con_details details 
-        res'     <- case res of
-          ResTyH98 -> return ResTyH98
-          ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
-        return (ConDecl name expl ex_tvs' ex_ctxt' details' res')
-
-    kc_con_details (PrefixCon btys) 
-       = do { btys' <- mappM kc_larg_ty btys ; return (PrefixCon btys') }
-    kc_con_details (InfixCon bty1 bty2) 
-       = do { bty1' <- kc_larg_ty bty1; bty2' <- kc_larg_ty bty2; return (InfixCon bty1' bty2') }
-    kc_con_details (RecCon fields) 
-       = do { fields' <- mappM kc_field fields; return (RecCon fields') }
-
-    kc_field (fld, bty) = do { bty' <- kc_larg_ty bty ; return (fld, bty') }
+kcTyClDecl decl@(TyData {})
+  = ASSERT( not . isJust $ tcdTyPats decl )   -- must not be instance of idx ty
+    kcTyClDeclBody decl        $
+      kcDataDecl decl
 
-    kc_larg_ty bty = case new_or_data of
-                       DataType -> kcHsSigType bty
-                       NewType  -> kcHsLiftedSigType bty
-       -- Can't allow an unlifted type for newtypes, because we're effectively
-       -- going to remove the constructor while coercing it to a lifted type.
-       -- And newtypes can't be bang'd
+kcTyClDecl decl@(TyFunction {})
+  = kcTyClDeclBody decl $ \ tvs' ->
+      return (decl {tcdTyVars = tvs'})
 
-kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt,  tcdSigs = sigs})
+kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
   = kcTyClDeclBody decl        $ \ tvs' ->
     do { is_boot <- tcIsHsBoot
-       ; checkTc (not is_boot) badBootClassDeclErr
        ; ctxt' <- kcHsContext ctxt     
-       ; sigs' <- mappM (wrapLocM kc_sig) sigs
-       ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs'}) }
+       ; ats'  <- mappM (wrapLocM kcTyClDecl) ats
+       ; sigs' <- mappM (wrapLocM kc_sig    ) sigs
+       ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs',
+                       tcdATs = ats'}) }
   where
     kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
                                   ; return (TypeSig nm op_ty') }
@@ -342,7 +548,7 @@ kcTyClDeclBody :: TyClDecl Name
 -- Unpack it, and attribute those kinds to the type variables
 -- Extend the env with bindings for the tyvars, taken from
 -- the kind of the tycon/class.  Give it to the thing inside, and 
- -- check the result kind matches
+-- check the result kind matches
 kcTyClDeclBody decl thing_inside
   = tcAddDeclCtxt decl         $
     do         { tc_ty_thing <- tcLookupLocated (tcdLName decl)
@@ -353,6 +559,42 @@ kcTyClDeclBody decl thing_inside
                           [ L loc (KindedTyVar (hsTyVarName tv) k)
                           | (L loc tv, k) <- zip hs_tvs kinds]
        ; tcExtendKindEnvTvs kinded_tvs (thing_inside kinded_tvs) }
+
+-- 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).
+--
+kcDataDecl :: TyClDecl Name -> [LHsTyVarBndr Name] -> TcM (TyClDecl Name)
+kcDataDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
+          tvs
+  = do { ctxt' <- kcHsContext ctxt     
+       ; cons' <- mappM (wrapLocM kc_con_decl) cons
+       ; return (decl {tcdTyVars = tvs, tcdCtxt = ctxt', tcdCons = cons'}) }
+  where
+    kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res) = do
+      kcHsTyVars ex_tvs $ \ex_tvs' -> do
+        ex_ctxt' <- kcHsContext ex_ctxt
+        details' <- kc_con_details details 
+        res'     <- case res of
+          ResTyH98 -> return ResTyH98
+          ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
+        return (ConDecl name expl ex_tvs' ex_ctxt' details' res')
+
+    kc_con_details (PrefixCon btys) 
+       = do { btys' <- mappM kc_larg_ty btys ; return (PrefixCon btys') }
+    kc_con_details (InfixCon bty1 bty2) 
+       = do { bty1' <- kc_larg_ty bty1; bty2' <- kc_larg_ty bty2; return (InfixCon bty1' bty2') }
+    kc_con_details (RecCon fields) 
+       = do { fields' <- mappM kc_field fields; return (RecCon fields') }
+
+    kc_field (fld, bty) = do { bty' <- kc_larg_ty bty ; return (fld, bty') }
+
+    kc_larg_ty bty = case new_or_data of
+                       DataType -> kcHsSigType bty
+                       NewType  -> kcHsLiftedSigType bty
+       -- Can't allow an unlifted type for newtypes, because we're effectively
+       -- going to remove the constructor while coercing it to a lifted type.
+       -- And newtypes can't be bang'd
 \end{code}
 
 
@@ -363,28 +605,63 @@ kcTyClDeclBody decl thing_inside
 %************************************************************************
 
 \begin{code}
-tcSynDecls :: (Name -> ArgVrcs) -> [LTyClDecl Name] -> TcM [TyThing]
-tcSynDecls calc_vrcs [] = return []
-tcSynDecls calc_vrcs (decl : decls) 
-  = do { syn_tc <- addLocM (tcSynDecl calc_vrcs) decl
-       ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls calc_vrcs decls)
+tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
+tcSynDecls [] = return []
+tcSynDecls (decl : decls) 
+  = do { syn_tc <- addLocM tcSynDecl decl
+       ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
        ; return (syn_tc : syn_tcs) }
 
-tcSynDecl calc_vrcs 
+tcSynDecl
   (TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { traceTc (text "tcd1" <+> ppr tc_name) 
     ; rhs_ty' <- tcHsKindedType rhs_ty
-    ; return (ATyCon (buildSynTyCon tc_name tvs' rhs_ty' (calc_vrcs tc_name))) }
+    ; return (ATyCon (buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty'))) }
 
 --------------------
-tcTyClDecl :: (Name -> ArgVrcs) -> (Name -> RecFlag) 
-          -> TyClDecl Name -> TcM TyThing
+tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
+
+tcTyClDecl calc_isrec decl
+  = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
 
-tcTyClDecl calc_vrcs calc_isrec decl
-  = tcAddDeclCtxt decl (tcTyClDecl1 calc_vrcs calc_isrec decl)
+  -- kind signature for a type function
+tcTyClDecl1 _calc_isrec 
+  (TyFunction {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = kind})
+  = tcTyVarBndrs tvs  $ \ tvs' -> do 
+  { traceTc (text "type family: " <+> ppr tc_name) 
+  ; gla_exts <- doptM Opt_IndexedTypes
+
+       -- Check that we don't use kind signatures without Glasgow extensions
+  ; checkTc gla_exts $ badSigTyDecl tc_name
+
+  ; return [ATyCon $ buildSynTyCon tc_name tvs' (OpenSynTyCon kind)]
+  }
 
-tcTyClDecl1 calc_vrcs calc_isrec 
+  -- kind signature for an indexed data type
+tcTyClDecl1 _calc_isrec 
+  (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
+          tcdLName = L _ tc_name, tcdKindSig = Just ksig, tcdCons = []})
+  = tcTyVarBndrs tvs  $ \ tvs' -> do 
+  { traceTc (text "data/newtype family: " <+> ppr tc_name) 
+  ; extra_tvs <- tcDataKindSig (Just ksig)
+  ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
+
+  ; checkTc (null . unLoc $ ctxt) $ badKindSigCtxt tc_name
+  ; gla_exts <- doptM Opt_IndexedTypes
+
+       -- Check that we don't use kind signatures without Glasgow extensions
+  ; checkTc gla_exts $ badSigTyDecl tc_name
+
+  ; tycon <- buildAlgTyCon tc_name final_tvs [] 
+              (case new_or_data of
+                 DataType -> OpenDataTyCon
+                 NewType  -> OpenNewTyCon)
+              Recursive False True Nothing
+  ; return [ATyCon tycon]
+  }
+
+tcTyClDecl1 calc_isrec
   (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
           tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
   = tcTyVarBndrs tvs   $ \ tvs' -> do 
@@ -399,8 +676,14 @@ tcTyClDecl1 calc_vrcs calc_isrec
        -- Check that we don't use GADT syntax in H98 world
   ; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
 
+       -- Check that we don't use kind signatures without Glasgow extensions
+  ; checkTc (gla_exts || isNothing mb_ksig) (badSigTyDecl tc_name)
+
+       -- Check that the stupid theta is empty for a GADT-style declaration
+  ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+
        -- Check that there's at least one condecl,
-       -- or else we're reading an interface file, or -fglasgow-exts
+       -- or else we're reading an hs-boot file, or -fglasgow-exts
   ; checkTc (not (null cons) || gla_exts || is_boot)
            (emptyConDeclsErr tc_name)
     
@@ -412,77 +695,98 @@ tcTyClDecl1 calc_vrcs calc_isrec
        { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data 
                                                 tycon final_tvs)) 
                             cons
-       ; let tc_rhs 
-               | null cons && is_boot  -- In a hs-boot file, empty cons means
-               = AbstractTyCon         -- "don't know"; hence Abstract
-               | otherwise
-               = case new_or_data of
-                       DataType -> mkDataTyConRhs data_cons
-                       NewType  -> ASSERT( isSingleton data_cons )
-                                   mkNewTyConRhs tycon (head data_cons)
-       ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs arg_vrcs is_rec
-                       (want_generic && canDoGenerics data_cons)
+       ; tc_rhs <-
+           if null cons && is_boot     -- In a hs-boot file, empty cons means
+           then return AbstractTyCon   -- "don't know"; hence Abstract
+           else case new_or_data of
+                  DataType -> return (mkDataTyConRhs data_cons)
+                  NewType  -> 
+                       ASSERT( isSingleton data_cons )
+                       mkNewTyConRhs tc_name tycon (head data_cons)
+       ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
+           (want_generic && canDoGenerics data_cons) h98_syntax Nothing
        })
-  ; return (ATyCon tycon)
+  ; return [ATyCon tycon]
   }
   where
-    arg_vrcs = calc_vrcs tc_name
     is_rec   = calc_isrec tc_name
     h98_syntax = case cons of  -- All constructors have same shape
                        L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
                        other -> True
 
-tcTyClDecl1 calc_vrcs calc_isrec 
+tcTyClDecl1 calc_isrec 
   (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs, 
              tcdCtxt = ctxt, tcdMeths = meths,
-             tcdFDs = fundeps, tcdSigs = sigs} )
+             tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
   { ctxt' <- tcHsKindedContext ctxt
   ; fds' <- mappM (addLocM tc_fundep) fundeps
+  ; atss <- mappM (addLocM (tcTyClDecl1 (const Recursive))) ats
+  ; let ats' = zipWith setTyThingPoss atss (map (tcdTyVars . unLoc) ats)
   ; sig_stuff <- tcClassSigs class_name sigs meths
   ; clas <- fixM (\ clas ->
                let     -- This little knot is just so we can get
                        -- hold of the name of the class TyCon, which we
-                       -- need to look up its recursiveness and variance
+                       -- need to look up its recursiveness
                    tycon_name = tyConName (classTyCon clas)
                    tc_isrec = calc_isrec tycon_name
-                   tc_vrcs  = calc_vrcs  tycon_name
                in
-               buildClass class_name tvs' ctxt' fds' 
-                          sig_stuff tc_isrec tc_vrcs)
-  ; return (AClass clas) }
+               buildClass class_name tvs' ctxt' fds' ats'
+                          sig_stuff tc_isrec)
+  ; return (AClass clas : ats')
+      -- NB: Order is important due to the call to `mkGlobalThings' when
+      --     tying the the type and class declaration type checking knot.
+  }
   where
     tc_fundep (tvs1, tvs2) = do { tvs1' <- mappM tcLookupTyVar tvs1 ;
                                ; tvs2' <- mappM tcLookupTyVar tvs2 ;
                                ; return (tvs1', tvs2') }
 
-
-tcTyClDecl1 calc_vrcs calc_isrec 
+    -- For each AT argument compute the position of the corresponding class
+    -- parameter in the class head.  This will later serve as a permutation
+    -- vector when checking the validity of instance declarations.
+    setTyThingPoss [ATyCon tycon] atTyVars = 
+      let classTyVars = hsLTyVarNames tvs
+         poss        =   catMaybes 
+                       . map (`elemIndex` classTyVars) 
+                       . hsLTyVarNames 
+                       $ atTyVars
+                    -- There will be no Nothing, as we already passed renaming
+      in 
+      ATyCon (setTyConArgPoss tycon poss)
+    setTyThingPoss _             _ = panic "TcTyClsDecls.setTyThingPoss"
+
+tcTyClDecl1 calc_isrec 
   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
-  = returnM (ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0 []))
+  = returnM [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
 
 -----------------------------------
 tcConDecl :: Bool              -- True <=> -funbox-strict_fields
-         -> NewOrData -> TyCon -> [TyVar]
-         -> ConDecl Name -> TcM DataCon
+         -> NewOrData 
+         -> TyCon -> [TyVar] 
+         -> ConDecl Name 
+         -> TcM DataCon
 
 tcConDecl unbox_strict NewType tycon tc_tvs    -- Newtypes
          (ConDecl name _ ex_tvs ex_ctxt details ResTyH98)
   = do { let tc_datacon field_lbls arg_ty
                = do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
                     ; buildDataCon (unLoc name) False {- Prefix -} 
-                                   True {- Vanilla -} [NotMarkedStrict]
+                                   [NotMarkedStrict]
                                    (map unLoc field_lbls)
-                                   tc_tvs [] [arg_ty']
-                                   tycon (mkTyVarTys tc_tvs) }
+                                   tc_tvs []  -- No existentials
+                                   [] []      -- No equalities, predicates
+                                   [arg_ty']
+                                   tycon }
 
                -- Check that a newtype has no existential stuff
        ; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
 
        ; case details of
-           PrefixCon [arg_ty] -> tc_datacon [] arg_ty
+           PrefixCon [arg_ty]           -> tc_datacon [] arg_ty
            RecCon [(field_lbl, arg_ty)] -> tc_datacon [field_lbl] arg_ty
-           other -> failWithTc (newtypeFieldErr name (length (hsConArgs details)))
+           other                        -> 
+             failWithTc (newtypeFieldErr name (length (hsConArgs details)))
                        -- Check that the constructor has exactly one field
        }
 
@@ -490,30 +794,19 @@ tcConDecl unbox_strict DataType tycon tc_tvs      -- Data types
          (ConDecl name _ tvs ctxt details res_ty)
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { ctxt' <- tcHsKindedContext ctxt
-    ; (data_tc, res_ty_args) <- tcResultType tycon tc_tvs res_ty
+    ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
     ; let 
-       con_tvs = case res_ty of
-                   ResTyH98    -> tc_tvs ++ tvs'
-                   ResTyGADT _ -> tryVanilla tvs' res_ty_args
-
-       -- Vanilla iff result type matches the quantified vars exactly,
-       -- and there is no existential context
-       -- Must check the context too because of implicit params; e.g.
-       --      data T = (?x::Int) => MkT Int
-       is_vanilla = res_ty_args `tcEqTypes` mkTyVarTys con_tvs
-                    && null (unLoc ctxt)
-
        tc_datacon is_infix field_lbls btys
          = do { let bangs = map getBangStrictness btys
               ; arg_tys <- mappM tcHsBangType btys
-              ; buildDataCon (unLoc name) is_infix is_vanilla
+              ; buildDataCon (unLoc name) is_infix
                    (argStrictness unbox_strict tycon bangs arg_tys)
                    (map unLoc field_lbls)
-                   con_tvs ctxt' arg_tys
-                   data_tc res_ty_args }
-               -- NB:  we put data_tc, the type constructor gotten from the constructor 
-               --      type signature into the data constructor; that way 
-               --      checkValidDataCon can complain if it's wrong.
+                   univ_tvs ex_tvs eq_preds ctxt' arg_tys
+                   data_tc }
+               -- NB:  we put data_tc, the type constructor gotten from the
+               --      constructor type signature into the data constructor;
+               --      that way checkValidDataCon can complain if it's wrong.
 
     ; case details of
        PrefixCon btys     -> tc_datacon False [] btys
@@ -524,19 +817,48 @@ tcConDecl unbox_strict DataType tycon tc_tvs      -- Data types
                               
     }
 
-tcResultType :: TyCon -> [TyVar] -> ResType Name -> TcM (TyCon, [TcType])
-tcResultType tycon tvs ResTyH98           = return (tycon, mkTyVarTys tvs)
-tcResultType _     _   (ResTyGADT res_ty) = tcLHsConResTy res_ty
-
-tryVanilla :: [TyVar] -> [TcType] -> [TyVar]
--- (tryVanilla tvs tys) returns a permutation of tvs.
--- It tries to re-order the tvs so that it exactly 
--- matches the [Type], if that is possible
-tryVanilla tvs (ty:tys) | Just tv <- tcGetTyVar_maybe ty       -- The type is a tyvar
-                       , tv `elem` tvs                         -- That tyvar is in the list
-                       = tv : tryVanilla (delete tv tvs) tys
-tryVanilla tvs tys = tvs       -- Fall through case
-
+tcResultType :: TyCon
+            -> [TyVar]         -- data T a b c = ...
+            -> [TyVar]         -- where MkT :: forall a b c. ...
+            -> ResType Name
+            -> TcM ([TyVar],           -- Universal
+                    [TyVar],           -- Existential
+                    [(TyVar,Type)],    -- Equality predicates
+                    TyCon)             -- TyCon given in the ResTy
+       -- We don't check that the TyCon given in the ResTy is
+       -- the same as the parent tycon, becuase we are in the middle
+       -- of a recursive knot; so it's postponed until checkValidDataCon
+
+tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
+  = return (tc_tvs, dc_tvs, [], decl_tycon)
+       -- In H98 syntax the dc_tvs are the existential ones
+       --      data T a b c = forall d e. MkT ...
+       -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
+
+tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
+       -- E.g.  data T a b c where
+       --         MkT :: forall x y z. T (x,y) z z
+       -- Then we generate
+       --      ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
+
+  = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
+               -- NB: tc_tvs and dc_tvs are distinct
+       ; let univ_tvs = choose_univs [] tc_tvs res_tys
+               -- Each univ_tv is either a dc_tv or a tc_tv
+             ex_tvs = dc_tvs `minusList` univ_tvs
+             eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys, 
+                                     tv `elem` tc_tvs]
+       ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
+  where
+       -- choose_univs uses the res_ty itself if it's a type variable
+       -- and hasn't already been used; otherwise it uses one of the tc_tvs
+    choose_univs used tc_tvs []
+       = ASSERT( null tc_tvs ) []
+    choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys) 
+       | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
+       = tv    : choose_univs (tv:used) tc_tvs res_tys
+       | otherwise
+       = tc_tv : choose_univs used tc_tvs res_tys
 
 -------------------
 argStrictness :: Bool          -- True <=> -funbox-strict_fields
@@ -549,19 +871,28 @@ argStrictness unbox_strict tycon bangs arg_tys
 -- We attempt to unbox/unpack a strict field when either:
 --   (i)  The field is marked '!!', or
 --   (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
-
+--
+-- We have turned off unboxing of newtypes because coercions make unboxing 
+-- and reboxing more complicated
 chooseBoxingStrategy :: Bool -> TyCon -> TcType -> HsBang -> StrictnessMark
 chooseBoxingStrategy unbox_strict_fields tycon arg_ty bang
   = case bang of
        HsNoBang                                    -> NotMarkedStrict
-       HsStrict | unbox_strict_fields && can_unbox -> MarkedUnboxed
-       HsUnbox  | can_unbox                        -> MarkedUnboxed
+       HsStrict | unbox_strict_fields 
+                   && can_unbox arg_ty                     -> MarkedUnboxed
+       HsUnbox  | can_unbox arg_ty                 -> MarkedUnboxed
        other                                       -> MarkedStrict
   where
-    can_unbox = case splitTyConApp_maybe arg_ty of
-                  Nothing             -> False
-                  Just (arg_tycon, _) -> not (isRecursiveTyCon tycon) &&
-                                         isProductTyCon arg_tycon
+    -- we can unbox if the type is a chain of newtypes with a product tycon
+    -- at the end
+    can_unbox arg_ty = case splitTyConApp_maybe arg_ty of
+                  Nothing                      -> False
+                  Just (arg_tycon, tycon_args) -> 
+                       not (isRecursiveTyCon tycon) &&
+                      isProductTyCon arg_tycon &&
+                       (if isNewTyCon arg_tycon then 
+                            can_unbox (newTyConInstRhs arg_tycon tycon_args)
+                        else True)
 \end{code}
 
 %************************************************************************
@@ -607,9 +938,11 @@ checkValidTyCl decl
 -- of the constructor.
 
 checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
+checkValidTyCon tc 
   | isSynTyCon tc 
-  = checkValidType syn_ctxt syn_rhs
+  = case synTyConRhs tc of
+      OpenSynTyCon _  -> return ()
+      SynonymTyCon ty -> checkValidType syn_ctxt ty
   | otherwise
   =    -- Check the context on the data decl
     checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)    `thenM_` 
@@ -623,7 +956,6 @@ checkValidTyCon tc
   where
     syn_ctxt  = TySynCtxt name
     name      = tyConName tc
-    syn_rhs   = synTyConRhs tc
     data_cons = tyConDataCons tc
 
     groups = equivClasses cmp_fld (concatMap get_fields data_cons)
@@ -631,14 +963,20 @@ checkValidTyCon tc
     get_fields con = dataConFieldLabels con `zip` repeat con
        -- dataConFieldLabels may return the empty list, which is fine
 
-    -- XXX - autrijus - Make this far more complex to acommodate 
-    --       for different return types.  Add res_ty to the mix,
-    --       comparing them in two steps, all for good error messages.
-    --       Plan: Use Unify.tcMatchTys to compare the first candidate's
-    --             result type against other candidates' types (check bothways).
-    --             If they magically agrees, take the substitution and
-    --             apply them to the latter ones, and see if they match perfectly.
-    -- check_fields fields@((first_field_label, field_ty) : other_fields)
+    -- See Note [GADT record selectors] in MkId.lhs
+    -- We must check (a) that the named field has the same 
+    --                   type in each constructor
+    --               (b) that those constructors have the same result type
+    --
+    -- However, the constructors may have differently named type variable
+    -- and (worse) we don't know how the correspond to each other.  E.g.
+    --     C1 :: forall a b. { f :: a, g :: b } -> T a b
+    --     C2 :: forall d c. { f :: c, g :: c } -> T c d
+    -- 
+    -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
+    -- result type against other candidates' types BOTH WAYS ROUND.
+    -- If they magically agrees, take the substitution and
+    -- apply them to the latter ones, and see if they match perfectly.
     check_fields fields@((label, con1) : other_fields)
        -- These fields all have the same name, but are from
        -- different constructors in the data type
@@ -647,7 +985,7 @@ checkValidTyCon tc
                -- NB: this check assumes that all the constructors of a given
                -- data type use the same type variables
         where
-        tvs1 = mkVarSet (dataConTyVars con1)
+        tvs1 = mkVarSet (dataConAllTyVars con1)
         res1 = dataConResTys con1
         fty1 = dataConFieldType con1 label
 
@@ -655,7 +993,7 @@ checkValidTyCon tc
            = do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
                 ; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
            where        
-                tvs2 = mkVarSet (dataConTyVars con2)
+                tvs2 = mkVarSet (dataConAllTyVars con2)
                res2 = dataConResTys con2 
                 fty2 = dataConFieldType con2 label
 
@@ -672,18 +1010,9 @@ checkValidDataCon tc con
   = setSrcSpan (srcLocSpan (getSrcLoc con))    $
     addErrCtxt (dataConCtxt con)               $ 
     do { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
-       ; checkValidType ctxt (idType (dataConWrapId con)) }
-
-               -- This checks the argument types and
-               -- ambiguity of the existential context (if any)
-               -- 
-               -- Note [Sept 04] Now that tvs is all the tvs, this
-               -- test doesn't actually check anything
---     ; checkFreeness tvs ex_theta }
+       ; checkValidType ctxt (dataConUserType con) }
   where
     ctxt = ConArgCtxt (dataConName con) 
---    (tvs, ex_theta, _, _, _) = dataConSig con
-
 
 -------------------------------
 checkValidClass :: Class -> TcM ()
@@ -809,6 +1138,9 @@ badGadtDecl tc_name
   = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
         , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
 
+badStupidTheta tc_name
+  = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
+
 newtypeConError tycon n
   = sep [ptext SLIT("A newtype must have exactly one constructor,"),
         nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]
@@ -821,9 +1153,46 @@ newtypeFieldErr con_name n_flds
   = sep [ptext SLIT("The constructor of a newtype must have exactly one field"), 
         nest 2 $ ptext SLIT("but") <+> quotes (ppr con_name) <+> ptext SLIT("has") <+> speakN n_flds]
 
+badSigTyDecl tc_name
+  = vcat [ ptext SLIT("Illegal kind signature") <+>
+          quotes (ppr tc_name)
+        , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow indexed types")) ]
+
+badKindSigCtxt tc_name
+  = vcat [ ptext SLIT("Illegal context in kind signature") <+>
+          quotes (ppr tc_name)
+        , nest 2 (parens $ ptext SLIT("Currently, kind signatures cannot have a context")) ]
+
+badIdxTyDecl tc_name
+  = vcat [ ptext SLIT("Illegal indexed type instance for") <+>
+          quotes (ppr tc_name)
+        , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow indexed types")) ]
+
+badGadtIdxTyDecl tc_name
+  = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+>
+          quotes (ppr tc_name)
+        , nest 2 (parens $ ptext SLIT("Indexed types cannot use GADT declarations")) ]
+
+tooManyParmsErr tc_name
+  = ptext SLIT("Indexed type instance has too many parameters:") <+> 
+    quotes (ppr tc_name)
+
+tooFewParmsErr tc_name
+  = ptext SLIT("Indexed type instance has too few parameters:") <+> 
+    quotes (ppr tc_name)
+
+badBootTyIdxDeclErr = 
+  ptext SLIT("Illegal indexed type instance in hs-boot file")
+
+wrongKindOfFamily family =
+  ptext SLIT("Wrong category of type instance; declaration was for a") <+>
+  kindOfFamily
+  where
+    kindOfFamily | isSynTyCon  family = ptext SLIT("type synonym")
+                | isDataTyCon family = ptext SLIT("data type")
+                | isNewTyCon  family = ptext SLIT("newtype")
+
 emptyConDeclsErr tycon
   = sep [quotes (ppr tycon) <+> ptext SLIT("has no constructors"),
         nest 2 $ ptext SLIT("(-fglasgow-exts permits this)")]
-
-badBootClassDeclErr = ptext SLIT("Illegal class declaration in hs-boot file")
 \end{code}