[project @ 2005-03-08 09:47:35 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 832ee9c..b4a0ac7 100644 (file)
@@ -11,29 +11,34 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, newHoleTyVarTy,
-  newTyVarTy,          -- Kind -> NF_TcM TcType
-  newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
-  newKindVar, newKindVars, newBoxityVar,
-  putTcTyVar, getTcTyVar,
+  newFlexiTyVar,
+  newTyFlexiVarTy,             -- Kind -> TcM TcType
+  newTyFlexiVarTys,            -- Int -> Kind -> TcM [TcType]
+  newKindVar, newKindVars, 
+  lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, 
 
   --------------------------------
   -- Instantiation
 
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars,
-  tcInstSigTyVars, tcInstType,
-  tcSplitRhoTyM,
+  tcInstTyVar, tcInstTyVars, tcInstType, 
+  tcSkolType, tcSkolTyVars, tcInstSigType,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
 
   --------------------------------
   -- Checking type validity
-  Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
-  SourceTyCtxt(..), checkValidTheta, 
-  checkValidInstHead, instTypeErr,
+  Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
+  SourceTyCtxt(..), checkValidTheta, checkFreeness,
+  checkValidInstHead, instTypeErr, checkAmbiguity,
+  arityErr, 
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar
 
   ) where
 
 
   ) where
 
@@ -41,50 +46,45 @@ module TcMType (
 
 
 -- friends:
 
 
 -- friends:
-import TypeRep         ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
-                         Kind, ThetaType
+import HsSyn           ( LHsType )
+import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
+                         ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
-                         tcEqType, tcCmpPred,
-                         tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
+                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
+                         MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
+                         tcCmpPred, isClassPred, 
+                         tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
-
+                         tcIsTyVarTy, tcSplitSigmaTy, 
+                         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           ( classArity, className )
-import TyCon           ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
+import Type            ( TvSubst, zipTopTvSubst, substTy )
+import Class           ( Class, classArity, className )
+import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
                          tyConArity, tyConName )
                          tyConArity, tyConName )
-import PrimRep         ( PrimRep(VoidRep) )
-import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Var             ( TyVar, tyVarKind, tyVarName, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
 
 -- others:
 
 -- others:
-import TcMonad          -- TcType, amongst others
-import TysWiredIn      ( voidTy )
-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, mkSysLocalName,
-                         mkLocalName, mkDerivedTyConOcc
-                       )
+import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import VarSet
+import VarEnv
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import CmdLineOpts     ( dopt, DynFlag(..) )
-import Unique          ( Uniquable(..) )
-import SrcLoc          ( noSrcLoc )
-import Util            ( nOfThem, isSingleton, equalLength )
+import UniqSupply      ( uniqsFromSupply )
+import Util            ( nOfThem, isSingleton, equalLength, notNull )
 import ListSetOps      ( removeDups )
 import ListSetOps      ( removeDups )
+import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
 
 import Outputable
 \end{code}
 
@@ -96,38 +96,39 @@ import Outputable
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-newTyVar :: Kind -> NF_TcM TcTyVar
-newTyVar kind
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
-
-newTyVarTy  :: Kind -> NF_TcM TcType
-newTyVarTy kind
-  = newTyVar kind      `thenNF_Tc` \ tc_tyvar ->
-    returnNF_Tc (TyVarTy tc_tyvar)
-
-newHoleTyVarTy :: NF_TcM TcType
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv  `thenNF_Tc` \ tv ->
-    returnNF_Tc (TyVarTy tv)
-
-newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
-
-newKindVar :: NF_TcM TcKind
-newKindVar
-  = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("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 (mkSysLocalName uniq SLIT("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)
+
+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}
 
 
@@ -137,98 +138,125 @@ newBoxityVar
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-I don't understand why this is needed
-An old comments says "No need for tcSplitForAllTyM because a type 
-       variable can't be instantiated to a for-all type"
-But the same is true of rho types!
-
-\begin{code}
-tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
-tcSplitRhoTyM t
-  = go t t []
- where
-       -- A type variable is never instantiated to a dictionary type,
-       -- so we don't need to do a tcReadVar on the "arg".
-    go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
-                                       Just pair -> go res res (pair:ts)
-                                       Nothing   -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (NoteTy n t)    ts = go syn_t t ts
-    go syn_t (TyVarTy tv)    ts = getTcTyVar tv                `thenNF_Tc` \ maybe_ty ->
-                                 case maybe_ty of
-                                   Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
-                                   other                          -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (UsageTy _ t)   ts = go syn_t t ts
-    go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
-\end{code}
-
+Instantiating a bunch of type variables
 
 
-%************************************************************************
-%*                                                                     *
-\subsection{Type instantiation}
-%*                                                                     *
-%************************************************************************
+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.
 
 
-Instantiating a bunch of type variables
 
 \begin{code}
 
 \begin{code}
-tcInstTyVars :: [TyVar] 
-            -> NF_TcM ([TcTyVar], [TcType], Subst)
-
+-----------------------
+tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 tcInstTyVars tyvars
 tcInstTyVars tyvars
-  = mapNF_Tc tcInstTyVar tyvars        `thenNF_Tc` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+  = 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 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 mkSysLocalName.
-    in
-    tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
-
-tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
-tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
-  = tcGetUniques       `thenNF_Tc` \ uniqs ->
-    listTc [ ASSERT( not (kind `eqKind` openTypeKind) )        -- Shouldn't happen
-            tcNewMutTyVar name kind details
-          | (tyvar, uniq) <- tyvars `zip` uniqs,
-            let name = setNameUnique (tyVarName tyvar) uniq, 
-            let kind = tyVarKind tyvar
-          ]
-\end{code}
+               -- any existing for-alls.  Hence zipTopTvSubst
 
 
-@tcInstType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, splits off the dictionary part, and returns the results.
+tcInstTyVar tyvar      -- Freshen the Name of the tyvar
+  = do { uniq <- newUnique
+        ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
+                      (tyVarKind tyvar) Flexi }
 
 
-\begin{code}
-tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
-tcInstType ty
+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 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 but no type variables;
+       ([],     rho) -> let    -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
                                --      (?x :: Int) => Int -> Int
-                        let
-                          (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
+                          (theta, tau) = tcSplitPhiTy rho
                         in
                         in
-                        returnNF_Tc ([], theta, tau)
+                        return ([], theta, tau)
 
 
-       (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
-                        let
-                          (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
-                        in
-                        returnNF_Tc (tyvars', theta, tau)
-\end{code}
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 
 
+                           ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+                               -- Either the tyvars are freshly made, by inst_tyvars,
+                               -- or (in the call from tcSkolSigType) any nested foralls
+                               -- have different binders.  Either way, zipTopTvSubst is ok
+
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }
+\end{code}
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -238,31 +266,26 @@ tcInstType 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 )
-    UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
-    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.
@@ -270,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) $
   = 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}
 
 
@@ -312,126 +392,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
-
-zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
-                          returnNF_Tc (tyVarsOfTypes tys)
-
-zonkTcTyVar :: TcTyVar -> NF_TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
-
-zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
--- This guy is to zonk the tyvars we're about to feed into tcSimplify
--- Usually this job is done by checkSigTyVars, but in a couple of places
--- that is overkill, so we use this simpler chap
-zonkTcSigTyVars tyvars
-  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
-    returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
+zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
+zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
+
+zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars    `thenM` \ tys ->
+                          returnM (tyVarsOfTypes tys)
+
+zonkTcTyVar :: TcTyVar -> TcM TcType
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) 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
-       --      Void            if it has kind Lifted
-       --      :Void           otherwise
-       -- We know it's unbound even though we don't carry an environment,
-       -- because at the binding site for a type variable we bind the
-       -- mutable tyvar to a fresh immutable one.  So the mutable store
-       -- plays the role of an environment.  If we come across a mutable
-       -- type variable that isn't so bound, it must be completely free.
-    zonk_unbound_tyvar tv
-       | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
-       = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
-                               -- this vastly common case
-       | otherwise
-       = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
-       where
-         kind = tyVarKind tv
-
-    mk_void_tycon tv kind      -- Make a new TyCon with the same kind as the 
-                               -- type variable tv.  Same name too, apart from
-                               -- making it start with a colon (sigh)
-               -- I dread to think what will happen if this gets out into an 
-               -- interface file.  Catastrophe likely.  Major sigh.
-       = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
-         mkPrimTyCon tc_name kind 0 [] VoidRep
-       where
-         tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
-
--- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
--- of a type variable, at the *end* of type checking.  It changes
--- the *mutable* type variable into an *immutable* one.
--- 
--- 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.
+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}
 
 
-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
+[Silly Type Synonyms]
 
 
-        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 ->
+Consider this:
+       type C u a = u  -- Note 'a' unused
 
 
-    WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
+       foo :: (forall a. C u a -> C u a) -> u
+       foo x = ...
 
 
-    returnNF_Tc immut_tv
-\end{code}
+       bar :: Num u => u
+       bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type  {Num d} =>  d -> d
+  where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+       {Num (C d a)} =>  C d a -> C d a
+  where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  The arg to foo becomes
+       /\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+       a = ()
+  [Note Sept 04: now that we are zonking quantified type variables
+  on construction, the 'a' will be frozen as a regular tyvar on
+  quantification, so the floated dict will still have type (C d a).
+  Which renders this whole note moot; happily!]
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly.   I think its harmless to ignore the problem.  We'll end up with
+a /\a in the final result but all the occurrences of a will be zonked to ()
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -443,77 +512,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 (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
-                                    go ty               `thenNF_Tc` \ ty' ->
-                                    returnNF_Tc (UsageTy u' ty')
+    go (AppTy fun arg)           = go fun              `thenM` \ fun' ->
+                                   go arg              `thenM` \ arg' ->
+                                   returnM (mkAppTy fun' arg')
+               -- NB the mkAppTy; we might have instantiated a
+               -- type variable to a type constructor, so we need
+               -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
 
        -- 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
+          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}
 %*                                                                     *
 %************************************************************************
@@ -560,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 = []
@@ -572,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
-  = 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
@@ -605,39 +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
+                                  ExprSigCtxt -> UT_Ok
+                                  other       -> UT_NotOk
+               -- Unboxed tuples ok in function results,
+               -- but for type synonyms we allow them even at
+               -- top level
     in
     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 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}
 
 
@@ -648,17 +755,23 @@ decRank :: Rank -> Rank
 decRank Arbitrary = Arbitrary
 decRank (Rank n)  = Rank (n-1)
 
 decRank Arbitrary = Arbitrary
 decRank (Rank n)  = Rank (n-1)
 
-check_poly_type :: Rank -> Type -> TcM ()
-check_poly_type (Rank 0) ty 
-  = check_tau_type (Rank 0) False ty
+----------------------------------------
+data UbxTupFlag = UT_Ok        | UT_NotOk
+       -- The "Ok" version means "ok if -fglasgow-exts is on"
+
+----------------------------------------
+check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+check_poly_type (Rank 0) ubx_tup ty 
+  = check_tau_type (Rank 0) ubx_tup ty
 
 
-check_poly_type rank ty 
+check_poly_type rank ubx_tup ty 
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
-    check_valid_theta SigmaCtxt theta          `thenTc_`
-    check_tau_type (decRank rank) False tau    `thenTc_`
-    checkAmbiguity tvs theta tau
+    check_valid_theta SigmaCtxt theta          `thenM_`
+    check_tau_type (decRank rank) ubx_tup tau  `thenM_`
+    checkFreeness tvs theta                    `thenM_`
+    checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
 check_arg_type :: Type -> TcM ()
 
 ----------------------------------------
 check_arg_type :: Type -> TcM ()
@@ -677,49 +790,84 @@ check_arg_type :: Type -> TcM ()
 -- NB: unboxed tuples can have polymorphic or unboxed args.
 --     This happens in the workers for functions returning
 --     product types with polymorphic components.
 -- NB: unboxed tuples can have polymorphic or unboxed args.
 --     This happens in the workers for functions returning
 --     product types with polymorphic components.
---     But not in user code
--- 
--- Question: what about nested unboxed tuples?
---          Currently rejected.
+--     But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
 check_arg_type ty 
 check_arg_type ty 
-  = check_tau_type (Rank 0) False ty   `thenTc_` 
+  = check_tau_type (Rank 0) UT_NotOk ty                `thenM_` 
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
-check_tau_type :: Rank -> Bool -> Type -> TcM ()
+check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 -- Rank is allowed rank for function args
 -- No foralls otherwise
--- Bool is True iff unboxed tuple are allowed here
-
-check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = failWithTc (usageTyErr ty)
-check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc          `thenNF_Tc` \ dflags ->
-                                                  check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
-check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
-  = check_poly_type rank      arg_ty   `thenTc_`
-    check_tau_type  rank True res_ty
-
-check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
-  = check_arg_type ty1 `thenTc_` check_arg_type ty2
-
-check_tau_type rank ubx_tup_ok (NoteTy note ty)
-  = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
-
-check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
-  | isSynTyCon tc
-  = checkTc syn_arity_ok arity_msg     `thenTc_`
-    mapTc_ check_arg_type tys
+
+check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup 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 UT_Ok    res_ty
+
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+  = check_arg_type ty1 `thenM_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
+       -- Synonym notes are built only when the synonym is 
+       -- saturated (see Type.mkSynTy)
+  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
+    (if gla_exts then
+       -- If -fglasgow-exts then don't check the 'note' part.
+       -- This  allows us to instantiate a synonym defn with a 
+       -- for-all type, or with a partially-applied type synonym.
+       --      e.g.   type T a b = a
+       --             type S m   = m ()
+       --             f :: S (T Int)
+       -- Here, T is partially applied, so it's illegal in H98.
+       -- But if you expand S first, then T we get just 
+       --             f :: Int
+       -- which is fine.
+       returnM ()
+    else
+       -- For H98, do check the un-expanded part
+       check_tau_type rank ubx_tup syn         
+    )                                          `thenM_`
+
+    check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+  = check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup ty@(TyConApp tc tys)
+  | isSynTyCon tc      
+  =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
+       -- synonym application, leaving it to checkValidType (i.e. right here)
+       -- to find the error
+    checkTc syn_arity_ok arity_msg     `thenM_`
+    mappM_ check_arg_type tys
     
   | isUnboxedTupleTyCon tc
     
   | isUnboxedTupleTyCon tc
-  = checkTc ubx_tup_ok ubx_tup_msg     `thenTc_`
-    mapTc_ (check_tau_type (Rank 0) True) tys  -- Args are allowed to be unlifted, or
-                                               -- more unboxed tuples, so can't use check_arg_ty
+  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
+    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenM_`
+    mappM_ (check_tau_type (Rank 0) UT_Ok) tys 
+               -- Args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty
 
   | otherwise
 
   | otherwise
-  = mapTc_ check_arg_type tys
+  = mappM_ check_arg_type tys
 
   where
 
   where
+    ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+
     syn_arity_ok = tc_arity <= n_args
                -- It's OK to have an *over-applied* type synonym
                --      data Tree a b = ...
     syn_arity_ok = tc_arity <= n_args
                -- It's OK to have an *over-applied* type synonym
                --      data Tree a b = ...
@@ -732,86 +880,13 @@ check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-check_note (FTVNote _)  = returnTc ()
-check_note (SynNote ty) = check_tau_type (Rank 0) False ty
-\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
-
-NOTE: 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.
-This is the is_free test below.
-
-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 -> Type -> TcM ()
-checkAmbiguity forall_tyvars theta tau
-  = mapTc_ check_pred theta    `thenTc_`
-    returnTc ()
-  where
-    tau_vars         = tyVarsOfType tau
-    extended_tau_vars = grow theta tau_vars
-
-    is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
-                       not (ct_var `elemVarSet` extended_tau_vars)
-    is_free ct_var    = not (ct_var `elem` forall_tyvars)
-    
-    check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
-                     checkTc (isIPPred pred || not all_free) (freeErr  pred)
-             where 
-               ct_vars   = varSetElems (tyVarsOfPred pred)
-               all_free  = all is_free ct_vars
-               any_ambig = any is_ambig ct_vars
+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}
 
 \end{code}
 
-\begin{code}
-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 '=>'"))]
-
 
 
-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"))
-    ]
-
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
-usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
-unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
-ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
-kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
-\end{code}
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -820,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")
@@ -839,24 +926,31 @@ 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) (predTyVarErr pred)
+    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
     class_name = className cls
 
   where
     class_name = className cls
@@ -864,11 +958,10 @@ 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
+                    other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 
 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type
 
 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type
@@ -880,12 +973,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
@@ -894,14 +996,98 @@ tyvar_head ty                     -- Haskell 98 allows predicates of form
        Nothing      -> False
 \end{code}
 
        Nothing      -> False
 \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
+  = mappM_ complain (filter is_ambig theta)
+  where
+    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))
+
+    ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
+                       not (ct_var `elemVarSet` extended_tau_vars)
+
+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}
 \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)
+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)
+
+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}
 
 
+\begin{code}
 checkThetaCtxt ctxt theta
   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 checkThetaCtxt ctxt theta
   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+
+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)
+
+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}
 
 
@@ -921,7 +1107,7 @@ compiled elsewhere). In these cases, we let them go through anyway.
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}
-checkValidInstHead :: Type -> TcM ()
+checkValidInstHead :: Type -> TcM (Class, [TcType])
 
 checkValidInstHead ty  -- Should be a source type
   = case tcSplitPredTy_maybe ty of {
 
 checkValidInstHead ty  -- Should be a source type
   = case tcSplitPredTy_maybe ty of {
@@ -932,21 +1118,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
+    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
@@ -958,7 +1136,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)
@@ -966,31 +1144,24 @@ 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")
-               $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
+                  $$ undecidableMsg)
+
+undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
 \end{code}
 
 \begin{code}
 instTypeErr pp_ty msg
   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
         nest 4 msg]
 \end{code}
 
 \begin{code}
 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}
-
-