projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
[project @ 2005-02-25 13:06:31 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index 15d4150..2a3dc75 100644 (file)
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -11,30 +11,34 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, 
-  newTyVarTy,          -- Kind -> NF_TcM TcType
-  newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
-  newKindVar, newKindVars, newBoxityVar,
-  putTcTyVar, getTcTyVar,
-
-  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, isRigidType,
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar
 
   ) where
 
 
   ) where
 
@@ -42,56 +46,45 @@ module TcMType (
 
 
 -- friends:
 
 
 -- friends:
-import TypeRep         ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
+import HsSyn           ( LHsType )
+import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
                          Kind, ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          Kind, ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
-                         tcEqType, tcCmpPred,
+                         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, 
-                         isUnLiftedType, isIPPred, isHoleTyVar,
-
+                         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, isAnyTypeKind,
-
-                         isFFIArgumentTy, isFFIImportResultTy
+                         pprPred, pprTheta, pprClassPred )
+import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+                         liftedTypeKind, defaultKind
                        )
                        )
-import qualified Type  ( splitFunTys )
-import Subst           ( Subst, mkTopTyVarSubst, substTy )
-import Class           ( Class, DefMeth(..), classArity, className, classBigSig )
-import TyCon           ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName, tyConKind, tyConTheta, 
-                         getSynTyConDefn, tyConDataCons )
-import DataCon         ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
-import FieldLabel      ( fieldLabelName, fieldLabelType )
-import PrimRep         ( PrimRep(VoidRep) )
-import Var             ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Type            ( TvSubst, zipTopTvSubst, substTy )
+import Class           ( Class, classArity, className )
+import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
+                         tyConArity, tyConName )
+import Var             ( TyVar, tyVarKind, tyVarName, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
 
 -- others:
 
 -- others:
-import Generics                ( validGenericMethodType )
-import TcMonad          -- TcType, amongst others
-import TysWiredIn      ( voidTy, listTyCon, tupleTyCon )
-import PrelNames       ( cCallableClassKey, cReturnableClassKey, hasKey )
-import ForeignCall     ( Safety(..) )
+import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )
 import FunDeps         ( grow )
-import PprType         ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name            ( Name, NamedThing(..), setNameUnique, mkSystemName,
-                         mkInternalName, mkDerivedTyConOcc
-                       )
+import Name            ( Name, setNameUnique, mkSysTvName, mkSystemName, getOccName )
 import VarSet
 import VarSet
-import BasicTypes      ( Boxity(Boxed) )
+import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import CmdLineOpts     ( dopt, DynFlag(..) )
-import Unique          ( Uniquable(..) )
-import SrcLoc          ( noSrcLoc )
-import Util            ( nOfThem, isSingleton, equalLength )
-import ListSetOps      ( equivClasses, removeDups )
+import UniqSupply      ( uniqsFromSupply )
+import Util            ( nOfThem, isSingleton, equalLength, notNull )
+import ListSetOps      ( removeDups )
+import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
 
 import Outputable
 \end{code}
 
@@ -103,125 +96,171 @@ import Outputable
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-newTyVar :: Kind -> NF_TcM TcTyVar
-newTyVar kind
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
-
-newTyVarTy  :: Kind -> NF_TcM TcType
-newTyVarTy kind
-  = newTyVar kind      `thenNF_Tc` \ tc_tyvar ->
-    returnNF_Tc (TyVarTy tc_tyvar)
-
-newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
-
-newKindVar :: NF_TcM TcKind
-newKindVar
-  = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv   `thenNF_Tc` \ kv ->
-    returnNF_Tc (TyVarTy kv)
-
-newKindVars :: Int -> NF_TcM [TcKind]
-newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
-
-newBoxityVar :: NF_TcM TcKind
-newBoxityVar
-  = tcGetUnique                                                          `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
-    returnNF_Tc (TyVarTy kv)
+newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
+newMetaTyVar name kind details
+  = do { ref <- newMutVar details ;
+        return (mkTcTyVar name kind (MetaTv ref)) }
+
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+                     readMutVar (metaTvRef tyvar)
+
+writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
+writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 
+                          writeMutVar (metaTvRef tyvar) val
+
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind
+  = newUnique  `thenM` \ uniq ->
+    newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
+
+newTyFlexiVarTy  :: Kind -> TcM TcType
+newTyFlexiVarTy kind
+  = newFlexiTyVar kind `thenM` \ tc_tyvar ->
+    returnM (TyVarTy tc_tyvar)
+
+newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
+newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
+
+isRigidType :: TcType -> TcM Bool
+-- Check that the type is rigid, *taking the type refinement into account*
+-- In other words if a rigid type variable tv is refined to a wobbly type,
+-- the answer should be False
+-- ToDo: can this happen?
+isRigidType ty
+  = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
+       ; return (and rigids) }
+  where
+    is_rigid tv = do { details <- lookupTcTyVar tv
+                    ; case details of
+                       RigidTv            -> return True
+                       IndirectTv True ty -> isRigidType ty
+                       other              -> return False
+                    }
+
+newKindVar :: TcM TcKind
+newKindVar = do        { uniq <- newUnique
+               ; ref <- newMutVar Nothing
+               ; return (KindVar (mkKindVar uniq ref)) }
+
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{'hole' type variables}
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-newHoleTyVarTy :: NF_TcM TcType
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv   `thenNF_Tc` \ tv ->
-    returnNF_Tc (TyVarTy tv)
-
-readHoleResult :: TcType -> NF_TcM TcType
--- Read the answer out of a hole, constructed by newHoleTyVarTy
-readHoleResult (TyVarTy tv)
-  = ASSERT( isHoleTyVar tv )
-    getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
-    case maybe_res of
-       Just ty -> returnNF_Tc ty
-       Nothing ->  pprPanic "readHoleResult: empty" (ppr tv)
-readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
-
-zapToType :: TcType -> NF_TcM TcType
-zapToType (TyVarTy tv)
-  | isHoleTyVar tv
-  = getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
-    case maybe_res of
-       Nothing -> newTyVarTy openTypeKind      `thenNF_Tc` \ ty ->
-                  putTcTyVar tv ty             `thenNF_Tc_`
-                  returnNF_Tc ty
-       Just ty  -> returnNF_Tc ty      -- No need to loop; we never
-                                       -- have chains of holes
-
-zapToType other_ty = returnNF_Tc other_ty
-\end{code}                
-
-%************************************************************************
-%*                                                                     *
 \subsection{Type instantiation}
 %*                                                                     *
 %************************************************************************
 
 Instantiating a bunch of type variables
 
 \subsection{Type instantiation}
 %*                                                                     *
 %************************************************************************
 
 Instantiating a bunch of type variables
 
-\begin{code}
-tcInstTyVars :: TyVarDetails -> [TyVar] 
-            -> NF_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
-  = mapNF_Tc (tcInstTyVar tv_details) tyvars   `thenNF_Tc` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnNF_Tc (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
-  = tcGetUnique                `thenNF_Tc` \ 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
-    tcNewMutTyVar name (tyVarKind tyvar) tv_details
+               -- any existing for-alls.  Hence zipTopTvSubst
 
 
-tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+tcInstTyVar tyvar      -- Use the OccName of the tyvar we are instantiating
+                       -- but make a System Name, so that it's updated in 
+                       -- preference to a tcInstSigTyVar
+  = do { uniq <- newUnique
+        ; newMetaTyVar (mkSystemName uniq (getOccName tyvar)) 
+                      (tyVarKind tyvar) Flexi }
+
+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 :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh meta type variables, but
+-- ones which have the same Name as the original type 
+-- variable.  This is used for type signatures, where we must
+-- instantiate with meta type variables, but we'd like to avoid
+-- instantiating them were possible; and the unifier unifies
+-- tyvars with System Names by preference
+-- 
+-- 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
+tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
+
+tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars tyvars
+  = mapM new_tv tyvars
+  where
+    new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
+                           
+
+---------------------------------------------
+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
-                        returnNF_Tc ([], theta, tau)
+                        return ([], theta, tau)
 
 
-       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenNF_Tc` \ (tyvars', _, tenv) ->
-                        let
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnNF_Tc (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}
 
 
@@ -232,30 +271,26 @@ tcInstType tv_details ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
-getTcTyVar :: TcTyVar -> NF_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) $
-    returnNF_Tc ty
+    returnM ()
 
   | otherwise
 
   | otherwise
-  = ASSERT( isMutTyVar tyvar )
-    tcWriteMutTyVar tyvar (Just ty)    `thenNF_Tc_`
-    returnNF_Tc 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 = tcReadMutTyVar 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.
@@ -263,36 +298,80 @@ 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
+  = FlexiTv
+  | RigidTv
+  | 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
+--
+-- The boolean returned with Indirect
+lookupTcTyVar tyvar 
+  = case tcTyVarDetails tyvar of
+      SkolemTv _ -> do { type_reft <- getTypeRefinement
+                       ; case lookupVarEnv type_reft tyvar of
+                           Just ty -> return (IndirectTv True ty)
+                           Nothing -> return RigidTv
+                       }
+      MetaTv ref -> do         { details <- readMutVar ref
+                       ; case details of
+                           Indirect ty -> return (IndirectTv False ty)
+                           Flexi       -> return FlexiTv
+                       }
+
+-- 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 tcTyVarDetails tyvar of
+      SkolemTv _ -> return RigidTv
+      MetaTv ref -> do { details <- readMutVar ref
+                       ; case details of
+                           Indirect ty -> return (IndirectTv False ty)
+                           Flexi       -> return FlexiTv
+                       }
+
+{- 
+-- 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) $
   = pprTrace "getTcTyVar" (ppr tyvar) $
-    returnNF_Tc (Just (mkTyVarTy tyvar))
+    returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
 
   | otherwise
-  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
-    tcReadMutTyVar tyvar                               `thenNF_Tc` \ maybe_ty ->
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+    readMetaTyVar tyvar                                `thenM` \ maybe_ty ->
     case maybe_ty of
     case maybe_ty of
-       Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
-                  tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
-                  returnNF_Tc (Just ty')
+       Just ty -> short_out ty                         `thenM` \ ty' ->
+                  writeMetaTyVar tyvar (Just ty')      `thenM_`
+                  returnM (Just ty')
 
 
-       Nothing    -> returnNF_Tc Nothing
+       Nothing    -> returnM Nothing
 
 
-short_out :: TcType -> NF_TcM TcType
+short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)
 short_out ty@(TyVarTy tyvar)
-  | not (isMutTyVar tyvar)
-  = returnNF_Tc ty
+  | not (isTcTyVar tyvar)
+  = returnM ty
 
   | otherwise
 
   | otherwise
-  = tcReadMutTyVar tyvar       `thenNF_Tc` \ maybe_ty ->
+  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->
     case maybe_ty of
     case maybe_ty of
-       Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
-                   tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
-                   returnNF_Tc ty'
+       Just ty' -> short_out ty'                       `thenM` \ ty' ->
+                   writeMetaTyVar tyvar (Just ty')     `thenM_`
+                   returnM ty'
 
 
-       other    -> returnNF_Tc ty
+       other    -> returnM ty
 
 
-short_out other_ty = returnNF_Tc other_ty
+short_out other_ty = returnM other_ty
+-}
 \end{code}
 
 
 \end{code}
 
 
@@ -305,150 +384,115 @@ short_out other_ty = returnNF_Tc other_ty
 -----------------  Type variables
 
 \begin{code}
 -----------------  Type variables
 
 \begin{code}
-zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
-zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
+zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
+zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
 
 
-zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
-                          returnNF_Tc (tyVarsOfTypes tys)
+zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars    `thenM` \ tys ->
+                          returnM (tyVarsOfTypes tys)
 
 
-zonkTcTyVar :: TcTyVar -> NF_TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+zonkTcTyVar :: TcTyVar -> TcM TcType
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
 \end{code}
 
 -----------------  Types
 
 \begin{code}
 \end{code}
 
 -----------------  Types
 
 \begin{code}
-zonkTcType :: TcType -> NF_TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+zonkTcType :: TcType -> TcM TcType
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
 
 
-zonkTcTypes :: [TcType] -> NF_TcM [TcType]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mappM zonkTcType tys
 
 
-zonkTcClassConstraints cts = mapNF_Tc zonk cts
+zonkTcClassConstraints cts = mappM zonk cts
     where zonk (clas, tys)
     where zonk (clas, tys)
-           = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
-             returnNF_Tc (clas, new_tys)
+           = zonkTcTypes tys   `thenM` \ new_tys ->
+             returnM (clas, new_tys)
 
 
-zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
-zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+zonkTcThetaType :: TcThetaType -> TcM TcThetaType
+zonkTcThetaType theta = mappM zonkTcPredType theta
 
 
-zonkTcPredType :: TcPredType -> NF_TcM TcPredType
+zonkTcPredType :: TcPredType -> TcM TcPredType
 zonkTcPredType (ClassP c ts)
 zonkTcPredType (ClassP c ts)
-  = zonkTcTypes ts     `thenNF_Tc` \ new_ts ->
-    returnNF_Tc (ClassP c new_ts)
+  = zonkTcTypes ts     `thenM` \ new_ts ->
+    returnM (ClassP c new_ts)
 zonkTcPredType (IParam n t)
 zonkTcPredType (IParam n t)
-  = zonkTcType t       `thenNF_Tc` \ new_t ->
-    returnNF_Tc (IParam n new_t)
+  = zonkTcType t       `thenM` \ new_t ->
+    returnM (IParam n new_t)
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
                     are used at the end of type checking
 
 \begin{code}
-zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
-zonkKindEnv pairs 
-  = mapNF_Tc zonk_it pairs
- where
-    zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
-                             returnNF_Tc (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)
-                       
-zonkTcTypeToType :: TcType -> NF_TcM Type
-zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
-  where
-       -- Zonk a mutable but unbound type variable to an arbitrary type
-       -- We know it's unbound even though we don't carry an environment,
-       -- because at the binding site for a type variable we bind the
-       -- mutable tyvar to a fresh immutable one.  So the mutable store
-       -- plays the role of an environment.  If we come across a mutable
-       -- type variable that isn't so bound, it must be completely free.
-    zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
-
-
--- When the type checker finds a type variable with no binding,
--- which means it can be instantiated with an arbitrary type, it
--- usually instantiates it to Void.  Eg.
--- 
---     length []
--- ===>
---     length Void (Nil Void)
--- 
--- But in really obscure programs, the type variable might have
--- a kind other than *, so we need to invent a suitably-kinded type.
--- 
--- This commit uses
---     Void for kind *
---     List for kind *->*
---     Tuple for kind *->...*->*
--- 
--- which deals with most cases.  (Previously, it only dealt with
--- kind *.)   
--- 
--- In the other cases, it just makes up a TyCon with a suitable
--- kind.  If this gets into an interface file, anyone reading that
--- file won't understand it.  This is fixable (by making the client
--- of the interface file make up a TyCon too) but it is tiresome and
--- never happens, so I am leaving it 
-
-mkArbitraryType :: TcTyVar -> Type
--- Make up an arbitrary type whose kind is the same as the tyvar.
--- We'll use this to instantiate the (unbound) tyvar.
-mkArbitraryType tv 
-  | isAnyTypeKind kind = voidTy                -- The vastly common case
-  | otherwise         = TyConApp tycon []
-  where
-    kind       = tyVarKind tv
-    (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
+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}
 
 
-    tycon | kind `eqKind` tyConKind listTyCon  -- *->*
-         = listTyCon                           -- No tuples this size
+[Silly Type Synonyms]
 
 
-         | all isTypeKind args && isTypeKind res
-         = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
+Consider this:
+       type C u a = u  -- Note 'a' unused
 
 
-         | otherwise
-         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
-           mkPrimTyCon tc_name kind 0 [] VoidRep
-               -- Same name as the tyvar, apart from making it start with a colon (sigh)
-               -- I dread to think what will happen if this gets out into an 
-               -- interface file.  Catastrophe likely.  Major sigh.
+       foo :: (forall a. C u a -> C u a) -> u
+       foo x = ...
 
 
-    tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+       bar :: Num u => u
+       bar = foo (\t -> t + t)
 
 
--- 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.
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
 
 
-zonkTcTyVarToTyVar :: TcTyVar -> NF_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
+* Now unify with type of foo's arg, and we get:
+       {Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
 
 
-        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           `thenNF_Tc` \ ty2 ->
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  The arg to foo becomes
+       /\a -> \t -> t+t
 
 
-    WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
+* 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!]
 
 
-    returnNF_Tc immut_tv
-\end{code}
+* Then the /\a abstraction has a zonked 'a' in it.
+
+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 ()
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -460,76 +504,114 @@ zonkTcTyVarToTyVar tv
 %************************************************************************
 
 \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
 
 -- 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 -> NF_TcM Type)   -- What to do with unbound mutable type variables
+zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
                                        -- see zonkTcType, and zonkTcTypeToType
-        -> TcType
-        -> NF_TcM Type
-zonkType unbound_var_fn ty
+        -> Bool                        -- Should we consult the current type refinement?
+         -> TcType
+        -> TcM Type
+zonkType unbound_var_fn rflag ty
   = go ty
   where
   = go ty
   where
-    go (TyConApp tycon tys)      = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
-                                   returnNF_Tc (TyConApp tycon tys')
+    go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
+                                   returnM (TyConApp tycon tys')
 
 
-    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenNF_Tc` \ ty1' ->
-                                   go ty2              `thenNF_Tc` \ ty2' ->
-                                   returnNF_Tc (NoteTy (SynNote ty1') ty2')
+    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
+                                   go ty2              `thenM` \ ty2' ->
+                                   returnM (NoteTy (SynNote ty1') ty2')
 
     go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
 
 
     go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
 
-    go (SourceTy p)              = go_pred p           `thenNF_Tc` \ p' ->
-                                   returnNF_Tc (SourceTy p')
+    go (PredTy p)                = go_pred p           `thenM` \ p' ->
+                                   returnM (PredTy p')
 
 
-    go (FunTy arg res)           = go arg              `thenNF_Tc` \ arg' ->
-                                   go res              `thenNF_Tc` \ res' ->
-                                   returnNF_Tc (FunTy arg' res')
+    go (FunTy arg res)           = go arg              `thenM` \ arg' ->
+                                   go res              `thenM` \ res' ->
+                                   returnM (FunTy arg' res')
  
  
-    go (AppTy fun arg)           = go fun              `thenNF_Tc` \ fun' ->
-                                   go arg              `thenNF_Tc` \ arg' ->
-                                   returnNF_Tc (mkAppTy fun' arg')
+    go (AppTy fun arg)           = go fun              `thenM` \ fun' ->
+                                   go arg              `thenM` \ arg' ->
+                                   returnM (mkAppTy fun' arg')
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
-    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
-
-    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenNF_Tc` \ tyvar' ->
-                            go ty                      `thenNF_Tc` \ ty' ->
-                            returnNF_Tc (ForAllTy tyvar' ty')
-
-    go_pred (ClassP c tys) = mapNF_Tc go tys   `thenNF_Tc` \ tys' ->
-                            returnNF_Tc (ClassP c tys')
-    go_pred (NType tc tys) = mapNF_Tc go tys   `thenNF_Tc` \ tys' ->
-                            returnNF_Tc (NType tc tys')
-    go_pred (IParam n ty)  = go ty             `thenNF_Tc` \ ty' ->
-                            returnNF_Tc (IParam n ty')
-
-zonkTyVar :: (TcTyVar -> NF_TcM Type)          -- What to do for an unbound mutable variable
-         -> TcTyVar -> NF_TcM TcType
-zonkTyVar unbound_var_fn tyvar 
-  | not (isMutTyVar tyvar)     -- Not a mutable tyvar.  This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be mutable
-  = ASSERT( isTyVar tyvar )            -- Should not be any immutable kind vars
-    returnNF_Tc (TyVarTy tyvar)
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar
+
+    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 (IParam n ty)  = go ty             `thenM` \ ty' ->
+                            returnM (IParam n ty')
+
+zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable
+          -> 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  `thenNF_Tc` \ 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
+          FlexiTv         -> unbound_var_fn tyvar         -- Unbound flexi
+          RigidTv         -> 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}
 %*                                                                     *
 %************************************************************************
@@ -576,6 +658,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 = []
@@ -588,28 +671,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
-  = doptsTc Opt_GlasgowExts    `thenNF_Tc` \ 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
@@ -621,47 +713,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
-    tcAddErrCtxt (checkTypeCtxt ctxt ty)       $
-
        -- Check that the thing has kind Type, and is lifted if necessary
        -- Check that the thing has kind Type, and is lifted if necessary
-    checkTc kind_ok (kindErr actual_kind)      `thenTc_`
+    checkTc kind_ok (kindErr actual_kind)      `thenM_`
 
        -- Check the internal validity of the type itself
 
        -- Check 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 && not (null 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}
 
 
@@ -685,9 +760,9 @@ check_poly_type rank ubx_tup ty
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
-    check_valid_theta SigmaCtxt theta          `thenTc_`
-    check_tau_type (decRank rank) ubx_tup tau  `thenTc_`
-    checkFreeness tvs theta                    `thenTc_`
+    check_valid_theta SigmaCtxt theta          `thenM_`
+    check_tau_type (decRank rank) ubx_tup tau  `thenM_`
+    checkFreeness tvs theta                    `thenM_`
     checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
     checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
@@ -711,7 +786,7 @@ check_arg_type :: Type -> TcM ()
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type ty 
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type ty 
-  = check_tau_type (Rank 0) UT_NotOk ty                `thenTc_` 
+  = check_tau_type (Rank 0) UT_NotOk ty                `thenM_` 
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
@@ -719,42 +794,68 @@ 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)    = getDOptsTc             `thenNF_Tc` \ dflags ->
-                                               check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup (TyVarTy _)       = returnTc ()
+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_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
-  = check_poly_type rank UT_NotOk arg_ty       `thenTc_`
+  = check_poly_type rank UT_NotOk arg_ty       `thenM_`
     check_tau_type  rank UT_Ok    res_ty
 
 check_tau_type rank ubx_tup (AppTy ty1 ty2)
     check_tau_type  rank UT_Ok    res_ty
 
 check_tau_type rank ubx_tup (AppTy ty1 ty2)
-  = check_arg_type ty1 `thenTc_` check_arg_type ty2
+  = check_arg_type ty1 `thenM_` check_arg_type ty2
 
 
-check_tau_type rank ubx_tup (NoteTy note ty)
-  = check_tau_type rank ubx_tup ty
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
        -- Synonym notes are built only when the synonym is 
        -- saturated (see Type.mkSynTy)
        -- Synonym notes are built only when the synonym is 
        -- saturated (see Type.mkSynTy)
-       -- Not checking the 'note' part allows us to instantiate a synonym
-       -- defn with a for-all type, or with a partially-applied type synonym,
-       -- but that seems OK too
+  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
+    (if gla_exts then
+       -- If -fglasgow-exts then don't check the 'note' part.
+       -- This  allows us to instantiate a synonym defn with a 
+       -- for-all type, or with a partially-applied type synonym.
+       --      e.g.   type T a b = a
+       --             type S m   = m ()
+       --             f :: S (T Int)
+       -- Here, T is partially applied, so it's illegal in H98.
+       -- But if you expand S first, then T we get just 
+       --             f :: Int
+       -- which is fine.
+       returnM ()
+    else
+       -- For H98, do check the un-expanded part
+       check_tau_type rank ubx_tup syn         
+    )                                          `thenM_`
+
+    check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+  = check_tau_type rank ubx_tup ty
 
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc      
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
 
 check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   | isSynTyCon tc      
   =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
-       -- synonym application, leaving it to checkValidType (i.e. right here
+       -- synonym application, leaving it to checkValidType (i.e. right here)
        -- to find the error
        -- to find the error
-    checkTc syn_arity_ok arity_msg     `thenTc_`
-    mapTc_ check_arg_type tys
+    checkTc syn_arity_ok arity_msg     `thenM_`
+    mappM_ check_arg_type tys
     
   | isUnboxedTupleTyCon tc
     
   | isUnboxedTupleTyCon tc
-  = doptsTc Opt_GlasgowExts                    `thenNF_Tc` \ gla_exts ->
-    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenTc_`
-    mapTc_ (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
+  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
+    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
+    mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
+               -- Args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty
 
   | otherwise
 
   | otherwise
-  = mapTc_ check_arg_type tys
+  = mappM_ check_arg_type tys
 
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
@@ -771,82 +872,12 @@ 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}
 
-Check for ambiguity
-~~~~~~~~~~~~~~~~~~~
-         forall V. P => tau
-is ambiguous if P contains generic variables
-(i.e. one of the Vs) that are not mentioned in tau
-
-However, we need to take account of functional dependencies
-when we speak of 'mentioned in tau'.  Example:
-       class C a b | a -> b where ...
-Then the type
-       forall x y. (C x y) => x
-is not ambiguous because x is mentioned and x determines y
-
-NB; the ambiguity check is only used for *user* types, not for types
-coming from inteface files.  The latter can legitimately have
-ambiguous types. Example
-
-   class S a where s :: a -> (Int,Int)
-   instance S Char where s _ = (1,1)
-   f:: S a => [a] -> Int -> (Int,Int)
-   f (_::[a]) x = (a*x,b)
-       where (a,b) = s (undefined::a)
-
-Here the worker for f gets the type
-       fw :: forall a. S a => Int -> (# Int, Int #)
-
-If the list of tv_names is empty, we have a monotype, and then we
-don't need to check for ambiguity either, because the test can't fail
-(see is_ambig).
-
-\begin{code}
-checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
-checkAmbiguity forall_tyvars theta tau_tyvars
-  = mapTc_ complain (filter is_ambig theta)
-  where
-    complain pred     = addErrTc (ambigErr pred)
-    extended_tau_vars = grow theta tau_tyvars
-    is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
-
-    ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
-                       not (ct_var `elemVarSet` extended_tau_vars)
-
-    is_free ct_var    = not (ct_var `elem` forall_tyvars)
-
-ambigErr pred
-  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
-        nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
-                ptext SLIT("must be reachable from the type after the '=>'"))]
-\end{code}
-    
-In addition, GHC insists that at least one type variable
-in each constraint is in V.  So we disallow a type like
-       forall a. Eq b => b -> b
-even in a scope where b is in scope.
-
-\begin{code}
-checkFreeness forall_tyvars theta
-  = mapTc_ complain (filter is_free theta)
-  where    
-    is_free pred     =  not (isIPPred pred)
-                    && not (any bound_var (varSetElems (tyVarsOfPred pred)))
-    bound_var ct_var = ct_var `elem` forall_tyvars
-    complain pred    = addErrTc (freeErr pred)
-
-freeErr pred
-  = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
-                  ptext SLIT("are already in scope"),
-        nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
-    ]
-\end{code}
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -856,13 +887,25 @@ freeErr pred
 %************************************************************************
 
 \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")
@@ -875,24 +918,30 @@ pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 \begin{code}
 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 checkValidTheta ctxt theta 
 \begin{code}
 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 checkValidTheta ctxt theta 
-  = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
+  = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 
 -------------------------
 check_valid_theta ctxt []
 
 -------------------------
 check_valid_theta ctxt []
-  = returnTc ()
+  = returnM ()
 check_valid_theta ctxt theta
 check_valid_theta ctxt theta
-  = getDOptsTc                                 `thenNF_Tc` \ dflags ->
-    warnTc (not (null dups)) (dupPredWarn dups)        `thenNF_Tc_`
-    mapTc_ (check_source_ty dflags ctxt) theta
+  = getDOpts                                   `thenM` \ dflags ->
+    warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
+       -- Actually, in instance decls and type signatures, 
+       -- 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
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
 check_source_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
 check_source_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
-    mapTc_ check_arg_type tys          `thenTc_`
-    checkTc (arity == n_tys) arity_err         `thenTc_`
-    checkTc (all tyvar_head tys || arby_preds_ok)
+    checkTc (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)
 
   where
            (predTyVarErr pred $$ how_to_allow)
 
   where
@@ -901,12 +950,6 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
 
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
 
-    arby_preds_ok = case ctxt of
-                       InstHeadCtxt  -> True   -- We check for instance-head formation
-                                               -- in checkValidInstHead
-                       InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
-                       other         -> dopt Opt_GlasgowExts               dflags
-
     how_to_allow = case ctxt of
                     InstHeadCtxt  -> empty     -- Should not happen
                     InstThetaCtxt -> parens undecidableMsg
     how_to_allow = case ctxt of
                     InstHeadCtxt  -> empty     -- Should not happen
                     InstThetaCtxt -> parens undecidableMsg
@@ -922,12 +965,21 @@ 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)   = mapTc_ 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)
 
 -------------------------
+check_class_pred_tys dflags ctxt tys 
+  = case ctxt of
+       InstHeadCtxt  -> True   -- We check for instance-head 
+                               -- formation in checkValidInstHead
+       InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
+       other         -> gla_exts       || all tyvar_head tys
+  where
+    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
+    gla_exts      = dopt Opt_GlasgowExts dflags
+
+-------------------------
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable
@@ -936,141 +988,98 @@ tyvar_head ty                    -- Haskell 98 allows predicates of form
        Nothing      -> False
 \end{code}
 
        Nothing      -> False
 \end{code}
 
-\begin{code}
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
-predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
-dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
-
-checkThetaCtxt ctxt theta
-  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
-         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
-\end{code}
+Check for ambiguity
+~~~~~~~~~~~~~~~~~~~
+         forall V. P => tau
+is ambiguous if P contains generic variables
+(i.e. one of the Vs) that are not mentioned in tau
 
 
+However, we need to take account of functional dependencies
+when we speak of 'mentioned in tau'.  Example:
+       class C a b | a -> b where ...
+Then the type
+       forall x y. (C x y) => x
+is not ambiguous because x is mentioned and x determines y
 
 
-%************************************************************************
-%*                                                                     *
-\subsection{Validity check for TyCons}
-%*                                                                     *
-%************************************************************************
+NB; the ambiguity check is only used for *user* types, not for types
+coming from inteface files.  The latter can legitimately have
+ambiguous types. Example
 
 
-checkValidTyCon is called once the mutually-recursive knot has been
-tied, so we can look at things freely.
+   class S a where s :: a -> (Int,Int)
+   instance S Char where s _ = (1,1)
+   f:: S a => [a] -> Int -> (Int,Int)
+   f (_::[a]) x = (a*x,b)
+       where (a,b) = s (undefined::a)
 
 
-\begin{code}
-checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
-  | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
-  | otherwise
-  =    -- Check the context on the data decl
-    checkValidTheta (DataTyCtxt name) (tyConTheta tc)  `thenTc_` 
-       
-       -- Check arg types of data constructors
-    mapTc_ checkValidDataCon data_cons                 `thenTc_`
+Here the worker for f gets the type
+       fw :: forall a. S a => Int -> (# Int, Int #)
 
 
-       -- Check that fields with the same name share a type
-    mapTc_ check_fields groups
+If the list of tv_names is empty, we have a monotype, and then we
+don't need to check for ambiguity either, because the test can't fail
+(see is_ambig).
 
 
+\begin{code}
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+  = mappM_ complain (filter is_ambig theta)
   where
   where
-    name         = tyConName tc
-    (_, syn_rhs) = getSynTyConDefn tc
-    data_cons    = tyConDataCons tc
-
-    fields = [field | con <- data_cons, field <- dataConFieldLabels con]
-    groups = equivClasses cmp_name fields
-    cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
-
-    check_fields fields@(first_field_label : other_fields)
-       -- These fields all have the same name, but are from
-       -- different constructors in the data type
-       =       -- Check that all the fields in the group have the same type
-               -- NB: this check assumes that all the constructors of a given
-               -- data type use the same type variables
-         checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
-       where
-           field_ty   = fieldLabelType first_field_label
-           field_name = fieldLabelName first_field_label
-           other_tys  = map fieldLabelType other_fields
-
-checkValidDataCon :: DataCon -> TcM ()
-checkValidDataCon con
-  = checkValidType ctxt (idType (dataConWrapId con))   `thenTc_`
-               -- This checks the argument types and
-               -- ambiguity of the existential context (if any)
-    tcAddErrCtxt (existentialCtxt con)
-                (checkFreeness ex_tvs ex_theta)
-  where
-    ctxt = ConArgCtxt (dataConName con) 
-    (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
+    complain pred     = addErrTc (ambigErr pred)
+    extended_tau_vars = grow theta tau_tyvars
 
 
+       -- Only a *class* predicate can give rise to ambiguity
+       -- An *implicit parameter* cannot.  For example:
+       --      foo :: (?x :: [a]) => Int
+       --      foo = length ?x
+       -- is fine.  The call site will suppply a particular 'x'
+    is_ambig pred     = isClassPred  pred &&
+                       any ambig_var (varSetElems (tyVarsOfPred pred))
 
 
-fieldTypeMisMatch field_name
-  = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
+    ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
+                       not (ct_var `elemVarSet` extended_tau_vars)
 
 
-existentialCtxt con = ptext SLIT("When checking the existential context of constructor") 
-                     <+> quotes (ppr con)
+ambigErr pred
+  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
+        nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
+                ptext SLIT("must be reachable from the type after the '=>'"))]
 \end{code}
 \end{code}
-
-
-checkValidClass is called once the mutually-recursive knot has been
-tied, so we can look at things freely.
+    
+In addition, GHC insists that at least one type variable
+in each constraint is in V.  So we disallow a type like
+       forall a. Eq b => b -> b
+even in a scope where b is in scope.
 
 \begin{code}
 
 \begin{code}
-checkValidClass :: Class -> TcM ()
-checkValidClass cls
-  =    -- CHECK ARITY 1 FOR HASKELL 1.4
-    doptsTc Opt_GlasgowExts                            `thenTc` \ gla_exts ->
-
-       -- Check that the class is unary, unless GlaExs
-    checkTc (not (null tyvars))                (nullaryClassErr cls)   `thenTc_`
-    checkTc (gla_exts || unary) (classArityErr cls)    `thenTc_`
+checkFreeness forall_tyvars theta
+  = mappM_ complain (filter is_free theta)
+  where    
+    is_free pred     =  not (isIPPred pred)
+                    && not (any bound_var (varSetElems (tyVarsOfPred pred)))
+    bound_var ct_var = ct_var `elem` forall_tyvars
+    complain pred    = addErrTc (freeErr pred)
 
 
-       -- Check the super-classes
-    checkValidTheta (ClassSCCtxt (className cls)) theta        `thenTc_`
+freeErr pred
+  = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
+                  ptext SLIT("are already in scope"),
+        nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
+    ]
+\end{code}
 
 
-       -- Check the class operations
-    mapTc_ check_op op_stuff           `thenTc_`
+\begin{code}
+checkThetaCtxt ctxt theta
+  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
+         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 
-       -- 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)
+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)
 
 
-  where
-    (tyvars, theta, _, op_stuff) = classBigSig cls
-    unary      = isSingleton tyvars
-    no_generics = null [() | (_, GenDefMeth) <- op_stuff]
-
-    check_op (sel_id, dm) 
-       = checkValidTheta SigmaCtxt (tail theta)        `thenTc_`
-               -- The 'tail' removes the initial (C a) from the
-               -- class itself, leaving just the method type
-
-         checkValidType (FunSigCtxt op_name) tau       `thenTc_`
-
-               -- Check that for a generic method, the type of 
-               -- the method is sufficiently simple
-         checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
-                 (badGenericMethodType op_name op_ty)
-       where
-         op_name = idName sel_id
-         op_ty   = idType sel_id
-         (_,theta,tau) = tcSplitSigmaTy op_ty
-
-nullaryClassErr cls
-  = ptext SLIT("No parameters for class")  <+> quotes (ppr cls)
-
-classArityErr cls
-  = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
-         parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
-
-genericMultiParamErr clas
-  = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+> 
-    ptext SLIT("cannot have generic methods")
-
-badGenericMethodType op op_ty
-  = hang (ptext SLIT("Generic method type is too complex"))
-       4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
-               ptext SLIT("You can only use type variables, arrows, and tuples")])
+arityErr kind name n m
+  = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
+          n_arguments <> comma, text "but has been given", int m]
+    where
+       n_arguments | n == 0 = ptext SLIT("no arguments")
+                   | n == 1 = ptext SLIT("1 argument")
+                   | True   = hsep [int n, ptext SLIT("arguments")]
 \end{code}
 
 
 \end{code}
 
 
@@ -1101,22 +1110,13 @@ checkValidInstHead ty   -- Should be a source type
        Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
         Just (clas,tys) ->
 
        Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
         Just (clas,tys) ->
 
-    getDOptsTc                                 `thenNF_Tc` \ dflags ->
-    mapTc_ check_arg_type tys                  `thenTc_`
-    check_inst_head dflags clas tys            `thenTc_`
-    returnTc (clas, tys)
+    getDOpts                                   `thenM` \ dflags ->
+    mappM_ check_arg_type tys                  `thenM_`
+    check_inst_head dflags clas tys            `thenM_`
+    returnM (clas, tys)
     }}
 
 check_inst_head dflags clas tys
     }}
 
 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
@@ -1128,7 +1128,7 @@ check_inst_head dflags clas tys
     all tcIsTyVarTy arg_tys,           -- Applied to type variables
     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
           -- This last condition checks that all the type variables are distinct
     all tcIsTyVarTy arg_tys,           -- Applied to type variables
     equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
           -- This last condition checks that all the type variables are distinct
-  = returnTc ()
+  = returnM ()
 
   | otherwise
   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
 
   | otherwise
   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
@@ -1136,17 +1136,14 @@ 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")
 
 check_tyvars dflags clas tys
        -- Check that at least one isn't a type variable
        -- unless -fallow-undecideable-instances
     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")
 
 check_tyvars dflags clas tys
        -- Check that at least one isn't a type variable
        -- unless -fallow-undecideable-instances
-  | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
-  | not (all tcIsTyVarTy tys)                = returnTc ()
+  | dopt Opt_AllowUndecidableInstances dflags = returnM ()
+  | not (all tcIsTyVarTy tys)                = returnM ()
   | otherwise                                = failWithTc (instTypeErr (pprClassPred clas tys) msg)
   where
     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
   | otherwise                                = failWithTc (instTypeErr (pprClassPred clas tys) msg)
   where
     msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
@@ -1159,8 +1156,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}
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)