[project @ 2005-03-07 15:16:58 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 097c7f9..4a9df50 100644 (file)
@@ -11,33 +11,34 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, 
-  newTyVarTy,          -- Kind -> TcM TcType
-  newTyVarTys,         -- Int -> Kind -> TcM [TcType]
-  newKindVar, newKindVars, newOpenTypeKind,
-  putTcTyVar, getTcTyVar,
-  newMutTyVar, readMutTyVar, writeMutTyVar, 
-
-  newHoleTyVarTy, readHoleResult, zapToType,
+  newFlexiTyVar,
+  newTyFlexiVarTy,             -- Kind -> TcM TcType
+  newTyFlexiVarTys,            -- Int -> Kind -> TcM [TcType]
+  newKindVar, newKindVars, 
+  lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, 
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
+  tcSkolType, tcSkolTyVars, tcInstSigType,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
-  Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
-  SourceTyCtxt(..), checkValidTheta, 
-  checkValidTyCon, checkValidClass, 
+  Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
+  SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,
-  arityErr,
+  arityErr, 
 
   --------------------------------
   -- Zonking
-  zonkType,
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar
 
   ) where
 
@@ -45,48 +46,45 @@ module TcMType (
 
 
 -- friends:
-import TypeRep         ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
-                         Kind, ThetaType, typeCon
+import HsSyn           ( LHsType )
+import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
+                         Kind, ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
-                         tcEqType, tcCmpPred, isClassPred,
+                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
+                         MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
+                         tcCmpPred, isClassPred, 
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
-                         isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
-
+                         tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
+                         isUnLiftedType, isIPPred, isImmutableTyVar,
+                         typeKind, isFlexi, isSkolemTyVar,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
-
-                         liftedTypeKind, openTypeKind, defaultKind, superKind,
-                         superBoxity, liftedBoxity, typeKind,
                          tyVarsOfType, tyVarsOfTypes, 
-                         eqKind, isTypeKind, 
-                         isFFIArgumentTy, isFFIImportResultTy
+                         pprPred, pprTheta, pprClassPred )
+import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+                         liftedTypeKind, defaultKind
                        )
-import Subst           ( Subst, mkTopTyVarSubst, substTy )
-import Class           ( Class, DefMeth(..), classArity, className, classBigSig )
+import Type            ( TvSubst, zipTopTvSubst, substTy )
+import Class           ( Class, classArity, className )
 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 )
+                         tyConArity, tyConName )
+import Var             ( TyVar, tyVarKind, tyVarName, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
 
 -- others:
-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, setNameUnique, mkSystemTvNameEncoded )
+import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
+import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
+import UniqSupply      ( uniqsFromSupply )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps      ( equivClasses, removeDups )
+import ListSetOps      ( removeDups )
+import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
 
@@ -98,136 +96,166 @@ import Outputable
 %************************************************************************
 
 \begin{code}
-newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
-newMutTyVar name kind details
-  = do { ref <- newMutVar Nothing ;
-        return (mkMutTyVar name kind details ref) }
+newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
+newMetaTyVar name kind details
+  = do { ref <- newMutVar details ;
+        return (mkTcTyVar name kind (MetaTv ref)) }
 
-readMutTyVar :: TyVar -> TcM (Maybe Type)
-readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+                     readMutVar (metaTvRef tyvar)
 
-writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
-writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
+writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
+writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 
+                          writeMutVar (metaTvRef tyvar) val
 
-newTyVar :: Kind -> TcM TcTyVar
-newTyVar kind
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind
   = newUnique  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
+    newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
 
-newTyVarTy  :: Kind -> TcM TcType
-newTyVarTy kind
-  = newTyVar kind      `thenM` \ tc_tyvar ->
+newTyFlexiVarTy  :: Kind -> TcM TcType
+newTyFlexiVarTy kind
+  = newFlexiTyVar kind `thenM` \ tc_tyvar ->
     returnM (TyVarTy tc_tyvar)
 
-newTyVarTys :: Int -> Kind -> TcM [TcType]
-newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
+newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
+newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
 
 newKindVar :: TcM TcKind
-newKindVar
-  = newUnique                                                  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv    `thenM` \ kv ->
-    returnM (TyVarTy kv)
+newKindVar = do        { uniq <- newUnique
+               ; ref <- newMutVar Nothing
+               ; return (KindVar (mkKindVar uniq ref)) }
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
-
-newOpenTypeKind :: TcM TcKind  -- Returns the kind (Type bx), where bx is fresh
-newOpenTypeKind
-  = newUnique                                                    `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv  `thenM` \ kv ->
-    returnM (mkTyConApp typeCon [TyVarTy kv])
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{'hole' type variables}
-%*                                                                     *
-%************************************************************************
-
-\begin{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}                
-
-%************************************************************************
-%*                                                                     *
 \subsection{Type instantiation}
 %*                                                                     *
 %************************************************************************
 
 Instantiating a bunch of type variables
 
-\begin{code}
-tcInstTyVars :: TyVarDetails -> [TyVar] 
-            -> TcM ([TcTyVar], [TcType], Subst)
+Note [TyVarName]
+~~~~~~~~~~~~~~~~
+Note that we don't change the print-name
+This won't confuse the type checker but there's a chance
+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 mkSystemName.
 
-tcInstTyVars tv_details tyvars
-  = mappM (tcInstTyVar tv_details) tyvars      `thenM` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+
+\begin{code}
+-----------------------
+tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVars tyvars
+  = do { tc_tvs <- mappM tcInstTyVar tyvars
+       ; let tys = mkTyVarTys tc_tvs
+       ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
-               -- any existing for-alls.  Hence mkTopTyVarSubst
-
-tcInstTyVar tv_details tyvar
-  = newUnique          `thenM` \ uniq ->
-    let
-       name = setNameUnique (tyVarName tyvar) uniq
-       -- Note that we don't change the print-name
-       -- This won't confuse the type checker but there's a chance
-       -- 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 mkSystemName.
-    in
-    newMutTyVar name (tyVarKind tyvar) tv_details
+               -- any existing for-alls.  Hence zipTopTvSubst
+
+tcInstTyVar tyvar      -- Freshen the Name of the tyvar
+  = do { uniq <- newUnique
+        ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
+                      (tyVarKind tyvar) Flexi }
 
-tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType :: 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
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
+
+
+---------------------------------------------
+tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.
+-- 
+-- Tne new type variables have the sane Name as the original *iff* they are scoped.
+-- For scoped tyvars, we don't need a fresh unique, because the renamer has made them
+-- unique, and it's better not to do so because we extend the envt
+-- with them as scoped type variables, and we'd like to avoid spurious
+-- 's = s' bindings in error messages
+--
+-- For non-scoped ones, we *must* instantiate fresh ones:
+--     
+--     type T = forall a. [a] -> [a]
+--     f :: T; 
+--     f = g where { g :: T; g = <rhs> }
+--
+-- We must not use the same 'a' from the defn of T at both places!!
+
+tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty
+
+tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name scoped_names tyvars
+  = mapM new_tv tyvars
+  where
+    new_tv tv 
+      = do { let name = tyVarName tv
+          ; ref <- newMutVar Flexi
+          ; name' <- if name `elem` scoped_names 
+                     then return name
+                     else do { uniq <- newUnique; return (setNameUnique name uniq) }
+          ; return (mkTcTyVar name' (tyVarKind tv) 
+                              (SigSkolTv id_name ref)) }
+                           
+
+---------------------------------------------
+tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
+
+tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcSkolTyVars info tyvars
+  = do { us <- newUniqueSupply
+       ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
+  where
+    skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
+                               (tyVarKind tv) (SkolemTv info)
+       -- See Note [TyVarName]
+                           
+
+---------------------------------------------
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but 
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty
+  = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info) 
+                             | tv <- tyvars ]
+
+-----------------------
+tc_inst_type :: ([TyVar] -> TcM [TcTyVar])             -- How to instantiate the type variables
+            -> TcType                                  -- Type to instantiate
+            -> TcM ([TcTyVar], TcThetaType, TcType)    -- Result
+tc_inst_type inst_tyvars ty
   = case tcSplitForAllTys ty of
-       ([],     rho) ->        -- There may be overloading despite no type variables;
+       ([],     rho) -> let    -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
-                        let
                           (theta, tau) = tcSplitPhiTy rho
                         in
-                        returnM ([], theta, tau)
+                        return ([], theta, tau)
 
-       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenM` \ (tyvars', _, tenv) ->
-                        let
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+                           ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+                               -- Either the tyvars are freshly made, by inst_tyvars,
+                               -- or (in the call from tcSkolSigType) any nested foralls
+                               -- have different binders.  Either way, zipTopTvSubst is ok
+
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }
 \end{code}
 
 
@@ -238,30 +266,26 @@ tcInstType tv_details ty
 %************************************************************************
 
 \begin{code}
-putTcTyVar :: TcTyVar -> TcType -> TcM TcType
-getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
-\end{code}
-
-Putting is easy:
-
-\begin{code}
-putTcTyVar tyvar ty 
-  | not (isMutTyVar tyvar)
+putMetaTyVar :: TcTyVar -> TcType -> TcM ()
+#ifndef DEBUG
+putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
+#else
+putMetaTyVar tyvar ty
+  | not (isMetaTyVar tyvar)
   = pprTrace "putTcTyVar" (ppr tyvar) $
-    returnM ty
+    returnM ()
 
   | otherwise
-  = ASSERT( isMutTyVar tyvar )
-    writeMutTyVar tyvar (Just ty)      `thenM_`
-    returnM ty
+  = ASSERT( isMetaTyVar tyvar )
+    ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
+    do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
+       ; writeMetaTyVar tyvar (Indirect ty) }
+  where
+    k1 = tyVarKind tyvar
+    k2 = typeKind ty
+#endif
 \end{code}
 
-Getting is more interesting.  The easy thing to do is just to read, thus:
-
-\begin{verbatim}
-getTcTyVar tyvar = readMutTyVar tyvar
-\end{verbatim}
-
 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.
@@ -269,36 +293,93 @@ any other type, then there might be bound TyVars embedded inside it.
 We return Nothing iff the original box was unbound.
 
 \begin{code}
+data LookupTyVarResult -- The result of a lookupTcTyVar call
+  = DoneTv TcTyVarDetails
+  | IndirectTv Bool TcType
+       --      True  => This is a non-wobbly type refinement, 
+       --               gotten from GADT match unification
+       --      False => This is a wobbly type, 
+       --               gotten from inference unification
+
+lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
+-- This function is the ONLY PLACE that we consult the 
+-- type refinement carried by the monad
+lookupTcTyVar tyvar 
+  = let 
+       details =  tcTyVarDetails tyvar
+    in
+    case details of
+      MetaTv ref -> lookup_wobbly details ref
+
+      SkolemTv _ -> do { type_reft <- getTypeRefinement
+                       ; case lookupVarEnv type_reft tyvar of
+                           Just ty -> return (IndirectTv True ty)
+                           Nothing -> return (DoneTv details)
+                       }
+
+       -- For SigSkolTvs try the refinement, and, failing that
+       -- see if it's been unified to anything.  It's a combination
+       -- of SkolemTv and MetaTv
+      SigSkolTv _  ref -> do { type_reft <- getTypeRefinement
+                            ; case lookupVarEnv type_reft tyvar of
+                               Just ty -> return (IndirectTv True ty)
+                               Nothing -> lookup_wobbly details ref
+                            }
+
+-- Look up a meta type variable, conditionally consulting 
+-- the current type refinement
+condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
+condLookupTcTyVar use_refinement tyvar 
+  | use_refinement = lookupTcTyVar tyvar
+  | otherwise
+  = case details of
+      MetaTv ref      -> lookup_wobbly details ref
+      SkolemTv _      -> return (DoneTv details)
+      SigSkolTv _ ref -> lookup_wobbly details ref
+  where 
+    details = tcTyVarDetails tyvar
+
+lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
+lookup_wobbly details ref
+  = do { meta_details <- readMutVar ref
+       ; case meta_details of
+           Indirect ty -> return (IndirectTv False ty)
+           Flexi       -> return (DoneTv details)
+       }
+
+{- 
+-- gaw 2004 We aren't shorting anything out anymore, at least for now
 getTcTyVar tyvar
-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)
   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
-  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
-    readMutTyVar tyvar                         `thenM` \ maybe_ty ->
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+    readMetaTyVar tyvar                                `thenM` \ maybe_ty ->
     case maybe_ty of
        Just ty -> short_out ty                         `thenM` \ ty' ->
-                  writeMutTyVar tyvar (Just ty')       `thenM_`
+                  writeMetaTyVar tyvar (Just ty')      `thenM_`
                   returnM (Just ty')
 
        Nothing    -> returnM Nothing
 
 short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)
-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)
   = returnM ty
 
   | otherwise
-  = readMutTyVar tyvar `thenM` \ maybe_ty ->
+  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->
     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ ty' ->
-                   writeMutTyVar tyvar (Just ty')      `thenM_`
+                   writeMetaTyVar tyvar (Just ty')     `thenM_`
                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty
+-}
 \end{code}
 
 
@@ -319,14 +400,14 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars       `thenM` \ tys ->
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
 \end{code}
 
 -----------------  Types
 
 \begin{code}
 zonkTcType :: TcType -> TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys
@@ -352,50 +433,38 @@ zonkTcPredType (IParam n t)
                     are used at the end of type checking
 
 \begin{code}
-zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
-zonkKindEnv pairs 
-  = mappM zonk_it pairs
- where
-    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 *)
-       --      zonk a *boxity* variable to *
-    zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
-                            | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
-                            | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
-                       
--- 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.
--- 
--- It does this by making an immutable version of tv and binds tv to it.
--- Now any bound occurences of the original type variable will get 
--- zonked to the immutable version.
-
-zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
-zonkTcTyVarToTyVar tv
-  = let
-               -- Make an immutable version, defaulting 
-               -- the kind to lifted if necessary
-       immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
-       immut_tv_ty = mkTyVarTy immut_tv
-
-        zap tv = putTcTyVar tv immut_tv_ty
-               -- Bind the mutable version to the immutable one
-    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           `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 )
-
-    returnM immut_tv
+zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
+-- When we do this, we also default the kind -- see notes with Kind.defaultKind
+-- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+-- bound occurences of the original type variable will get zonked to 
+-- the immutable version.
+--
+-- We leave skolem TyVars alone; they are immutable.
+zonkQuantifiedTyVar tv
+  | isSkolemTyVar tv = return tv
+       -- It might be a skolem type variable, 
+       -- for example from a user type signature
+
+  | otherwise  -- It's a meta-type-variable
+  = do { details <- readMetaTyVar tv
+
+       -- Create the new, frozen, regular type variable
+       ; let final_kind = defaultKind (tyVarKind tv)
+             final_tv   = mkTyVar (tyVarName tv) final_kind
+
+       -- Bind the meta tyvar to the new tyvar
+       ; case details of
+           Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                          return ()
+               -- [Sept 04] I don't think this should happen
+               -- See note [Silly Type Synonym]
+
+           other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
+
+       -- Return the new tyvar
+       ; return final_tv }
 \end{code}
 
 [Silly Type Synonyms]
@@ -423,10 +492,15 @@ Consider this:
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()
+  [Note Sept 04: now that we are zonking quantified type variables
+  on construction, the 'a' will be frozen as a regular tyvar on
+  quantification, so the floated dict will still have type (C d a).
+  Which renders this whole note moot; happily!]
 
 * Then the /\a abstraction has a zonked 'a' in it.
 
-All very silly.   I think its harmless to ignore the problem.
+All very silly.   I think its harmless to ignore the problem.  We'll end up with
+a /\a in the final result but all the occurrences of a will be zonked to ()
 
 
 %************************************************************************
@@ -438,17 +512,16 @@ All very silly.   I think its harmless to ignore the problem.
 %************************************************************************
 
 \begin{code}
--- zonkType is used for Kinds as well
-
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
-        -> TcType
+        -> Bool                        -- Should we consult the current type refinement?
+         -> TcType
         -> TcM Type
-zonkType unbound_var_fn ty
+zonkType unbound_var_fn rflag ty
   = go ty
   where
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
@@ -460,8 +533,8 @@ zonkType unbound_var_fn ty
 
     go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
 
-    go (SourceTy p)              = go_pred p           `thenM` \ p' ->
-                                   returnM (SourceTy p')
+    go (PredTy p)                = go_pred p           `thenM` \ p' ->
+                                   returnM (PredTy p')
 
     go (FunTy arg res)           = go arg              `thenM` \ arg' ->
                                    go res              `thenM` \ res' ->
@@ -475,39 +548,78 @@ zonkType unbound_var_fn ty
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
-    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar
 
-    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenM` \ tyvar' ->
-                            go ty                      `thenM` \ ty' ->
-                            returnM (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
+                            go ty              `thenM` \ ty' ->
+                            returnM (ForAllTy tyvar 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 -> 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
-    returnM (TyVarTy tyvar)
+          -> Bool                               -- Consult the type refinement?
+         -> TcTyVar -> TcM TcType
+zonkTyVar unbound_var_fn rflag tyvar 
+  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
+                               -- the quantified variable 'a' are TyVars not TcTyVars
+  = returnM (TyVarTy tyvar)
 
   | otherwise
-  =  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
+  =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
+     case details of
+          -- If b is true, the variable was refined, and therefore it is okay
+          -- to continue refining inside.  Otherwise it was wobbly and we should
+          -- not refine further inside.
+         IndirectTv b ty   -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+          DoneTv (MetaTv _) -> unbound_var_fn tyvar        -- Unbound meta type variable
+          DoneTv other      -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary
 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *
+                       Zonking kinds
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+readKindVar  :: KindVar -> TcM (Maybe TcKind)
+writeKindVar :: KindVar -> TcKind -> TcM ()
+readKindVar  (KVar _ ref)     = readMutVar ref
+writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+
+-------------
+zonkTcKind :: TcKind -> TcM TcKind
+zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
+                               ; k2' <- zonkTcKind k2
+                               ; returnM (FunKind k1' k2') }
+zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
+                              ; case mb_kind of
+                                   Nothing -> returnM k
+                                   Just k  -> zonkTcKind k }
+zonkTcKind other_kind = returnM other_kind
+
+-------------
+zonkTcKindToKind :: TcKind -> TcM Kind
+zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
+                                     ; k2' <- zonkTcKindToKind k2
+                                     ; returnM (FunKind k1' k2') }
+
+zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
+                                  ; case mb_kind of
+                                      Nothing -> return liftedTypeKind
+                                      Just k  -> zonkTcKindToKind k }
+
+zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
+zonkTcKindToKind other_kind   = returnM other_kind
+\end{code}
+                       
+%************************************************************************
+%*                                                                     *
 \subsection{Checking a user type}
 %*                                                                     *
 %************************************************************************
@@ -554,6 +666,7 @@ data UserTypeCtxt
                        --      f x :: t = ....
   | ForSigCtxt Name    -- Foreign inport or export signature
   | RuleSigCtxt Name   -- Signature on a forall'd variable in a RULE
+  | DefaultDeclCtxt    -- Types in a default declaration
 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []
@@ -566,28 +679,37 @@ data UserTypeCtxt
 -- With gla-exts that's right, but for H98 we should complain. 
 
 
-pprUserTypeCtxt (FunSigCtxt n)         = ptext SLIT("the type signature for") <+> quotes (ppr n)
-pprUserTypeCtxt ExprSigCtxt            = ptext SLIT("an expression type signature")
-pprUserTypeCtxt (ConArgCtxt c)         = ptext SLIT("the type of constructor") <+> quotes (ppr c)
-pprUserTypeCtxt (TySynCtxt c)          = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
-pprUserTypeCtxt GenPatCtxt             = ptext SLIT("the type pattern of a generic definition")
-pprUserTypeCtxt PatSigCtxt             = ptext SLIT("a pattern type signature")
-pprUserTypeCtxt ResSigCtxt             = ptext SLIT("a result type signature")
-pprUserTypeCtxt (ForSigCtxt n)         = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
-pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
+pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
+pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
+
+pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
+pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty (ConArgCtxt c)  = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
+pprUserTypeCtxt ty (TySynCtxt c)   = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
+                                         nest 2 (ptext SLIT(", namely") <+> ppr ty)]
+pprUserTypeCtxt ty GenPatCtxt      = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty PatSigCtxt      = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
+pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
+pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
+pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
+
+pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 \end{code}
 
 \begin{code}
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
-  = doptM Opt_GlasgowExts      `thenM` \ gla_exts ->
+  = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
+    doptM Opt_GlasgowExts      `thenM` \ gla_exts ->
     let 
        rank | gla_exts = Arbitrary
             | otherwise
             = case ctxt of     -- Haskell 98
                 GenPatCtxt     -> Rank 0
                 PatSigCtxt     -> Rank 0
+                DefaultDeclCtxt-> Rank 0
                 ResSigCtxt     -> Rank 0
                 TySynCtxt _    -> Rank 0
                 ExprSigCtxt    -> Rank 1
@@ -599,47 +721,30 @@ checkValidType ctxt ty
 
        actual_kind = typeKind ty
 
-       actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
-
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
-                       GenPatCtxt   -> actual_kind_is_lifted
-                       ForSigCtxt _ -> actual_kind_is_lifted
-                       other        -> isTypeKind actual_kind
+                       ResSigCtxt   -> isOpenTypeKind   actual_kind
+                       ExprSigCtxt  -> isOpenTypeKind   actual_kind
+                       GenPatCtxt   -> isLiftedTypeKind actual_kind
+                       ForSigCtxt _ -> isLiftedTypeKind actual_kind
+                       other        -> isArgTypeKind       actual_kind
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
                                   TySynCtxt _ -> UT_Ok
+                                  ExprSigCtxt -> UT_Ok
                                   other       -> UT_NotOk
                -- Unboxed tuples ok in function results,
                -- but for type synonyms we allow them even at
                -- top level
     in
-    addErrCtxt (checkTypeCtxt ctxt ty) $
-
        -- Check that the thing has kind Type, and is lifted if necessary
     checkTc kind_ok (kindErr actual_kind)      `thenM_`
 
        -- Check the internal validity of the type itself
-    check_poly_type rank ubx_tup ty
-
-
-checkTypeCtxt ctxt ty
-  = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
-         ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
-
-       -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
-       -- something strange like {Eq k} -> k -> k, because there is no
-       -- ForAll at the top of the type.  Since this is going to the user
-       -- we want it to look like a proper Haskell type even then; hence the hack
-       -- 
-       -- This shows up in the complaint about
-       --      case C a where
-       --        op :: Eq a => a -> a
-ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
-          | otherwise                       = ppr ty
-          where
-           (forall_tvs, theta, tau) = tcSplitSigmaTy ty
+    check_poly_type rank ubx_tup ty            `thenM_`
+
+    traceTc (text "checkValidType done" <+> ppr ty)
 \end{code}
 
 
@@ -697,9 +802,17 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
-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 ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
+       -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
+
+-- Naked PredTys don't usually show up, but they can as a result of
+--     {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy 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_`
@@ -746,8 +859,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   = 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
+               -- Args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty
 
   | otherwise
   = mappM_ check_arg_type tys
@@ -767,9 +880,9 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic 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
+forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
+unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
+ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
@@ -782,13 +895,25 @@ kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of
 %************************************************************************
 
 \begin{code}
+-- Enumerate the contexts in which a "source type", <S>, can occur
+--     Eq a 
+-- or  ?x::Int
+-- or  r <: {x::Int}
+-- or  (N a) where N is a newtype
+
 data SourceTyCtxt
   = ClassSCCtxt Name   -- Superclasses of clas
-  | SigmaCtxt          -- Context of a normal for-all type
-  | DataTyCtxt Name    -- Context of a data decl
+                       --      class <S> => C a where ...
+  | SigmaCtxt          -- Theta part of a normal for-all type
+                       --      f :: <S> => a -> a
+  | DataTyCtxt Name    -- Theta part of a data decl
+                       --      data <S> => T a = MkT a
   | TypeCtxt           -- Source type in an ordinary type
+                       --      f :: N a -> N a
   | InstThetaCtxt      -- Context of an instance decl
+                       --      instance <S> => C [a] where ...
   | InstHeadCtxt       -- Head of an instance decl
+                       --      instance ... => Eq a where ...
                
 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
@@ -810,7 +935,7 @@ 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,
+       -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
        -- so this error can only fire for the context of a class or
        -- data type decl.
     mappM_ (check_source_ty dflags ctxt) theta
@@ -820,8 +945,10 @@ check_valid_theta ctxt 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_`
+
+       -- Check the form of the argument types
+    mappM_ check_arg_type tys                          `thenM_`
     checkTc (check_class_pred_tys dflags ctxt tys)
            (predTyVarErr pred $$ how_to_allow)
 
@@ -846,8 +973,6 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- 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)
 
@@ -856,7 +981,7 @@ 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
+       InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
        other         -> gla_exts       || all tyvar_head tys
   where
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
@@ -952,7 +1077,7 @@ 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
+badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 
@@ -968,133 +1093,6 @@ arityErr kind name n m
 
 %************************************************************************
 %*                                                                     *
-\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)  `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}
-checkValidClass :: Class -> TcM ()
-checkValidClass cls
-  =    -- CHECK ARITY 1 FOR HASKELL 1.4
-    doptM Opt_GlasgowExts                              `thenM` \ gla_exts ->
-
-       -- Check that the class is unary, unless GlaExs
-    checkTc (notNull tyvars)   (nullaryClassErr cls)   `thenM_`
-    checkTc (gla_exts || unary) (classArityErr cls)    `thenM_`
-
-       -- Check the super-classes
-    checkValidTheta (ClassSCCtxt (className cls)) theta        `thenM_`
-
-       -- Check the class operations
-    mappM_ check_op op_stuff           `thenM_`
-
-       -- 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)        `thenM_`
-               -- The 'tail' removes the initial (C a) from the
-               -- class itself, leaving just the method type
-
-         checkValidType (FunSigCtxt op_name) tau       `thenM_`
-
-               -- 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}
 %*                                                                     *
 %************************************************************************
@@ -1127,15 +1125,6 @@ checkValidInstHead ty    -- Should be a source type
     }}
 
 check_inst_head dflags clas tys
-  |    -- CCALL CHECK
-       -- A user declaration of a CCallable/CReturnable instance
-       -- must be for a "boxed primitive" type.
-        (clas `hasKey` cCallableClassKey   
-            && not (ccallable_type first_ty)) 
-  ||    (clas `hasKey` cReturnableClassKey 
-            && not (creturnable_type first_ty))
-  = failWithTc (nonBoxedPrimCCallErr clas first_ty)
-
        -- If GlasgowExts then check at least one isn't a type variable
   | dopt Opt_GlasgowExts dflags
   = check_tyvars dflags clas tys
@@ -1155,9 +1144,6 @@ check_inst_head dflags clas tys
   where
     (first_ty : _)       = tys
 
-    ccallable_type   ty = isFFIArgumentTy dflags PlayRisky ty
-    creturnable_type ty = isFFIImportResultTy dflags ty
-       
     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
                             text "where T is not a synonym, and a,b,c are distinct type variables")
 
@@ -1178,8 +1164,4 @@ undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
 instTypeErr pp_ty msg
   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
         nest 4 msg]
-
-nonBoxedPrimCCallErr clas inst_ty
-  = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
-        4 (pprClassPred clas [inst_ty])
 \end{code}