[project @ 2002-11-05 14:10:44 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index e50be22..daf2acf 100644 (file)
@@ -11,29 +11,33 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, newHoleTyVarTy,
-  newTyVarTy,          -- Kind -> NF_TcM TcType
-  newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
+  newTyVar, 
+  newTyVarTy,          -- Kind -> TcM TcType
+  newTyVarTys,         -- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, newBoxityVar,
   putTcTyVar, getTcTyVar,
+  newMutTyVar, readMutTyVar, writeMutTyVar, 
+
+  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,
+  arityErr,
 
   --------------------------------
   -- Zonking
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+  zonkType,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
+  zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
 
   ) where
 
@@ -47,10 +51,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,
-                         tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
+                         tcIsTyVarTy, tcSplitSigmaTy, 
+                         isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
 
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
@@ -58,33 +62,31 @@ import TcType               ( TcType, TcThetaType, TcTauType, TcPredType,
                          liftedTypeKind, openTypeKind, defaultKind, superKind,
                          superBoxity, liftedBoxity, typeKind,
                          tyVarsOfType, tyVarsOfTypes, 
-                         eqKind, isTypeKind,
-
+                         eqKind, isTypeKind, 
                          isFFIArgumentTy, isFFIImportResultTy
                        )
 import Subst           ( Subst, mkTopTyVarSubst, substTy )
-import Class           ( Class, classArity, className )
-import TyCon           ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName )
-import PrimRep         ( PrimRep(VoidRep) )
-import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Class           ( Class, DefMeth(..), classArity, className, classBigSig )
+import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
+                         tyConArity, tyConName, tyConTheta, 
+                         getSynTyConDefn, tyConDataCons )
+import DataCon         ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
+import FieldLabel      ( fieldLabelName, fieldLabelType )
+import Var             ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, 
+                         mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
 
 -- others:
-import TcMonad          -- TcType, amongst others
-import TysWiredIn      ( voidTy )
+import Generics                ( validGenericMethodType )
+import TcRnMonad          -- TcType, amongst others
 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, setNameUnique, mkSystemTvNameEncoded )
 import VarSet
 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}
 
@@ -96,71 +98,82 @@ import Outputable
 %************************************************************************
 
 \begin{code}
-newTyVar :: Kind -> NF_TcM TcTyVar
+newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
+newMutTyVar name kind details
+  = do { ref <- newMutVar Nothing ;
+        return (mkMutTyVar name kind details ref) }
+
+readMutTyVar :: TyVar -> TcM (Maybe Type)
+readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
+
+writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
+writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
+
+newTyVar :: Kind -> TcM TcTyVar
 newTyVar kind
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
+  = newUnique  `thenM` \ uniq ->
+    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
 
-newTyVarTy  :: Kind -> NF_TcM TcType
+newTyVarTy  :: Kind -> 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 SLIT("h")) openTypeKind HoleTv  `thenNF_Tc` \ tv ->
-    returnNF_Tc (TyVarTy tv)
+  = newTyVar kind      `thenM` \ tc_tyvar ->
+    returnM (TyVarTy tc_tyvar)
 
-newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
+newTyVarTys :: Int -> Kind -> TcM [TcType]
+newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
 
-newKindVar :: NF_TcM TcKind
+newKindVar :: TcM TcKind
 newKindVar
-  = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv  `thenNF_Tc` \ kv ->
-    returnNF_Tc (TyVarTy kv)
+  = newUnique                                                  `thenM` \ uniq ->
+    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv    `thenM` \ kv ->
+    returnM (TyVarTy kv)
 
-newKindVars :: Int -> NF_TcM [TcKind]
-newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 
-newBoxityVar :: NF_TcM TcKind
+newBoxityVar :: TcM TcKind
 newBoxityVar
-  = tcGetUnique                                                          `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
-    returnNF_Tc (TyVarTy kv)
+  = newUnique                                                    `thenM` \ uniq ->
+    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv  `thenM` \ kv ->
+    returnM (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 (UsageTy _ t)   ts = go syn_t t ts
-    go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
-\end{code}
-
+newHoleTyVarTy :: TcM TcType
+  = newUnique  `thenM` \ uniq ->
+    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv    `thenM` \ tv ->
+    returnM (TyVarTy tv)
+
+readHoleResult :: TcType -> TcM TcType
+-- Read the answer out of a hole, constructed by newHoleTyVarTy
+readHoleResult (TyVarTy tv)
+  = ASSERT( isHoleTyVar tv )
+    getTcTyVar tv              `thenM` \ maybe_res ->
+    case maybe_res of
+       Just ty -> returnM ty
+       Nothing ->  pprPanic "readHoleResult: empty" (ppr tv)
+readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
+
+zapToType :: TcType -> TcM TcType
+zapToType (TyVarTy tv)
+  | isHoleTyVar tv
+  = getTcTyVar tv              `thenM` \ maybe_res ->
+    case maybe_res of
+       Nothing -> newTyVarTy openTypeKind      `thenM` \ ty ->
+                  putTcTyVar tv ty             `thenM_`
+                  returnM ty
+       Just ty  -> returnM ty  -- No need to loop; we never
+                                       -- have chains of holes
+
+zapToType other_ty = returnM other_ty
+\end{code}                
 
 %************************************************************************
 %*                                                                     *
@@ -171,21 +184,21 @@ tcSplitRhoTyM t
 Instantiating a bunch of type variables
 
 \begin{code}
-tcInstTyVars :: [TyVar] 
-            -> NF_TcM ([TcTyVar], [TcType], Subst)
+tcInstTyVars :: TyVarDetails -> [TyVar] 
+            -> TcM ([TcTyVar], [TcType], Subst)
 
-tcInstTyVars tyvars
-  = mapNF_Tc tcInstTyVar tyvars        `thenNF_Tc` \ tc_tyvars ->
+tcInstTyVars tv_details tyvars
+  = mappM (tcInstTyVar tv_details) tyvars      `thenM` \ tc_tyvars ->
     let
        tys = mkTyVarTys tc_tyvars
     in
-    returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+    returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence mkTopTyVarSubst
 
-tcInstTyVar tyvar
-  = tcGetUnique                `thenNF_Tc` \ uniq ->
+tcInstTyVar tv_details tyvar
+  = newUnique          `thenM` \ uniq ->
     let
        name = setNameUnique (tyVarName tyvar) uniq
        -- Note that we don't change the print-name
@@ -193,66 +206,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}
-
-@tcInstType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, splits off the dictionary part, and returns the results.
+    newMutTyVar name (tyVarKind tyvar) tv_details
 
-\begin{code}
-tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
-tcInstType ty
+tcInstType :: TyVarDetails -> TcType -> 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)
+                        returnM ([], theta, tau)
 
-       (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
+       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenM` \ (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')
+                        returnM (tyvars', theta, tau)
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Putting and getting  mutable type variables}
@@ -260,8 +238,8 @@ tcInstSigType tv_details poly_ty
 %************************************************************************
 
 \begin{code}
-putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
-getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
+putTcTyVar :: TcTyVar -> TcType -> TcM TcType
+getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
 \end{code}
 
 Putting is easy:
@@ -270,19 +248,18 @@ Putting is easy:
 putTcTyVar tyvar ty 
   | not (isMutTyVar tyvar)
   = pprTrace "putTcTyVar" (ppr tyvar) $
-    returnNF_Tc ty
+    returnM ty
 
   | otherwise
   = ASSERT( isMutTyVar tyvar )
-    UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
-    tcWriteMutTyVar tyvar (Just ty)    `thenNF_Tc_`
-    returnNF_Tc ty
+    writeMutTyVar tyvar (Just ty)      `thenM_`
+    returnM ty
 \end{code}
 
 Getting is more interesting.  The easy thing to do is just to read, thus:
 
 \begin{verbatim}
-getTcTyVar tyvar = tcReadMutTyVar tyvar
+getTcTyVar tyvar = readMutTyVar tyvar
 \end{verbatim}
 
 But it's more fun to short out indirections on the way: If this
@@ -295,33 +272,33 @@ We return Nothing iff the original box was unbound.
 getTcTyVar tyvar
   | not (isMutTyVar tyvar)
   = pprTrace "getTcTyVar" (ppr tyvar) $
-    returnNF_Tc (Just (mkTyVarTy tyvar))
+    returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
-    tcReadMutTyVar tyvar                               `thenNF_Tc` \ maybe_ty ->
+    readMutTyVar tyvar                         `thenM` \ maybe_ty ->
     case maybe_ty of
-       Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
-                  tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
-                  returnNF_Tc (Just ty')
+       Just ty -> short_out ty                         `thenM` \ ty' ->
+                  writeMutTyVar tyvar (Just ty')       `thenM_`
+                  returnM (Just ty')
 
-       Nothing    -> returnNF_Tc Nothing
+       Nothing    -> returnM Nothing
 
-short_out :: TcType -> NF_TcM TcType
+short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)
   | not (isMutTyVar tyvar)
-  = returnNF_Tc ty
+  = returnM ty
 
   | otherwise
-  = tcReadMutTyVar tyvar       `thenNF_Tc` \ maybe_ty ->
+  = readMutTyVar tyvar `thenM` \ maybe_ty ->
     case maybe_ty of
-       Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
-                   tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
-                   returnNF_Tc ty'
+       Just ty' -> short_out ty'                       `thenM` \ ty' ->
+                   writeMutTyVar tyvar (Just ty')      `thenM_`
+                   returnM ty'
 
-       other    -> returnNF_Tc ty
+       other    -> returnM ty
 
-short_out other_ty = returnNF_Tc other_ty
+short_out other_ty = returnM other_ty
 \end{code}
 
 
@@ -334,61 +311,53 @@ short_out other_ty = returnNF_Tc other_ty
 -----------------  Type variables
 
 \begin{code}
-zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
-zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
-
-zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
-                          returnNF_Tc (tyVarsOfTypes tys)
-
-zonkTcTyVar :: TcTyVar -> NF_TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
-
-zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
--- This guy is to zonk the tyvars we're about to feed into tcSimplify
--- Usually this job is done by checkSigTyVars, but in a couple of places
--- that is overkill, so we use this simpler chap
-zonkTcSigTyVars tyvars
-  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
-    returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
+zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
+zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
+
+zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars    `thenM` \ tys ->
+                          returnM (tyVarsOfTypes tys)
+
+zonkTcTyVar :: TcTyVar -> TcM TcType
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
 \end{code}
 
 -----------------  Types
 
 \begin{code}
-zonkTcType :: TcType -> NF_TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+zonkTcType :: TcType -> TcM TcType
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 
-zonkTcTypes :: [TcType] -> NF_TcM [TcType]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mappM zonkTcType tys
 
-zonkTcClassConstraints cts = mapNF_Tc zonk cts
+zonkTcClassConstraints cts = mappM zonk cts
     where zonk (clas, tys)
-           = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
-             returnNF_Tc (clas, new_tys)
+           = zonkTcTypes tys   `thenM` \ new_tys ->
+             returnM (clas, new_tys)
 
-zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
-zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+zonkTcThetaType :: TcThetaType -> TcM TcThetaType
+zonkTcThetaType theta = mappM zonkTcPredType theta
 
-zonkTcPredType :: TcPredType -> NF_TcM TcPredType
+zonkTcPredType :: TcPredType -> TcM TcPredType
 zonkTcPredType (ClassP c ts)
-  = zonkTcTypes ts     `thenNF_Tc` \ new_ts ->
-    returnNF_Tc (ClassP c new_ts)
+  = zonkTcTypes ts     `thenM` \ new_ts ->
+    returnM (ClassP c new_ts)
 zonkTcPredType (IParam n t)
-  = zonkTcType t       `thenNF_Tc` \ new_t ->
-    returnNF_Tc (IParam n new_t)
+  = zonkTcType t       `thenM` \ new_t ->
+    returnM (IParam n new_t)
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
-zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
+zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
 zonkKindEnv pairs 
-  = mapNF_Tc zonk_it pairs
+  = mappM zonk_it pairs
  where
-    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
-                             returnNF_Tc (name, kind)
+    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
+                             returnM (name, kind)
 
        -- When zonking a kind, we want to
        --      zonk a *kind* variable to (Type *)
@@ -397,36 +366,6 @@ zonkKindEnv pairs
                             | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
                             | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
                        
-zonkTcTypeToType :: TcType -> NF_TcM Type
-zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
-  where
-       -- Zonk a mutable but unbound type variable to
-       --      Void            if it has kind Lifted
-       --      :Void           otherwise
-       -- We know it's unbound even though we don't carry an environment,
-       -- because at the binding site for a type variable we bind the
-       -- mutable tyvar to a fresh immutable one.  So the mutable store
-       -- plays the role of an environment.  If we come across a mutable
-       -- type variable that isn't so bound, it must be completely free.
-    zonk_unbound_tyvar tv
-       | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
-       = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
-                               -- this vastly common case
-       | otherwise
-       = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
-       where
-         kind = tyVarKind tv
-
-    mk_void_tycon tv kind      -- Make a new TyCon with the same kind as the 
-                               -- type variable tv.  Same name too, 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.
-       = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
-         mkPrimTyCon tc_name kind 0 [] VoidRep
-       where
-         tc_name = mkLocalName (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
 -- the *mutable* type variable into an *immutable* one.
@@ -435,7 +374,7 @@ zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 -- Now any bound occurences of the original type variable will get 
 -- zonked to the immutable version.
 
-zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
+zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
 zonkTcTyVarToTyVar tv
   = let
                -- Make an immutable version, defaulting 
@@ -448,13 +387,47 @@ zonkTcTyVarToTyVar tv
     in 
        -- If the type variable is mutable, then bind it to immut_tv_ty
        -- so that all other occurrences of the tyvar will get zapped too
-    zonkTyVar zap tv           `thenNF_Tc` \ ty2 ->
+    zonkTyVar zap tv           `thenM` \ 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
+    returnM 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.
+
 
 %************************************************************************
 %*                                                                     *
@@ -471,62 +444,61 @@ zonkTcTyVarToTyVar tv
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
-zonkType :: (TcTyVar -> NF_TcM Type)   -- What to do with unbound mutable type variables
+zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
         -> TcType
-        -> NF_TcM Type
+        -> TcM Type
 zonkType unbound_var_fn ty
   = go ty
   where
-    go (TyConApp tycon tys)      = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
-                                   returnNF_Tc (TyConApp tycon tys')
+    go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
+                                   returnM (TyConApp tycon tys')
 
-    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenNF_Tc` \ ty1' ->
-                                   go ty2              `thenNF_Tc` \ ty2' ->
-                                   returnNF_Tc (NoteTy (SynNote ty1') ty2')
+    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
+                                   go ty2              `thenM` \ ty2' ->
+                                   returnM (NoteTy (SynNote ty1') ty2')
 
     go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
 
-    go (SourceTy p)              = go_pred p           `thenNF_Tc` \ p' ->
-                                   returnNF_Tc (SourceTy p')
+    go (SourceTy p)              = go_pred p           `thenM` \ p' ->
+                                   returnM (SourceTy p')
 
-    go (FunTy arg res)           = go arg              `thenNF_Tc` \ arg' ->
-                                   go res              `thenNF_Tc` \ res' ->
-                                   returnNF_Tc (FunTy arg' res')
+    go (FunTy arg res)           = go arg              `thenM` \ arg' ->
+                                   go res              `thenM` \ res' ->
+                                   returnM (FunTy arg' res')
  
-    go (AppTy fun arg)           = go fun              `thenNF_Tc` \ fun' ->
-                                   go arg              `thenNF_Tc` \ arg' ->
-                                   returnNF_Tc (mkAppTy fun' arg')
-
-    go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
-                                    go ty               `thenNF_Tc` \ ty' ->
-                                    returnNF_Tc (UsageTy u' ty')
+    go (AppTy fun arg)           = go fun              `thenM` \ fun' ->
+                                   go arg              `thenM` \ arg' ->
+                                   returnM (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
 
-    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenNF_Tc` \ tyvar' ->
-                            go ty                      `thenNF_Tc` \ ty' ->
-                            returnNF_Tc (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenM` \ tyvar' ->
+                            go ty                      `thenM` \ ty' ->
+                            returnM (ForAllTy tyvar' ty')
 
-    go_pred (ClassP c tys) = mapNF_Tc go tys   `thenNF_Tc` \ tys' ->
-                            returnNF_Tc (ClassP c tys')
-    go_pred (NType tc tys) = mapNF_Tc go tys   `thenNF_Tc` \ tys' ->
-                            returnNF_Tc (NType tc tys')
-    go_pred (IParam n ty)  = go ty             `thenNF_Tc` \ ty' ->
-                            returnNF_Tc (IParam n ty')
+    go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
+                            returnM (ClassP c tys')
+    go_pred (NType tc tys) = mappM go tys      `thenM` \ tys' ->
+                            returnM (NType tc tys')
+    go_pred (IParam n ty)  = go ty             `thenM` \ ty' ->
+                            returnM (IParam n ty')
 
-zonkTyVar :: (TcTyVar -> NF_TcM Type)          -- What to do for an unbound mutable variable
-         -> TcTyVar -> NF_TcM TcType
+zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable
+         -> TcTyVar -> TcM TcType
 zonkTyVar unbound_var_fn tyvar 
   | not (isMutTyVar tyvar)     -- Not a mutable tyvar.  This can happen when
                                -- zonking a forall type, when the bound type variable
                                -- needn't be mutable
   = ASSERT( isTyVar tyvar )            -- Should not be any immutable kind vars
-    returnNF_Tc (TyVarTy tyvar)
+    returnM (TyVarTy tyvar)
 
   | otherwise
-  =  getTcTyVar tyvar  `thenNF_Tc` \ maybe_ty ->
+  =  getTcTyVar tyvar  `thenM` \ maybe_ty ->
      case maybe_ty of
          Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
          Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
@@ -609,7 +581,7 @@ pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
-  = doptsTc Opt_GlasgowExts    `thenNF_Tc` \ gla_exts ->
+  = doptM Opt_GlasgowExts      `thenM` \ gla_exts ->
     let 
        rank | gla_exts = Arbitrary
             | otherwise
@@ -634,14 +606,22 @@ checkValidType ctxt ty
                        GenPatCtxt   -> actual_kind_is_lifted
                        ForSigCtxt _ -> actual_kind_is_lifted
                        other        -> isTypeKind actual_kind
+       
+       ubx_tup | not gla_exts = UT_NotOk
+               | otherwise    = case ctxt of
+                                  TySynCtxt _ -> UT_Ok
+                                  other       -> UT_NotOk
+               -- Unboxed tuples ok in function results,
+               -- but for type synonyms we allow them even at
+               -- top level
     in
-    tcAddErrCtxt (checkTypeCtxt ctxt ty)       $
+    addErrCtxt (checkTypeCtxt ctxt ty) $
 
        -- Check that the thing has kind Type, and is lifted if necessary
-    checkTc kind_ok (kindErr actual_kind)      `thenTc_`
+    checkTc kind_ok (kindErr actual_kind)      `thenM_`
 
        -- Check the internal validity of the type itself
-    check_poly_type rank ty
+    check_poly_type rank ubx_tup ty
 
 
 checkTypeCtxt ctxt ty
@@ -656,7 +636,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
@@ -670,17 +650,22 @@ decRank :: Rank -> Rank
 decRank Arbitrary = Arbitrary
 decRank (Rank n)  = Rank (n-1)
 
-check_poly_type :: Rank -> Type -> TcM ()
-check_poly_type (Rank 0) ty 
-  = check_tau_type (Rank 0) False ty
+----------------------------------------
+data UbxTupFlag = UT_Ok        | UT_NotOk
+       -- The "Ok" version means "ok if -fglasgow-exts is on"
+
+----------------------------------------
+check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+check_poly_type (Rank 0) ubx_tup ty 
+  = check_tau_type (Rank 0) ubx_tup ty
 
-check_poly_type rank ty 
+check_poly_type rank ubx_tup ty 
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
-    check_valid_theta SigmaCtxt theta          `thenTc_`
-    check_tau_type (decRank rank) False tau    `thenTc_`
-    checkFreeness tvs theta                    `thenTc_`
+    check_valid_theta SigmaCtxt theta          `thenM_`
+    check_tau_type (decRank rank) ubx_tup tau  `thenM_`
+    checkFreeness tvs theta                    `thenM_`
     checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
@@ -700,49 +685,76 @@ check_arg_type :: Type -> TcM ()
 -- NB: unboxed tuples can have polymorphic or unboxed args.
 --     This happens in the workers for functions returning
 --     product types with polymorphic components.
---     But not in user code
--- 
--- Question: what about nested unboxed tuples?
---          Currently rejected.
+--     But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
 check_arg_type ty 
-  = check_tau_type (Rank 0) False ty   `thenTc_` 
+  = check_tau_type (Rank 0) UT_NotOk ty                `thenM_` 
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
-check_tau_type :: Rank -> Bool -> Type -> TcM ()
+check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
--- Bool is True iff unboxed tuple are allowed here
-
-check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = failWithTc (usageTyErr ty)
-check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc          `thenNF_Tc` \ dflags ->
-                                                  check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
-check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
-  = check_poly_type rank      arg_ty   `thenTc_`
-    check_tau_type  rank True res_ty
-
-check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
-  = check_arg_type ty1 `thenTc_` check_arg_type ty2
-
-check_tau_type rank ubx_tup_ok (NoteTy note ty)
-  = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
-
-check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
-  | isSynTyCon tc
-  = checkTc syn_arity_ok arity_msg     `thenTc_`
-    mapTc_ check_arg_type tys
+
+check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup (SourceTy sty)    = getDOpts               `thenM` \ dflags ->
+                                               check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
+check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+  = check_poly_type rank UT_NotOk arg_ty       `thenM_`
+    check_tau_type  rank UT_Ok    res_ty
+
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+  = check_arg_type ty1 `thenM_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
+       -- Synonym notes are built only when the synonym is 
+       -- saturated (see Type.mkSynTy)
+  = doptM Opt_GlasgowExts                      `thenM` \ 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.
+       returnM ()
+    else
+       -- For H98, do check the un-expanded part
+       check_tau_type rank ubx_tup syn         
+    )                                          `thenM_`
+
+    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)
+       -- to find the error
+    checkTc syn_arity_ok arity_msg     `thenM_`
+    mappM_ check_arg_type tys
     
   | isUnboxedTupleTyCon tc
-  = checkTc ubx_tup_ok ubx_tup_msg     `thenTc_`
-    mapTc_ (check_tau_type (Rank 0) True) tys  -- Args are allowed to be unlifted, or
-                                               -- more unboxed tuples, so can't use check_arg_ty
+  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
+    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
+    mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
+                       -- Args are allowed to be unlifted, or
+                       -- more unboxed tuples, so can't use check_arg_ty
 
   | otherwise
-  = mapTc_ check_arg_type tys
+  = mappM_ check_arg_type tys
 
   where
+    ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+
     syn_arity_ok = tc_arity <= n_args
                -- It's OK to have an *over-applied* type synonym
                --      data Tree a b = ...
@@ -755,17 +767,110 @@ check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-check_note (FTVNote _)  = returnTc ()
-check_note (SynNote ty) = check_tau_type (Rank 0) False ty
-
-----------------------------------------
 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
-usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Checking a theta or source type}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+data SourceTyCtxt
+  = ClassSCCtxt Name   -- Superclasses of clas
+  | SigmaCtxt          -- Context of a normal for-all type
+  | DataTyCtxt Name    -- Context of a data decl
+  | TypeCtxt           -- Source type in an ordinary type
+  | InstThetaCtxt      -- Context of an instance decl
+  | InstHeadCtxt       -- Head of an instance decl
+               
+pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
+pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
+pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
+pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
+pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
+pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
+\end{code}
+
+\begin{code}
+checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
+checkValidTheta ctxt theta 
+  = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
+
+-------------------------
+check_valid_theta ctxt []
+  = returnM ()
+check_valid_theta ctxt theta
+  = getDOpts                                   `thenM` \ dflags ->
+    warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
+       -- 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.
+    mappM_ (check_source_ty dflags ctxt) theta
+  where
+    (_,dups) = removeDups tcCmpPred theta
+
+-------------------------
+check_source_ty dflags ctxt pred@(ClassP cls tys)
+  =    -- Class predicates are valid in all contexts
+    mappM_ check_arg_type tys          `thenM_`
+    checkTc (arity == n_tys) arity_err         `thenM_`
+    checkTc (check_class_pred_tys dflags ctxt tys)
+           (predTyVarErr pred $$ how_to_allow)
+
+  where
+    class_name = className cls
+    arity      = classArity cls
+    n_tys      = length tys
+    arity_err  = arityErr "Class" class_name arity n_tys
+
+    how_to_allow = case ctxt of
+                    InstHeadCtxt  -> empty     -- Should not happen
+                    InstThetaCtxt -> parens undecidableMsg
+                    other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+
+check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+       -- Implicit parameters only allows in type
+       -- signatures; not in instance decls, superclasses etc
+       -- The reason for not allowing implicit params in instances is a bit subtle
+       -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
+       -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
+       -- discharge all the potential usas of the ?x in e.   For example, a
+       -- constraint Foo [Int] might come out of e,and applying the
+       -- instance decl would show up two uses of ?x.
+
+check_source_ty dflags TypeCtxt  (NType tc tys)   = mappM_ check_arg_type tys
+
+-- Catch-all
+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
+  = case tcSplitAppTy_maybe ty of
+       Just (ty, _) -> tyvar_head ty
+       Nothing      -> False
+\end{code}
+
 Check for ambiguity
 ~~~~~~~~~~~~~~~~~~~
          forall V. P => tau
@@ -799,7 +904,7 @@ don't need to check for ambiguity either, because the test can't fail
 \begin{code}
 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 checkAmbiguity forall_tyvars theta tau_tyvars
-  = mapTc_ complain (filter is_ambig theta)
+  = mappM_ complain (filter is_ambig theta)
   where
     complain pred     = addErrTc (ambigErr pred)
     extended_tau_vars = grow theta tau_tyvars
@@ -808,8 +913,6 @@ checkAmbiguity forall_tyvars theta tau_tyvars
     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
                        not (ct_var `elemVarSet` extended_tau_vars)
 
-    is_free ct_var    = not (ct_var `elem` forall_tyvars)
-
 ambigErr pred
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
         nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
@@ -823,7 +926,7 @@ even in a scope where b is in scope.
 
 \begin{code}
 checkFreeness forall_tyvars theta
-  = mapTc_ complain (filter is_free theta)
+  = mappM_ complain (filter is_free theta)
   where    
     is_free pred     =  not (isIPPred pred)
                     && not (any bound_var (varSetElems (tyVarsOfPred pred)))
@@ -833,106 +936,153 @@ 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}
 
+\begin{code}
+checkThetaCtxt ctxt theta
+  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
+         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+
+badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
+predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+
+arityErr kind name n m
+  = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
+          n_arguments <> comma, text "but has been given", int m]
+    where
+       n_arguments | n == 0 = ptext SLIT("no arguments")
+                   | n == 1 = ptext SLIT("1 argument")
+                   | True   = hsep [int n, ptext SLIT("arguments")]
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
-\subsection{Checking a theta or source type}
+\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}
-data SourceTyCtxt
-  = ClassSCCtxt Name   -- Superclasses of clas
-  | SigmaCtxt          -- Context of a normal for-all type
-  | DataTyCtxt Name    -- Context of a data decl
-  | TypeCtxt           -- Source type in an ordinary type
-  | InstThetaCtxt      -- Context of an instance decl
-  | InstHeadCtxt       -- Head of an instance decl
-               
-pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
-pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
-pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
-pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
-pprSourceTyCtxt InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
-pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
+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)  `thenM_` 
+       
+       -- Check arg types of data constructors
+    mappM_ checkValidDataCon data_cons                 `thenM_`
+
+       -- Check that fields with the same name share a type
+    mappM_ 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))   `thenM_`
+               -- This checks the argument types and
+               -- ambiguity of the existential context (if any)
+    addErrCtxt (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}
-checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
-checkValidTheta ctxt theta 
-  = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
+checkValidClass :: Class -> TcM ()
+checkValidClass cls
+  =    -- CHECK ARITY 1 FOR HASKELL 1.4
+    doptM Opt_GlasgowExts                              `thenM` \ gla_exts ->
 
--------------------------
-check_valid_theta ctxt []
-  = returnTc ()
-check_valid_theta ctxt theta
-  = getDOptsTc                                 `thenNF_Tc` \ dflags ->
-    warnTc (not (null dups)) (dupPredWarn dups)        `thenNF_Tc_`
-    mapTc_ (check_source_ty dflags ctxt) theta
-  where
-    (_,dups) = removeDups tcCmpPred theta
+       -- Check that the class is unary, unless GlaExs
+    checkTc (notNull tyvars)   (nullaryClassErr cls)   `thenM_`
+    checkTc (gla_exts || unary) (classArityErr cls)    `thenM_`
 
--------------------------
-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)
-           (predTyVarErr pred $$ how_to_allow)
+       -- Check the super-classes
+    checkValidTheta (ClassSCCtxt (className cls)) theta        `thenM_`
 
-  where
-    class_name = className cls
-    arity      = classArity cls
-    n_tys      = length tys
-    arity_err  = arityErr "Class" class_name arity n_tys
+       -- Check the class operations
+    mappM_ check_op op_stuff           `thenM_`
 
-    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
+       -- 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)
 
-    how_to_allow = case ctxt of
-                    InstHeadCtxt  -> empty     -- Should not happen
-                    InstThetaCtxt -> parens undecidableMsg
-                    other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+  where
+    (tyvars, theta, _, op_stuff) = classBigSig cls
+    unary      = isSingleton tyvars
+    no_generics = null [() | (_, GenDefMeth) <- op_stuff]
 
-check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-       -- Implicit parameters only allows in type
-       -- signatures; not in instance decls, superclasses etc
-       -- The reason for not allowing implicit params in instances is a bit subtle
-       -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
-       -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
-       -- discharge all the potential usas of the ?x in e.   For example, a
-       -- constraint Foo [Int] might come out of e,and applying the
-       -- instance decl would show up two uses of ?x.
+    check_op (sel_id, dm) 
+       = checkValidTheta SigmaCtxt (tail theta)        `thenM_`
+               -- The 'tail' removes the initial (C a) from the
+               -- class itself, leaving just the method type
 
-check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
+         checkValidType (FunSigCtxt op_name) tau       `thenM_`
 
--- Catch-all
-check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+               -- 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
 
--------------------------
-tyvar_head ty                  -- Haskell 98 allows predicates of form 
-  | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
-  | otherwise                  -- where a is a type variable
-  = case tcSplitAppTy_maybe ty of
-       Just (ty, _) -> tyvar_head ty
-       Nothing      -> False
-\end{code}
+nullaryClassErr cls
+  = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
 
-\begin{code}
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
-predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
-dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+classArityErr cls
+  = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
+         parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
 
-checkThetaCtxt ctxt theta
-  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
-         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+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}
 
 
@@ -963,10 +1113,10 @@ checkValidInstHead ty    -- Should be a source type
        Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
         Just (clas,tys) ->
 
-    getDOptsTc                                 `thenNF_Tc` \ dflags ->
-    mapTc_ check_arg_type tys                  `thenTc_`
-    check_inst_head dflags clas tys            `thenTc_`
-    returnTc (clas, tys)
+    getDOpts                                   `thenM` \ dflags ->
+    mappM_ check_arg_type tys                  `thenM_`
+    check_inst_head dflags clas tys            `thenM_`
+    returnM (clas, tys)
     }}
 
 check_inst_head dflags clas tys
@@ -990,7 +1140,7 @@ check_inst_head dflags clas tys
     all tcIsTyVarTy arg_tys,           -- Applied to type variables
     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
           -- This last condition checks that all the type variables are distinct
-  = returnTc ()
+  = returnM ()
 
   | otherwise
   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
@@ -1007,8 +1157,8 @@ check_inst_head dflags clas tys
 check_tyvars dflags clas tys
        -- Check that at least one isn't a type variable
        -- unless -fallow-undecideable-instances
-  | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
-  | not (all tcIsTyVarTy tys)                = returnTc ()
+  | dopt Opt_AllowUndecidableInstances dflags = returnM ()
+  | not (all tcIsTyVarTy tys)                = returnM ()
   | otherwise                                = failWithTc (instTypeErr (pprClassPred clas tys) msg)
   where
     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
@@ -1026,5 +1176,3 @@ nonBoxedPrimCCallErr clas inst_ty
   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
         4 (pprClassPred clas [inst_ty])
 \end{code}
-
-