Beautiful new approach to the skolem-escape check and untouchable
[ghc.git] / compiler / typecheck / TcMType.lhs
index f206b5e..950d733 100644 (file)
@@ -18,42 +18,49 @@ module TcMType (
   newFlexiTyVarTy,             -- Kind -> TcM TcType
   newFlexiTyVarTys,            -- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, 
   newFlexiTyVarTy,             -- Kind -> TcM TcType
   newFlexiTyVarTys,            -- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, 
-  lookupTcTyVar, LookupTyVarResult(..),
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, 
 
 
-  --------------------------------
-  -- Boxy type variables
-  newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
+  isFilledMetaTyVar, isFlexiMetaTyVar,
 
   --------------------------------
 
   --------------------------------
-  -- Creating new coercion variables
-  newCoVars,
+  -- Creating new evidence variables
+  newEvVar, newCoVar, newEvVars,
+  newWantedCoVar, writeWantedCoVar, readWantedCoVar, 
+  newIP, newDict, newSelfDict, isSelfDict,
+
+  newWantedEvVar, newWantedEvVars, 
+  newKindConstraint,
+  newTcEvBinds, addTcEvBind,
 
   --------------------------------
   -- Instantiation
 
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
-  tcInstSigTyVars, zonkSigTyVar,
-  tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars,
+  tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
+  tcInstType, tcInstSigType,
+  tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
+  tcSkolSigType, tcSkolSigTyVars, 
 
   --------------------------------
   -- Checking type validity
 
   --------------------------------
   -- Checking type validity
-  Rank, UserTypeCtxt(..), checkValidType, 
-  SourceTyCtxt(..), checkValidTheta, checkFreeness,
-  checkValidInstHead, checkValidInstance, checkAmbiguity,
-  checkInstTermination,
+  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
+  SourceTyCtxt(..), checkValidTheta, 
+  checkValidInstHead, checkValidInstance, 
+  checkInstTermination, checkValidTypeInst, checkTyFamFreeness, 
   arityErr, 
   arityErr, 
+  growPredTyVars, growThetaTyVars, validDerivPred,
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking
-  zonkType, zonkTcPredType, 
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, mkZonkTcTyVar, zonkTcPredType, 
+  zonkTcTypeCarefully,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
-  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
+  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcKindToKind, zonkTcKind, 
+  zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+  zonkTcTypeAndSubst,
+  tcGetGlobalTyVars, 
 
   readKindVar, writeKindVar
 
   readKindVar, writeKindVar
-
   ) where
 
 #include "HsVersions.h"
   ) where
 
 #include "HsVersions.h"
@@ -68,7 +75,9 @@ import TyCon
 import Var
 
 -- others:
 import Var
 
 -- others:
-import TcRnMonad          -- TcType, amongst others
+import HsSyn           -- HsType
+import TcRnMonad        -- TcType, amongst others
+import Id
 import FunDeps
 import Name
 import VarSet
 import FunDeps
 import Name
 import VarSet
@@ -77,66 +86,119 @@ import DynFlags
 import Util
 import Maybes
 import ListSetOps
 import Util
 import Maybes
 import ListSetOps
-import UniqSupply
+import BasicTypes
 import SrcLoc
 import Outputable
 import SrcLoc
 import Outputable
+import FastString
+import Bag
 
 
-import Control.Monad   ( when )
+import Control.Monad
 import Data.List       ( (\\) )
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 import Data.List       ( (\\) )
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-       Instantiation in general
+       Kind variables
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-tcInstType :: ([TyVar] -> TcM [TcTyVar])               -- How to instantiate the type variables
-          -> TcType                                    -- Type to instantiate
-          -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
-tcInstType inst_tyvars ty
-  = case tcSplitForAllTys ty of
-       ([],     rho) -> let    -- There may be overloading despite no type variables;
-                               --      (?x :: Int) => Int -> Int
-                          (theta, tau) = tcSplitPhiTy rho
-                        in
-                        return ([], 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
+newKindVar :: TcM TcKind
+newKindVar = do        { uniq <- newUnique
+               ; ref <- newMutVar Flexi
+               ; return (mkTyVarTy (mkKindVar uniq ref)) }
 
 
-                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                           ; return (tyvars', theta, tau) }
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-       Kind variables
+     Evidence variables; range over constraints we can abstract over
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
-newCoVars spec
-  = do { us <- newUniqueSupply 
-       ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
-                          (mkCoKind ty1 ty2)
-                | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
-
-newKindVar :: TcM TcKind
-newKindVar = do        { uniq <- newUnique
-               ; ref <- newMutVar Flexi
-               ; return (mkTyVarTy (mkKindVar uniq ref)) }
+newEvVars :: TcThetaType -> TcM [EvVar]
+newEvVars theta = mapM newEvVar theta
+
+newWantedEvVar :: TcPredType -> TcM EvVar 
+newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
+newWantedEvVar (ClassP cls tys) = newDict cls tys
+newWantedEvVar (IParam ip ty)   = newIP ip ty
+
+newWantedEvVars :: TcThetaType -> TcM [EvVar] 
+newWantedEvVars theta = mapM newWantedEvVar theta 
+
+newWantedCoVar :: TcType -> TcType -> TcM CoVar 
+newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
+
+-- We used to create a mutable co-var
+{-
+-- A wanted coercion variable is a MetaTyVar
+-- that can be filled in with its binding
+  = do { uniq <- newUnique 
+       ; ref <- newMutVar Flexi 
+       ; let name = mkSysTvName uniq (fsLit "c")
+             kind = mkPredTy (EqPred ty1 ty2) 
+       ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
+-}
 
 
-newKindVars :: Int -> TcM [TcKind]
-newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
+--------------
+newEvVar :: TcPredType -> TcM EvVar
+-- Creates new *rigid* variables for predicates
+newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
+newEvVar (ClassP cls tys) = newDict  cls tys
+newEvVar (IParam ip ty)   = newIP    ip ty
+
+newCoVar :: TcType -> TcType -> TcM CoVar
+newCoVar ty1 ty2
+  = do { name <- newName (mkTyVarOccFS (fsLit "co"))
+       ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+
+newIP :: IPName Name -> TcType -> TcM IpId
+newIP ip ty
+  = do         { name <- newName (getOccName (ipNameName ip))
+        ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
+
+newDict :: Class -> [TcType] -> TcM DictId
+newDict cls tys 
+  = do { name <- newName (mkDictOcc (getOccName cls))
+       ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+
+newName :: OccName -> TcM Name
+newName occ
+  = do { uniq <- newUnique
+       ; loc  <- getSrcSpanM
+       ; return (mkInternalName uniq occ loc) }
+
+-----------------
+newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
+-- Create a new wanted CoVar that constrains the type
+-- to have the specified kind
+newKindConstraint ty kind
+  = do { ty_k <- newFlexiTyVarTy kind
+       ; co_var <- newWantedCoVar ty ty_k
+       ; return (co_var, ty_k) }
+
+-----------------
+newSelfDict :: Class -> [TcType] -> TcM DictId
+-- Make a dictionary for "self". It behaves just like a normal DictId
+-- except that it responds True to isSelfDict
+-- This is used only to suppress confusing error reports
+newSelfDict cls tys 
+  = do { uniq <- newUnique
+       ; let name = mkSystemName uniq selfDictOcc
+       ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+
+selfDictOcc :: OccName
+selfDictOcc = mkVarOcc "self"
+
+isSelfDict :: EvVar -> Bool
+isSelfDict v = isSystemName (Var.varName v)
+  -- Notice that all *other* evidence variables get Internal Names
 \end{code}
 
 
 \end{code}
 
 
@@ -147,13 +209,35 @@ newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
+tcInstType :: ([TyVar] -> TcM [TcTyVar])               -- How to instantiate the type variables
+          -> TcType                                    -- Type to instantiate
+          -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
+               -- (type vars (excl coercion vars), preds (incl equalities), rho)
+tcInstType inst_tyvars ty
+  = case tcSplitForAllTys ty of
+       ([],     rho) -> let    -- There may be overloading despite no type variables;
+                               --      (?x :: Int) => Int -> Int
+                          (theta, tau) = tcSplitPhiTy rho
+                        in
+                        return ([], 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) }
+
 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 
 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
 mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
 mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
 
 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.
+-- be in the type environment: it is lexically scoped.
 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 
 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
 
 tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
@@ -161,30 +245,48 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcLoc -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
 -- Instantiate the tyvar, using 
 --     * the occ-name and kind of the supplied tyvar, 
 --     * the unique from the monad,
 -- Instantiate the tyvar, using 
 --     * the occ-name and kind of the supplied tyvar, 
 --     * the unique from the monad,
---     * the location either from the tyvar (mb_loc = Nothing)
---       or from mb_loc (Just loc)
-tcInstSkolTyVar info mb_loc tyvar
+--     * the location either from the tyvar (skol_info = SigSkol)
+--                    or from the monad (otehrwise)
+tcInstSkolTyVar skol_info tyvar
   = do { uniq <- newUnique
   = do { uniq <- newUnique
-       ; let old_name = tyVarName tyvar
-             kind     = tyVarKind tyvar
-             loc      = mb_loc `orElse` getSrcLoc old_name
-             new_name = mkInternalName uniq (nameOccName old_name) loc
-       ; return (mkSkolTyVar new_name kind info) }
+       ; loc <- case skol_info of
+                    SigSkol {} -> return (getSrcSpan old_name)
+                    _          -> getSrcSpanM
+       ; let new_name = mkInternalName uniq occ loc
+       ; return (mkSkolTyVar new_name kind skol_info) }
+  where
+    old_name = tyVarName tyvar
+    occ      = nameOccName old_name
+    kind     = tyVarKind tyvar
 
 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 -- Get the location from the monad
 tcInstSkolTyVars info tyvars 
 
 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 -- Get the location from the monad
 tcInstSkolTyVars info tyvars 
-  = do         { span <- getSrcSpanM
-       ; mapM (tcInstSkolTyVar info (Just (srcSpanStart span))) tyvars }
+  = mapM (tcInstSkolTyVar info) tyvars
 
 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 
 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigType use_skols name ty
+  | use_skols
+  = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
+  | otherwise
+  = tcInstType tcInstSigTyVars ty
+
+tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
+-- Make meta SigTv type variables for patten-bound scoped type varaibles
+-- We use SigTvs for them, so that they can't unify with arbitrary types
+tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
+               -- ToDo: the "function binding site is bogus
 \end{code}
 
 
 \end{code}
 
 
@@ -195,54 +297,105 @@ tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
+newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
 -- Make a new meta tyvar out of thin air
 -- Make a new meta tyvar out of thin air
-newMetaTyVar box_info kind
-  = do { uniq <- newUnique
-       ; ref <- newMutVar Flexi ;
+newMetaTyVar meta_info kind
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
        ; let name = mkSysTvName uniq fs 
        ; let name = mkSysTvName uniq fs 
-             fs = case box_info of
-                       BoxTv   -> FSLIT("t")
-                       TauTv   -> FSLIT("t")
-                       SigTv _ -> FSLIT("a")
-               -- We give BoxTv and TauTv the same string, because
-               -- otherwise we get user-visible differences in error
-               -- messages, which are confusing.  If you want to see
-               -- the box_info of each tyvar, use -dppr-debug
-       ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
-
-instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
+             fs = case meta_info of
+                       TauTv   -> fsLit "t"
+                       SigTv _ -> fsLit "a"
+       ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
+
+instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
 -- Make a new meta tyvar whose Name and Kind 
 -- come from an existing TyVar
 -- Make a new meta tyvar whose Name and Kind 
 -- come from an existing TyVar
-instMetaTyVar box_info tyvar
-  = do { uniq <- newUnique
-       ; ref <- newMutVar Flexi ;
+instMetaTyVar meta_info tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
        ; let name = setNameUnique (tyVarName tyvar) uniq
              kind = tyVarKind tyvar
        ; let name = setNameUnique (tyVarName tyvar) uniq
              kind = tyVarKind tyvar
-       ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
+       ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
                      readMutVar (metaTvRef tyvar)
 
 
 readMetaTyVar :: TyVar -> TcM MetaDetails
 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
                      readMutVar (metaTvRef tyvar)
 
+readWantedCoVar :: CoVar -> TcM MetaDetails
+readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
+                       readMutVar (metaTvRef covar)
+
+
+
+isFilledMetaTyVar :: TyVar -> TcM Bool
+-- True of a filled-in (Indirect) meta type variable
+isFilledMetaTyVar tv
+  | not (isTcTyVar tv) = return False
+  | MetaTv _ ref <- tcTyVarDetails tv
+  = do         { details <- readMutVar ref
+       ; return (isIndirect details) }
+  | otherwise = return False
+
+isFlexiMetaTyVar :: TyVar -> TcM Bool
+-- True of a un-filled-in (Flexi) meta type variable
+isFlexiMetaTyVar tv
+  | not (isTcTyVar tv) = return False
+  | MetaTv _ ref <- tcTyVarDetails tv
+  = do         { details <- readMutVar ref
+       ; return (isFlexi details) }
+  | otherwise = return False
+
+--------------------
 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
-#ifndef DEBUG
-writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
-#else
+-- Write into a currently-empty MetaTyVar
+
 writeMetaTyVar tyvar ty
 writeMetaTyVar tyvar ty
-  | not (isMetaTyVar tyvar)
-  = pprTrace "writeMetaTyVar" (ppr tyvar) $
-    returnM ()
+  | not debugIsOn 
+  = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
+
+-- Everything from here on only happens if DEBUG is on
+  | not (isTcTyVar tyvar)
+  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
+    return ()
+
+  | MetaTv _ ref <- tcTyVarDetails tyvar
+  = writeMetaTyVarRef tyvar ref ty
 
   | otherwise
 
   | otherwise
-  = ASSERT( isMetaTyVar tyvar )
-    ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
-    do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
-       ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
+  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
+    return ()
+
+writeWantedCoVar :: CoVar -> Coercion -> TcM () 
+writeWantedCoVar cv co = writeMetaTyVar cv co 
+
+--------------------
+writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
+-- Here the tyvar is for error checking only; 
+-- the ref cell must be for the same tyvar
+writeMetaTyVarRef tyvar ref ty
+  | not debugIsOn 
+  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
+       ; writeMutVar ref (Indirect ty) }
+
+-- Everything from here on only happens if DEBUG is on
+  | not (isPredTy tv_kind)   -- Don't check kinds for updates to coercion variables
+  , not (ty_kind `isSubKind` tv_kind)
+  = WARN( True, hang (text "Ill-kinded update to meta tyvar")
+                   2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
+    return ()
+
+  | otherwise
+  = do { meta_details <- readMutVar ref; 
+       ; WARN( not (isFlexi meta_details), 
+                hang (text "Double update of meta tyvar")
+                   2 (ppr tyvar $$ ppr meta_details) )
+
+         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
+       ; writeMutVar ref (Indirect ty) }
   where
   where
-    k1 = tyVarKind tyvar
-    k2 = typeKind ty
-#endif
+    tv_kind = tyVarKind tyvar
+    ty_kind = typeKind ty
 \end{code}
 
 
 \end{code}
 
 
@@ -257,12 +410,12 @@ newFlexiTyVar :: Kind -> TcM TcTyVar
 newFlexiTyVar kind = newMetaTyVar TauTv kind
 
 newFlexiTyVarTy  :: Kind -> TcM TcType
 newFlexiTyVar kind = newMetaTyVar TauTv kind
 
 newFlexiTyVarTy  :: Kind -> TcM TcType
-newFlexiTyVarTy kind
-  = newFlexiTyVar kind `thenM` \ tc_tyvar ->
-    returnM (TyVarTy tc_tyvar)
+newFlexiTyVarTy kind = do
+    tc_tyvar <- newFlexiTyVar kind
+    return (TyVarTy tc_tyvar)
 
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
 
 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
-newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
+newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 
 tcInstTyVar :: TyVar -> TcM TcTyVar
 -- Instantiate with a META type variable
 
 tcInstTyVar :: TyVar -> TcM TcTyVar
 -- Instantiate with a META type variable
@@ -273,7 +426,7 @@ tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 tcInstTyVars tyvars
   = do { tc_tvs <- mapM tcInstTyVar tyvars
        ; let tys = mkTyVarTys tc_tvs
 tcInstTyVars tyvars
   = do { tc_tvs <- mapM tcInstTyVar tyvars
        ; let tys = mkTyVarTys tc_tvs
-       ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
+       ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
@@ -287,16 +440,6 @@ tcInstTyVars tyvars
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigTyVars use_skols skol_info tyvars 
-  | use_skols
-  = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
-
-  | otherwise
-  = mapM (instMetaTyVar (SigTv skol_info)) tyvars
-
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 zonkSigTyVar sig_tv 
   | isSkolemTyVar sig_tv 
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 zonkSigTyVar sig_tv 
   | isSkolemTyVar sig_tv 
@@ -310,207 +453,140 @@ zonkSigTyVar sig_tv
 \end{code}
 
 
 \end{code}
 
 
-%************************************************************************
-%*                                                                     *
-       MetaTvs: BoxTvs
-%*                                                                     *
-%************************************************************************
-
-\begin{code}
-newBoxyTyVar :: Kind -> TcM BoxyTyVar
-newBoxyTyVar kind = newMetaTyVar BoxTv kind
-
-newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
-newBoxyTyVars kinds = mapM newBoxyTyVar kinds
-
-newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
-newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
-
-readFilledBox :: BoxyTyVar -> TcM TcType
--- Read the contents of the box, which should be filled in by now
-readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
-                      do { cts <- readMetaTyVar box_tv
-                         ; case cts of
-                               Flexi       -> pprPanic "readFilledBox" (ppr box_tv)
-                               Indirect ty -> return ty }
-
-tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
--- Instantiate with a BOXY type variable
-tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
-\end{code}
-
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
-\subsection{Putting and getting  mutable type variables}
+\subsection{Zonking -- the exernal interfaces}
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-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.
-
-We return Nothing iff the original box was unbound.
+@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
+To improve subsequent calls to the same function it writes the zonked set back into
+the environment.
 
 \begin{code}
 
 \begin{code}
-data LookupTyVarResult -- The result of a lookupTcTyVar call
-  = DoneTv TcTyVarDetails      -- SkolemTv or virgin MetaTv
-  | IndirectTv TcType
-
-lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
-lookupTcTyVar tyvar 
-  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
-    case details of
-      SkolemTv _   -> return (DoneTv details)
-      MetaTv _ ref -> do { meta_details <- readMutVar ref
-                        ; case meta_details of
-                           Indirect ty -> return (IndirectTv ty)
-                           Flexi       -> return (DoneTv details) }
-  where
-    details =  tcTyVarDetails tyvar
-
-{- 
--- gaw 2004 We aren't shorting anything out anymore, at least for now
-getTcTyVar tyvar
-  | not (isTcTyVar tyvar)
-  = pprTrace "getTcTyVar" (ppr tyvar) $
-    returnM (Just (mkTyVarTy tyvar))
-
-  | otherwise
-  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
-    readMetaTyVar tyvar                                `thenM` \ maybe_ty ->
-    case maybe_ty of
-       Just ty -> short_out ty                         `thenM` \ ty' ->
-                  writeMetaTyVar tyvar (Just ty')      `thenM_`
-                  returnM (Just ty')
-
-       Nothing    -> returnM Nothing
-
-short_out :: TcType -> TcM TcType
-short_out ty@(TyVarTy tyvar)
-  | not (isTcTyVar tyvar)
-  = returnM ty
-
-  | otherwise
-  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->
-    case maybe_ty of
-       Just ty' -> short_out ty'                       `thenM` \ ty' ->
-                   writeMetaTyVar tyvar (Just ty')     `thenM_`
-                   returnM ty'
-
-       other    -> returnM ty
-
-short_out other_ty = returnM other_ty
--}
+tcGetGlobalTyVars :: TcM TcTyVarSet
+tcGetGlobalTyVars
+  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
+       ; gbl_tvs  <- readMutVar gtv_var
+       ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
+       ; writeMutVar gtv_var gbl_tvs'
+       ; return gbl_tvs' }
 \end{code}
 
 \end{code}
 
-
-%************************************************************************
-%*                                                                     *
-\subsection{Zonking -- the exernal interfaces}
-%*                                                                     *
-%************************************************************************
-
 -----------------  Type variables
 
 \begin{code}
 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
 -----------------  Type variables
 
 \begin{code}
 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
-zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
-
-zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars    `thenM` \ tys ->
-                          returnM (tyVarsOfTypes tys)
+zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
 
 
-zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
-                   zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
-\end{code}
+zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
 
 -----------------  Types
 
 
 -----------------  Types
 
-\begin{code}
+zonkTcTypeCarefully :: TcType -> TcM TcType
+-- Do not zonk type variables free in the environment
+zonkTcTypeCarefully ty
+  = do { env_tvs <- tcGetGlobalTyVars
+       ; zonkType (zonk_tv env_tvs) ty }
+  where
+    zonk_tv env_tvs tv
+      | tv `elemVarSet` env_tvs 
+      = return (TyVarTy tv)
+      | otherwise
+      = ASSERT( isTcTyVar tv )
+       case tcTyVarDetails tv of
+         SkolemTv {}    -> return (TyVarTy tv)
+         FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> return (TyVarTy tv)
+                                  Indirect ty -> zonkType (zonk_tv env_tvs) ty }
+
 zonkTcType :: TcType -> TcM TcType
 zonkTcType :: TcType -> TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
+-- Simply look through all Flexis
+zonkTcType ty = zonkType zonkTcTyVar ty
 
 
-zonkTcTypes :: [TcType] -> TcM [TcType]
-zonkTcTypes tys = mappM zonkTcType tys
+zonkTcTyVar :: TcTyVar -> TcM TcType
+-- Simply look through all Flexis
+zonkTcTyVar tv
+  = ASSERT2( isTcTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
+      SkolemTv {}    -> return (TyVarTy tv)
+      FlatSkol ty  -> zonkTcType ty
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> return (TyVarTy tv)
+                              Indirect ty -> zonkTcType ty }
+
+zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
+-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
+zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
+  where
+    zonk_tv tv 
+      = case tcTyVarDetails tv of
+         SkolemTv {}    -> return (TyVarTy tv)
+         FlatSkol ty    -> zonkType zonk_tv ty
+         MetaTv _ ref   -> do { cts <- readMutVar ref
+                              ; case cts of    
+                                  Flexi       -> zonk_flexi tv
+                                  Indirect ty -> zonkType zonk_tv ty }
+    zonk_flexi tv
+      = case lookupTyVar subst tv of
+          Just ty -> zonkType zonk_tv ty
+          Nothing -> return (TyVarTy tv)
 
 
-zonkTcClassConstraints cts = mappM zonk cts
-    where zonk (clas, tys)
-           = zonkTcTypes tys   `thenM` \ new_tys ->
-             returnM (clas, new_tys)
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mapM zonkTcType tys
 
 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 
 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
-zonkTcThetaType theta = mappM zonkTcPredType theta
+zonkTcThetaType theta = mapM zonkTcPredType theta
 
 zonkTcPredType :: TcPredType -> TcM TcPredType
 
 zonkTcPredType :: TcPredType -> TcM TcPredType
-zonkTcPredType (ClassP c ts)
-  = zonkTcTypes ts     `thenM` \ new_ts ->
-    returnM (ClassP c new_ts)
-zonkTcPredType (IParam n t)
-  = zonkTcType t       `thenM` \ new_t ->
-    returnM (IParam n new_t)
-zonkTcPredType (EqPred t1 t2)
-  = zonkTcType t1      `thenM` \ new_t1 ->
-    zonkTcType t2      `thenM` \ new_t2 ->
-    returnM (EqPred new_t1 new_t2)
+zonkTcPredType (ClassP c ts)  = ClassP c <$> zonkTcTypes ts
+zonkTcPredType (IParam n t)   = IParam n <$> zonkTcType t
+zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
 \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}
-zonkTopTyVar :: TcTyVar -> TcM TcTyVar
--- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
--- to default the kind of ? and ?? etc to *.  This is important to ensure that
--- instance declarations match.  For example consider
---     instance Show (a->b)
---     foo x = show (\_ -> True)
--- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
--- and that won't match the typeKind (*) in the instance decl.
---
--- Because we are at top level, no further constraints are going to affect these
--- type variables, so it's time to do it by hand.  However we aren't ready
--- to default them fully to () or whatever, because the type-class defaulting
--- rules have yet to run.
-
-zonkTopTyVar tv
-  | k `eqKind` default_k = return tv
-  | otherwise
-  = do { tv' <- newFlexiTyVar default_k
-       ; writeMetaTyVar tv (mkTyVarTy tv') 
-       ; return tv' }
-  where
-    k = tyVarKind tv
-    default_k = defaultKind k
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
+zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
 
 
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
-zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
-
-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 --
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 --                     -- see notes with Kind.defaultKind
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 --
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
 --                     -- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+-- The meta tyvar is updated to point to the new skolem 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
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | ASSERT( isTcTyVar tv ) 
-    isSkolemTyVar tv = return tv
+  | ASSERT2( isTcTyVar tv, ppr tv ) 
+    isSkolemTyVar tv 
+  = do { kind <- zonkTcType (tyVarKind tv)
+       ; return $ setTyVarKind tv kind
+       }
        -- 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
 
        -- 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
+       -- Create the new, frozen, skolem type variable
+        -- We zonk to a skolem, not to a regular TcVar
+        -- See Note [Zonking to Skolem]
+        ; uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
        ; let final_kind = defaultKind (tyVarKind tv)
        ; let final_kind = defaultKind (tyVarKind tv)
-             final_tv   = mkTyVar (tyVarName tv) final_kind
+              final_name = setNameUnique (tyVarName tv) uniq
+             final_tv   = mkSkolTyVar final_name final_kind UnkSkol
 
        -- Bind the meta tyvar to the new tyvar
        ; case details of
 
        -- Bind the meta tyvar to the new tyvar
        ; case details of
@@ -525,8 +601,29 @@ zonkQuantifiedTyVar tv
        ; return final_tv }
 \end{code}
 
        ; return final_tv }
 \end{code}
 
-[Silly Type Synonyms]
+\begin{code}
+zonkImplication :: Implication -> TcM Implication
+zonkImplication implic@(Implic { ic_given = given 
+                               , ic_wanted = wanted })
+  = do { given'   <- mapM zonkEvVar given
+       ; wanted'  <- mapBagM zonkWanted wanted
+       ; return (implic { ic_given = given', ic_wanted = wanted' }) }
+
+zonkEvVar :: EvVar -> TcM EvVar
+zonkEvVar var = do { ty' <- zonkTcType (varType var)
+                   ; return (setVarType var ty') }
+
+zonkWanted :: WantedConstraint -> TcM WantedConstraint
+zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
+zonkWanted (WcEvVar ev)   = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
+
+zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
+zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
+\end{code}
+
 
 
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
        type C u a = u  -- Note 'a' unused
 
 Consider this:
        type C u a = u  -- Note 'a' unused
 
@@ -546,7 +643,7 @@ Consider this:
 * Now abstract over the 'a', but float out the Num (C d a) constraint
   because it does not 'really' mention a.  (see exactTyVarsOfType)
   The arg to foo becomes
 * Now abstract over the 'a', but float out the Num (C d a) constraint
   because it does not 'really' mention a.  (see exactTyVarsOfType)
   The arg to foo becomes
-       /\a -> \t -> t+t
+       \/\a -> \t -> t+t
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()
@@ -555,10 +652,41 @@ Consider this:
   quantification, so the floated dict will still have type (C d a).
   Which renders this whole note moot; happily!]
 
   quantification, so the floated dict will still have type (C d a).
   Which renders this whole note moot; happily!]
 
-* Then the /\a abstraction has a zonked 'a' in it.
+* Then the \/\a abstraction has a zonked 'a' in it.
 
 All very silly.   I think its harmless to ignore the problem.  We'll end up with
 
 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 ()
+a \/\a in the final result but all the occurrences of a will be zonked to ()
+
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars.  However, this
+leads to problems.  Consider this program from the regression test suite:
+
+  eval :: Int -> String -> String -> String
+  eval 0 root actual = evalRHS 0 root actual
+
+  evalRHS :: Int -> a
+  evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality (wrapped in an implication constraint)
+
+  forall a. (String -> String -> String) ~ a
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem.  The skolem is rigid
+(which we require for a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -578,56 +706,66 @@ zonkType :: (TcTyVar -> TcM Type)         -- What to do with unbound mutable type varia
                                        -- see zonkTcType, and zonkTcTypeToType
          -> TcType
         -> TcM Type
                                        -- see zonkTcType, and zonkTcTypeToType
          -> TcType
         -> TcM Type
-zonkType unbound_var_fn ty
+zonkType zonk_tc_tyvar ty
   = go ty
   where
   = go ty
   where
-    go (NoteTy _ ty2)   = go ty2       -- Discard free-tyvar annotations
-                        
-    go (TyConApp tc tys) = mappM go tys        `thenM` \ tys' ->
-                          returnM (TyConApp tc tys')
-                           
-    go (PredTy p)       = go_pred p            `thenM` \ p' ->
-                          returnM (PredTy p')
-                        
-    go (FunTy arg res)   = go arg              `thenM` \ arg' ->
-                          go res               `thenM` \ res' ->
-                          returnM (FunTy arg' res')
-                        
-    go (AppTy fun arg)  = go fun               `thenM` \ fun' ->
-                          go arg               `thenM` \ arg' ->
-                          returnM (mkAppTy fun' arg')
+    go (TyConApp tc tys) = do tys' <- mapM go tys
+                              return (TyConApp tc tys')
+
+    go (PredTy p)        = do p' <- go_pred p
+                              return (PredTy p')
+
+    go (FunTy arg res)   = do arg' <- go arg
+                              res' <- go res
+                              return (FunTy arg' res')
+
+    go (AppTy fun arg)   = do fun' <- go fun
+                              arg' <- go arg
+                              return (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) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
-                      | otherwise       = return (TyVarTy tyvar)
+    go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
+                      | otherwise       = liftM TyVarTy $ 
+                                           zonkTyVar zonk_tc_tyvar tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
 
                -- Ordinary (non Tc) tyvars occur inside quantified types
 
-    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
-                            go ty              `thenM` \ ty' ->
-                            returnM (ForAllTy tyvar ty')
+    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
+                             ty' <- go ty
+                             tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+                             return (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')
-    go_pred (EqPred ty1 ty2) = go ty1          `thenM` \ ty1' ->
-                              go ty2           `thenM` \ ty2' ->
-                              returnM (EqPred ty1' ty2')
+    go_pred (ClassP c tys)   = do tys' <- mapM go tys
+                                  return (ClassP c tys')
+    go_pred (IParam n ty)    = do ty' <- go ty
+                                  return (IParam n ty')
+    go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
+                                  ty2' <- go ty2
+                                  return (EqPred ty1' ty2')
 
 
-zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
              -> TcTyVar -> TcM TcType
              -> TcTyVar -> TcM TcType
-zonk_tc_tyvar unbound_var_fn tyvar 
-  | not (isMetaTyVar tyvar)    -- Skolems
-  = returnM (TyVarTy tyvar)
-
-  | otherwise                  -- Mutables
-  = do { cts <- readMetaTyVar tyvar
-       ; case cts of
-           Flexi       -> unbound_var_fn tyvar    -- Unbound meta type variable
-           Indirect ty -> zonkType unbound_var_fn ty  }
+mkZonkTcTyVar unbound_var_fn tyvar 
+  = ASSERT( isTcTyVar tyvar )
+    case tcTyVarDetails tyvar of
+      SkolemTv {}    -> return (TyVarTy tyvar)
+      FlatSkol ty    -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
+      MetaTv _ ref   -> do { cts <- readMutVar ref
+                          ; case cts of    
+                              Flexi       -> unbound_var_fn tyvar  
+                              Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable 
+-- (their kind contains types).
+zonkTyVar :: (TcTyVar -> TcM Type)      -- What to do for a TcTyVar
+         -> TyVar -> TcM TyVar
+zonkTyVar zonk_tc_tyvar tv 
+  | isCoVar tv
+  = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
+       ; return $ setTyVarKind tv kind }
+  | otherwise = return tv
 \end{code}
 
 
 \end{code}
 
 
@@ -652,7 +790,8 @@ zonkTcKind k = zonkTcType k
 zonkTcKindToKind :: TcKind -> TcM Kind
 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
 -- Haskell specifies that * is to be used, so we follow that.
 zonkTcKindToKind :: TcKind -> TcM Kind
 -- When zonking a TcKind to a kind, we need to instantiate kind variables,
 -- Haskell specifies that * is to be used, so we follow that.
-zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
+zonkTcKindToKind k 
+  = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
 \end{code}
                        
 %************************************************************************
 \end{code}
                        
 %************************************************************************
@@ -692,84 +831,181 @@ This might not necessarily show up in kind checking.
 \begin{code}
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 \begin{code}
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
-checkValidType ctxt ty
-  = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
-    doptM Opt_GlasgowExts      `thenM` \ gla_exts ->
+checkValidType ctxt ty = do
+    traceTc "checkValidType" (ppr ty)
+    unboxed  <- xoptM Opt_UnboxedTuples
+    rank2    <- xoptM Opt_Rank2Types
+    rankn    <- xoptM Opt_RankNTypes
+    polycomp <- xoptM Opt_PolymorphicComponents
     let 
     let 
-       rank | gla_exts = Arbitrary
-            | otherwise
-            = case ctxt of     -- Haskell 98
-                GenPatCtxt     -> Rank 0
-                LamPatSigCtxt  -> Rank 0
-                BindPatSigCtxt -> Rank 0
-                DefaultDeclCtxt-> Rank 0
-                ResSigCtxt     -> Rank 0
-                TySynCtxt _    -> Rank 0
-                ExprSigCtxt    -> Rank 1
-                FunSigCtxt _   -> Rank 1
-                ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
-                                               -- constructor, hence rank 1
-                ForSigCtxt _   -> Rank 1
-                SpecInstCtxt   -> Rank 1
+       gen_rank n | rankn     = ArbitraryRank
+                  | rank2     = Rank 2
+                  | otherwise = Rank n
+       rank
+         = case ctxt of
+                DefaultDeclCtxt-> MustBeMonoType
+                ResSigCtxt     -> MustBeMonoType
+                LamPatSigCtxt  -> gen_rank 0
+                BindPatSigCtxt -> gen_rank 0
+                TySynCtxt _    -> gen_rank 0
+                GenPatCtxt     -> gen_rank 1
+                       -- This one is a bit of a hack
+                       -- See the forall-wrapping in TcClassDcl.mkGenericInstance              
+
+                ExprSigCtxt    -> gen_rank 1
+                FunSigCtxt _   -> gen_rank 1
+                ConArgCtxt _   | polycomp -> gen_rank 2
+                                -- We are given the type of the entire
+                                -- constructor, hence rank 1
+                               | otherwise -> gen_rank 1
+
+                ForSigCtxt _   -> gen_rank 1
+                SpecInstCtxt   -> gen_rank 1
+                ThBrackCtxt    -> gen_rank 1
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
-                       TySynCtxt _  -> True    -- Any kind will do
-                       ResSigCtxt   -> isSubOpenTypeKind        actual_kind
-                       ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
+                       TySynCtxt _  -> True -- Any kind will do
+                       ThBrackCtxt  -> True -- Any kind will do
+                       ResSigCtxt   -> isSubOpenTypeKind actual_kind
+                       ExprSigCtxt  -> isSubOpenTypeKind actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       other        -> isSubArgTypeKind    actual_kind
+                       _            -> isSubArgTypeKind 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
-       -- Check that the thing has kind Type, and is lifted if necessary
-    checkTc kind_ok (kindErr actual_kind)      `thenM_`
+       ubx_tup = case ctxt of
+                     TySynCtxt _ | unboxed -> UT_Ok
+                     ExprSigCtxt | unboxed -> UT_Ok
+                     ThBrackCtxt | unboxed -> UT_Ok
+                     _                     -> UT_NotOk
 
        -- Check the internal validity of the type itself
 
        -- Check the internal validity of the type itself
-    check_poly_type rank ubx_tup ty            `thenM_`
+    check_type rank ubx_tup ty
 
 
-    traceTc (text "checkValidType done" <+> ppr ty)
+       -- Check that the thing has kind Type, and is lifted if necessary
+       -- Do this second, becuase we can't usefully take the kind of an 
+       -- ill-formed type such as (a~Int)
+    checkTc kind_ok (kindErr actual_kind)
+
+    traceTc "checkValidType done" (ppr ty)
+
+checkValidMonoType :: Type -> TcM ()
+checkValidMonoType ty = check_mono_type MustBeMonoType ty
 \end{code}
 
 
 \begin{code}
 \end{code}
 
 
 \begin{code}
-data Rank = Rank Int | Arbitrary
-
-decRank :: Rank -> Rank
-decRank Arbitrary = Arbitrary
-decRank (Rank n)  = Rank (n-1)
+data Rank = ArbitraryRank        -- Any rank ok
+          | MustBeMonoType       -- Monotype regardless of flags
+         | TyConArgMonoType      -- Monotype but could be poly if -XImpredicativeTypes
+         | SynArgMonoType        -- Monotype but could be poly if -XLiberalTypeSynonyms
+          | Rank Int             -- Rank n, but could be more with -XRankNTypes
+
+decRank :: Rank -> Rank                  -- Function arguments
+decRank (Rank 0)   = Rank 0
+decRank (Rank n)   = Rank (n-1)
+decRank other_rank = other_rank
+
+nonZeroRank :: Rank -> Bool
+nonZeroRank ArbitraryRank = True
+nonZeroRank (Rank n)     = n>0
+nonZeroRank _            = False
 
 ----------------------------------------
 data UbxTupFlag = UT_Ok        | UT_NotOk
 
 ----------------------------------------
 data UbxTupFlag = UT_Ok        | UT_NotOk
-       -- The "Ok" version means "ok if -fglasgow-exts is on"
+       -- The "Ok" version means "ok if UnboxedTuples 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 ubx_tup ty 
-  | null tvs && null theta
-  = check_tau_type rank ubx_tup ty
-  | otherwise
-  = do { check_valid_theta SigmaCtxt theta
-       ; check_poly_type rank ubx_tup tau      -- Allow foralls to right of arrow
-       ; checkFreeness tvs theta
+check_mono_type :: Rank -> Type -> TcM ()      -- No foralls anywhere
+                                               -- No unlifted types of any kind
+check_mono_type rank ty
+   = do { check_type rank UT_NotOk ty
+       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+
+check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+-- The args say what the *type context* requires, independent
+-- of *flag* settings.  You test the flag settings at usage sites.
+-- 
+-- Rank is allowed rank for function args
+-- Rank 0 means no for-alls anywhere
+
+check_type rank ubx_tup ty
+  | not (null tvs && null theta)
+  = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
+               -- Reject e.g. (Maybe (?x::Int => Int)), 
+               -- with a decent error message
+       ; check_valid_theta SigmaCtxt theta
+       ; check_type rank ubx_tup tau   -- Allow foralls to right of arrow
        ; checkAmbiguity tvs theta (tyVarsOfType tau) }
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
    
        ; checkAmbiguity tvs theta (tyVarsOfType tau) }
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
    
+-- Naked PredTys should, I think, have been rejected before now
+check_type _ _ ty@(PredTy {})
+  = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type") 
+
+check_type _ _ (TyVarTy _) = return ()
+
+check_type rank _ (FunTy arg_ty res_ty)
+  = do { check_type (decRank rank) UT_NotOk arg_ty
+       ; check_type rank           UT_Ok    res_ty }
+
+check_type rank _ (AppTy ty1 ty2)
+  = do { check_arg_type rank ty1
+       ; check_arg_type rank ty2 }
+
+check_type rank ubx_tup ty@(TyConApp tc tys)
+  | isSynTyCon tc
+  = do {       -- Check that the synonym has enough args
+               -- This applies equally to open and closed synonyms
+               -- It's OK to have an *over-applied* type synonym
+               --      data Tree a b = ...
+               --      type Foo a = Tree [a]
+               --      f :: Foo a b -> ...
+         checkTc (tyConArity tc <= length tys) arity_msg
+
+       -- See Note [Liberal type synonyms]
+       ; liberal <- xoptM Opt_LiberalTypeSynonyms
+       ; if not liberal || isSynFamilyTyCon tc then
+               -- For H98 and synonym families, do check the type args
+               mapM_ (check_mono_type SynArgMonoType) tys
+
+         else  -- In the liberal case (only for closed syns), expand then check
+         case tcView ty of   
+            Just ty' -> check_type rank ubx_tup ty' 
+            Nothing  -> pprPanic "check_tau_type" (ppr ty)
+    }
+    
+  | isUnboxedTupleTyCon tc
+  = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
+       ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
+
+       ; impred <- xoptM Opt_ImpredicativeTypes        
+       ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
+               -- c.f. check_arg_type
+               -- However, args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty
+       ; mapM_ (check_type rank' UT_Ok) tys }
+
+  | otherwise
+  = mapM_ (check_arg_type rank) tys
+
+  where
+    ubx_tup_ok ub_tuples_allowed = case ubx_tup of
+                                   UT_Ok -> ub_tuples_allowed
+                                   _     -> False
+
+    n_args    = length tys
+    tc_arity  = tyConArity tc
+
+    arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
+    ubx_tup_msg = ubxArgTyErr ty
+
+check_type _ _ ty = pprPanic "check_type" (ppr ty)
+
 ----------------------------------------
 ----------------------------------------
-check_arg_type :: Type -> TcM ()
+check_arg_type :: Rank -> Type -> TcM ()
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
 -- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
@@ -788,91 +1024,67 @@ check_arg_type :: Type -> TcM ()
 --     But not in user code.
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 --     But not in user code.
 -- Anyway, they are dealt with by a special case in check_tau_type
 
-check_arg_type ty 
-  = check_poly_type Arbitrary UT_NotOk ty      `thenM_` 
-    checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
-
-----------------------------------------
-check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
--- Rank is allowed rank for function args
--- No foralls otherwise
-
-check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup 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_pred_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 (decRank rank) UT_NotOk arg_ty     `thenM_`
-    check_poly_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_arg_type rank ty 
+  = do { impred <- xoptM Opt_ImpredicativeTypes
+       ; let rank' = case rank of          -- Predictive => must be monotype
+                       MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
+                       _other | impred    -> ArbitraryRank
+                              | otherwise -> TyConArgMonoType
+                       -- Make sure that MustBeMonoType is propagated, 
+                       -- so that we don't suggest -XImpredicativeTypes in
+                       --    (Ord (forall a.a)) => a -> a
+                       -- and so that if it Must be a monotype, we check that it is!
 
 
-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      
-  = do {       -- It's OK to have an *over-applied* type synonym
-               --      data Tree a b = ...
-               --      type Foo a = Tree [a]
-               --      f :: Foo a b -> ...
-       ; case tcView ty of
-            Just ty' -> check_tau_type rank ubx_tup ty'        -- Check expansion
-            Nothing  -> failWithTc arity_msg
-
-       ; gla_exts <- doptM Opt_GlasgowExts
-       ; if gla_exts then
-       -- If -fglasgow-exts then don't check the type arguments
-       -- 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 type args
-               mappM_ check_arg_type tys
-       }
-    
-  | isUnboxedTupleTyCon tc
-  = 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
-  = mappM_ check_arg_type tys
+       ; check_type rank' UT_NotOk ty
+       ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
 
 
+----------------------------------------
+forAllTyErr :: Rank -> Type -> SDoc
+forAllTyErr rank ty 
+   = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
+          , suggestion ]
   where
   where
-    ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+    suggestion = case rank of
+                  Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
+                  TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+                  SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
+                  _ -> empty      -- Polytype is always illegal
+
+unliftedArgErr, ubxArgTyErr :: Type -> SDoc
+unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
+ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
+
+kindErr :: Kind -> SDoc
+kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
+\end{code}
 
 
-    n_args    = length tys
-    tc_arity  = tyConArity tc
+Note [Liberal type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
+doing validity checking.  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.
 
 
-    arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
-    ubx_tup_msg = ubxArgTyErr ty
+IMPORTANT: suppose T is a type synonym.  Then we must do validity
+checking on an appliation (T ty1 ty2)
 
 
-----------------------------------------
-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}
+       *either* before expansion (i.e. check ty1, ty2)
+       *or* after expansion (i.e. expand T ty1 ty2, and then check)
+       BUT NOT BOTH
+
+If we do both, we get exponential behaviour!!
 
 
+  data TIACons1 i r c = c i ::: r c
+  type TIACons2 t x = TIACons1 t (TIACons1 t x)
+  type TIACons3 t x = TIACons2 t (TIACons1 t x)
+  type TIACons4 t x = TIACons2 t (TIACons2 t x)
+  type TIACons7 t x = TIACons4 t (TIACons3 t x)
 
 
 %************************************************************************
 
 
 %************************************************************************
@@ -900,11 +1112,12 @@ data SourceTyCtxt
   | InstThetaCtxt      -- Context of an instance decl
                        --      instance <S> => C [a] where ...
                
   | InstThetaCtxt      -- Context of an instance decl
                        --      instance <S> => C [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 (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
-pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
-pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
+pprSourceTyCtxt :: SourceTyCtxt -> SDoc
+pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
+pprSourceTyCtxt SigmaCtxt       = ptext (sLit "the context of a polymorphic type")
+pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
+pprSourceTyCtxt InstThetaCtxt   = ptext (sLit "the context of an instance declaration")
+pprSourceTyCtxt TypeCtxt        = ptext (sLit "the context of a type")
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
@@ -913,22 +1126,24 @@ checkValidTheta ctxt theta
   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 
 -------------------------
   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 
 -------------------------
-check_valid_theta ctxt []
-  = returnM ()
-check_valid_theta ctxt theta
-  = getDOpts                                   `thenM` \ dflags ->
-    warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
-    mappM_ (check_pred_ty dflags ctxt) theta
+check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
+check_valid_theta _ []
+  = return ()
+check_valid_theta ctxt theta = do
+    dflags <- getDOpts
+    warnTc (notNull dups) (dupPredWarn dups)
+    mapM_ (check_pred_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
+check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
 check_pred_ty dflags ctxt pred@(ClassP cls tys)
   = do {       -- Class predicates are valid in all contexts
        ; checkTc (arity == n_tys) arity_err
 
                -- Check the form of the argument types
 check_pred_ty dflags ctxt pred@(ClassP cls tys)
   = do {       -- Class predicates are valid in all contexts
        ; checkTc (arity == n_tys) arity_err
 
                -- Check the form of the argument types
-       ; mappM_ check_arg_type tys
+       ; mapM_ checkValidMonoType tys
        ; checkTc (check_class_pred_tys dflags ctxt tys)
                 (predTyVarErr pred $$ how_to_allow)
        }
        ; checkTc (check_class_pred_tys dflags ctxt tys)
                 (predTyVarErr pred $$ how_to_allow)
        }
@@ -937,21 +1152,20 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
-    how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+    how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
 
 
-check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
-  = do {       -- Equational constraints are valid in all contexts if indexed
-               -- types are permitted
-       ; checkTc (dopt Opt_IndexedTypes dflags) (eqPredTyErr pred)
+
+check_pred_ty dflags _ pred@(EqPred ty1 ty2)
+  = do {       -- Equational constraints are valid in all contexts if type
+               -- families are permitted
+       ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
 
                -- Check the form of the argument types
 
                -- Check the form of the argument types
-       ; check_eq_arg_type ty1
-       ; check_eq_arg_type ty2
+       ; checkValidMonoType ty1
+       ; checkValidMonoType ty2
        }
        }
-  where 
-    check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
 
 
-check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
        -- Implicit parameters only allowed in type
        -- signatures; not in instance decls, superclasses etc
        -- The reason for not allowing implicit params in instances is a bit
        -- Implicit parameters only allowed in type
        -- signatures; not in instance decls, superclasses etc
        -- The reason for not allowing implicit params in instances is a bit
@@ -963,21 +1177,23 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
-check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
+check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
 
 -------------------------
 
 -------------------------
+check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
        TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
-       InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
+       InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
                                -- Further checks on head and theta in
                                -- checkInstTermination
                                -- Further checks on head and theta in
                                -- checkInstTermination
-       other         -> gla_exts || all tyvar_head tys
+       _             -> flexible_contexts || all tyvar_head tys
   where
   where
-    gla_exts       = dopt Opt_GlasgowExts dflags
-    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
+    flexible_contexts = xopt Opt_FlexibleContexts dflags
+    undecidable_ok = xopt Opt_UndecidableInstances dflags
 
 -------------------------
 
 -------------------------
+tyvar_head :: Type -> Bool
 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
@@ -1016,77 +1232,110 @@ 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).
 
 don't need to check for ambiguity either, because the test can't fail
 (see is_ambig).
 
+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}
 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 checkAmbiguity forall_tyvars theta tau_tyvars
 \begin{code}
 checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
 checkAmbiguity forall_tyvars theta tau_tyvars
-  = mappM_ complain (filter is_ambig theta)
+  = mapM_ complain (filter is_ambig theta)
   where
     complain pred     = addErrTc (ambigErr pred)
   where
     complain pred     = addErrTc (ambigErr pred)
-    extended_tau_vars = grow theta tau_tyvars
+    extended_tau_vars = growThetaTyVars 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'
+       -- See Note [Implicit parameters and ambiguity] in TcSimplify
     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)
 
     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 :: PredType -> SDoc
 ambigErr pred
 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 '=>'"))]
+  = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
+        nest 2 (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}
-    
-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.
+
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growInstsTyVars insts tvs) is the result of extending the set 
+    of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then grow precs tvs = {a,b,c}
 
 \begin{code}
 
 \begin{code}
-checkFreeness forall_tyvars theta
-  = do { gla_exts <- doptM Opt_GlasgowExts
-       ; if gla_exts then return ()    -- New!  Oct06
-         else 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)"))
-    ]
+growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars theta tvs
+  | null theta = tvs
+  | otherwise  = fixVarSet mk_next tvs
+  where
+    mk_next tvs = foldr grow_one tvs theta
+    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
+
+growPredTyVars :: TcPredType
+               -> TyVarSet     -- The set to extend
+              -> TyVarSet      -- TyVars of the predicate if it intersects
+                               -- the set, or is implicit parameter
+growPredTyVars pred tvs 
+  | IParam {} <- pred               = pred_tvs -- See Note [Implicit parameters and ambiguity]
+  | pred_tvs `intersectsVarSet` tvs = pred_tvs
+  | otherwise                       = emptyVarSet
+  where
+    pred_tvs = tyVarsOfPred pred
 \end{code}
 \end{code}
+    
+Note [Implicit parameters and ambiguity] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others.  E.g.
+       foo :: (Show a, ?x::[a]) => Int
+       foo = show (?x++?x)
+The type of foo looks ambiguous.  But it isn't, because at a call site
+we might have
+       let ?x = 5::Int in foo
+and all is well.  In effect, implicit parameters are, well, parameters,
+so we can take their type variables into account as part of the
+"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
+
 
 \begin{code}
 
 \begin{code}
+checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
 checkThetaCtxt ctxt theta
 checkThetaCtxt ctxt theta
-  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
-         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+  = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
+         ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
 
 
-badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
+badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
+eqPredTyErr  sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
                   $$
                   $$
-                  parens (ptext SLIT("Use -findexed-types to permit this"))
-predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
-                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
-dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+                  parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
+                         nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+dupPredWarn :: [[PredType]] -> SDoc
+dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 
 
+arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
 arityErr kind name n m
 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]
+  = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
+          n_arguments <> comma, text "but has been given", 
+           if m==0 then text "none" else int m]
     where
     where
-       n_arguments | n == 0 = ptext SLIT("no arguments")
-                   | n == 1 = ptext SLIT("1 argument")
-                   | True   = hsep [int n, ptext SLIT("arguments")]
+       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}
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Checking for a decent instance head type}
 %************************************************************************
 %*                                                                     *
 \subsection{Checking for a decent instance head type}
@@ -1112,41 +1361,56 @@ checkValidInstHead ty   -- Should be a source type
 
     case getClassPredTys_maybe pred of {
        Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
 
     case getClassPredTys_maybe pred of {
        Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
-        Just (clas,tys) ->
+        Just (clas,tys) -> do
 
 
-    getDOpts                                   `thenM` \ dflags ->
-    mappM_ check_arg_type tys                  `thenM_`
-    check_inst_head dflags clas tys            `thenM_`
-    returnM (clas, tys)
+    dflags <- getDOpts
+    check_inst_head dflags clas tys
+    return (clas, tys)
     }}
 
     }}
 
+check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
 check_inst_head dflags clas tys
 check_inst_head dflags clas tys
-       -- If GlasgowExts then check at least one isn't a type variable
-  | dopt Opt_GlasgowExts dflags
-  = mapM_ check_one tys
-
-       -- WITH HASKELL 98, MUST HAVE C (T a b c)
-  | otherwise
-  = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
-           (instTypeErr (pprClassPred clas tys) head_shape_msg)
-
-  where
-    (first_ty : _) = tys
-
-    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")
-
+  = do { -- If GlasgowExts then check at least one isn't a type variable
+       ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
+                  all tcInstHeadTyNotSynonym tys)
+                 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+       ; checkTc (xopt Opt_FlexibleInstances dflags ||
+                  all tcInstHeadTyAppAllTyVars tys)
+                 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+       ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
+                  isSingleton tys)
+                 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+         -- May not contain type family applications
+       ; mapM_ checkTyFamFreeness tys
+
+       ; mapM_ checkValidMonoType tys
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
        --      E.g.  instance C (forall a. a->a) is rejected
        -- One could imagine generalising that, but I'm not sure
        -- what all the consequences might be
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
        --      E.g.  instance C (forall a. a->a) is rejected
        -- One could imagine generalising that, but I'm not sure
        -- what all the consequences might be
-    check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
-                     ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+       }
 
 
+  where
+    head_type_synonym_msg = parens (
+                text "All instance types must be of the form (T t1 ... tn)" $$
+                text "where T is not a synonym." $$
+                text "Use -XTypeSynonymInstances if you want to disable this.")
+
+    head_type_args_tyvars_msg = parens (vcat [
+                text "All instance types must be of the form (T a1 ... an)",
+                text "where a1 ... an are type *variables*,",
+                text "and each type variable appears at most once in the instance head.",
+                text "Use -XFlexibleInstances if you want to disable this."])
+
+    head_one_type_msg = parens (
+                text "Only one type can be given in an instance head." $$
+                text "Use -XMultiParamTypeClasses if you want to allow more.")
+
+instTypeErr :: SDoc -> SDoc -> SDoc
 instTypeErr pp_ty msg
 instTypeErr pp_ty msg
-  = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
-        nest 4 msg]
+  = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
+        nest 2 msg]
 \end{code}
 
 
 \end{code}
 
 
@@ -1156,31 +1420,46 @@ instTypeErr pp_ty msg
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-
 \begin{code}
 \begin{code}
-checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
-checkValidInstance tyvars theta clas inst_tys
-  = do { gla_exts <- doptM Opt_GlasgowExts
-       ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type 
+                   -> TcM (Class, [TcType])
+checkValidInstance hs_type tyvars theta tau
+  = setSrcSpan (getLoc hs_type) $
+    do { (clas, inst_tys) <- setSrcSpan head_loc $
+                              checkValidInstHead tau
+
+        ; undecidable_ok <- xoptM Opt_UndecidableInstances
 
        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
 
        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
-       -- For Haskell 98, checkValidTheta has already done that
-       ; when (gla_exts && not undecidable_ok) $
-         mapM_ failWithTc (checkInstTermination inst_tys theta)
+       -- For Haskell 98 this will already have been done by checkValidTheta,
+        -- but as we may be using other extensions we need to check.
+       ; unless undecidable_ok $
+         mapM_ addErrTc (checkInstTermination inst_tys theta)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
+
+        ; return (clas, inst_tys)
        }
   where
        }
   where
-    msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+    msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
                         undecidableMsg])
                         undecidableMsg])
+
+       -- The location of the "head" of the instance
+    head_loc = case hs_type of
+                 L _ (HsForAllTy _ _ _ (L loc _)) -> loc
+                 L loc _                          -> loc
 \end{code}
 
 \end{code}
 
-Termination test: each assertion in the context satisfies
+Termination test: the so-called "Paterson conditions" (see Section 5 of
+"Understanding functionsl dependencies via Constraint Handling Rules, 
+JFP Jan 2007).
+
+We check that each assertion in the context satisfies:
  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
  (1) no variable has more occurrences in the assertion than in the head, and
  (2) the assertion has fewer constructors and variables (taken together
      and counting repetitions) than the head.
@@ -1208,19 +1487,123 @@ checkInstTermination tys theta
       | otherwise
       = Nothing
 
       | otherwise
       = Nothing
 
+predUndecErr :: PredType -> SDoc -> SDoc
 predUndecErr pred msg = sep [msg,
 predUndecErr pred msg = sep [msg,
-                       nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+                       nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
 
 
-nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
-smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
+nomoreMsg, smallerMsg, undecidableMsg :: SDoc
+nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
+undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
+\end{code}
+
+validDeivPred checks for OK 'deriving' context.  See Note [Exotic
+derived instance contexts] in TcSimplify.  However the predicate is
+here because it uses sizeTypes, fvTypes.
+
+\begin{code}
+validDerivPred :: PredType -> Bool
+validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
+                              where fvs = fvTypes tys
+validDerivPred _              = False
+\end{code}
 
 
+
+%************************************************************************
+%*                                                                     *
+       Checking type instance well-formedness and termination
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+-- Check that a "type instance" is well-formed (which includes decidability
+-- unless -XUndecidableInstances is given).
+--
+checkValidTypeInst :: [Type] -> Type -> TcM ()
+checkValidTypeInst typats rhs
+  = do { -- left-hand side contains no type family applications
+         -- (vanilla synonyms are fine, though)
+       ; mapM_ checkTyFamFreeness typats
+
+         -- the right-hand side is a tau type
+       ; checkValidMonoType rhs
+
+         -- we have a decidable instance unless otherwise permitted
+       ; undecidable_ok <- xoptM Opt_UndecidableInstances
+       ; unless undecidable_ok $
+          mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
+       }
+
+-- Make sure that each type family instance is 
+--   (1) strictly smaller than the lhs,
+--   (2) mentions no type variable more often than the lhs, and
+--   (3) does not contain any further type family instances.
+--
+checkFamInst :: [Type]                  -- lhs
+             -> [(TyCon, [Type])]       -- type family instances
+             -> [Message]
+checkFamInst lhsTys famInsts
+  = mapCatMaybes check famInsts
+  where
+   size = sizeTypes lhsTys
+   fvs  = fvTypes lhsTys
+   check (tc, tys)
+      | not (all isTyFamFree tys)
+      = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
+      | not (null (fvTypes tys \\ fvs))
+      = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
+      | size <= sizeTypes tys
+      = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
+      | otherwise
+      = Nothing
+      where
+        famInst = TyConApp tc tys
+
+-- Ensure that no type family instances occur in a type.
+--
+checkTyFamFreeness :: Type -> TcM ()
+checkTyFamFreeness ty
+  = checkTc (isTyFamFree ty) $
+      tyFamInstIllegalErr ty
+
+-- Check that a type does not contain any type family applications.
+--
+isTyFamFree :: Type -> Bool
+isTyFamFree = null . tyFamInsts
+
+-- Error messages
+
+tyFamInstIllegalErr :: Type -> SDoc
+tyFamInstIllegalErr ty
+  = hang (ptext (sLit "Illegal type synonym family application in instance") <> 
+         colon) 2 $
+      ppr ty
+
+famInstUndecErr :: Type -> SDoc -> SDoc
+famInstUndecErr ty msg 
+  = sep [msg, 
+         nest 2 (ptext (sLit "in the type family application:") <+> 
+                 pprType ty)]
+
+nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
+nestedMsg     = ptext (sLit "Nested type family application")
+nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
+smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Auxiliary functions}
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
 -- Free variables of a type, retaining repetitions, and expanding synonyms
 fvType :: Type -> [TyVar]
 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
 fvType (TyVarTy tv)        = [tv]
 fvType (TyConApp _ tys)    = fvTypes tys
 -- Free variables of a type, retaining repetitions, and expanding synonyms
 fvType :: Type -> [TyVar]
 fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
 fvType (TyVarTy tv)        = [tv]
 fvType (TyConApp _ tys)    = fvTypes tys
-fvType (NoteTy _ ty)       = fvType ty
 fvType (PredTy pred)       = fvPred pred
 fvType (FunTy arg res)     = fvType arg ++ fvType res
 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
 fvType (PredTy pred)       = fvPred pred
 fvType (FunTy arg res)     = fvType arg ++ fvType res
 fvType (AppTy fun arg)     = fvType fun ++ fvType arg
@@ -1239,7 +1622,6 @@ sizeType :: Type -> Int
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy _)       = 1
 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
 sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
 sizeType (TyVarTy _)       = 1
 sizeType (TyConApp _ tys)  = sizeTypes tys + 1
-sizeType (NoteTy _ ty)     = sizeType ty
 sizeType (PredTy pred)     = sizePred pred
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
 sizeType (PredTy pred)     = sizePred pred
 sizeType (FunTy arg res)   = sizeType arg + sizeType res + 1
 sizeType (AppTy fun arg)   = sizeType fun + sizeType arg
@@ -1248,8 +1630,14 @@ sizeType (ForAllTy _ ty)   = sizeType ty
 sizeTypes :: [Type] -> Int
 sizeTypes xs               = sum (map sizeType xs)
 
 sizeTypes :: [Type] -> Int
 sizeTypes xs               = sum (map sizeType xs)
 
+-- Size of a predicate
+--
+-- We are considering whether *class* constraints terminate
+-- Once we get into an implicit parameter or equality we
+-- can't get back to a class constraint, so it's safe
+-- to say "size 0".  See Trac #4200.
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
-sizePred (IParam _ ty)     = sizeType ty
-sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
+sizePred (IParam {})       = 0
+sizePred (EqPred {})       = 0
 \end{code}
 \end{code}