[project @ 2002-09-09 12:50:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 4df29b2..d4d506a 100644 (file)
@@ -11,22 +11,23 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, newHoleTyVarTy,
+  newTyVar, 
   newTyVarTy,          -- Kind -> NF_TcM TcType
   newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
   newKindVar, newKindVars, newBoxityVar,
   putTcTyVar, getTcTyVar,
 
+  newHoleTyVarTy, readHoleResult, zapToType,
+
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars,
-  tcInstSigTyVars, tcInstType, tcInstSigType,
-  tcSplitRhoTyM,
+  tcInstTyVar, tcInstTyVars, tcInstType, 
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
   SourceTyCtxt(..), checkValidTheta, 
+  checkValidTyCon, checkValidClass, 
   checkValidInstHead, instTypeErr, checkAmbiguity,
 
   --------------------------------
@@ -47,10 +48,10 @@ import TypeRep              ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see repr
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
                          tcEqType, tcCmpPred,
-                         tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
+                         tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
+                         isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
 
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
@@ -64,29 +65,34 @@ import TcType               ( TcType, TcThetaType, TcTauType, TcPredType,
                        )
 import qualified Type  ( splitFunTys )
 import Subst           ( Subst, mkTopTyVarSubst, substTy )
-import Class           ( Class, classArity, className )
+import Class           ( Class, DefMeth(..), classArity, className, classBigSig )
 import TyCon           ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName, tyConKind )
+                         tyConArity, tyConName, tyConKind, tyConTheta, 
+                         getSynTyConDefn, tyConDataCons )
+import DataCon         ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
+import FieldLabel      ( fieldLabelName, fieldLabelType )
 import PrimRep         ( PrimRep(VoidRep) )
-import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Var             ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
 
 -- others:
+import Generics                ( validGenericMethodType )
 import TcMonad          -- TcType, amongst others
 import TysWiredIn      ( voidTy, listTyCon, tupleTyCon )
 import PrelNames       ( cCallableClassKey, cReturnableClassKey, hasKey )
 import ForeignCall     ( Safety(..) )
 import FunDeps         ( grow )
 import PprType         ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name            ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
-                         mkLocalName, mkDerivedTyConOcc
+import Name            ( Name, NamedThing(..), setNameUnique, 
+                         mkInternalName, mkDerivedTyConOcc, 
+                         mkSystemTvNameEncoded,
                        )
 import VarSet
 import BasicTypes      ( Boxity(Boxed) )
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import Unique          ( Uniquable(..) )
 import SrcLoc          ( noSrcLoc )
-import Util            ( nOfThem, isSingleton, equalLength )
-import ListSetOps      ( removeDups )
+import Util            ( nOfThem, isSingleton, equalLength, notNull )
+import ListSetOps      ( equivClasses, removeDups )
 import Outputable
 \end{code}
 
@@ -101,25 +107,20 @@ import Outputable
 newTyVar :: Kind -> NF_TcM TcTyVar
 newTyVar kind
   = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq FSLIT("t")) kind VanillaTv
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
 
 newTyVarTy  :: Kind -> NF_TcM TcType
 newTyVarTy kind
   = newTyVar kind      `thenNF_Tc` \ tc_tyvar ->
     returnNF_Tc (TyVarTy tc_tyvar)
 
-newHoleTyVarTy :: NF_TcM TcType
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
-    returnNF_Tc (TyVarTy tv)
-
 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 
 newKindVar :: NF_TcM TcKind
 newKindVar
   = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 
 newKindVars :: Int -> NF_TcM [TcKind]
@@ -128,40 +129,46 @@ newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 newBoxityVar :: NF_TcM TcKind
 newBoxityVar
   = tcGetUnique                                                          `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Type instantiation}
+\subsection{'hole' type variables}
 %*                                                                     *
 %************************************************************************
 
-I don't understand why this is needed
-An old comments says "No need for tcSplitForAllTyM because a type 
-       variable can't be instantiated to a for-all type"
-But the same is true of rho types!
-
 \begin{code}
-tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
-tcSplitRhoTyM t
-  = go t t []
- where
-       -- A type variable is never instantiated to a dictionary type,
-       -- so we don't need to do a tcReadVar on the "arg".
-    go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
-                                       Just pair -> go res res (pair:ts)
-                                       Nothing   -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (NoteTy n t)    ts = go syn_t t ts
-    go syn_t (TyVarTy tv)    ts = getTcTyVar tv                `thenNF_Tc` \ maybe_ty ->
-                                 case maybe_ty of
-                                   Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
-                                   other                          -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
-\end{code}
+newHoleTyVarTy :: NF_TcM TcType
+  = tcGetUnique        `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv  `thenNF_Tc` \ tv ->
+    returnNF_Tc (TyVarTy tv)
 
+readHoleResult :: TcType -> NF_TcM TcType
+-- Read the answer out of a hole, constructed by newHoleTyVarTy
+readHoleResult (TyVarTy tv)
+  = ASSERT( isHoleTyVar tv )
+    getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
+    case maybe_res of
+       Just ty -> returnNF_Tc ty
+       Nothing ->  pprPanic "readHoleResult: empty" (ppr tv)
+readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
+
+zapToType :: TcType -> NF_TcM TcType
+zapToType (TyVarTy tv)
+  | isHoleTyVar tv
+  = getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
+    case maybe_res of
+       Nothing -> newTyVarTy openTypeKind      `thenNF_Tc` \ ty ->
+                  putTcTyVar tv ty             `thenNF_Tc_`
+                  returnNF_Tc ty
+       Just ty  -> returnNF_Tc ty      -- No need to loop; we never
+                                       -- have chains of holes
+
+zapToType other_ty = returnNF_Tc other_ty
+\end{code}                
 
 %************************************************************************
 %*                                                                     *
@@ -172,11 +179,11 @@ tcSplitRhoTyM t
 Instantiating a bunch of type variables
 
 \begin{code}
-tcInstTyVars :: [TyVar] 
+tcInstTyVars :: TyVarDetails -> [TyVar] 
             -> NF_TcM ([TcTyVar], [TcType], Subst)
 
-tcInstTyVars tyvars
-  = mapNF_Tc tcInstTyVar tyvars        `thenNF_Tc` \ tc_tyvars ->
+tcInstTyVars tv_details tyvars
+  = mapNF_Tc (tcInstTyVar tv_details) tyvars   `thenNF_Tc` \ tc_tyvars ->
     let
        tys = mkTyVarTys tc_tyvars
     in
@@ -185,7 +192,7 @@ tcInstTyVars tyvars
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence mkTopTyVarSubst
 
-tcInstTyVar tyvar
+tcInstTyVar tv_details tyvar
   = tcGetUnique                `thenNF_Tc` \ uniq ->
     let
        name = setNameUnique (tyVarName tyvar) uniq
@@ -194,66 +201,31 @@ tcInstTyVar tyvar
        -- that two different tyvars will print the same way 
        -- in an error message.  -dppr-debug will show up the difference
        -- Better watch out for this.  If worst comes to worst, just
-       -- use mkSysLocalName.
+       -- use mkSystemName.
     in
-    tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
-
-tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
-tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
-  = tcGetUniques       `thenNF_Tc` \ uniqs ->
-    listTc [ ASSERT( not (kind `eqKind` openTypeKind) )        -- Shouldn't happen
-            tcNewMutTyVar name kind details
-          | (tyvar, uniq) <- tyvars `zip` uniqs,
-            let name = setNameUnique (tyVarName tyvar) uniq, 
-            let kind = tyVarKind tyvar
-          ]
-\end{code}
+    tcNewMutTyVar name (tyVarKind tyvar) tv_details
 
-@tcInstType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, splits off the dictionary part, and returns the results.
-
-\begin{code}
-tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
-tcInstType ty
+tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+-- tcInstType instantiates the outer-level for-alls of a TcType with
+-- fresh (mutable) type variables, splits off the dictionary part, 
+-- and returns the pieces.
+tcInstType tv_details ty
   = case tcSplitForAllTys ty of
-       ([],     rho) ->        -- There may be overloading but no type variables;
+       ([],     rho) ->        -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
                         let
-                          (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
+                          (theta, tau) = tcSplitPhiTy rho
                         in
                         returnNF_Tc ([], theta, tau)
 
-       (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
+       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenNF_Tc` \ (tyvars', _, tenv) ->
                         let
-                          (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
+                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
                         in
                         returnNF_Tc (tyvars', theta, tau)
-
-
-tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
--- Very similar to tcInstSigType, but uses signature type variables
--- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
-tcInstSigType tv_details poly_ty
- = let
-       (tyvars, rho) = tcSplitForAllTys poly_ty
-   in
-   tcInstSigTyVars tv_details tyvars           `thenNF_Tc` \ tyvars' ->
-       -- Make *signature* type variables
-
-   let
-     tyvar_tys' = mkTyVarTys tyvars'
-     rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
-       -- mkTopTyVarSubst because the tyvars' are fresh
-
-     (theta', tau') = tcSplitRhoTy rho'
-       -- This splitRhoTy tries hard to make sure that tau' is a type synonym
-       -- wherever possible, which can improve interface files.
-   in
-   returnNF_Tc (tyvars', theta', tau')
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Putting and getting  mutable type variables}
@@ -443,13 +415,13 @@ mkArbitraryType tv
          = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
 
          | otherwise
-         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+         = pprTrace "Urk! Inventing strangely-kinded void TyCon:" (ppr tc_name $$ ppr kind) $
            mkPrimTyCon tc_name kind 0 [] VoidRep
                -- Same name as the tyvar, apart from making it start with a colon (sigh)
                -- I dread to think what will happen if this gets out into an 
                -- interface file.  Catastrophe likely.  Major sigh.
 
-    tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+    tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 
 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
 -- of a type variable, at the *end* of type checking.  It changes
@@ -474,11 +446,45 @@ zonkTcTyVarToTyVar tv
        -- so that all other occurrences of the tyvar will get zapped too
     zonkTyVar zap tv           `thenNF_Tc` \ ty2 ->
 
+       -- This warning shows up if the allegedly-unbound tyvar is
+       -- already bound to something.  It can actually happen, and 
+       -- in a harmless way (see [Silly Type Synonyms] below) so
+       -- it's only a warning
     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 
     returnNF_Tc immut_tv
 \end{code}
 
+[Silly Type Synonyms]
+
+Consider this:
+       type C u a = u  -- Note 'a' unused
+
+       foo :: (forall a. C u a -> C u a) -> u
+       foo x = ...
+
+       bar :: Num u => u
+       bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+       {Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  The arg to foo becomes
+       /\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+       a = ()
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly.   I think its harmless to ignore the problem.
+
 
 %************************************************************************
 %*                                                                     *
@@ -521,6 +527,9 @@ zonkType unbound_var_fn ty
     go (AppTy fun arg)           = go fun              `thenNF_Tc` \ fun' ->
                                    go arg              `thenNF_Tc` \ arg' ->
                                    returnNF_Tc (mkAppTy fun' arg')
+               -- NB the mkAppTy; we might have instantiated a
+               -- type variable to a type constructor, so we need
+               -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
@@ -684,7 +693,7 @@ checkTypeCtxt ctxt ty
        -- This shows up in the complaint about
        --      case C a where
        --        op :: Eq a => a -> a
-ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
+ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
           | otherwise                       = ppr ty
           where
            (forall_tvs, theta, tau) = tcSplitSigmaTy ty
@@ -756,17 +765,36 @@ check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
 check_tau_type rank ubx_tup (AppTy ty1 ty2)
   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 
-check_tau_type rank ubx_tup (NoteTy note ty)
-  = check_tau_type rank ubx_tup ty
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
        -- Synonym notes are built only when the synonym is 
        -- saturated (see Type.mkSynTy)
-       -- Not checking the 'note' part allows us to instantiate a synonym
-       -- defn with a for-all type, but that seems OK too
+  = doptsTc Opt_GlasgowExts                    `thenNF_Tc` \ gla_exts ->
+    (if gla_exts then
+       -- If -fglasgow-exts then don't check the 'note' part.
+       -- This  allows us to instantiate a synonym defn with a 
+       -- for-all type, or with a partially-applied type synonym.
+       --      e.g.   type T a b = a
+       --             type S m   = m ()
+       --             f :: S (T Int)
+       -- Here, T is partially applied, so it's illegal in H98.
+       -- But if you expand S first, then T we get just 
+       --             f :: Int
+       -- which is fine.
+       returnTc ()
+    else
+       -- For H98, do check the un-expanded part
+       check_tau_type rank ubx_tup syn         
+    )                                          `thenTc_`
+
+    check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+  = check_tau_type rank ubx_tup ty
 
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc      
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
-       -- synonym application, leaving it to checkValidType (i.e. right here
+       -- synonym application, leaving it to checkValidType (i.e. right here)
        -- to find the error
     checkTc syn_arity_ok arity_msg     `thenTc_`
     mapTc_ check_arg_type tys
@@ -869,7 +897,7 @@ checkFreeness forall_tyvars theta
 freeErr pred
   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
                   ptext SLIT("are already in scope"),
-        nest 4 (ptext SLIT("At least one must be universally quantified here"))
+        nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
     ]
 \end{code}
 
@@ -907,7 +935,11 @@ check_valid_theta ctxt []
   = returnTc ()
 check_valid_theta ctxt theta
   = getDOptsTc                                 `thenNF_Tc` \ dflags ->
-    warnTc (not (null dups)) (dupPredWarn dups)        `thenNF_Tc_`
+    warnTc (notNull dups) (dupPredWarn dups)   `thenNF_Tc_`
+       -- Actually, in instance decls and type signatures, 
+       -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
+       -- so this error can only fire for the context of a class or
+       -- data type decl.
     mapTc_ (check_source_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
@@ -917,7 +949,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
     mapTc_ check_arg_type tys          `thenTc_`
     checkTc (arity == n_tys) arity_err         `thenTc_`
-    checkTc (all tyvar_head tys || arby_preds_ok)
+    checkTc (check_class_pred_tys dflags ctxt tys)
            (predTyVarErr pred $$ how_to_allow)
 
   where
@@ -926,12 +958,6 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
 
-    arby_preds_ok = case ctxt of
-                       InstHeadCtxt  -> True   -- We check for instance-head formation
-                                               -- in checkValidInstHead
-                       InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
-                       other         -> dopt Opt_GlasgowExts               dflags
-
     how_to_allow = case ctxt of
                     InstHeadCtxt  -> empty     -- Should not happen
                     InstThetaCtxt -> parens undecidableMsg
@@ -953,6 +979,17 @@ check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 
 -------------------------
+check_class_pred_tys dflags ctxt tys 
+  = case ctxt of
+       InstHeadCtxt  -> True   -- We check for instance-head 
+                               -- formation in checkValidInstHead
+       InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
+       other         -> gla_exts       || all tyvar_head tys
+  where
+    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
+    gla_exts      = dopt Opt_GlasgowExts dflags
+
+-------------------------
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable
@@ -974,6 +1011,133 @@ checkThetaCtxt ctxt theta
 
 %************************************************************************
 %*                                                                     *
+\subsection{Validity check for TyCons}
+%*                                                                     *
+%************************************************************************
+
+checkValidTyCon is called once the mutually-recursive knot has been
+tied, so we can look at things freely.
+
+\begin{code}
+checkValidTyCon :: TyCon -> TcM ()
+checkValidTyCon tc
+  | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
+  | otherwise
+  =    -- Check the context on the data decl
+    checkValidTheta (DataTyCtxt name) (tyConTheta tc)  `thenTc_` 
+       
+       -- Check arg types of data constructors
+    mapTc_ checkValidDataCon data_cons                 `thenTc_`
+
+       -- Check that fields with the same name share a type
+    mapTc_ check_fields groups
+
+  where
+    name         = tyConName tc
+    (_, syn_rhs) = getSynTyConDefn tc
+    data_cons    = tyConDataCons tc
+
+    fields = [field | con <- data_cons, field <- dataConFieldLabels con]
+    groups = equivClasses cmp_name fields
+    cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
+
+    check_fields fields@(first_field_label : 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) other_tys) (fieldTypeMisMatch field_name)
+       where
+           field_ty   = fieldLabelType first_field_label
+           field_name = fieldLabelName first_field_label
+           other_tys  = map fieldLabelType other_fields
+
+checkValidDataCon :: DataCon -> TcM ()
+checkValidDataCon con
+  = checkValidType ctxt (idType (dataConWrapId con))   `thenTc_`
+               -- This checks the argument types and
+               -- ambiguity of the existential context (if any)
+    tcAddErrCtxt (existentialCtxt con)
+                (checkFreeness ex_tvs ex_theta)
+  where
+    ctxt = ConArgCtxt (dataConName con) 
+    (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
+
+
+fieldTypeMisMatch field_name
+  = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
+
+existentialCtxt con = ptext SLIT("When checking the existential context of constructor") 
+                     <+> quotes (ppr con)
+\end{code}
+
+
+checkValidClass is called once the mutually-recursive knot has been
+tied, so we can look at things freely.
+
+\begin{code}
+checkValidClass :: Class -> TcM ()
+checkValidClass cls
+  =    -- CHECK ARITY 1 FOR HASKELL 1.4
+    doptsTc Opt_GlasgowExts                            `thenTc` \ gla_exts ->
+
+       -- Check that the class is unary, unless GlaExs
+    checkTc (notNull tyvars)   (nullaryClassErr cls)   `thenTc_`
+    checkTc (gla_exts || unary) (classArityErr cls)    `thenTc_`
+
+       -- Check the super-classes
+    checkValidTheta (ClassSCCtxt (className cls)) theta        `thenTc_`
+
+       -- Check the class operations
+    mapTc_ check_op op_stuff           `thenTc_`
+
+       -- 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) 
+       = checkValidTheta SigmaCtxt (tail theta)        `thenTc_`
+               -- The 'tail' removes the initial (C a) from the
+               -- class itself, leaving just the method type
+
+         checkValidType (FunSigCtxt op_name) tau       `thenTc_`
+
+               -- Check that for a generic method, the type of 
+               -- the method is sufficiently simple
+         checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
+                 (badGenericMethodType op_name op_ty)
+       where
+         op_name = idName sel_id
+         op_ty   = idType sel_id
+         (_,theta,tau) = tcSplitSigmaTy op_ty
+
+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"))]
+
+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, and tuples")])
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection{Checking for a decent instance head type}
 %*                                                                     *
 %************************************************************************