Tidy up SigTv

[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 23c3381..1d163aa 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -1,9 +1,12 @@
 %
 %

+% (c) The University of Glasgow 2006

 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %

-\section{Monadic type operations}

 
 

-This module contains monadic operations over types that contain mutable type variables
+Monadic type operations
+
+This module contains monadic operations over types that contain
+mutable type variables

 
 \begin{code}
 module TcMType (
 
 \begin{code}
 module TcMType (

@@ -15,153 +18,171 @@ 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, 
+  mkTcTyVarName,

 
 

-  --------------------------------
-  -- 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,
+  writeWantedCoVar, readWantedCoVar, 
+  newIP, newDict, newSilentGiven, isSilentEvVar,
+
+  newWantedEvVar, newWantedEvVars,
+  newTcEvBinds, addTcEvBind,

 
   --------------------------------
   -- Instantiation
 
   --------------------------------
   -- Instantiation

-  tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
-  tcInstSigTyVars, zonkSigTyVar,
-  tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
-  tcSkolSigType, tcSkolSigTyVars,
+  tcInstTyVars, tcInstSigTyVars,
+  tcInstType, 
+  tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+  tcSkolDFunType, tcSuperSkolTyVars,

 
   --------------------------------
   -- Checking type validity
 
   --------------------------------
   -- Checking type validity

-  Rank, UserTypeCtxt(..), checkValidType, 
-  SourceTyCtxt(..), checkValidTheta, checkFreeness,
-  checkValidInstHead, checkValidInstance, checkAmbiguity,
-  checkInstTermination,
+  Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
+  SourceTyCtxt(..), checkValidTheta, 
+  checkValidInstance,
+  checkValidTypeInst, checkTyFamFreeness,

   arityErr, 
   arityErr, 

+  growPredTyVars, growThetaTyVars, validDerivPred,

 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking

-  zonkType, zonkTcPredType, 
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
-  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcKindToKind, zonkTcKind,
+  zonkType, mkZonkTcTyVar, zonkTcPredType, 
+  zonkTcTypeCarefully,
+  skolemiseUnboundMetaTyVar,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
+  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
+  zonkTcType, zonkTcTypes, zonkTcThetaType,
+  zonkTcKindToKind, zonkTcKind, 
+  zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar,
+  zonkWC, zonkWantedEvVars,
+  zonkTcTypeAndSubst,
+  tcGetGlobalTyVars, 

 
 

-  readKindVar, writeKindVar

 
 

+  readKindVar, writeKindVar

   ) where
 
 #include "HsVersions.h"
 
   ) where
 
 #include "HsVersions.h"
 

-

 -- friends:
 -- friends:

-import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
-                         ThetaType
-                       ) 
-import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
-                         MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
-                         BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef,
-                         mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, tcGetTyVar,
-                         tcSplitPhiTy, tcSplitPredTy_maybe,
-                         tcSplitAppTy_maybe,  
-                         tcValidInstHeadTy, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
-                         typeKind, isSkolemTyVar,
-                         mkAppTy, mkTyVarTy, mkTyVarTys, 
-                         tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, tcView,
-                         pprPred, pprTheta, pprClassPred )
-import Type            ( Kind, KindVar, 
-                         isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind,
-                         liftedTypeKind, defaultKind
-                       )
-import Type            ( TvSubst, zipTopTvSubst, substTy )
-import Coercion                ( mkCoKind )
-import Class           ( Class, classArity, className )
-import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName )
-import Var             ( TyVar, tyVarKind, tyVarName, isTcTyVar, 
-                         mkTyVar, mkTcTyVar, tcTyVarDetails,
-                         CoVar, mkCoVar )
-
-       -- Assertions
-#ifdef DEBUG
-import TcType          ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Type            ( isSubKind )
-#endif
+import TypeRep
+import TcType
+import Type
+import Coercion
+import Class
+import TyCon
+import Var

 
 -- others:
 
 -- others:

-import TcRnMonad          -- TcType, amongst others
-import FunDeps         ( grow, checkInstCoverage )
-import Name            ( Name, setNameUnique, mkSysTvName )
+import HsSyn           -- HsType
+import TcRnMonad        -- TcType, amongst others
+import Id
+import FunDeps
+import Name

 import VarSet
 import VarSet

-import DynFlags                ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, notNull )
-import ListSetOps      ( removeDups )
-import UniqSupply      ( uniqsFromSupply )
+import ErrUtils
+import DynFlags
+import Util
+import Maybes
+import ListSetOps
+import BasicTypes
+import SrcLoc

 import Outputable
 import Outputable

+import FastString
+import Unique( Unique )
+import Bag

 
 

-import Control.Monad   ( when )
-import Data.List       ( (\\) )
-
+import Control.Monad
+import Data.List        ( (\\) )

 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 \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)) }
-
-newKindVars :: Int -> TcM [TcKind]
-newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
+newEvVars :: TcThetaType -> TcM [EvVar]
+newEvVars theta = mapM newEvVar theta
+
+newWantedEvVar :: TcPredType -> TcM EvVar 
+newWantedEvVar (EqPred ty1 ty2) = newCoVar 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 
+
+--------------
+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) }
+
+-----------------
+newSilentGiven :: PredType -> TcM EvVar
+-- Make a dictionary for a "silent" given dictionary
+-- Behaves just like any EvVar except that it responds True to isSilentDict
+-- This is used only to suppress confusing error reports
+newSilentGiven (ClassP cls tys)
+  = do { uniq <- newUnique
+       ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
+       ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+newSilentGiven (EqPred ty1 ty2)
+  = do { uniq <- newUnique
+       ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
+       ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+newSilentGiven pred@(IParam {})
+  = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
+
+isSilentEvVar :: EvVar -> Bool
+isSilentEvVar v = isSystemName (Var.varName v)
+  -- Notice that all *other* evidence variables get Internal Names

 \end{code}
 
 
 \end{code}
 
 

@@ -172,33 +193,82 @@ newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
-mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
+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)

 
 

-tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+                           ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+                               -- Either the tyvars are freshly made, by inst_tyvars,
+                                -- or any nested foralls have different binders.
+                                -- Either way, zipTopTvSubst is ok
+
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }
+
+tcSkolDFunType :: 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
 -- Instantiate a type signature with skolem constants, but 
 -- do *not* give them fresh names, because we want the name to

--- be in the type environment -- it is lexically scoped.
-tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+-- be in the type environment: it is lexically scoped.
+tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty

 
 

-tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSuperSkolTyVars :: [TyVar] -> [TcTyVar]

 -- Make skolem constants, but do *not* give them new names, as above
 -- Make skolem constants, but do *not* give them new names, as above

-tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
-                             | tv <- tyvars ]
+-- Moreover, make them "super skolems"; see comments with superSkolemTv
+tcSuperSkolTyVars tyvars
+  = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv
+    | tv <- tyvars ]
+
+tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar
+-- Instantiate the tyvar, using 
+--     * the occ-name and kind of the supplied tyvar, 
+--     * the unique from the monad,
+--     * the location either from the tyvar (skol_info = SigSkol)
+--                     or from the monad (otherwise)
+tcInstSkolTyVar overlappable tyvar
+  = do { uniq <- newUnique
+        ; loc <-  getSrcSpanM
+       ; let new_name = mkInternalName uniq occ loc
+        ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) }
+  where
+    old_name = tyVarName tyvar
+    occ      = nameOccName old_name
+    kind     = tyVarKind tyvar

 
 

-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh skolem constants
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars

 
 

-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcInstSkolTyVar info tyvar
-  = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-             kind = tyVarKind tyvar
-       ; return (mkSkolTyVar name kind info) }
+tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
+tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars

 
 

-tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
+tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+-- Binding location comes from the monad
+tcInstSkolType ty = tcInstType tcInstSkolTyVars 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 tcInstSigTyVar
+
+tcInstSigTyVar :: TyVar -> TcM TcTyVar
+tcInstSigTyVar tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+        ; let name = setNameUnique (tyVarName tyvar) uniq
+               -- Use the same OccName so that the tidy-er 
+               -- doesn't rename 'a' to 'a0' etc
+             kind = tyVarKind tyvar
+       ; return (mkTcTyVar name kind (MetaTv SigTv ref)) }

 \end{code}
 
 
 \end{code}
 
 

@@ -209,54 +279,99 @@ tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
 %************************************************************************
 
 \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 ;
-       ; 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
--- Make a new meta tyvar whose Name and Kind 
--- come from an existing TyVar
-instMetaTyVar box_info tyvar
-  = do { uniq <- newUnique
-       ; ref <- newMutVar Flexi ;
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-             kind = tyVarKind tyvar
-       ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
+newMetaTyVar meta_info kind
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+        ; let name = mkTcTyVarName uniq s
+              s = case meta_info of
+                        TauTv -> fsLit "t"
+                        TcsTv -> fsLit "u"
+                        SigTv -> fsLit "a"
+       ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
+
+mkTcTyVarName :: Unique -> FastString -> Name
+-- Make sure that fresh TcTyVar names finish with a digit
+-- leaving the un-cluttered names free for user names
+mkTcTyVarName uniq str = mkSysTvName uniq str

 
 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
+  = 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
 
   | 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) }
+  = do { meta_details <- readMutVar ref; 
+       ; ASSERT2( 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}
 
 

@@ -271,26 +386,32 @@ 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)
-
-tcInstTyVar :: TyVar -> TcM TcTyVar
--- Instantiate with a META type variable
-tcInstTyVar tyvar = instMetaTyVar TauTv tyvar
+newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)

 
 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 -- Instantiate with META type variables
 tcInstTyVars tyvars
   = do { tc_tvs <- mapM tcInstTyVar tyvars
        ; let tys = mkTyVarTys tc_tvs
 
 tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
 -- Instantiate with META type variables
 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

+
+tcInstTyVar :: TyVar -> TcM TcTyVar
+-- Make a new unification variable tyvar whose Name and Kind 
+-- come from an existing TyVar
+tcInstTyVar tyvar
+  = do { uniq <- newMetaUnique
+       ; ref <- newMutVar Flexi
+        ; let name = mkSystemName uniq (getOccName tyvar)
+             kind = tyVarKind tyvar
+       ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }

 \end{code}
 
 
 \end{code}
 
 

@@ -301,11 +422,6 @@ tcInstTyVars tyvars
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with meta SigTvs
-tcInstSigTyVars skol_info tyvars 
-  = 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 

@@ -319,191 +435,219 @@ 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 
-  = 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
+zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars

 
 

-zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars    `thenM` \ tys ->
-                          returnM (tyVarsOfTypes tys)
-
-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

+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)
+          RuntimeUnk {} -> 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 }

 
 

-\begin{code}

 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)
+      RuntimeUnk {} -> 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)
+          RuntimeUnk {} -> 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}

-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
--- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
--- When we do this, we also default the kind -- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
+zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
+
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
+-- 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 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

-  | isSkolemTyVar tv = return tv
+  = ASSERT2( isTcTyVar tv, ppr tv ) 
+    case tcTyVarDetails tv of
+      SkolemTv {} -> WARN( True, ppr tv )  -- Dec10: Can this really happen?
+                     do { kind <- zonkTcType (tyVarKind tv)
+                        ; return $ setTyVarKind tv kind }

        -- It might be a skolem type variable, 
        -- for example from a user type signature
 
        -- 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
+      MetaTv _ _ref -> 
+#ifdef DEBUG               
+                       -- [Sept 04] Check for non-empty.  
+                       -- See note [Silly Type Synonym]
+                      (readMutVar _ref >>= \cts -> 
+                       case cts of 
+                             Flexi -> return ()
+                             Indirect ty -> WARN( True, ppr tv $$ ppr ty )
+                                            return ()) >>
+#endif
+                      skolemiseUnboundMetaTyVar tv vanillaSkolemTv
+      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
+
+skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
+-- We have a Meta tyvar with a ref-cell inside it
+-- Skolemise it, including giving it a new Name, so that
+--   we are totally out of Meta-tyvar-land
+-- We create a skolem TyVar, not a regular TyVar
+--   See Note [Zonking to Skolem]
+skolemiseUnboundMetaTyVar tv details
+  = ASSERT2( isMetaTyVar tv, ppr tv ) 
+    do  { span <- getSrcSpanM    -- Get the location from "here"
+                                 -- ie where we are generalising
+        ; 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
-
-       -- Bind the meta tyvar to the new tyvar
-       ; case details of
-           Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
-                          return ()
-               -- [Sept 04] I don't think this should happen
-               -- See note [Silly Type Synonym]
-
-           Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-
-       -- Return the new tyvar
+              final_name = mkInternalName uniq (getOccName tv) span
+              final_tv   = mkTcTyVar final_name final_kind details
+       ; writeMetaTyVar tv (mkTyVarTy final_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
+                               , ic_loc = loc })
+  = do {    -- No need to zonk the skolems
+       ; given'  <- mapM zonkEvVar given
+       ; loc'    <- zonkGivenLoc loc
+       ; wanted' <- zonkWC wanted
+       ; return (implic { ic_given = given'
+                        , ic_wanted = wanted'
+                        , ic_loc = loc' }) }
+
+zonkEvVar :: EvVar -> TcM EvVar
+zonkEvVar var = do { ty' <- zonkTcType (varType var)
+                   ; return (setVarType var ty') }
+
+zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar
+zonkFlavoredEvVar (EvVarX ev fl)
+  = do { ev' <- zonkEvVar ev
+       ; fl' <- zonkFlavor fl
+       ; return (EvVarX ev' fl') }
+
+zonkWC :: WantedConstraints -> TcM WantedConstraints
+zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
+  = do { flat'   <- zonkWantedEvVars flat
+       ; implic' <- mapBagM zonkImplication implic
+       ; insol'  <- mapBagM zonkFlavoredEvVar insol
+       ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }
+
+zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar)
+zonkWantedEvVars = mapBagM zonkWantedEvVar
+
+zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
+zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) }
+
+zonkFlavor :: CtFlavor -> TcM CtFlavor
+zonkFlavor (Given loc) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
+zonkFlavor fl          = return fl
+
+zonkGivenLoc :: GivenLoc -> TcM GivenLoc
+-- GivenLocs may have unification variables inside them!
+zonkGivenLoc (CtLoc skol_info span ctxt)
+  = do { skol_info' <- zonkSkolemInfo skol_info
+       ; return (CtLoc skol_info' span ctxt) }
+
+zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
+zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
+                                     ; return (SigSkol cx ty') }
+zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
+                                     ; return (InferSkol ntys') }
+  where
+    do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
+zonkSkolemInfo skol_info = return skol_info
+\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
 

@@ -523,7 +667,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 = ()

@@ -532,10 +676,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.

 
 
 %************************************************************************
 
 
 %************************************************************************

@@ -551,60 +726,69 @@ a /\a in the final result but all the occurrences of a will be zonked to ()
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 

-zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
-                                       -- see zonkTcType, and zonkTcTypeToType
-         -> TcType
-        -> TcM Type
-zonkType unbound_var_fn ty
+zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
+         -> TcType -> TcM Type
+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 *mutable Flexi* 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)
+      RuntimeUnk {}  -> 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}
 
 

@@ -629,7 +813,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}
                        
 %************************************************************************

@@ -669,85 +854,183 @@ 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
-                RuleSigCtxt _  -> 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
+                 GenSigCtxt     -> panic "checkValidType"
+                                     -- Can't happen; GenSigCtxt not used for *user* sigs

 
        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)

@@ -766,91 +1049,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_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 -> 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_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)

 
 
 %************************************************************************
 
 
 %************************************************************************

@@ -878,11 +1137,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}

@@ -891,36 +1151,52 @@ 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)
 check_pred_ty dflags ctxt pred@(ClassP cls tys)

-  =    -- Class predicates are valid in all contexts
-    checkTc (arity == n_tys) arity_err         `thenM_`
-
-       -- Check the form of the argument types
-    mappM_ check_arg_type tys                          `thenM_`
-    checkTc (check_class_pred_tys dflags ctxt tys)
-           (predTyVarErr pred $$ how_to_allow)
-
+  = do {       -- Class predicates are valid in all contexts
+       ; checkTc (arity == n_tys) arity_err
+
+               -- Check the form of the argument types
+       ; mapM_ checkValidMonoType tys
+       ; checkTc (check_class_pred_tys dflags ctxt tys)
+                (predTyVarErr pred $$ how_to_allow)
+       }

   where
     class_name = className cls
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
   where
     class_name = className cls
     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 type
+               -- families are permitted
+       ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+       ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
+                 (eqSuperClassErr pred)

 
 

-check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
-       -- Implicit parameters only allows in type
+               -- Check the form of the argument types
+       ; checkValidMonoType ty1
+       ; checkValidMonoType ty2
+       }
+
+check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
+       -- Implicit parameters only allowed in type

        -- signatures; not in instance decls, superclasses etc
        -- signatures; not in instance decls, superclasses etc

-       -- The reason for not allowing implicit params in instances is a bit subtle
+       -- The reason for not allowing implicit params in instances is a bit
+       -- subtle.

        -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
        -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
        -- discharge all the potential usas of the ?x in e.   For example, a
        -- If we allowed        instance (?x::Int, Eq a) => Foo [a] where ...
        -- then when we saw (e :: (?x::Int) => t) it would be unclear how to 
        -- discharge all the potential usas of the ?x in e.   For example, a

@@ -928,21 +1204,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

@@ -981,72 +1259,115 @@ 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
-  = 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 ]
-
-badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-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)
-
+  = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
+         ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
+
+eqSuperClassErr :: PredType -> SDoc
+eqSuperClassErr pred
+  = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
+       2 (ppr pred)
+
+badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
+badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
+eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
+                   $$
+                   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}

@@ -1063,50 +1384,52 @@ compiled elsewhere). In these cases, we let them go through anyway.
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}

-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-checkValidInstHead ty  -- Should be a source type
-  = case tcSplitPredTy_maybe ty of {
-       Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
-       Just pred -> 
-
-    case getClassPredTys_maybe pred of {
-       Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
-        Just (clas,tys) ->
-
-    getDOpts                                   `thenM` \ dflags ->
-    mappM_ check_arg_type tys                  `thenM_`
-    check_inst_head dflags clas tys            `thenM_`
-    returnM (clas, tys)
-    }}
-
-check_inst_head dflags clas tys
-       -- 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")
-
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+  = do { dflags <- getDOpts
+
+           -- If GlasgowExts then check at least one isn't a type variable
+       ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
+                  all tcInstHeadTyNotSynonym tys)
+                 (instTypeErr pp_pred head_type_synonym_msg)
+       ; checkTc (xopt Opt_FlexibleInstances dflags ||
+                  all tcInstHeadTyAppAllTyVars tys)
+                 (instTypeErr pp_pred head_type_args_tyvars_msg)
+       ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
+                  isSingleton tys)
+                 (instTypeErr pp_pred 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
+    pp_pred = pprClassPred clas tys
+    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 *distinct 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}
 
 

@@ -1116,30 +1439,41 @@ 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
-
-       ; checkValidTheta InstThetaCtxt theta
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
+                   -> Class -> [TcType] -> TcM ()
+checkValidInstance hs_type tyvars theta clas inst_tys
+  = setSrcSpan (getLoc hs_type) $
+    do  { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
+        ; checkValidTheta InstThetaCtxt theta

        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
        ; 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) $
-              checkInstTermination theta inst_tys
+       -- For Haskell 98 this will already have been done by checkValidTheta,
+        -- but as we may be using other extensions we need to check.
+       ; undecidable_ok <- xoptM Opt_UndecidableInstances
+        ; 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)

-       }
+        }

   where
   where

-    msg  = parens (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])
+
+        -- 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.

@@ -1153,34 +1487,137 @@ The underlying idea is that
 
 
 \begin{code}
 
 
 \begin{code}

-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
-  = do { mappM_ (check_nomore (fvTypes tys))    theta
-       ; mappM_ (check_smaller (sizeTypes tys)) theta }
+checkInstTermination :: [TcType] -> ThetaType -> [Message]
+checkInstTermination tys theta
+  = mapCatMaybes check theta
+  where
+   fvs  = fvTypes tys
+   size = sizeTypes tys
+   check pred 
+      | not (null (fvPred pred \\ fvs)) 
+      = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+      | sizePred pred >= size
+      = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+      | otherwise
+      = Nothing
+
+predUndecErr :: PredType -> SDoc -> SDoc
+predUndecErr pred msg = sep [msg,
+                       nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]

 
 

-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
-  = checkTc (null (fvPred pred \\ fvs))
-           (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+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}

 
 

-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
-  = checkTc (sizePred pred < n)
-           (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+validDeivPred checks for OK 'deriving' context.  See Note [Exotic
+derived instance contexts] in TcSimplify.  However the predicate is
+here because it uses sizeTypes, fvTypes.

 
 

-predUndecErr pred msg = sep [msg,
-                       nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+\begin{code}
+validDerivPred :: PredType -> Bool
+validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
+                              where fvs = fvTypes tys
+validDerivPred _              = False
+\end{code}

 
 

-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")

 
 

+%************************************************************************
+%*                                                                     *
+       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

@@ -1199,7 +1636,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

@@ -1208,8 +1644,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}