More import tidying and fixing the stage 2 build
[ghc-hetmet.git] / compiler / typecheck / TcTyClsDecls.lhs
index 3cf6145..8ab053e 100644 (file)
@@ -1,67 +1,49 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The AQUA Project, Glasgow University, 1996-1998
 %
-\section[TcTyClsDecls]{Typecheck type and class declarations}
+
+TcTyClsDecls: Typecheck type and class declarations
 
 \begin{code}
 module TcTyClsDecls (
-       tcTyAndClassDecls
+       tcTyAndClassDecls, tcIdxTyInstDecl
     ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( TyClDecl(..),  HsConDetails(..), HsTyVarBndr(..),
-                         ConDecl(..),   Sig(..), NewOrData(..), ResType(..),
-                         tyClDeclTyVars, isSynDecl, isClassDecl, hsConArgs,
-                         LTyClDecl, tcdName, hsTyVarName, LHsTyVarBndr
-                       )
-import HsTypes          ( HsBang(..), getBangStrictness )
-import BasicTypes      ( RecFlag(..), StrictnessMark(..) )
-import HscTypes                ( implicitTyThings, ModDetails )
-import BuildTyCl       ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
-                         mkDataTyConRhs, mkNewTyConRhs )
+import HsSyn
+import HsTypes
+import BasicTypes
+import HscTypes
+import BuildTyCl
 import TcRnMonad
-import TcEnv           ( TyThing(..), 
-                         tcLookupLocated, tcLookupLocatedGlobal, 
-                         tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
-                         tcExtendRecEnv, tcLookupTyVar, InstInfo )
-import TcTyDecls       ( calcRecFlags, calcClassCycles, calcSynCycles )
-import TcClassDcl      ( tcClassSigs, tcAddDeclCtxt )
-import TcHsType                ( kcHsTyVars, kcHsLiftedSigType, kcHsType, 
-                         kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
-                         kcHsSigType, tcHsBangType, tcLHsConResTy, tcDataKindSig )
-import TcMType         ( newKindVar, checkValidTheta, checkValidType, 
-                         -- checkFreeness, 
-                         UserTypeCtxt(..), SourceTyCtxt(..) ) 
-import TcType          ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
-                         mkArrowKind, liftedTypeKind, mkTyVarTys, 
-                         tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type            ( PredType(..), splitTyConApp_maybe, mkTyVarTy
-                         -- pprParendType, pprThetaArrow
-                       )
-import Generics                ( validGenericMethodType, canDoGenerics )
-import Class           ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
-import TyCon           ( TyCon, AlgTyConRhs( AbstractTyCon ),
-                         tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
-                         tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName )
-import DataCon         ( DataCon, dataConUserType, dataConName, 
-                         dataConFieldLabels, dataConTyCon, dataConAllTyVars,
-                         dataConFieldType, dataConResTys )
-import Var             ( TyVar, idType, idName )
-import VarSet          ( elemVarSet, mkVarSet )
-import Name            ( Name, getSrcLoc )
+import TcEnv
+import TcTyDecls
+import TcClassDcl
+import TcHsType
+import TcMType
+import TcType
+import Type
+import Generics
+import Class
+import TyCon
+import DataCon
+import Var
+import VarSet
+import Name
+import OccName
 import Outputable
-import Maybe           ( isJust )
-import Maybes          ( expectJust )
-import Unify           ( tcMatchTys, tcMatchTyX )
-import Util            ( zipLazy, isSingleton, notNull, sortLe )
-import List            ( partition )
-import SrcLoc          ( Located(..), unLoc, getLoc, srcLocSpan )
-import ListSetOps      ( equivClasses, minusList )
-import List            ( delete )
-import Digraph         ( SCC(..) )
-import DynFlags                ( DynFlag( Opt_GlasgowExts, Opt_Generics, 
-                                       Opt_UnboxStrictFields ) )
+import Maybes
+import Monad
+import Unify
+import Util
+import SrcLoc
+import ListSetOps
+import Digraph
+import DynFlags
+
+import Data.List        ( partition, elemIndex )
 \end{code}
 
 
@@ -148,37 +130,50 @@ indeed type families).  I think.
 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
+         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 }
+                                                  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_rec  = calcRecFlags boot_details rec_alg_tyclss
+               ; let { -- Calculate rec-flag
+                     ; calc_rec  = calcRecFlags boot_details rec_alg_tyclss
                      ; tc_decl   = addLocM (tcTyClDecl calc_rec) }
+
                        -- Type-check the type synonyms, and extend the envt
                ; 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
@@ -192,10 +187,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
@@ -214,6 +221,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 <- TcRnMonad.zipWithM kcCheckHsType hs_typats kinds
+       ; thing_inside tvs typats resultKind family
+       }
+  where
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
                Kind checking
 %*                                                                     *
 %************************************************************************
@@ -240,11 +385,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
@@ -256,18 +414,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) }
@@ -275,8 +444,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
 
@@ -317,44 +488,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') }
+kcTyClDecl decl@(TyData {})
+  = ASSERT( not . isJust $ tcdTyPats decl )   -- must not be instance of idx ty
+    kcTyClDeclBody decl        $
+      kcDataDecl decl
 
-    kc_field (fld, bty) = do { bty' <- kc_larg_ty bty ; return (fld, bty') }
+kcTyClDecl decl@(TyFunction {})
+  = kcTyClDeclBody decl $ \ tvs' ->
+      return (decl {tcdTyVars = tvs'})
 
-    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
-
--- !!!TODO -=chak
-kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt,  tcdSigs = sigs})
+kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
   = kcTyClDeclBody decl        $ \ tvs' ->
     do { is_boot <- tcIsHsBoot
        ; 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') }
@@ -370,7 +520,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)
@@ -381,6 +531,43 @@ 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
+    -- doc comments are typechecked to Nothing here
+    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' Nothing)
+
+    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 (HsRecField fld bty d) = do { bty' <- kc_larg_ty bty ; return (HsRecField fld bty' d) }
+
+    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}
 
 
@@ -403,15 +590,51 @@ tcSynDecl
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { traceTc (text "tcd1" <+> ppr tc_name) 
     ; rhs_ty' <- tcHsKindedType rhs_ty
-    ; return (ATyCon (buildSynTyCon tc_name tvs' rhs_ty')) }
+    ; return (ATyCon (buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty'))) }
 
 --------------------
-tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM TyThing
+tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
 
 tcTyClDecl calc_isrec decl
   = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
 
-tcTyClDecl1 calc_isrec 
+  -- 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)]
+  }
+
+  -- 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 
@@ -426,6 +649,9 @@ tcTyClDecl1 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)
 
@@ -451,9 +677,9 @@ tcTyClDecl1 calc_isrec
                        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
+           (want_generic && canDoGenerics data_cons) h98_syntax Nothing
        })
-  ; return (ATyCon tycon)
+  ; return [ATyCon tycon]
   }
   where
     is_rec   = calc_isrec tc_name
@@ -468,35 +694,54 @@ tcTyClDecl1 calc_isrec
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
   { ctxt' <- tcHsKindedContext ctxt
   ; fds' <- mappM (addLocM tc_fundep) fundeps
-  -- !!!TODO: process `ats`; what do we want to store in the `Class'? -=chak
+  ; 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
                in
-               buildClass class_name tvs' ctxt' fds' 
+               buildClass class_name tvs' ctxt' fds' ats'
                           sig_stuff tc_isrec)
-  ; return (AClass clas) }
+  ; 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') }
 
+    -- 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)
+         (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 -} 
@@ -511,36 +756,38 @@ tcConDecl unbox_strict NewType tycon tc_tvs       -- Newtypes
        ; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
 
        ; case details of
-           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)))
+           PrefixCon [arg_ty]           -> tc_datacon [] arg_ty
+           RecCon [HsRecField field_lbl arg_ty _] -> tc_datacon [field_lbl] arg_ty
+           other                        -> 
+             failWithTc (newtypeFieldErr name (length (hsConArgs details)))
                        -- Check that the constructor has exactly one field
        }
 
 tcConDecl unbox_strict DataType tycon tc_tvs   -- Data types
-         (ConDecl name _ tvs ctxt details res_ty)
+         (ConDecl name _ tvs ctxt details res_ty _)
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { ctxt' <- tcHsKindedContext ctxt
     ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
     ; let 
+       -- Tiresome: tidy the tyvar binders, since tc_tvs and tvs' may have the same OccNames
        tc_datacon is_infix field_lbls btys
          = do { let bangs = map getBangStrictness btys
               ; arg_tys <- mappM tcHsBangType btys
               ; buildDataCon (unLoc name) is_infix
-                   (argStrictness unbox_strict tycon bangs arg_tys)
+                   (argStrictness unbox_strict bangs arg_tys)
                    (map unLoc field_lbls)
                    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.
+               -- 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
        InfixCon bty1 bty2 -> tc_datacon True  [] [bty1,bty2]
        RecCon fields      -> tc_datacon False field_names btys
                           where
-                             (field_names, btys) = unzip fields
+                             (field_names, btys) = unzip [ (n, t) | HsRecField n t _ <- fields ] 
                               
     }
 
@@ -549,7 +796,7 @@ tcResultType :: TyCon
             -> [TyVar]         -- where MkT :: forall a b c. ...
             -> ResType Name
             -> TcM ([TyVar],           -- Universal
-                    [TyVar],           -- Existential
+                    [TyVar],           -- Existential (distinct OccNames from univs)
                     [(TyVar,Type)],    -- Equality predicates
                     TyCon)             -- TyCon given in the ResTy
        -- We don't check that the TyCon given in the ResTy is
@@ -569,8 +816,8 @@ tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
        --      ([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
+
+       ; let univ_tvs = choose_univs [] tidy_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, 
@@ -587,32 +834,61 @@ tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
        | otherwise
        = tc_tv : choose_univs used tc_tvs res_tys
 
--------------------
+       -- NB: tc_tvs and dc_tvs are distinct, but
+       -- we want them to be *visibly* distinct, both for
+       -- interface files and general confusion.  So rename
+       -- the tc_tvs, since they are not used yet (no 
+       -- consequential renaming needed)
+    init_occ_env     = initTidyOccEnv (map getOccName dc_tvs)
+    (_, tidy_tc_tvs) = mapAccumL tidy_one init_occ_env tc_tvs
+    tidy_one env tv  = (env', setTyVarName tv (tidyNameOcc name occ'))
+             where
+                name = tyVarName tv
+                (env', occ') = tidyOccName env (getOccName name) 
+
+             -------------------
 argStrictness :: Bool          -- True <=> -funbox-strict_fields
-             -> TyCon -> [HsBang]
+             -> [HsBang]
              -> [TcType] -> [StrictnessMark]
-argStrictness unbox_strict tycon bangs arg_tys
+argStrictness unbox_strict bangs arg_tys
  = ASSERT( length bangs == length arg_tys )
-   zipWith (chooseBoxingStrategy unbox_strict tycon) arg_tys bangs
+   zipWith (chooseBoxingStrategy unbox_strict) arg_tys bangs
 
 -- 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.
-
-chooseBoxingStrategy :: Bool -> TyCon -> TcType -> HsBang -> StrictnessMark
-chooseBoxingStrategy unbox_strict_fields tycon arg_ty bang
+--
+-- We have turned off unboxing of newtypes because coercions make unboxing 
+-- and reboxing more complicated
+chooseBoxingStrategy :: Bool -> TcType -> HsBang -> StrictnessMark
+chooseBoxingStrategy unbox_strict_fields 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 arg_tycon) &&     -- Note [Recusive unboxing]
+                      isProductTyCon arg_tycon &&
+                       (if isNewTyCon arg_tycon then 
+                            can_unbox (newTyConInstRhs arg_tycon tycon_args)
+                        else True)
 \end{code}
 
+Note [Recursive unboxing]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Be careful not to try to unbox this!
+       data T = MkT !T Int
+But it's the *argument* type that matters. This is fine:
+       data S = MkS S !Int
+because Int is non-recursive.
+
 %************************************************************************
 %*                                                                     *
 \subsection{Dependency analysis}
@@ -658,7 +934,9 @@ checkValidTyCl decl
 checkValidTyCon :: TyCon -> TcM ()
 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_` 
@@ -672,7 +950,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)
@@ -751,15 +1028,11 @@ checkValidClass cls
        -- class has only one parameter.  We can't do generic
        -- multi-parameter type classes!
        ; checkTc (unary || no_generics) (genericMultiParamErr cls)
-
-       -- Check that the class has no associated types, unless GlaExs
-       ; checkTc (gla_exts || no_ats) (badATDecl cls)
        }
   where
     (tyvars, theta, _, op_stuff) = classBigSig cls
     unary      = isSingleton tyvars
     no_generics = null [() | (_, GenDefMeth) <- op_stuff]
-    no_ats      = True -- !!!TODO: determine whether the class has ATs -=chak
 
     check_op gla_exts (sel_id, dm) 
       = addErrCtxt (classOpCtxt sel_id tau) $ do
@@ -874,9 +1147,44 @@ 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]
 
-badATDecl cl_name
-  = vcat [ ptext SLIT("Illegal associated type declaration in") <+> quotes (ppr cl_name)
-        , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow ATs")) ]
+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"),