[project @ 2005-12-16 15:15:08 by simonpj]

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

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index c1c7bce..7ac2677 100644 (file)
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -11,16 +11,18 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
 
   --------------------------------
   -- Creating new mutable type variables

-  newTyVar, newSigTyVar,
-  newTyVarTy,          -- Kind -> TcM TcType
-  newTyVarTys,         -- Int -> Kind -> TcM [TcType]
-  newKindVar, newKindVars, newOpenTypeKind,
-  putTcTyVar, getTcTyVar,
-  newMutTyVar, readMutTyVar, writeMutTyVar, 
+  newFlexiTyVar,
+  newTyFlexiVarTy,             -- Kind -> TcM TcType
+  newTyFlexiVarTys,            -- Int -> Kind -> TcM [TcType]
+  newKindVar, newKindVars, 
+  lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
+  newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar, 

 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 

+  tcSkolType, tcSkolTyVars, tcInstSigType,
+  tcSkolSigType, tcSkolSigTyVars,

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

@@ -31,11 +33,12 @@ module TcMType (
 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking

-  zonkType,
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
+  zonkType, zonkTcPredType, 
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,

   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,

-  zonkTcPredType, zonkTcTyVarToTyVar, 
-  zonkTcKindToKind
+  zonkTcKindToKind, zonkTcKind,
+
+  readKindVar, writeKindVar

 
   ) where
 
 
   ) where
 

@@ -43,41 +46,45 @@ module TcMType (
 
 
 -- friends:
 
 
 -- friends:

-import HsSyn           ( HsType )
-import TypeRep         ( Type(..), PredType(..), TyNote(..),    -- Friend; can see representation
-                         Kind, ThetaType
+import HsSyn           ( LHsType )
+import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
+                         ThetaType

                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                        ) 
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,

-                         TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
-                         tcEqType, tcCmpPred, isClassPred, mkTyConApp, typeCon,
+                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
+                         MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
+                         tcCmpPred, tcEqType, isClassPred, 

                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 

-                         tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
-                         isUnLiftedType, isIPPred, 
-
+                         tcValidInstHeadTy, tcSplitForAllTys,
+                         tcIsTyVarTy, tcSplitSigmaTy, 
+                         isUnLiftedType, isIPPred, isImmutableTyVar,
+                         typeKind, isFlexi, isSkolemTyVar,

                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,

-
-                         liftedTypeKind, defaultKind, superKind,
-                         superBoxity, liftedBoxity, typeKind,
-                         tyVarsOfType, tyVarsOfTypes, 
-                         eqKind, isTypeKind, pprThetaArrow, 
+                         tyVarsOfType, tyVarsOfTypes, tcView,

                          pprPred, pprTheta, pprClassPred )
                          pprPred, pprTheta, pprClassPred )

-import Subst           ( Subst, mkTopTyVarSubst, substTy )
+import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind,
+                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+                         liftedTypeKind, defaultKind
+                       )
+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, isTyVar, 
-                         mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
+import Var             ( TyVar, tyVarKind, tyVarName, 
+                         mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )

 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
 import FunDeps         ( grow )

-import Name            ( Name, setNameUnique, mkSystemTvNameEncoded )
+import Name            ( Name, setNameUnique, mkSysTvName )

 import VarSet
 import VarSet

-import CmdLineOpts     ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps      ( removeDups )
+import VarEnv
+import DynFlags        ( dopt, DynFlag(..) )
+import UniqSupply      ( uniqsFromSupply )
+import Util            ( nOfThem, isSingleton, notNull )
+import ListSetOps      ( removeDups, findDupsEq )
+import SrcLoc          ( unLoc )

 import Outputable
 \end{code}
 
 import Outputable
 \end{code}
 

@@ -89,53 +96,39 @@ import Outputable
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
-newMutTyVar name kind details
-  = do { ref <- newMutVar Nothing ;
-        return (mkMutTyVar name kind details ref) }
+newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
+newMetaTyVar name kind details
+  = do { ref <- newMutVar details ;
+        return (mkTcTyVar name kind (MetaTv ref)) }

 
 

-readMutTyVar :: TyVar -> TcM (Maybe Type)
-readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+                     readMutVar (metaTvRef tyvar)

 
 

-writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
-writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
+writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
+writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 
+                          writeMutVar (metaTvRef tyvar) val

 
 

-newTyVar :: Kind -> TcM TcTyVar
-newTyVar kind
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind

   = newUnique  `thenM` \ uniq ->
   = newUnique  `thenM` \ uniq ->

-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
+    newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi

 
 

-newSigTyVar :: Kind -> TcM TcTyVar
-newSigTyVar kind
-  = newUnique  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("s")) kind SigTv
-
-newTyVarTy  :: Kind -> TcM TcType
-newTyVarTy kind
-  = newTyVar kind      `thenM` \ tc_tyvar ->
+newTyFlexiVarTy  :: Kind -> TcM TcType
+newTyFlexiVarTy kind
+  = newFlexiTyVar kind `thenM` \ tc_tyvar ->

     returnM (TyVarTy tc_tyvar)
 
     returnM (TyVarTy tc_tyvar)
 

-newTyVarTys :: Int -> Kind -> TcM [TcType]
-newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
+newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
+newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)

 
 newKindVar :: TcM TcKind
 
 newKindVar :: TcM TcKind

-newKindVar
-  = newUnique                                                  `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv    `thenM` \ kv ->
-    returnM (TyVarTy kv)
+newKindVar = do        { uniq <- newUnique
+               ; ref <- newMutVar Nothing
+               ; return (KindVar (mkKindVar uniq ref)) }

 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())

-
-newBoxityVar :: TcM TcKind     -- Really TcBoxity
-  = newUnique                                            `thenM` \ uniq ->
-    newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) 
-               superBoxity VanillaTv                     `thenM` \ kv ->
-    returnM (TyVarTy kv)
-
-newOpenTypeKind :: TcM TcKind
-newOpenTypeKind = newBoxityVar `thenM` \ bx_var ->
-                 returnM (mkTyConApp typeCon [bx_var])

 \end{code}
 
 
 \end{code}
 
 

@@ -147,51 +140,122 @@ newOpenTypeKind = newBoxityVar   `thenM` \ bx_var ->
 
 Instantiating a bunch of type variables
 
 
 Instantiating a bunch of type variables
 

-\begin{code}
-tcInstTyVars :: TyVarDetails -> [TyVar] 
-            -> TcM ([TcTyVar], [TcType], Subst)
+Note [TyVarName]
+~~~~~~~~~~~~~~~~
+Note that we don't change the print-name
+This won't confuse the type checker but there's a chance
+that two different tyvars will print the same way 
+in an error message.  -dppr-debug will show up the difference
+Better watch out for this.  If worst comes to worst, just
+use mkSystemName.

 
 

-tcInstTyVars tv_details tyvars
-  = mappM (tcInstTyVar tv_details) tyvars      `thenM` \ tc_tyvars ->
-    let
-       tys = mkTyVarTys tc_tyvars
-    in
-    returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+
+\begin{code}
+-----------------------
+tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
+tcInstTyVars tyvars
+  = do { tc_tvs <- mappM tcInstTyVar tyvars
+       ; let tys = mkTyVarTys tc_tvs
+       ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }

                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by
                -- Since the tyvars are freshly made,
                -- they cannot possibly be captured by

-               -- any existing for-alls.  Hence mkTopTyVarSubst
-
-tcInstTyVar tv_details tyvar
-  = newUnique          `thenM` \ uniq ->
-    let
-       name = setNameUnique (tyVarName tyvar) uniq
-       -- Note that we don't change the print-name
-       -- This won't confuse the type checker but there's a chance
-       -- that two different tyvars will print the same way 
-       -- in an error message.  -dppr-debug will show up the difference
-       -- Better watch out for this.  If worst comes to worst, just
-       -- use mkSystemName.
-    in
-    newMutTyVar name (tyVarKind tyvar) tv_details
+               -- any existing for-alls.  Hence zipTopTvSubst
+
+tcInstTyVar tyvar      -- Freshen the Name of the tyvar
+  = do { uniq <- newUnique
+        ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
+                      (tyVarKind tyvar) Flexi }

 
 

-tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)

 -- tcInstType instantiates the outer-level for-alls of a TcType with
 -- fresh (mutable) type variables, splits off the dictionary part, 
 -- and returns the pieces.
 -- tcInstType instantiates the outer-level for-alls of a TcType with
 -- fresh (mutable) type variables, splits off the dictionary part, 
 -- and returns the pieces.

-tcInstType tv_details ty
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
+
+
+---------------------------------------------
+tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.
+-- 
+-- Tne new type variables have the sane Name as the original *iff* they are scoped.
+-- For scoped tyvars, we don't need a fresh unique, because the renamer has made them
+-- unique, and it's better not to do so because we extend the envt
+-- with them as scoped type variables, and we'd like to avoid spurious
+-- 's = s' bindings in error messages
+--
+-- For non-scoped ones, we *must* instantiate fresh ones:
+--     
+--     type T = forall a. [a] -> [a]
+--     f :: T; 
+--     f = g where { g :: T; g = <rhs> }
+--
+-- We must not use the same 'a' from the defn of T at both places!!
+
+tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty
+
+tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name scoped_names tyvars
+  = mapM new_tv tyvars
+  where
+    new_tv tv 
+      = do { let name = tyVarName tv
+          ; ref <- newMutVar Flexi
+          ; name' <- if name `elem` scoped_names 
+                     then return name
+                     else do { uniq <- newUnique; return (setNameUnique name uniq) }
+          ; return (mkTcTyVar name' (tyVarKind tv) 
+                              (SigSkolTv id_name ref)) }
+                           
+
+---------------------------------------------
+tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcSkolType info ty = tc_inst_type (tcSkolTyVars info) ty
+
+tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcSkolTyVars info tyvars
+  = do { us <- newUniqueSupply
+       ; return (zipWith skol_tv tyvars (uniqsFromSupply us)) }
+  where
+    skol_tv tv uniq = mkTcTyVar (setNameUnique (tyVarName tv) uniq)
+                               (tyVarKind tv) (SkolemTv info)
+       -- See Note [TyVarName]
+                           
+
+---------------------------------------------
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but 
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty
+  = tc_inst_type (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
+tcSkolSigTyVars info tyvars = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info) 
+                             | tv <- tyvars ]
+
+-----------------------
+tc_inst_type :: ([TyVar] -> TcM [TcTyVar])             -- How to instantiate the type variables
+            -> TcType                                  -- Type to instantiate
+            -> TcM ([TcTyVar], TcThetaType, TcType)    -- Result
+tc_inst_type inst_tyvars ty

   = case tcSplitForAllTys ty of
   = case tcSplitForAllTys ty of

-       ([],     rho) ->        -- There may be overloading despite no type variables;
+       ([],     rho) -> let    -- There may be overloading despite no type variables;

                                --      (?x :: Int) => Int -> Int
                                --      (?x :: Int) => Int -> Int

-                        let

                           (theta, tau) = tcSplitPhiTy rho
                         in
                           (theta, tau) = tcSplitPhiTy rho
                         in

-                        returnM ([], theta, tau)
+                        return ([], theta, tau)

 
 

-       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenM` \ (tyvars', _, tenv) ->
-                        let
-                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
-                        in
-                        returnM (tyvars', theta, tau)
+       (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+                           ; let  tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+                               -- Either the tyvars are freshly made, by inst_tyvars,
+                               -- or (in the call from tcSkolSigType) any nested foralls
+                               -- have different binders.  Either way, zipTopTvSubst is ok
+
+                           ; let  (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+                           ; return (tyvars', theta, tau) }

 \end{code}
 
 
 \end{code}
 
 

@@ -202,30 +266,26 @@ tcInstType tv_details ty
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

-putTcTyVar :: TcTyVar -> TcType -> TcM TcType
-getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
-\end{code}
-
-Putting is easy:
-
-\begin{code}
-putTcTyVar tyvar ty 
-  | not (isMutTyVar tyvar)
+putMetaTyVar :: TcTyVar -> TcType -> TcM ()
+#ifndef DEBUG
+putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
+#else
+putMetaTyVar tyvar ty
+  | not (isMetaTyVar tyvar)

   = pprTrace "putTcTyVar" (ppr tyvar) $
   = pprTrace "putTcTyVar" (ppr tyvar) $

-    returnM ty
+    returnM ()

 
   | otherwise
 
   | otherwise

-  = ASSERT( isMutTyVar tyvar )
-    writeMutTyVar tyvar (Just ty)      `thenM_`
-    returnM ty
+  = ASSERT( isMetaTyVar tyvar )
+    ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
+    do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
+       ; writeMetaTyVar tyvar (Indirect ty) }
+  where
+    k1 = tyVarKind tyvar
+    k2 = typeKind ty
+#endif

 \end{code}
 
 \end{code}
 

-Getting is more interesting.  The easy thing to do is just to read, thus:
-
-\begin{verbatim}
-getTcTyVar tyvar = readMutTyVar tyvar
-\end{verbatim}
-

 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.
 But it's more fun to short out indirections on the way: If this
 version returns a TyVar, then that TyVar is unbound.  If it returns
 any other type, then there might be bound TyVars embedded inside it.

@@ -233,36 +293,93 @@ any other type, then there might be bound TyVars embedded inside it.
 We return Nothing iff the original box was unbound.
 
 \begin{code}
 We return Nothing iff the original box was unbound.
 
 \begin{code}

+data LookupTyVarResult -- The result of a lookupTcTyVar call
+  = DoneTv TcTyVarDetails      -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv
+  | IndirectTv Bool TcType
+       --      True  => This is a non-wobbly type refinement, 
+       --               gotten from GADT match unification
+       --      False => This is a wobbly type, 
+       --               gotten from inference unification
+
+lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
+-- This function is the ONLY PLACE that we consult the 
+-- type refinement carried by the monad
+lookupTcTyVar tyvar 
+  = let 
+       details =  tcTyVarDetails tyvar
+    in
+    case details of
+      MetaTv ref -> lookup_wobbly details ref
+
+      SkolemTv _ -> do { type_reft <- getTypeRefinement
+                       ; case lookupVarEnv type_reft tyvar of
+                           Just ty -> return (IndirectTv True ty)
+                           Nothing -> return (DoneTv details)
+                       }
+
+       -- For SigSkolTvs try the refinement, and, failing that
+       -- see if it's been unified to anything.  It's a combination
+       -- of SkolemTv and MetaTv
+      SigSkolTv _  ref -> do { type_reft <- getTypeRefinement
+                            ; case lookupVarEnv type_reft tyvar of
+                               Just ty -> return (IndirectTv True ty)
+                               Nothing -> lookup_wobbly details ref
+                            }
+
+-- Look up a meta type variable, conditionally consulting 
+-- the current type refinement
+condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
+condLookupTcTyVar use_refinement tyvar 
+  | use_refinement = lookupTcTyVar tyvar
+  | otherwise
+  = case details of
+      MetaTv ref      -> lookup_wobbly details ref
+      SkolemTv _      -> return (DoneTv details)
+      SigSkolTv _ ref -> lookup_wobbly details ref
+  where 
+    details = tcTyVarDetails tyvar
+
+lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
+lookup_wobbly details ref
+  = do { meta_details <- readMutVar ref
+       ; case meta_details of
+           Indirect ty -> return (IndirectTv False ty)
+           Flexi       -> return (DoneTv details)
+       }
+
+{- 
+-- gaw 2004 We aren't shorting anything out anymore, at least for now

 getTcTyVar tyvar
 getTcTyVar tyvar

-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)

   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise
   = pprTrace "getTcTyVar" (ppr tyvar) $
     returnM (Just (mkTyVarTy tyvar))
 
   | otherwise

-  = ASSERT2( isMutTyVar tyvar, ppr tyvar )
-    readMutTyVar tyvar                         `thenM` \ maybe_ty ->
+  = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+    readMetaTyVar tyvar                                `thenM` \ maybe_ty ->

     case maybe_ty of
        Just ty -> short_out ty                         `thenM` \ ty' ->
     case maybe_ty of
        Just ty -> short_out ty                         `thenM` \ ty' ->

-                  writeMutTyVar tyvar (Just ty')       `thenM_`
+                  writeMetaTyVar tyvar (Just ty')      `thenM_`

                   returnM (Just ty')
 
        Nothing    -> returnM Nothing
 
 short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)
                   returnM (Just ty')
 
        Nothing    -> returnM Nothing
 
 short_out :: TcType -> TcM TcType
 short_out ty@(TyVarTy tyvar)

-  | not (isMutTyVar tyvar)
+  | not (isTcTyVar tyvar)

   = returnM ty
 
   | otherwise
   = returnM ty
 
   | otherwise

-  = readMutTyVar tyvar `thenM` \ maybe_ty ->
+  = readMetaTyVar tyvar        `thenM` \ maybe_ty ->

     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ ty' ->
     case maybe_ty of
        Just ty' -> short_out ty'                       `thenM` \ ty' ->

-                   writeMutTyVar tyvar (Just ty')      `thenM_`
+                   writeMetaTyVar tyvar (Just ty')     `thenM_`

                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty
                    returnM ty'
 
        other    -> returnM ty
 
 short_out other_ty = returnM other_ty

+-}

 \end{code}
 
 
 \end{code}
 
 

@@ -283,14 +400,14 @@ 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)) tyvar
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True 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)) ty
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty

 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys
 
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mappM zonkTcType tys

@@ -316,48 +433,38 @@ zonkTcPredType (IParam n t)
                     are used at the end of type checking
 
 \begin{code}
                     are used at the end of type checking
 
 \begin{code}

-zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind tc_kind 
-  = zonkType zonk_unbound_kind_var tc_kind
-  where
-       -- When zonking a kind, we want to
-       --      zonk a *kind* variable to (Type *)
-       --      zonk a *boxity* variable to *
-    zonk_unbound_kind_var kv 
-       | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
-       | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
-       | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
-                       
--- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
--- of a type variable, at the *end* of type checking.  It changes
--- the *mutable* type variable into an *immutable* one.
--- 
--- It does this by making an immutable version of tv and binds tv to it.
--- Now any bound occurences of the original type variable will get 
--- zonked to the immutable version.
-
-zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
-zonkTcTyVarToTyVar tv
-  = let
-               -- Make an immutable version, defaulting 
-               -- the kind to lifted if necessary
-       immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
-       immut_tv_ty = mkTyVarTy immut_tv
-
-        zap tv = putTcTyVar tv immut_tv_ty
-               -- Bind the mutable version to the immutable one
-    in 
-       -- If the type variable is mutable, then bind it to immut_tv_ty
-       -- so that all other occurrences of the tyvar will get zapped too
-    zonkTyVar zap tv           `thenM` \ ty2 ->
-
-       -- This warning shows up if the allegedly-unbound tyvar is
-       -- already bound to something.  It can actually happen, and 
-       -- in a harmless way (see [Silly Type Synonyms] below) so
-       -- it's only a warning
-    WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
-
-    returnM immut_tv
+zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
+-- When we do this, we also default the kind -- see notes with Kind.defaultKind
+-- The meta tyvar is updated to point to the new regular TyVar.  Now any 
+-- bound occurences of the original type variable will get zonked to 
+-- the immutable version.
+--
+-- We leave skolem TyVars alone; they are immutable.
+zonkQuantifiedTyVar tv
+  | isSkolemTyVar tv = return tv
+       -- It might be a skolem type variable, 
+       -- for example from a user type signature
+
+  | otherwise  -- It's a meta-type-variable
+  = do { details <- readMetaTyVar tv
+
+       -- Create the new, frozen, regular type variable
+       ; let final_kind = defaultKind (tyVarKind tv)
+             final_tv   = mkTyVar (tyVarName tv) final_kind
+
+       -- Bind the meta tyvar to the new tyvar
+       ; case details of
+           Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                          return ()
+               -- [Sept 04] I don't think this should happen
+               -- See note [Silly Type Synonym]
+
+           other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
+
+       -- Return the new tyvar
+       ; return final_tv }

 \end{code}
 
 [Silly Type Synonyms]
 \end{code}
 
 [Silly Type Synonyms]

@@ -385,10 +492,15 @@ Consider this:
 
 * 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 = ()

+  [Note Sept 04: now that we are zonking quantified type variables
+  on construction, the 'a' will be frozen as a regular tyvar on
+  quantification, so the floated dict will still have type (C d a).
+  Which renders this whole note moot; happily!]

 
 * Then the /\a abstraction has a zonked 'a' in it.
 
 
 * Then the /\a abstraction has a zonked 'a' in it.
 

-All very silly.   I think its harmless to ignore the problem.
+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 ()

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

@@ -400,30 +512,22 @@ All very silly.   I think its harmless to ignore the problem.
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}

--- zonkType is used for Kinds as well
-

 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
 zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
                                        -- see zonkTcType, and zonkTcTypeToType

-        -> TcType
+        -> Bool                        -- Should we consult the current type refinement?
+         -> TcType

         -> TcM Type
         -> TcM Type

-zonkType unbound_var_fn ty
+zonkType unbound_var_fn rflag ty

   = go ty
   where
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
                                    returnM (TyConApp tycon tys')
 
   = go ty
   where
     go (TyConApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
                                    returnM (TyConApp tycon tys')
 

-    go (NewTcApp tycon tys)      = mappM go tys        `thenM` \ tys' ->
-                                   returnM (NewTcApp 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 (NoteTy _ ty2)            = go ty2      -- Discard free-tyvar annotations

 
     go (PredTy p)                = go_pred p           `thenM` \ p' ->
                                    returnM (PredTy p')
 
     go (PredTy p)                = go_pred p           `thenM` \ p' ->
                                    returnM (PredTy p')

@@ -440,11 +544,11 @@ zonkType unbound_var_fn ty
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
                -- to pull the TyConApp to the top.
 
        -- The two interesting cases!

-    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
+    go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn rflag tyvar

 
 

-    go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar  `thenM` \ tyvar' ->
-                            go ty                      `thenM` \ ty' ->
-                            returnM (ForAllTy tyvar' ty')
+    go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
+                            go ty              `thenM` \ ty' ->
+                            returnM (ForAllTy tyvar ty')

 
     go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
                             returnM (ClassP c tys')
 
     go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
                             returnM (ClassP c tys')

@@ -452,25 +556,66 @@ zonkType unbound_var_fn ty
                             returnM (IParam n ty')
 
 zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable
                             returnM (IParam n ty')
 
 zonkTyVar :: (TcTyVar -> TcM Type)             -- What to do for an unbound mutable variable

-         -> TcTyVar -> TcM TcType
-zonkTyVar unbound_var_fn tyvar 
-  | not (isMutTyVar tyvar)     -- Not a mutable tyvar.  This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be mutable
-  = ASSERT( isTyVar tyvar )            -- Should not be any immutable kind vars
-    returnM (TyVarTy tyvar)
+          -> Bool                               -- Consult the type refinement?
+         -> TcTyVar -> TcM TcType
+zonkTyVar unbound_var_fn rflag tyvar 
+  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
+                               -- the quantified variable 'a' are TyVars not TcTyVars
+  = returnM (TyVarTy tyvar)

 
   | otherwise
 
   | otherwise

-  =  getTcTyVar tyvar  `thenM` \ maybe_ty ->
-     case maybe_ty of
-         Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
-         Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
+  =  condLookupTcTyVar rflag tyvar  `thenM` \ details ->
+     case details of
+          -- If b is true, the variable was refined, and therefore it is okay
+          -- to continue refining inside.  Otherwise it was wobbly and we should
+          -- not refine further inside.
+         IndirectTv b ty   -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+          DoneTv (MetaTv _) -> unbound_var_fn tyvar        -- Unbound meta type variable
+          DoneTv other      -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary

 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *
 \end{code}
 
 
 
 %************************************************************************
 %*                                                                     *

+                       Zonking kinds
+%*                                                                     *
+%************************************************************************
+
+\begin{code}
+readKindVar  :: KindVar -> TcM (Maybe TcKind)
+writeKindVar :: KindVar -> TcKind -> TcM ()
+readKindVar  kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+
+-------------
+zonkTcKind :: TcKind -> TcM TcKind
+zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
+                               ; k2' <- zonkTcKind k2
+                               ; returnM (FunKind k1' k2') }
+zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
+                              ; case mb_kind of
+                                   Nothing -> returnM k
+                                   Just k  -> zonkTcKind k }
+zonkTcKind other_kind = returnM other_kind
+
+-------------
+zonkTcKindToKind :: TcKind -> TcM Kind
+zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
+                                     ; k2' <- zonkTcKindToKind k2
+                                     ; returnM (FunKind k1' k2') }
+
+zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
+                                  ; case mb_kind of
+                                      Nothing -> return liftedTypeKind
+                                      Just k  -> zonkTcKindToKind k }
+
+zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
+zonkTcKindToKind other_kind   = returnM other_kind
+\end{code}
+                       
+%************************************************************************
+%*                                                                     *

 \subsection{Checking a user type}
 %*                                                                     *
 %************************************************************************
 \subsection{Checking a user type}
 %*                                                                     *
 %************************************************************************

@@ -506,6 +651,7 @@ This might not necessarily show up in kind checking.
 \begin{code}
 data UserTypeCtxt 
   = FunSigCtxt Name    -- Function type signature
 \begin{code}
 data UserTypeCtxt 
   = FunSigCtxt Name    -- Function type signature

+                       -- Also used for types in SPECIALISE pragmas

   | ExprSigCtxt                -- Expression type signature
   | ConArgCtxt Name    -- Data constructor argument
   | TySynCtxt Name     -- RHS of a type synonym decl
   | ExprSigCtxt                -- Expression type signature
   | ConArgCtxt Name    -- Data constructor argument
   | TySynCtxt Name     -- RHS of a type synonym decl

@@ -518,6 +664,7 @@ data UserTypeCtxt
   | ForSigCtxt Name    -- Foreign inport or export signature
   | RuleSigCtxt Name   -- Signature on a forall'd variable in a RULE
   | DefaultDeclCtxt    -- Types in a default declaration
   | ForSigCtxt Name    -- Foreign inport or export signature
   | RuleSigCtxt Name   -- Signature on a forall'd variable in a RULE
   | DefaultDeclCtxt    -- Types in a default declaration

+  | SpecInstCtxt       -- SPECIALISE instance pragma

 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []
 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []

@@ -530,8 +677,8 @@ data UserTypeCtxt
 -- With gla-exts that's right, but for H98 we should complain. 
 
 
 -- With gla-exts that's right, but for H98 we should complain. 
 
 

-pprHsSigCtxt :: UserTypeCtxt -> HsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt hs_ty ctxt
+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 (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)]

@@ -544,6 +691,7 @@ pprUserTypeCtxt ty ResSigCtxt      = sep [ptext SLIT("In a result type signature
 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)]
 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)]

+pprUserTypeCtxt ty SpecInstCtxt    = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)]

 
 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 \end{code}
 
 pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
 \end{code}

@@ -569,20 +717,22 @@ 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
 

-       actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
-

        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do

-                       GenPatCtxt   -> actual_kind_is_lifted
-                       ForSigCtxt _ -> actual_kind_is_lifted
-                       other        -> isTypeKind actual_kind
+                       ResSigCtxt   -> isOpenTypeKind   actual_kind
+                       ExprSigCtxt  -> isOpenTypeKind   actual_kind
+                       GenPatCtxt   -> isLiftedTypeKind actual_kind
+                       ForSigCtxt _ -> isLiftedTypeKind actual_kind
+                       other        -> isArgTypeKind    actual_kind

        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
                                   TySynCtxt _ -> UT_Ok
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
                                   TySynCtxt _ -> UT_Ok

+                                  ExprSigCtxt -> UT_Ok

                                   other       -> UT_NotOk
                -- Unboxed tuples ok in function results,
                -- but for type synonyms we allow them even at
                                   other       -> UT_NotOk
                -- Unboxed tuples ok in function results,
                -- but for type synonyms we allow them even at

@@ -652,9 +802,17 @@ 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_`

@@ -663,49 +821,46 @@ check_tau_type rank ubx_tup ty@(FunTy arg_ty 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 
-       -- for-all type, or with a partially-applied type synonym.
-       --      e.g.   type T a b = a
-       --             type S m   = m ()
-       --             f :: S (T Int)
-       -- Here, T is partially applied, so it's illegal in H98.
-       -- But if you expand S first, then T we get just 
-       --             f :: Int
-       -- which is fine.
-       returnM ()
-    else
-       -- For H98, do check the un-expanded part
-       check_tau_type rank ubx_tup syn         
-    )                                          `thenM_`
-
-    check_tau_type rank ubx_tup ty
-

 check_tau_type rank ubx_tup (NoteTy other_note ty)
   = check_tau_type rank ubx_tup ty
 
 check_tau_type rank ubx_tup (NoteTy other_note ty)
   = check_tau_type rank ubx_tup ty
 

-check_tau_type rank ubx_tup (NewTcApp tc tys)
-  = mappM_ check_arg_type tys
-

 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
 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
+    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 
     
   | 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
+               -- Args are allowed to be unlifted, or
+               -- more unboxed tuples, so can't use check_arg_ty

 
   | otherwise
   = mappM_ check_arg_type tys
 
   | otherwise
   = mappM_ check_arg_type tys

@@ -713,11 +868,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
 

@@ -725,7 +875,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

@@ -824,15 +974,20 @@ 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

+       TypeCtxt      -> True   -- {-# SPECIALISE instance Eq (T Int) #-} is fine

        InstHeadCtxt  -> True   -- We check for instance-head 
                                -- formation in checkValidInstHead
        InstHeadCtxt  -> True   -- We check for instance-head 
                                -- formation in checkValidInstHead

-       InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys
+       InstThetaCtxt -> undecidable_ok || distinct_tyvars tys

        other         -> gla_exts       || all tyvar_head tys
   where
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
     gla_exts      = dopt Opt_GlasgowExts dflags
 
 -------------------------
        other         -> gla_exts       || all tyvar_head tys
   where
     undecidable_ok = dopt Opt_AllowUndecidableInstances dflags 
     gla_exts      = dopt Opt_GlasgowExts dflags
 
 -------------------------

+distinct_tyvars tys    -- Check that the types are all distinct type variables
+  = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys)
+
+-------------------------

 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

@@ -923,7 +1078,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 variables, or repeated type variables,"),
+                         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

@@ -974,20 +1130,16 @@ check_inst_head dflags clas tys
   | dopt Opt_GlasgowExts dflags
   = check_tyvars dflags clas tys
 
   | dopt Opt_GlasgowExts dflags
   = check_tyvars dflags clas tys
 

-       -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
+       -- WITH HASKELL 98, MUST HAVE C (T a b c)

   | isSingleton tys,
   | 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
+    tcValidInstHeadTy first_ty

   = returnM ()
 
   | otherwise
   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
 
   where
   = returnM ()
 
   | otherwise
   = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
 
   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")