[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
 
   --------------------------------
   -- 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, 
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
+  tcSkolType, tcSkolTyVars, tcInstSigType,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
 
   --------------------------------
   -- Checking type validity
-  Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
-  SourceTyCtxt(..), checkValidTheta, 
-  checkValidTyCon, checkValidClass, 
+  Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
+  SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,
   checkValidInstHead, instTypeErr, checkAmbiguity,
-  arityErr,
+  arityErr, 
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking
-  zonkType,
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar
 
   ) where
 
 
   ) where
 
@@ -45,48 +46,45 @@ module TcMType (
 
 
 -- friends:
 
 
 -- 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,
                        ) 
 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,
                          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,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
-
-                         liftedTypeKind, openTypeKind, defaultKind, superKind,
-                         superBoxity, liftedBoxity, typeKind,
                          tyVarsOfType, tyVarsOfTypes, 
                          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, 
 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:
 
 -- others:
-import Generics                ( validGenericMethodType )
 import TcRnMonad          -- TcType, amongst others
 import TcRnMonad          -- TcType, amongst others
-import PrelNames       ( cCallableClassKey, cReturnableClassKey, hasKey )
-import ForeignCall     ( Safety(..) )
 import FunDeps         ( grow )
 import FunDeps         ( grow )
-import PprType         ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name            ( Name, setNameUnique, mkSystemTvNameEncoded )
+import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import VarSet
+import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import CmdLineOpts     ( dopt, DynFlag(..) )
+import UniqSupply      ( uniqsFromSupply )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
 import Util            ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps      ( equivClasses, removeDups )
+import ListSetOps      ( removeDups )
+import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
 
 import Outputable
 \end{code}
 
@@ -98,136 +96,166 @@ import Outputable
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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 ->
   = 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)
 
     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 :: 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 ())
 
 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}
 
 
 %************************************************************************
 %*                                                                     *
 \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
 
 \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
                -- 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 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
   = 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
                                --      (?x :: Int) => Int -> Int
-                        let
                           (theta, tau) = tcSplitPhiTy rho
                         in
                           (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}
 
 
 \end{code}
 
 
@@ -238,30 +266,26 @@ tcInstType tv_details ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \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) $
   = pprTrace "putTcTyVar" (ppr tyvar) $
-    returnM ty
+    returnM ()
 
   | otherwise
 
   | 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}
 
 \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.
 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}
 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
 getTcTyVar tyvar
-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)
   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
   = 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' ->
     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)
                   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
   = returnM ty
 
   | otherwise
-  = readMutTyVar tyvar `thenM` \ maybe_ty ->
+  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->
     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ 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
                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty
+-}
 \end{code}
 
 
 \end{code}
 
 
@@ -319,14 +400,14 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars       `thenM` \ tys ->
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
                           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
 \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
 
 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}
                     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]
 \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 = ()
 
 * 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.
 
 
 * 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}
 %************************************************************************
 
 \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
 -- 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
         -> 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' ->
   = 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 (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' ->
 
     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!
                -- 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 (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
     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
 
   | 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}
 
 
 
 %************************************************************************
 %*                                                                     *
 \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}
 %*                                                                     *
 %************************************************************************
 \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
                        --      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 = []
 
 -- 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. 
 
 
 -- 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
 \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
     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
                 ResSigCtxt     -> Rank 0
                 TySynCtxt _    -> Rank 0
                 ExprSigCtxt    -> Rank 1
@@ -599,47 +721,30 @@ checkValidType ctxt ty
 
        actual_kind = typeKind ty
 
 
        actual_kind = typeKind ty
 
-       actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
-
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
        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
        
        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
                                   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 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}
 
 
 \end{code}
 
 
@@ -697,9 +802,17 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
 -- 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_`
 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 
   = 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
 
   | 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
 
 ----------------------------------------
     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}
 
 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}
 %************************************************************************
 
 \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
 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
   | TypeCtxt           -- Source type in an ordinary type
+                       --      f :: N a -> N a
   | InstThetaCtxt      -- Context of an instance decl
   | InstThetaCtxt      -- Context of an instance decl
+                       --      instance <S> => C [a] where ...
   | InstHeadCtxt       -- Head of an instance decl
   | 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")
                
 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, 
   = 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
        -- 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
 -------------------------
 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 (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)
 
     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.
 
        -- 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)
 
 -- 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
   = 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 
        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 ]
 
   = 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)
 
 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}
 %*                                                                     *
 %************************************************************************
 \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
     }}
 
 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
        -- 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
 
   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")
 
     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]
 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}
 \end{code}