Basic set up for global family instance environment
[ghc-hetmet.git] / compiler / typecheck / TcTyClsDecls.lhs
index 3cf6145..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, isClassDecl, hsConArgs,
-                         LTyClDecl, tcdName, hsTyVarName, LHsTyVarBndr
+                         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,27 +25,35 @@ import BuildTyCl    ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
 import TcRnMonad
 import TcEnv           ( TyThing(..), 
                          tcLookupLocated, tcLookupLocatedGlobal, 
-                         tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
-                         tcExtendRecEnv, tcLookupTyVar, InstInfo )
+                         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, Type, tyVarsOfType, mkPhiTy,
                          mkArrowKind, liftedTypeKind, mkTyVarTys, 
                          tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type            ( PredType(..), splitTyConApp_maybe, mkTyVarTy
+import Type            ( PredType(..), splitTyConApp_maybe, mkTyVarTy,
+                          newTyConInstRhs, isLiftedTypeKind, Kind
                          -- 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 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 )
@@ -51,17 +61,18 @@ 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 List            ( partition, elemIndex )
+import SrcLoc          ( Located(..), unLoc, getLoc, srcLocSpan, 
+                         srcSpanStart )
 import ListSetOps      ( equivClasses, minusList )
-import List            ( delete )
 import Digraph         ( SCC(..) )
 import DynFlags                ( DynFlag( Opt_GlasgowExts, Opt_Generics, 
-                                       Opt_UnboxStrictFields ) )
+                                  Opt_UnboxStrictFields, Opt_IndexedTypes ) )
 \end{code}
 
 
@@ -148,29 +159,41 @@ 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
@@ -178,7 +201,7 @@ tcTyAndClassDecls boot_details decls
 
                        -- 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 +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
@@ -214,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
 %*                                                                     *
 %************************************************************************
@@ -240,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
@@ -256,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) }
@@ -275,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
 
@@ -317,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')
+kcTyClDecl decl@(TyData {})
+  = ASSERT( not . isJust $ tcdTyPats decl )   -- must not be instance of idx ty
+    kcTyClDeclBody decl        $
+      kcDataDecl decl
 
-    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@(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 +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)
@@ -381,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}
 
 
@@ -403,15 +617,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 +676,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 +704,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,32 +721,51 @@ 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)
@@ -511,9 +783,10 @@ 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
+           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
        }
 
@@ -531,9 +804,9 @@ tcConDecl unbox_strict DataType tycon tc_tvs        -- Data types
                    (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
@@ -598,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}
 
 %************************************************************************
@@ -658,7 +940,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 +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)
@@ -751,15 +1034,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 +1153,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"),