[project @ 2004-10-11 16:16:20 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcTyClsDecls.lhs
index 225b4de..9516686 100644 (file)
 %
-% (c) The AQUA Project, Glasgow University, 1996
+% (c) The AQUA Project, Glasgow University, 1996-1998
 %
 \section[TcTyClsDecls]{Typecheck type and class declarations}
 
 \begin{code}
-#include "HsVersions.h"
-
 module TcTyClsDecls (
-       tcTyAndClassDecls1
+       tcTyAndClassDecls
     ) where
 
-IMP_Ubiq(){-uitous-}
+#include "HsVersions.h"
 
-import HsSyn           ( HsDecl(..), TyDecl(..),  ConDecl(..), ConDetails(..), BangType(..),
-                         ClassDecl(..), HsType(..), HsTyVar, DefaultDecl, InstDecl,
-                         IfaceSig, Sig(..), MonoBinds, Fake, InPat, HsBinds(..), HsExpr, NewOrData,
-                         hsDeclName
-                       )
-import RnHsSyn         ( RenamedTyDecl(..), RenamedClassDecl(..), SYN_IE(RenamedHsDecl)
+import HsSyn           ( TyClDecl(..),  HsConDetails(..), HsTyVarBndr(..),
+                         ConDecl(..),   Sig(..), , NewOrData(..), 
+                         tyClDeclTyVars, isSynDecl, LConDecl,
+                         LTyClDecl, tcdName, LHsTyVarBndr, LHsContext
                        )
-import TcHsSyn         ( SYN_IE(TcHsBinds), TcIdOcc(..) )
-
-import TcMonad
-import Inst            ( SYN_IE(InstanceMapper) )
-import TcClassDcl      ( tcClassDecl1 )
-import TcEnv           ( tcExtendTyConEnv, tcExtendClassEnv )
-import SpecEnv         ( SpecEnv )
-import TcKind          ( TcKind, newKindVars )
-import TcTyDecls       ( tcTyDecl, mkDataBinds )
-import TcMonoType      ( tcTyVarScope )
-
-import Bag     
-import Class           ( SYN_IE(Class) )
-import Digraph         ( stronglyConnComp, SCC(..) )
-import Name            ( Name, getSrcLoc, isTvOcc, nameOccName )
+import HsTypes          ( HsBang(..), getBangStrictness )
+import BasicTypes      ( RecFlag(..), StrictnessMark(..) )
+import HscTypes                ( implicitTyThings )
+import BuildTyCl       ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
+                         mkDataTyConRhs, mkNewTyConRhs )
+import TcRnMonad
+import TcEnv           ( TcTyThing(..), TyThing(..), 
+                         tcLookupLocated, tcLookupLocatedGlobal, 
+                         tcExtendGlobalEnv, tcExtendKindEnv,
+                         tcExtendRecEnv, tcLookupTyVar )
+import TcTyDecls       ( calcTyConArgVrcs, calcRecFlags, calcClassCycles, calcSynCycles )
+import TcClassDcl      ( tcClassSigs, tcAddDeclCtxt )
+import TcHsType                ( kcHsTyVars, kcHsLiftedSigType, kcHsType, 
+                         kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
+                         kcHsSigType, tcHsBangType, tcLHsConSig )
+import TcMType         ( newKindVar, checkValidTheta, checkValidType, checkFreeness, 
+                         UserTypeCtxt(..), SourceTyCtxt(..) ) 
+import TcUnify         ( unifyKind )
+import TcType          ( TcKind, ThetaType, TcType, tyVarsOfType, 
+                         mkArrowKind, liftedTypeKind, mkTyVarTys, tcEqTypes,
+                         tcSplitSigmaTy, tcEqType )
+import Type            ( splitTyConApp_maybe, pprThetaArrow, pprParendType )
+import Generics                ( validGenericMethodType, canDoGenerics )
+import Class           ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
+import TyCon           ( TyCon, ArgVrcs, 
+                         tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
+                         tyConStupidTheta, getSynTyConDefn, tyConDataCons, isSynTyCon, tyConName )
+import DataCon         ( DataCon, dataConWrapId, dataConName, dataConSig, 
+                         dataConFieldLabels, dataConOrigArgTys, dataConTyCon )
+import Type            ( zipTopTvSubst, substTys )
+import Var             ( TyVar, idType, idName )
+import VarSet          ( elemVarSet )
+import Name            ( Name )
 import Outputable
-import Pretty
-import Maybes          ( mapMaybe )
-import UniqSet         ( SYN_IE(UniqSet), emptyUniqSet,
-                         unitUniqSet, unionUniqSets, 
-                         unionManyUniqSets, uniqSetToList ) 
-import SrcLoc          ( SrcLoc )
-import TyCon           ( TyCon, SYN_IE(Arity) )
-import Unique          ( Unique, Uniquable(..) )
-import Util            ( panic{-, pprTrace-} )
-
+import Util            ( zipLazy, isSingleton, notNull, sortLe )
+import List            ( partition )
+import SrcLoc          ( Located(..), unLoc, getLoc )
+import ListSetOps      ( equivClasses )
+import Digraph         ( SCC(..) )
+import CmdLineOpts     ( DynFlag( Opt_GlasgowExts, Opt_Generics, Opt_UnboxStrictFields ) )
 \end{code}
 
-The main function
-~~~~~~~~~~~~~~~~~
-\begin{code}
-tcTyAndClassDecls1 :: TcEnv s -> InstanceMapper        -- Knot tying stuff
-                  -> [RenamedHsDecl]
-                  -> TcM s (TcEnv s)
 
-tcTyAndClassDecls1 unf_env inst_mapper decls
-  = sortByDependency decls             `thenTc` \ groups ->
-    tcGroups unf_env inst_mapper groups
+%************************************************************************
+%*                                                                     *
+\subsection{Type checking for type and class declarations}
+%*                                                                     *
+%************************************************************************
 
-tcGroups unf_env inst_mapper []
-  = tcGetEnv   `thenNF_Tc` \ env ->
-    returnTc env
+Dealing with a group
+~~~~~~~~~~~~~~~~~~~~
+Consider a mutually-recursive group, binding 
+a type constructor T and a class C.
 
-tcGroups unf_env inst_mapper (group:groups)
-  = tcGroup unf_env inst_mapper group  `thenTc` \ new_env ->
+Step 1:        getInitialKind
+       Construct a KindEnv by binding T and C to a kind variable 
 
-       -- Extend the environment using the new tycons and classes
-    tcSetEnv new_env $
+Step 2:        kcTyClDecl
+       In that environment, do a kind check
 
-       -- Do the remaining groups
-    tcGroups unf_env inst_mapper groups
-\end{code}
+Step 3: Zonk the kinds
 
-Dealing with a group
-~~~~~~~~~~~~~~~~~~~~
-\begin{code}
-tcGroup :: TcEnv s -> InstanceMapper -> Bag RenamedHsDecl -> TcM s (TcEnv s)
-tcGroup unf_env inst_mapper decls
-  =    -- TIE THE KNOT
-    fixTc ( \ ~(tycons,classes,_) ->
-
-               -- EXTEND TYPE AND CLASS ENVIRONMENTS
-               -- NB: it's important that the tycons and classes come back in just
-               -- the same order from this fix as from get_binders, so that these
-               -- extend-env things work properly.  A bit UGH-ish.
-      tcExtendTyConEnv tycon_names_w_arities tycons              $
-      tcExtendClassEnv class_names classes                       $
-
-               -- DEAL WITH TYPE VARIABLES
-      tcTyVarScope tyvar_names                         ( \ tyvars ->
-
-               -- DEAL WITH THE DEFINITIONS THEMSELVES
-       foldBag combine (tcDecl unf_env inst_mapper)
-               (returnTc (emptyBag, emptyBag))
-               decls
-      )                                                `thenTc` \ (tycon_bag,class_bag) ->
-      let
-       tycons = bagToList tycon_bag
-       classes = bagToList class_bag
-      in 
-
-               -- SNAFFLE ENV TO RETURN
-      tcGetEnv                                 `thenNF_Tc` \ final_env ->
-
-      returnTc (tycons, classes, final_env)
-    ) `thenTc` \ (_, _, final_env) ->
-
-    returnTc final_env
+Step 4:        buildTyConOrClass
+       Construct an environment binding T to a TyCon and C to a Class.
+       a) Their kinds comes from zonking the relevant kind variable
+       b) Their arity (for synonyms) comes direct from the decl
+       c) The funcional dependencies come from the decl
+       d) The rest comes a knot-tied binding of T and C, returned from Step 4
+       e) The variances of the tycons in the group is calculated from 
+               the knot-tied stuff
 
-  where
-    (tyvar_names, tycon_names_w_arities, class_names) = get_binders decls
+Step 5:        tcTyClDecl1
+       In this environment, walk over the decls, constructing the TyCons and Classes.
+       This uses in a strict way items (a)-(c) above, which is why they must
+       be constructed in Step 4. Feed the results back to Step 4.
+       For this step, pass the is-recursive flag as the wimp-out flag
+       to tcTyClDecl1.
+       
 
-    combine do_a do_b
-      = do_a `thenTc` \ (a1,a2) ->
-        do_b `thenTc` \ (b1,b2) ->
-       returnTc (a1 `unionBags` b1, a2 `unionBags` b2)
-\end{code}
+Step 6:                Extend environment
+       We extend the type environment with bindings not only for the TyCons and Classes,
+       but also for their "implicit Ids" like data constructors and class selectors
 
-Dealing with one decl
-~~~~~~~~~~~~~~~~~~~~~
-\begin{code}
-tcDecl  :: TcEnv s -> InstanceMapper
-       -> RenamedHsDecl
-       -> TcM s (Bag TyCon, Bag Class)
+Step 7:                checkValidTyCl
+       For a recursive group only, check all the decls again, just
+       to check all the side conditions on validity.  We could not
+       do this before because we were in a mutually recursive knot.
 
-tcDecl unf_env inst_mapper (TyD decl)
-  = tcTyDecl decl      `thenTc` \ tycon ->
-    returnTc (unitBag tycon, emptyBag)
 
-tcDecl unf_env inst_mapper (ClD decl)
-  = tcClassDecl1 unf_env inst_mapper decl   `thenTc` \ clas ->
-    returnTc (emptyBag, unitBag clas)
-\end{code}
+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.
 
-Dependency analysis
-~~~~~~~~~~~~~~~~~~~
 \begin{code}
-sortByDependency :: [RenamedHsDecl] -> TcM s [Bag RenamedHsDecl]
-sortByDependency decls
-  = let                -- CHECK FOR SYNONYM CYCLES
-       syn_sccs   = stronglyConnComp (filter is_syn_decl edges)
-       syn_cycles = [ decls | CyclicSCC decls <- syn_sccs]
-
-    in
-    checkTc (null syn_cycles) (typeCycleErr syn_cycles)                `thenTc_`
+tcTyAndClassDecls :: [Name] -> [LTyClDecl Name]
+                  -> TcM TcGblEnv      -- Input env extended by types and classes 
+                                       -- and their implicit Ids,DataCons
+tcTyAndClassDecls boot_names decls
+  = do {       -- First check for cyclic type synonysm or classes
+               -- See notes with checkCycleErrs
+         checkCycleErrs decls
+       ; mod <- getModule
+       ; traceTc (text "tcTyAndCl" <+> ppr mod <+> ppr boot_names)
+       ; (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 }
+
+                       -- 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 }
+               ; 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)
+                     ; calc_rec  = calcRecFlags boot_names rec_alg_tyclss
+                     ; tc_decl   = addLocM (tcTyClDecl calc_vrcs calc_rec) }
+                       -- Type-check the type synonyms, and extend the envt
+               ; syn_tycons <- tcSynDecls calc_vrcs 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)
+           }}})
+       -- Finished with knot-tying now
+       -- Extend the environment with the finished things
+       ; tcExtendGlobalEnv (syn_tycons ++ alg_tyclss) $ do
+
+       -- Perform the validity check
+       { traceTc (text "ready for validity check")
+       ; mappM_ (addLocM checkValidTyCl) decls
+       ; traceTc (text "done")
+   
+       -- Add the implicit things;
+       -- we want them in the environment because 
+       -- they may be mentioned in interface files
+       ; let { implicit_things = concatMap implicitTyThings alg_tyclss }
+       ; traceTc ((text "Adding" <+> ppr alg_tyclss) $$ (text "and" <+> ppr implicit_things))
+       ; tcExtendGlobalEnv implicit_things getGblEnv
+    }}
+
+mkGlobalThings :: [LTyClDecl Name]     -- The decls
+              -> [TyThing]             -- Knot-tied, in 1-1 correspondence with the decls
+              -> [(Name,TyThing)]
+-- Driven by the Decls, and treating the TyThings lazily
+-- make a TypeEnv for the new things
+mkGlobalThings decls things
+  = map mk_thing (decls `zipLazy` things)
+  where
+    mk_thing (L _ (ClassDecl {tcdLName = L _ name}), ~(AClass cl))
+        = (name, AClass cl)
+    mk_thing (L _ decl, ~(ATyCon tc))
+         = (tcdName decl, ATyCon tc)
+\end{code}
 
-    let                -- CHECK FOR CLASS CYCLES
-       cls_sccs   = stronglyConnComp (filter is_cls_decl edges)
-       cls_cycles = [ decls | CyclicSCC decls <- cls_sccs]
 
-    in
-    checkTc (null cls_cycles) (classCycleErr cls_cycles)       `thenTc_`
+%************************************************************************
+%*                                                                     *
+               Kind checking
+%*                                                                     *
+%************************************************************************
 
-               -- DO THE MAIN DEPENDENCY ANALYSIS
-    let
-       decl_sccs  = stronglyConnComp (filter is_ty_cls_decl edges)
-       scc_bags   = map bag_acyclic decl_sccs
-    in
-    returnTc (scc_bags)
+We need to kind check all types in the mutually recursive group
+before we know the kind of the type variables.  For example:
 
-  where
-    edges = mapMaybe mk_edges decls
-    
-bag_acyclic (AcyclicSCC scc) = unitBag scc
-bag_acyclic (CyclicSCC sccs) = listToBag sccs
+class C a where
+   op :: D b => a -> b -> b
 
-is_syn_decl (TyD (TySynonym _ _ _ _), _, _) = True
-is_syn_decl _                              = False
+class D c where
+   bop :: (Monad c) => ...
 
-is_ty_cls_decl (TyD _, _, _) = True
-is_ty_cls_decl (ClD _, _, _) = True
-is_ty_cls_decl other         = False
+Here, the kind of the locally-polymorphic type variable "b"
+depends on *all the uses of class D*.  For example, the use of
+Monad c in bop's type signature means that D must have kind Type->Type.
 
-is_cls_decl (ClD _, _, _) = True
-is_cls_decl other         = False
-\end{code}
+However type synonyms work differently.  They can have kinds which don't
+just involve (->) and *:
+       type R = Int#           -- Kind #
+       type S a = Array# a     -- Kind * -> #
+       type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
+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.
 
-Edges in Type/Class decls
-~~~~~~~~~~~~~~~~~~~~~~~~~
 \begin{code}
-mk_edges decl@(TyD (TyData _ ctxt name _ condecls derivs _ _))
-  = Just (decl, uniqueOf name, uniqSetToList (get_ctxt ctxt `unionUniqSets` 
-                                        get_cons condecls `unionUniqSets` 
-                                        get_deriv derivs))
+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
+       ; tcExtendKindEnv alg_kinds $ do
+
+               -- Now kind-check the type synonyms, in dependency order
+               -- We do these differently to data type and classes,
+               -- because a type synonym can be an unboxed type
+               --      type Foo = Int#
+               -- and a kind variable can't unify with UnboxedTypeKind
+               -- So we infer their kinds in dependency order
+       { (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
+
+       ; return (kc_syn_decls, kc_alg_decls) }}}
+
+------------------------------------------------------------------------
+getInitialKind :: LTyClDecl Name -> TcM (Name, TcKind)
+
+getInitialKind decl
+ = newKindVar                  `thenM` \ kind  ->
+   returnM (unLoc (tcdLName (unLoc decl)), kind)
+
+----------------
+kcSynDecls :: [SCC (LTyClDecl Name)] 
+          -> TcM ([LTyClDecl Name],    -- Kind-annotated decls
+                  [(Name,TcKind)])     -- Kind bindings
+kcSynDecls []
+  = return ([], [])
+kcSynDecls (group : groups)
+  = do { (decl,  nk)  <- kcSynDecl group
+       ; (decls, nks) <- tcExtendKindEnv [nk] (kcSynDecls groups)
+       ; return (decl:decls, nk:nks) }
+                       
+----------------
+kcSynDecl :: SCC (LTyClDecl Name) 
+          -> TcM (LTyClDecl Name,      -- Kind-annotated decls
+                  (Name,TcKind))       -- Kind bindings
+kcSynDecl (AcyclicSCC ldecl@(L loc decl))
+  = tcAddDeclCtxt decl $
+    kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
+    do { traceTc (text "kcd1" <+> ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl)) 
+                       <+> brackets (ppr k_tvs))
+       ; (k_rhs, rhs_kind) <- kcHsType (tcdSynRhs decl)
+       ; traceTc (text "kcd2" <+> ppr (unLoc (tcdLName decl)))
+       ; let tc_kind = foldr (mkArrowKind . kindedTyVarKind) rhs_kind k_tvs
+       ; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
+                (unLoc (tcdLName decl), tc_kind)) })
+
+kcSynDecl (CyclicSCC decls)
+  = do { recSynErr decls; failM }      -- Fail here to avoid error cascade
+                                       -- of out-of-scope tycons
+
+------------------------------------------------------------------------
+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 ex_tvs ex_ctxt details)
+      = kcHsTyVars ex_tvs              $ \ ex_tvs' ->
+       do { ex_ctxt' <- kcHsContext ex_ctxt
+          ; details' <- kc_con_details details 
+          ; return (ConDecl name ex_tvs' ex_ctxt' details')}
+    kc_con_decl (GadtDecl name ty)
+        = do { ty' <- kcHsSigType ty
+            ; return (GadtDecl name ty') }
+
+    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
+
+kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt,  tcdSigs = sigs})
+  = kcTyClDeclBody decl        $ \ tvs' ->
+    do { ctxt' <- kcHsContext ctxt     
+       ; sigs' <- mappM (wrapLocM kc_sig) sigs
+       ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs'}) }
+  where
+    kc_sig (Sig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
+                               ; return (Sig nm op_ty') }
+    kc_sig other_sig         = return other_sig
+
+kcTyClDecl decl@(ForeignType {})
+  = return decl
+
+kcTyClDeclBody :: TyClDecl Name
+              -> ([LHsTyVarBndr Name] -> TcM a)
+              -> TcM a
+  -- 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
+kcTyClDeclBody decl thing_inside
+  = tcAddDeclCtxt decl         $
+    kcHsTyVars (tyClDeclTyVars decl)   $ \ kinded_tvs ->
+    do         { tc_ty_thing <- tcLookupLocated (tcdLName decl)
+       ; let tc_kind = case tc_ty_thing of { AThing k -> k }
+       ; unifyKind tc_kind (foldr (mkArrowKind . kindedTyVarKind) 
+                                  (result_kind decl)
+                                  kinded_tvs)
+       ; thing_inside kinded_tvs }
+  where
+    result_kind (TyData { tcdKindSig = Just kind }) = kind
+    result_kind other                             = liftedTypeKind
+       -- On GADT-style declarations we allow a kind signature
+       --      data T :: *->* where { ... }
 
-mk_edges decl@(TyD (TySynonym name _ rhs _))
-  = Just (decl, uniqueOf name, uniqSetToList (get_ty rhs))
+kindedTyVarKind (L _ (KindedTyVar _ k)) = k
+\end{code}
 
-mk_edges decl@(ClD (ClassDecl ctxt name _ sigs _ _ _))
-  = Just (decl, uniqueOf name, uniqSetToList (get_ctxt ctxt `unionUniqSets`
-                                        get_sigs sigs))
 
-mk_edges other_decl = Nothing
+%************************************************************************
+%*                                                                     *
+\subsection{Type checking}
+%*                                                                     *
+%************************************************************************
 
-get_ctxt ctxt = unionManyUniqSets (map (set_name.fst) ctxt)
+\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)
+       ; return (syn_tc : syn_tcs) }
+
+tcSynDecl calc_vrcs 
+  (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))) }
+
+--------------------
+tcTyClDecl :: (Name -> ArgVrcs) -> (Name -> RecFlag) 
+          -> TyClDecl Name -> TcM TyThing
+
+tcTyClDecl calc_vrcs calc_isrec decl
+  = tcAddDeclCtxt decl (tcTyClDecl1 calc_vrcs calc_isrec decl)
+
+tcTyClDecl1 calc_vrcs calc_isrec 
+  (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
+          tcdLName = L _ tc_name, tcdCons = cons})
+  = tcTyVarBndrs tvs           $ \ tvs' -> do 
+  { stupid_theta <- tcStupidTheta ctxt cons
+  ; want_generic <- doptM Opt_Generics
+  ; tycon <- fixM (\ tycon -> do 
+       { unbox_strict <- doptM Opt_UnboxStrictFields
+       ; gla_exts <- doptM Opt_GlasgowExts
+       ; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
+
+       ; data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data tycon tvs')) cons
+       ; let tc_rhs = case new_or_data of
+                       DataType -> mkDataTyConRhs stupid_theta data_cons
+                       NewType  -> ASSERT( isSingleton data_cons )
+                                   mkNewTyConRhs tycon (head data_cons)
+       ; buildAlgTyCon tc_name tvs' tc_rhs arg_vrcs is_rec
+                       (want_generic && canDoGenerics data_cons)
+       })
+  ; 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 _ (GadtDecl {}) : _ -> False
+                       other -> True
+
+tcTyClDecl1 calc_vrcs calc_isrec 
+  (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs, 
+             tcdCtxt = ctxt, tcdMeths = meths,
+             tcdFDs = fundeps, tcdSigs = sigs} )
+  = tcTyVarBndrs tvs           $ \ tvs' -> do 
+  { ctxt' <- tcHsKindedContext ctxt
+  ; fds' <- mappM (addLocM tc_fundep) fundeps
+  ; 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
+                   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) }
+  where
+    tc_fundep (tvs1, tvs2) = do { tvs1' <- mappM tcLookupTyVar tvs1 ;
+                               ; tvs2' <- mappM tcLookupTyVar tvs2 ;
+                               ; return (tvs1', tvs2') }
+
+
+tcTyClDecl1 calc_vrcs calc_isrec 
+  (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
+  = returnM (ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0 []))
+
+-----------------------------------
+tcConDecl :: Bool              -- True <=> -funbox-strict_fields
+         -> NewOrData -> TyCon -> [TyVar]
+         -> ConDecl Name -> TcM DataCon
+
+tcConDecl unbox_strict NewType tycon tc_tvs    -- Newtypes
+         (ConDecl name ex_tvs ex_ctxt details)
+  = ASSERT( null ex_tvs && null (unLoc ex_ctxt) )      
+    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]
+                                   (map unLoc field_lbls)
+                                   tc_tvs [] [arg_ty']
+                                   tycon (mkTyVarTys tc_tvs) }
+       ; case details of
+           PrefixCon [arg_ty] -> tc_datacon [] arg_ty
+           RecCon [(field_lbl, arg_ty)] -> tc_datacon [field_lbl] arg_ty }
+
+tcConDecl unbox_strict DataType tycon tc_tvs   -- Ordinary data types
+         (ConDecl name ex_tvs ex_ctxt details)
+  = tcTyVarBndrs ex_tvs                $ \ ex_tvs' -> do 
+    { ex_ctxt' <- tcHsKindedContext ex_ctxt
+    ; let 
+       is_vanilla = null ex_tvs && null (unLoc ex_ctxt) 
+               -- Vanilla iff no ex_tvs and no context
+
+       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
+                   (argStrictness unbox_strict tycon bangs arg_tys)
+                   (map unLoc field_lbls)
+                   (tc_tvs ++ ex_tvs')
+                   ex_ctxt'
+                   arg_tys
+                   tycon (mkTyVarTys tc_tvs) }
+    ; case details of
+       PrefixCon btys     -> tc_datacon False [] btys
+       InfixCon bty1 bty2 -> tc_datacon True [] [bty1,bty2]
+       RecCon fields      -> do { checkTc is_vanilla (exRecConErr name)
+                                ; let { (field_names, btys) = unzip fields }
+                                ; tc_datacon False field_names btys } }
+
+tcConDecl unbox_strict DataType tycon tc_tvs   -- GADTs
+         decl@(GadtDecl name con_ty)
+  = do { traceTc (text "tcConDecl"  <+> ppr name)
+       ; (tvs, theta, bangs, arg_tys, tc, res_tys) <- tcLHsConSig con_ty
+               
+       ; traceTc (text "tcConDecl1"  <+> ppr name)
+       ; let   -- Now dis-assemble the type, and check its form
+             is_vanilla = null theta && mkTyVarTys tvs `tcEqTypes` res_tys
+
+               -- Vanilla datacons guarantee to use the same
+               -- type variables as the parent tycon
+             (tvs', arg_tys', res_tys') 
+                 | is_vanilla = (tc_tvs, substTys subst arg_tys, substTys subst res_tys)
+                 | otherwise  = (tvs, arg_tys, res_tys)
+             subst = zipTopTvSubst tvs (mkTyVarTys tc_tvs)
+
+       ; traceTc (text "tcConDecl3"  <+> ppr name)
+       ; buildDataCon (unLoc name) False {- Not infix -} is_vanilla
+                      (argStrictness unbox_strict tycon bangs arg_tys)
+                      [{- No field labels -}]
+                      tvs' theta arg_tys' tycon res_tys' }
+
+-------------------
+tcStupidTheta :: LHsContext Name -> [LConDecl Name] -> TcM (Maybe ThetaType)
+-- For GADTs we don't allow a context on the data declaration
+-- whereas for standard Haskell style data declarations, we do
+tcStupidTheta ctxt (L _ (ConDecl _ _ _ _) : _)
+  = do { theta <- tcHsKindedContext ctxt; return (Just theta) }
+tcStupidTheta ctxt other       -- Includes an empty constructor list
+  = ASSERT( null (unLoc ctxt) ) return Nothing
+
+-------------------
+argStrictness :: Bool          -- True <=> -funbox-strict_fields
+             -> TyCon -> [HsBang]
+             -> [TcType] -> [StrictnessMark]
+argStrictness unbox_strict tycon bangs arg_tys
+ = ASSERT( length bangs == length arg_tys )
+   zipWith (chooseBoxingStrategy unbox_strict tycon) 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
+  = case bang of
+       HsNoBang                                    -> NotMarkedStrict
+       HsStrict | unbox_strict_fields && can_unbox -> MarkedUnboxed
+       HsUnbox  | can_unbox                        -> MarkedUnboxed
+       other                                       -> MarkedStrict
+  where
+    can_unbox = case splitTyConApp_maybe arg_ty of
+                  Nothing             -> False
+                  Just (arg_tycon, _) -> not (isRecursiveTyCon tycon) &&
+                                         isProductTyCon arg_tycon
+\end{code}
 
-get_deriv Nothing     = emptyUniqSet
-get_deriv (Just clss) = unionManyUniqSets (map set_name clss)
+%************************************************************************
+%*                                                                     *
+\subsection{Dependency analysis}
+%*                                                                     *
+%************************************************************************
 
-get_cons cons = unionManyUniqSets (map get_con cons)
+Validity checking is done once the mutually-recursive knot has been
+tied, so we can look at things freely.
 
-get_con (ConDecl _ ctxt details _) 
-  = get_ctxt ctxt `unionUniqSets` get_con_details details
+\begin{code}
+checkCycleErrs :: [LTyClDecl Name] -> TcM ()
+checkCycleErrs tyclss
+  | null cls_cycles
+  = return ()
+  | otherwise
+  = do { mappM_ recClsErr cls_cycles
+       ; failM }       -- Give up now, because later checkValidTyCl
+                       -- will loop if the synonym is recursive
+  where
+    cls_cycles = calcClassCycles tyclss
+
+checkValidTyCl :: TyClDecl Name -> TcM ()
+-- We do the validity check over declarations, rather than TyThings
+-- only so that we can add a nice context with tcAddDeclCtxt
+checkValidTyCl decl
+  = tcAddDeclCtxt decl $
+    do { thing <- tcLookupLocatedGlobal (tcdLName decl)
+       ; traceTc (text "Validity of" <+> ppr thing)    
+       ; case thing of
+           ATyCon tc -> checkValidTyCon tc
+           AClass cl -> checkValidClass cl 
+       ; traceTc (text "Done validity of" <+> ppr thing)       
+       }
+
+-------------------------
+checkValidTyCon :: TyCon -> TcM ()
+checkValidTyCon tc
+  | isSynTyCon tc 
+  = checkValidType syn_ctxt syn_rhs
+  | otherwise
+  =    -- Check the context on the data decl
+    checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)    `thenM_` 
+       
+       -- Check arg types of data constructors
+    mappM_ (checkValidDataCon tc) data_cons                    `thenM_`
+
+       -- Check that fields with the same name share a type
+    mappM_ check_fields groups
 
-get_con_details (VanillaCon btys)    = unionManyUniqSets (map get_bty btys)
-get_con_details (InfixCon bty1 bty2) = unionUniqSets (get_bty bty1) (get_bty bty2)
-get_con_details (NewCon ty)          =  get_ty ty
-get_con_details (RecCon nbtys)       = unionManyUniqSets (map (get_bty.snd) nbtys)
+  where
+    syn_ctxt    = TySynCtxt name
+    name         = tyConName tc
+    (_, syn_rhs) = getSynTyConDefn tc
+    data_cons    = tyConDataCons tc
+
+    groups = equivClasses cmp_fld (concatMap get_fields data_cons)
+    cmp_fld (f1,_) (f2,_) = f1 `compare` f2
+    get_fields con = dataConFieldLabels con `zip` dataConOrigArgTys con
+       -- dataConFieldLabels may return the empty list, which is fine
+
+    check_fields fields@((first_field_label, field_ty) : other_fields)
+       -- These fields all have the same name, but are from
+       -- different constructors in the data type
+       =       -- Check that all the fields in the group have the same type
+               -- NB: this check assumes that all the constructors of a given
+               -- data type use the same type variables
+         checkTc (all (tcEqType field_ty . snd) other_fields) 
+                 (fieldTypeMisMatch first_field_label)
+
+-------------------------------
+checkValidDataCon :: TyCon -> DataCon -> TcM ()
+checkValidDataCon tc 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 }
+  where
+    ctxt = ConArgCtxt (dataConName con) 
+    (tvs, ex_theta, _, _, _) = dataConSig con
 
-get_bty (Banged ty)   = get_ty ty
-get_bty (Unbanged ty) = get_ty ty
 
-get_ty (MonoTyVar name)
-  = if isTvOcc (nameOccName name) then emptyUniqSet else set_name name
-get_ty (MonoTyApp ty1 ty2)
-  = unionUniqSets (get_ty ty1) (get_ty ty2)
-get_ty (MonoFunTy ty1 ty2)     
-  = unionUniqSets (get_ty ty1) (get_ty ty2)
-get_ty (MonoListTy tc ty)
-  = set_name tc `unionUniqSets` get_ty ty
-get_ty (MonoTupleTy tc tys)
-  = set_name tc `unionUniqSets` get_tys tys
-get_ty (HsForAllTy _ ctxt mty)
-  = get_ctxt ctxt `unionUniqSets` get_ty mty
-get_ty other = panic "TcTyClsDecls:get_ty"
+-------------------------------
+checkValidClass :: Class -> TcM ()
+checkValidClass cls
+  = do {       -- CHECK ARITY 1 FOR HASKELL 1.4
+         gla_exts <- doptM Opt_GlasgowExts
 
-get_tys tys
-  = unionManyUniqSets (map get_ty tys)
+       -- Check that the class is unary, unless GlaExs
+       ; checkTc (notNull tyvars) (nullaryClassErr cls)
+       ; checkTc (gla_exts || unary) (classArityErr cls)
 
-get_sigs sigs
-  = unionManyUniqSets (map get_sig sigs)
-  where 
-    get_sig (ClassOpSig _ _ ty _) = get_ty ty
-    get_sig other = panic "TcTyClsDecls:get_sig"
+       -- Check the super-classes
+       ; checkValidTheta (ClassSCCtxt (className cls)) theta
 
-set_name name = unitUniqSet (uniqueOf name)
+       -- Check the class operations
+       ; mappM_ check_op op_stuff
 
-set_to_bag set = listToBag (uniqSetToList set)
-\end{code}
+       -- Check that if the class has generic methods, then the
+       -- class has only one parameter.  We can't do generic
+       -- multi-parameter type classes!
+       ; checkTc (unary || no_generics) (genericMultiParamErr cls)
+       }
+  where
+    (tyvars, theta, _, op_stuff) = classBigSig cls
+    unary      = isSingleton tyvars
+    no_generics = null [() | (_, GenDefMeth) <- op_stuff]
 
+    check_op (sel_id, dm) 
+      = addErrCtxt (classOpCtxt sel_id tau) $ do
+       { checkValidTheta SigmaCtxt (tail theta)
+               -- The 'tail' removes the initial (C a) from the
+               -- class itself, leaving just the method type
 
-get_binders
-~~~~~~~~~~~
-Extract *binding* names from type and class decls.  Type variables are
-bound in type, data, newtype and class declarations and the polytypes
-in the class op sigs.
+       ; checkValidType (FunSigCtxt op_name) tau
 
-Why do we need to grab all these type variables at once, including
-those locally-quantified type variables in class op signatures?
-Because we can only commit to the final kind of a type variable when
-we've completed the mutually recursive group. For example:
+               -- Check that the type mentions at least one of
+               -- the class type variables
+       ; checkTc (any (`elemVarSet` tyVarsOfType tau) tyvars)
+                 (noClassTyVarErr cls sel_id)
 
-class C a where
-   op :: D b => a -> b -> b
+               -- Check that for a generic method, the type of 
+               -- the method is sufficiently simple
+       ; checkTc (dm /= GenDefMeth || validGenericMethodType tau)
+                 (badGenericMethodType op_name op_ty)
+       }
+       where
+         op_name = idName sel_id
+         op_ty   = idType sel_id
+         (_,theta,tau) = tcSplitSigmaTy op_ty
 
-class D c where
-   bop :: (Monad c) => ...
 
-Here, the kind of the locally-polymorphic type variable "b"
-depends on *all the uses of class D*.  For example, the use of
-Monad c in bop's type signature means that D must have kind Type->Type.
 
+---------------------------------------------------------------------
+fieldTypeMisMatch field_name
+  = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
 
-\begin{code}
-get_binders :: Bag RenamedHsDecl
-           -> ([HsTyVar Name],         -- TyVars;  no dups
-               [(Name, Maybe Arity)],  -- Tycons;  no dups; arities for synonyms
-               [Name])                 -- Classes; no dups
+dataConCtxt con = sep [ptext SLIT("When checking the data constructor:"),
+                      nest 2 (ex_part <+> pprThetaArrow ex_theta <+> ppr con <+> arg_part)]
+  where
+    (ex_tvs, ex_theta, arg_tys, _, _) = dataConSig con
+    ex_part | null ex_tvs = empty
+           | otherwise   = ptext SLIT("forall") <+> hsep (map ppr ex_tvs) <> dot
+       -- The 'ex_theta' part could be non-empty, if the user (bogusly) wrote
+       --      data T a = Eq a => T a a
+       -- So we make sure to print it
+
+    fields = dataConFieldLabels con
+    arg_part | null fields = sep (map pprParendType arg_tys)
+            | otherwise   = braces (sep (punctuate comma 
+                            [ ppr n <+> dcolon <+> ppr ty 
+                            | (n,ty) <- fields `zip` arg_tys]))
+
+classOpCtxt sel_id tau = sep [ptext SLIT("When checking the class method:"),
+                             nest 2 (ppr sel_id <+> dcolon <+> ppr tau)]
+
+nullaryClassErr cls
+  = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
+
+classArityErr cls
+  = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
+         parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
+
+noClassTyVarErr clas op
+  = sep [ptext SLIT("The class method") <+> quotes (ppr op),
+        ptext SLIT("mentions none of the type variables of the class") <+> 
+               ppr clas <+> hsep (map ppr (classTyVars clas))]
+
+genericMultiParamErr clas
+  = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+> 
+    ptext SLIT("cannot have generic methods")
+
+badGenericMethodType op op_ty
+  = hang (ptext SLIT("Generic method type is too complex"))
+       4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
+               ptext SLIT("You can only use type variables, arrows, lists, and tuples")])
+
+recSynErr syn_decls
+  = setSrcSpan (getLoc (head sorted_decls)) $
+    addErr (sep [ptext SLIT("Cycle in type synonym declarations:"),
+                nest 2 (vcat (map ppr_decl sorted_decls))])
+  where
+    sorted_decls = sortLocated syn_decls
+    ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
 
-get_binders decls = (bagToList tyvars, bagToList tycons, bagToList classes)
+recClsErr cls_decls
+  = setSrcSpan (getLoc (head sorted_decls)) $
+    addErr (sep [ptext SLIT("Cycle in class declarations (via superclasses):"),
+                nest 2 (vcat (map ppr_decl sorted_decls))])
   where
-    (tyvars, tycons, classes) = foldBag union3 get_binders1
-                                       (emptyBag,emptyBag,emptyBag)
-                                       decls
-
-    union3 (a1,a2,a3) (b1,b2,b3)
-      = (a1 `unionBags` b1, a2 `unionBags` b2, a3 `unionBags` b3)
-
-get_binders1 (TyD (TyData _ _ name tyvars _ _ _ _))
- = (listToBag tyvars, unitBag (name,Nothing), emptyBag)
-get_binders1 (TyD (TySynonym name tyvars _ _))
- = (listToBag tyvars, unitBag (name, Just (length tyvars)), emptyBag)
-get_binders1 (ClD (ClassDecl _ name tyvar sigs _ _ _))
- = (unitBag tyvar `unionBags` sigs_tvs sigs,
-    emptyBag, unitBag name)
-
-sigs_tvs sigs = unionManyBags (map sig_tvs sigs)
-  where 
-    sig_tvs (ClassOpSig _ _ ty _) = pty_tvs ty
-    pty_tvs (HsForAllTy tvs _ _)  = listToBag tvs      -- tvs doesn't include the class tyvar
-    pty_tvs other                = emptyBag
-\end{code}
+    sorted_decls = sortLocated cls_decls
+    ppr_decl (L loc decl) = ppr loc <> colon <+> ppr (decl { tcdSigs = [] })
 
+sortLocated :: [Located a] -> [Located a]
+sortLocated things = sortLe le things
+  where
+    le (L l1 _) (L l2 _) = l1 <= l2
 
-\begin{code}
-typeCycleErr syn_cycles sty
-  = vcat (map (pp_cycle sty "Cycle in type declarations ...") syn_cycles)
+exRecConErr name
+  = ptext SLIT("Can't combine named fields with locally-quantified type variables or context")
+    $$
+    (ptext SLIT("In the declaration of data constructor") <+> ppr name)
 
-classCycleErr cls_cycles sty
-  = vcat (map (pp_cycle sty "Cycle in class declarations ...") cls_cycles)
+badDataConTyCon data_con
+  = hang (ptext SLIT("Data constructor does not return its parent type:"))
+       2 (ppr data_con)
 
-pp_cycle sty str decls
-  = hang (text str)
-        4 (vcat (map pp_decl decls))
-  where
-    pp_decl decl
-      = hsep [ppr sty name, ppr sty (getSrcLoc name)]
-     where
-        name = hsDeclName decl
+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")) ]
 \end{code}