Reject polytypes in instance declarations (for now anyway)
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 570f2f5..6c1814e 100644 (file)
@@ -12,23 +12,30 @@ module TcMType (
   --------------------------------
   -- Creating new mutable type variables
   newFlexiTyVar,
   --------------------------------
   -- Creating new mutable type variables
   newFlexiTyVar,
-  newTyFlexiVarTy,             -- Kind -> TcM TcType
-  newTyFlexiVarTys,            -- Int -> Kind -> TcM [TcType]
+  newFlexiTyVarTy,             -- Kind -> TcM TcType
+  newFlexiTyVarTys,            -- Int -> Kind -> TcM [TcType]
   newKindVar, newKindVars, 
   newKindVar, newKindVars, 
-  lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
-  newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, 
+  lookupTcTyVar, LookupTyVarResult(..),
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, 
+
+  --------------------------------
+  -- Boxy type variables
+  newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
 
   --------------------------------
   -- Instantiation
 
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars, tcInstType, 
-  tcSkolTyVar, tcSkolTyVars, tcSkolType,
+  tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
+  tcInstSigTyVars, zonkSigTyVar,
+  tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
 
   --------------------------------
   -- Checking type validity
-  Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
+  Rank, UserTypeCtxt(..), checkValidType, 
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
-  checkValidInstHead, instTypeErr, checkAmbiguity,
-  arityErr, isRigidType,
+  checkValidInstHead, checkValidInstance, checkAmbiguity,
+  checkInstTermination,
+  arityErr, 
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking
@@ -45,24 +52,26 @@ module TcMType (
 
 
 -- friends:
 
 
 -- friends:
-import HsSyn           ( LHsType )
-import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
-                         Kind, ThetaType
+import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
+                         ThetaType
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
-                         MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, 
+                         MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
+                         BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType, 
+                         UserTypeCtxt(..),
+                         isMetaTyVar, isSigTyVar, metaTvRef,
+                         tcCmpPred, isClassPred, tcGetTyVar,
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
-                         tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
-                         isUnLiftedType, isIPPred, isImmutableTyVar,
-                         typeKind, isFlexi, isSkolemTyVar,
+                         tcValidInstHeadTy, tcSplitForAllTys,
+                         tcIsTyVarTy, tcSplitSigmaTy, 
+                         isUnLiftedType, isIPPred, 
+                         typeKind, isSkolemTyVar,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, 
+                         tyVarsOfType, tyVarsOfTypes, tcView,
                          pprPred, pprTheta, pprClassPred )
                          pprPred, pprTheta, pprClassPred )
-import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, 
                          isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
                          liftedTypeKind, defaultKind
                        )
                          isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
                          liftedTypeKind, defaultKind
                        )
@@ -70,72 +79,67 @@ import Type         ( TvSubst, zipTopTvSubst, substTy )
 import Class           ( Class, classArity, className )
 import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
                          tyConArity, tyConName )
 import Class           ( Class, classArity, className )
 import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
                          tyConArity, tyConName )
-import Var             ( TyVar, tyVarKind, tyVarName, 
-                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
+import Var             ( TyVar, tyVarKind, tyVarName, isTcTyVar, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails )
+
+       -- Assertions
+#ifdef DEBUG
+import TcType          ( isFlexi, isBoxyTyVar, isImmutableTyVar )
+import Kind            ( isSubKind )
+#endif
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
-import FunDeps         ( grow )
+import FunDeps         ( grow, checkInstCoverage )
 import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
-import VarEnv
-import CmdLineOpts     ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, equalLength, notNull )
+import DynFlags                ( dopt, DynFlag(..) )
+import Util            ( nOfThem, isSingleton, notNull )
 import ListSetOps      ( removeDups )
 import ListSetOps      ( removeDups )
-import SrcLoc          ( unLoc )
 import Outputable
 import Outputable
+
+import Control.Monad   ( when )
+import Data.List       ( (\\) )
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{New type variables}
+       Instantiation in general
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
-newMetaTyVar name kind details
-  = do { ref <- newMutVar details ;
-        return (mkTcTyVar name kind (MetaTv ref)) }
+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)
 
 
-readMetaTyVar :: TyVar -> TcM MetaDetails
-readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
-                     readMutVar (metaTvRef tyvar)
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
 
 
-writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
-writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 
-                          writeMutVar (metaTvRef tyvar) val
+                           ; 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
 
 
-newFlexiTyVar :: Kind -> TcM TcTyVar
-newFlexiTyVar kind
-  = newUnique  `thenM` \ uniq ->
-    newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }
+\end{code}
 
 
-newTyFlexiVarTy  :: Kind -> TcM TcType
-newTyFlexiVarTy kind
-  = newFlexiTyVar kind `thenM` \ tc_tyvar ->
-    returnM (TyVarTy tc_tyvar)
 
 
-newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
-newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
-
-isRigidType :: TcType -> TcM Bool
--- Check that the type is rigid, *taking the type refinement into account*
--- In other words if a rigid type variable tv is refined to a wobbly type,
--- the answer should be False
--- ToDo: can this happen?
-isRigidType ty
-  = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
-       ; return (and rigids) }
-  where
-    is_rigid tv = do { details <- lookupTcTyVar tv
-                    ; case details of
-                       RigidTv            -> return True
-                       IndirectTv True ty -> isRigidType ty
-                       other              -> return False
-                    }
+%************************************************************************
+%*                                                                     *
+       Kind variables
+%*                                                                     *
+%************************************************************************
 
 
+\begin{code}
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
                ; ref <- newMutVar Nothing
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
                ; ref <- newMutVar Nothing
@@ -148,116 +152,196 @@ newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
-\subsection{Type instantiation}
+       SkolemTvs (immutable)
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-Instantiating a bunch of type variables
-
-Note [TyVarName]
-~~~~~~~~~~~~~~~~
-Note that we don't change the print-name
-This won't confuse the type checker but there's a chance
-that two different tyvars will print the same way 
-in an error message.  -dppr-debug will show up the difference
-Better watch out for this.  If worst comes to worst, just
-use mkSystemName.
-
-
 \begin{code}
 \begin{code}
------------------------
-tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-tcInstTyVars tyvars
-  = do { tc_tvs <- mappM tcInstTyVar tyvars
-       ; let tys = mkTyVarTys tc_tvs
-       ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
-               -- Since the tyvars are freshly made,
-               -- they cannot possibly be captured by
-               -- any existing for-alls.  Hence zipTopTvSubst
-
-tcInstTyVar tyvar
-  = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; newMetaTyVar name (tyVarKind tyvar) Flexi }
-
-tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- tcInstType instantiates the outer-level for-alls of a TcType with
--- fresh (mutable) type variables, splits off the dictionary part, 
--- and returns the pieces.
-tcInstType ty
-  = case tcSplitForAllTys ty of
-       ([],     rho) ->        -- There may be overloading despite no type variables;
-                               --      (?x :: Int) => Int -> Int
-                        let
-                          (theta, tau) = tcSplitPhiTy rho
-                        in
-                        returnM ([], theta, tau)
-
-       (tyvars, rho) -> tcInstTyVars tyvars            `thenM` \ (tyvars', _, tenv) ->
-                        let
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
-
----------------------------------------------
--- Similar functions but for skolem constants
-
-tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-  
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
+mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
+mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
+
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but 
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+-- Make skolem constants, but do *not* give them new names, as above
+tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
+                             | tv <- tyvars ]
+
+tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar info tyvar
   = do { uniq <- newUnique
        ; let name = setNameUnique (tyVarName tyvar) uniq
   = do { uniq <- newUnique
        ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; return (mkTcTyVar name (tyVarKind tyvar) 
-                           (SkolemTv info)) }
-
-tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-tcSkolType info ty
-  = case tcSplitForAllTys ty of
-       ([],     rho) -> let
-                          (theta, tau) = tcSplitPhiTy rho
-                        in
-                        returnM ([], theta, tau)
+             kind = tyVarKind tyvar
+       ; return (mkSkolTyVar name kind info) }
 
 
-       (tyvars, rho) -> tcSkolTyVars info tyvars       `thenM` \ tyvars' ->
-                        let
-                          tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
+tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Putting and getting  mutable type variables}
+       MetaTvs (meta type variables; mutable)
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
 %*                                                                     *
 %************************************************************************
 
 \begin{code}
-putMetaTyVar :: TcTyVar -> TcType -> TcM ()
+newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
+-- 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("bx")
+                       TauTv   -> FSLIT("t")
+                       SigTv _ -> FSLIT("a")
+       ; 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)) }
+
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+                     readMutVar (metaTvRef tyvar)
+
+writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
 #ifndef DEBUG
 #ifndef DEBUG
-putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
+writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
 #else
 #else
-putMetaTyVar tyvar ty
+writeMetaTyVar tyvar ty
   | not (isMetaTyVar tyvar)
   | not (isMetaTyVar tyvar)
-  = pprTrace "putTcTyVar" (ppr tyvar) $
+  = pprTrace "writeMetaTyVar" (ppr tyvar) $
     returnM ()
 
   | otherwise
   = ASSERT( isMetaTyVar tyvar )
     ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
     returnM ()
 
   | otherwise
   = ASSERT( isMetaTyVar tyvar )
     ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
-    do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
-       ; writeMetaTyVar tyvar (Indirect ty) }
+    do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
+       ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
   where
     k1 = tyVarKind tyvar
     k2 = typeKind ty
 #endif
 \end{code}
 
   where
     k1 = tyVarKind tyvar
     k2 = typeKind ty
 #endif
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+       MetaTvs: TauTvs
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind = newMetaTyVar TauTv kind
+
+newFlexiTyVarTy  :: Kind -> TcM TcType
+newFlexiTyVarTy kind
+  = newFlexiTyVar kind `thenM` \ tc_tyvar ->
+    returnM (TyVarTy tc_tyvar)
+
+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
+
+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) }
+               -- Since the tyvars are freshly made,
+               -- they cannot possibly be captured by
+               -- any existing for-alls.  Hence zipTopTvSubst
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+       MetaTvs: SigTvs
+%*                                                                     *
+%************************************************************************
+
+\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 
+  = return sig_tv      -- Happens in the call in TcBinds.checkDistinctTyVars
+  | otherwise
+  = ASSERT( isSigTyVar sig_tv )
+    do { ty <- zonkTcTyVar sig_tv
+       ; return (tcGetTyVar "zonkSigTyVar" ty) }
+       -- 'ty' is bound to be a type variable, because SigTvs
+       -- can only be unified with type variables
+\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
+
+tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
+-- tcInstType instantiates the outer-level for-alls of a TcType with
+-- fresh BOXY type variables, splits off the dictionary part, 
+-- and returns the pieces.
+tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Putting and getting  mutable type variables}
+%*                                                                     *
+%************************************************************************
+
 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.
 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.
@@ -266,45 +350,19 @@ We return Nothing iff the original box was unbound.
 
 \begin{code}
 data LookupTyVarResult -- The result of a lookupTcTyVar call
 
 \begin{code}
 data LookupTyVarResult -- The result of a lookupTcTyVar call
-  = FlexiTv
-  | RigidTv
-  | IndirectTv Bool TcType
-       --      True  => This is a non-wobbly type refinement, 
-       --               gotten from GADT match unification
-       --      False => This is a wobbly type, 
-       --               gotten from inference unification
+  = DoneTv TcTyVarDetails      -- SkolemTv or virgin MetaTv
+  | IndirectTv TcType
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 
 lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
--- This function is the ONLY PLACE that we consult the 
--- type refinement carried by the monad
---
--- The boolean returned with Indirect
 lookupTcTyVar tyvar 
 lookupTcTyVar tyvar 
-  = case tcTyVarDetails tyvar of
-      SkolemTv _ -> do { type_reft <- getTypeRefinement
-                       ; case lookupVarEnv type_reft tyvar of
-                           Just ty -> return (IndirectTv True ty)
-                           Nothing -> return RigidTv
-                       }
-      MetaTv ref -> do         { details <- readMutVar ref
-                       ; case details of
-                           Indirect ty -> return (IndirectTv False ty)
-                           Flexi       -> return FlexiTv
-                       }
-
--- Look up a meta type variable, conditionally consulting 
--- the current type refinement
-condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
-condLookupTcTyVar use_refinement tyvar 
-  | use_refinement = lookupTcTyVar tyvar
-  | otherwise
-  = case tcTyVarDetails tyvar of
-      SkolemTv _ -> return RigidTv
-      MetaTv ref -> do { details <- readMutVar ref
-                       ; case details of
-                           Indirect ty -> return (IndirectTv False ty)
-                           Flexi       -> return FlexiTv
-                       }
+  = 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
 
 {- 
 -- gaw 2004 We aren't shorting anything out anymore, at least for now
@@ -359,14 +417,15 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars       `thenM` \ tys ->
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
                           returnM (tyVarsOfTypes tys)
 
 zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
+zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
+                   zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
 \end{code}
 
 -----------------  Types
 
 \begin{code}
 zonkTcType :: TcType -> TcM TcType
 \end{code}
 
 -----------------  Types
 
 \begin{code}
 zonkTcType :: TcType -> TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys
@@ -394,13 +453,13 @@ zonkTcPredType (IParam n t)
 \begin{code}
 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 \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 inot ano ordinary TyVar.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
 -- When we do this, we also default the kind -- see notes with Kind.defaultKind
 -- The meta tyvar is updated to point to the new regular TyVar.  Now any 
 -- bound occurences of the original type variable will get zonked to 
 -- the immutable version.
 --
--- We leave skolem TyVars alone; they are imutable.
+-- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
   | isSkolemTyVar tv = return tv
        -- It might be a skolem type variable, 
 zonkQuantifiedTyVar tv
   | isSkolemTyVar tv = return tv
        -- It might be a skolem type variable, 
@@ -420,7 +479,7 @@ zonkQuantifiedTyVar tv
                -- [Sept 04] I don't think this should happen
                -- See note [Silly Type Synonym]
 
                -- [Sept 04] I don't think this should happen
                -- See note [Silly Type Synonym]
 
-           other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
+           Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
 
        -- Return the new tyvar
        ; return final_tv }
 
        -- Return the new tyvar
        ; return final_tv }
@@ -445,7 +504,7 @@ Consider this:
   where a is fresh.
 
 * Now abstract over the 'a', but float out the Num (C d a) constraint
   where a is fresh.
 
 * Now abstract over the 'a', but float out the Num (C d a) constraint
-  because it does not 'really' mention a.  (see Type.tyVarsOfType)
+  because it does not 'really' mention a.  (see exactTyVarsOfType)
   The arg to foo becomes
        /\a -> \t -> t+t
 
   The arg to foo becomes
        /\a -> \t -> t+t
 
@@ -477,37 +536,34 @@ a /\a in the final result but all the occurrences of a will be zonked to ()
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
-        -> Bool                        -- Should we consult the current type refinement?
          -> TcType
         -> TcM Type
          -> TcType
         -> TcM Type
-zonkType unbound_var_fn rflag ty
+zonkType unbound_var_fn ty
   = go ty
   where
   = go ty
   where
-    go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
-                                   returnM (TyConApp tycon tys')
-
-    go (NoteTy (SynNote ty1) ty2) = go ty1             `thenM` \ ty1' ->
-                                   go ty2              `thenM` \ ty2' ->
-                                   returnM (NoteTy (SynNote ty1') ty2')
-
-    go (NoteTy (FTVNote _) ty2)   = go ty2     -- Discard free-tyvar annotations
-
-    go (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 (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')
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
-    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar
+    go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
+                      | otherwise       = return (TyVarTy tyvar)
+               -- Ordinary (non Tc) tyvars occur inside quantified types
 
     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
                             go ty              `thenM` \ ty' ->
 
     go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
                             go ty              `thenM` \ ty' ->
@@ -518,23 +574,17 @@ zonkType unbound_var_fn rflag ty
     go_pred (IParam n ty)  = go ty             `thenM` \ ty' ->
                             returnM (IParam n ty')
 
     go_pred (IParam n ty)  = go ty             `thenM` \ ty' ->
                             returnM (IParam n ty')
 
-zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable
-          -> Bool                               -- Consult the type refinement?
-         -> TcTyVar -> TcM TcType
-zonkTyVar unbound_var_fn rflag tyvar 
-  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
-                               -- the quantified variable a are TyVars not TcTyVars
+zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
+             -> TcTyVar -> TcM TcType
+zonk_tc_tyvar unbound_var_fn tyvar 
+  | not (isMetaTyVar tyvar)    -- Skolems
   = returnM (TyVarTy tyvar)
 
   = returnM (TyVarTy tyvar)
 
-  | otherwise
-  =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
-     case details of
-          -- If b is true, the variable was refined, and therefore it is okay
-          -- to continue refining inside.  Otherwise it was wobbly and we should
-          -- not refine further inside.
-         IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
-          FlexiTv         -> unbound_var_fn tyvar         -- Unbound flexi
-          RigidTv         -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary
+  | 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  }
 \end{code}
 
 
 \end{code}
 
 
@@ -548,8 +598,8 @@ zonkTyVar unbound_var_fn rflag tyvar
 \begin{code}
 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 writeKindVar :: KindVar -> TcKind -> TcM ()
 \begin{code}
 readKindVar  :: KindVar -> TcM (Maybe TcKind)
 writeKindVar :: KindVar -> TcKind -> TcM ()
-readKindVar  (KVar _ ref)     = readMutVar ref
-writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+readKindVar  kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
@@ -612,51 +662,6 @@ This might not necessarily show up in kind checking.
 
        
 \begin{code}
 
        
 \begin{code}
-data UserTypeCtxt 
-  = FunSigCtxt Name    -- Function type signature
-  | ExprSigCtxt                -- Expression type signature
-  | ConArgCtxt Name    -- Data constructor argument
-  | TySynCtxt Name     -- RHS of a type synonym decl
-  | GenPatCtxt         -- Pattern in generic decl
-                       --      f{| a+b |} (Inl x) = ...
-  | PatSigCtxt         -- Type sig in pattern
-                       --      f (x::t) = ...
-  | ResSigCtxt         -- Result type sig
-                       --      f x :: t = ....
-  | ForSigCtxt Name    -- Foreign inport or export signature
-  | RuleSigCtxt Name   -- Signature on a forall'd variable in a RULE
-  | DefaultDeclCtxt    -- Types in a default declaration
-
--- Notes re TySynCtxt
--- We allow type synonyms that aren't types; e.g.  type List = []
---
--- If the RHS mentions tyvars that aren't in scope, we'll 
--- quantify over them:
---     e.g.    type T = a->a
--- will become type T = forall a. a->a
---
--- With gla-exts that's right, but for H98 we should complain. 
-
-
-pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
-
-pprUserTypeCtxt ty (FunSigCtxt n)  = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
-pprUserTypeCtxt ty ExprSigCtxt     = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty (ConArgCtxt c)  = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
-pprUserTypeCtxt ty (TySynCtxt c)   = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
-                                         nest 2 (ptext SLIT(", namely") <+> ppr ty)]
-pprUserTypeCtxt ty GenPatCtxt      = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty PatSigCtxt      = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty (ForSigCtxt n)  = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
-pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
-pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
-
-pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
-\end{code}
-
-\begin{code}
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Checks that the type is valid for the given context
 checkValidType ctxt ty
@@ -667,7 +672,8 @@ checkValidType ctxt ty
             | otherwise
             = case ctxt of     -- Haskell 98
                 GenPatCtxt     -> Rank 0
             | otherwise
             = case ctxt of     -- Haskell 98
                 GenPatCtxt     -> Rank 0
-                PatSigCtxt     -> Rank 0
+                LamPatSigCtxt  -> Rank 0
+                BindPatSigCtxt -> Rank 0
                 DefaultDeclCtxt-> Rank 0
                 ResSigCtxt     -> Rank 0
                 TySynCtxt _    -> Rank 0
                 DefaultDeclCtxt-> Rank 0
                 ResSigCtxt     -> Rank 0
                 TySynCtxt _    -> Rank 0
@@ -677,6 +683,7 @@ checkValidType ctxt ty
                                                -- constructor, hence rank 1
                 ForSigCtxt _   -> Rank 1
                 RuleSigCtxt _  -> Rank 1
                                                -- constructor, hence rank 1
                 ForSigCtxt _   -> Rank 1
                 RuleSigCtxt _  -> Rank 1
+                SpecInstCtxt   -> Rank 1
 
        actual_kind = typeKind ty
 
 
        actual_kind = typeKind ty
 
@@ -686,7 +693,7 @@ checkValidType ctxt ty
                        ExprSigCtxt  -> isOpenTypeKind   actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
                        ExprSigCtxt  -> isOpenTypeKind   actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       other        -> isArgTypeKind       actual_kind
+                       other        -> isArgTypeKind    actual_kind
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
@@ -736,7 +743,7 @@ check_poly_type rank ubx_tup ty
 check_arg_type :: Type -> TcM ()
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
 check_arg_type :: Type -> TcM ()
 -- The sort of type that can instantiate a type variable,
 -- or be the argument of a type constructor.
--- Not an unboxed tuple, not a forall.
+-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
 -- Other unboxed types are very occasionally allowed as type
 -- arguments depending on the kind of the type constructor
 -- 
 -- Other unboxed types are very occasionally allowed as type
 -- arguments depending on the kind of the type constructor
 -- 
@@ -753,7 +760,7 @@ check_arg_type :: Type -> TcM ()
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type ty 
 -- Anyway, they are dealt with by a special case in check_tau_type
 
 check_arg_type ty 
-  = check_tau_type (Rank 0) UT_NotOk ty                `thenM_` 
+  = check_poly_type Arbitrary UT_NotOk ty      `thenM_` 
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
@@ -761,24 +768,42 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (PredTy sty)    = getDOpts         `thenM` \ dflags ->
-                                               check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup ty@(ForAllTy _ _)       = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
+       -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
+
+-- Naked PredTys don't usually show up, but they can as a result of
+--     {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy sty) = getDOpts            `thenM` \ dflags ->
+                                          check_source_ty dflags TypeCtxt sty
+
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
   = check_poly_type rank UT_NotOk arg_ty       `thenM_`
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
   = check_poly_type rank UT_NotOk arg_ty       `thenM_`
-    check_tau_type  rank UT_Ok    res_ty
+    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 (AppTy ty1 ty2)
   = check_arg_type ty1 `thenM_` check_arg_type ty2
 
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
-       -- Synonym notes are built only when the synonym is 
-       -- saturated (see Type.mkSynTy)
-  = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
-    (if gla_exts then
-       -- If -fglasgow-exts then don't check the 'note' part.
-       -- This  allows us to instantiate a synonym defn with a 
+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 ()
        -- for-all type, or with a partially-applied type synonym.
        --      e.g.   type T a b = a
        --             type S m   = m ()
@@ -787,24 +812,11 @@ check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
        -- But if you expand S first, then T we get just 
        --             f :: Int
        -- which is fine.
        -- But if you expand S first, then T we get just 
        --             f :: Int
        -- which is fine.
-       returnM ()
-    else
-       -- For H98, do check the un-expanded part
-       check_tau_type rank ubx_tup syn         
-    )                                          `thenM_`
-
-    check_tau_type rank ubx_tup ty
-
-check_tau_type rank ubx_tup (NoteTy other_note ty)
-  = check_tau_type rank ubx_tup ty
-
-check_tau_type rank ubx_tup ty@(TyConApp tc tys)
-  | isSynTyCon tc      
-  =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
-       -- synonym application, leaving it to checkValidType (i.e. right here)
-       -- to find the error
-    checkTc syn_arity_ok arity_msg     `thenM_`
-    mappM_ check_arg_type tys
+               returnM ()
+         else
+               -- For H98, do check the type args
+               mappM_ check_arg_type tys
+       }
     
   | isUnboxedTupleTyCon tc
   = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
     
   | isUnboxedTupleTyCon tc
   = doptM Opt_GlasgowExts                      `thenM` \ gla_exts ->
@@ -819,11 +831,6 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 
   where
     ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
 
-    syn_arity_ok = tc_arity <= n_args
-               -- It's OK to have an *over-applied* type synonym
-               --      data Tree a b = ...
-               --      type Foo a = Tree [a]
-               --      f :: Foo a b -> ...
     n_args    = length tys
     tc_arity  = tyConArity tc
 
     n_args    = length tys
     tc_arity  = tyConArity tc
 
@@ -831,7 +838,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
+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
 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
@@ -863,14 +870,11 @@ data SourceTyCtxt
                        --      f :: N a -> N a
   | InstThetaCtxt      -- Context of an instance decl
                        --      instance <S> => C [a] where ...
                        --      f :: N a -> N a
   | InstThetaCtxt      -- Context of an instance decl
                        --      instance <S> => C [a] where ...
-  | InstHeadCtxt       -- Head of an instance decl
-                       --      instance ... => Eq a where ...
                
 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 pprSourceTyCtxt (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 (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 InstHeadCtxt    = ptext SLIT("the head of an instance declaration")
 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 \end{code}
 
 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 \end{code}
 
@@ -885,10 +889,6 @@ check_valid_theta ctxt []
 check_valid_theta ctxt theta
   = getDOpts                                   `thenM` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
 check_valid_theta ctxt theta
   = getDOpts                                   `thenM` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
-       -- Actually, in instance decls and type signatures, 
-       -- duplicate constraints are eliminated by TcHsType.hoistForAllTys,
-       -- so this error can only fire for the context of a class or
-       -- data type decl.
     mappM_ (check_source_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
     mappM_ (check_source_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
@@ -908,11 +908,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
-
-    how_to_allow = case ctxt of
-                    InstHeadCtxt  -> empty     -- Should not happen
-                    InstThetaCtxt -> parens undecidableMsg
-                    other         -> parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+    how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 
 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type
 
 check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type
@@ -930,12 +926,12 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 -------------------------
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
 -------------------------
 check_class_pred_tys dflags ctxt tys 
   = case ctxt of
-       InstHeadCtxt  -> True   -- We check for instance-head 
-                               -- formation in checkValidInstHead
-       InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
-       other         -> gla_exts       || all tyvar_head tys
+       TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine
+       InstThetaCtxt -> gla_exts || all tcIsTyVarTy tys
+                               -- Further checks on head and theta in
+                               -- checkInstTermination
+       other         -> gla_exts || all tyvar_head tys
   where
   where
-    undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
     gla_exts      = dopt Opt_GlasgowExts dflags
 
 -------------------------
     gla_exts      = dopt Opt_GlasgowExts dflags
 
 -------------------------
@@ -1029,7 +1025,8 @@ checkThetaCtxt ctxt theta
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+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)
 
 arityErr kind name n m
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 
 arityErr kind name n m
@@ -1078,41 +1075,126 @@ checkValidInstHead ty  -- Should be a source type
 check_inst_head dflags clas tys
        -- If GlasgowExts then check at least one isn't a type variable
   | dopt Opt_GlasgowExts dflags
 check_inst_head dflags clas tys
        -- If GlasgowExts then check at least one isn't a type variable
   | dopt Opt_GlasgowExts dflags
-  = check_tyvars dflags clas tys
-
-       -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
-  | isSingleton tys,
-    Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
-    not (isSynTyCon tycon),            -- ...but not a synonym
-    all tcIsTyVarTy arg_tys,           -- Applied to type variables
-    equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
-          -- This last condition checks that all the type variables are distinct
-  = returnM ()
+  = mapM_ check_one tys
 
 
+       -- WITH HASKELL 98, MUST HAVE C (T a b c)
   | otherwise
   | otherwise
-  = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
+  = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
+           (instTypeErr (pprClassPred clas tys) head_shape_msg)
 
   where
 
   where
-    (first_ty : _)       = tys
+    (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")
 
 
     head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
                             text "where T is not a synonym, and a,b,c are distinct type variables")
 
-check_tyvars dflags clas tys
-       -- Check that at least one isn't a type variable
-       -- unless -fallow-undecideable-instances
-  | dopt Opt_AllowUndecidableInstances dflags = returnM ()
-  | not (all tcIsTyVarTy tys)                = returnM ()
-  | otherwise                                = failWithTc (instTypeErr (pprClassPred clas tys) msg)
-  where
-    msg =  parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
-                  $$ undecidableMsg)
-
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
-\end{code}
+       -- 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) }
 
 
-\begin{code}
 instTypeErr pp_ty msg
   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
         nest 4 msg]
 \end{code}
 instTypeErr pp_ty msg
   = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
         nest 4 msg]
 \end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Checking instance for termination}
+%*                                                                     *
+%************************************************************************
+
+
+\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
+       ; 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
+       
+       -- The Coverage Condition
+       ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
+                 (instTypeErr (pprClassPred clas inst_tys) msg)
+       }
+  where
+    msg  = parens (ptext SLIT("the instance types do not agree with the functional dependencies of the class"))
+\end{code}
+
+Termination test: 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.
+This is only needed with -fglasgow-exts, as Haskell 98 restrictions
+(which have already been checked) guarantee termination.
+
+\begin{code}
+checkInstTermination :: ThetaType -> [TcType] -> TcM ()
+checkInstTermination theta tys
+  = do
+    mappM_ (check_nomore (fvTypes tys)) theta
+    mappM_ (check_smaller (sizeTypes tys)) theta
+
+check_nomore :: [TyVar] -> PredType -> TcM ()
+check_nomore fvs pred
+  = checkTc (null (fvPred pred \\ fvs))
+           (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+
+check_smaller :: Int -> PredType -> TcM ()
+check_smaller n pred
+  = checkTc (sizePred pred < n)
+           (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+
+predUndecErr pred msg = sep [msg,
+                       nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+
+nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
+undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
+
+-- 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 (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
+
+fvTypes :: [Type] -> [TyVar]
+fvTypes tys                = concat (map fvType tys)
+
+fvPred :: PredType -> [TyVar]
+fvPred (ClassP _ tys')     = fvTypes tys'
+fvPred (IParam _ ty)       = fvType ty
+
+-- Size of a type: the number of variables and constructors
+sizeType :: Type -> Int
+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 (ForAllTy _ ty)   = sizeType ty
+
+sizeTypes :: [Type] -> Int
+sizeTypes xs               = sum (map sizeType xs)
+
+sizePred :: PredType -> Int
+sizePred (ClassP _ tys')   = sizeTypes tys'
+sizePred (IParam _ ty)     = sizeType ty
+\end{code}