[project @ 2005-12-16 15:15:08 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 8dda867..7ac2677 100644 (file)
@@ -21,14 +21,15 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstType, 
-  tcSkolTyVar, tcSkolTyVars, tcSkolType,
+  tcSkolType, tcSkolTyVars, tcInstSigType,
+  tcSkolSigType, tcSkolSigTyVars,
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,
-  arityErr, isRigidType,
+  arityErr, 
 
   --------------------------------
   -- Zonking
@@ -46,23 +47,23 @@ module TcMType (
 
 -- 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(..), 
                          MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, 
+                         tcCmpPred, tcEqType, isClassPred, 
                          tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
-                         tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
+                         tcValidInstHeadTy, tcSplitForAllTys,
+                         tcIsTyVarTy, tcSplitSigmaTy, 
                          isUnLiftedType, isIPPred, isImmutableTyVar,
                          typeKind, isFlexi, isSkolemTyVar,
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, 
+                         tyVarsOfType, tyVarsOfTypes, tcView,
                          pprPred, pprTheta, pprClassPred )
-import Kind            ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind,
                          isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
                          liftedTypeKind, defaultKind
                        )
@@ -79,9 +80,10 @@ import FunDeps               ( grow )
 import Name            ( Name, setNameUnique, mkSysTvName )
 import VarSet
 import VarEnv
-import CmdLineOpts     ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, equalLength, notNull )
-import ListSetOps      ( removeDups )
+import DynFlags        ( dopt, DynFlag(..) )
+import UniqSupply      ( uniqsFromSupply )
+import Util            ( nOfThem, isSingleton, notNull )
+import ListSetOps      ( removeDups, findDupsEq )
 import SrcLoc          ( unLoc )
 import Outputable
 \end{code}
@@ -120,22 +122,6 @@ newTyFlexiVarTy kind
 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
-                    }
-
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
                ; ref <- newMutVar Nothing
@@ -175,59 +161,101 @@ tcInstTyVars tyvars
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
 
-tcInstTyVar tyvar
+tcInstTyVar tyvar      -- Freshen the Name of the tyvar
   = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; newMetaTyVar name (tyVarKind tyvar) Flexi }
+        ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)
+                      (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)
+tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
 
-       (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
+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!!
 
-tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-  
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
-  = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-               -- See Note [TyVarName]
-       ; return (mkTcTyVar name (tyVarKind tyvar) 
-                           (SkolemTv info)) }
+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)
-tcSkolType info ty
+-- 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
-       ([],     rho) -> let
+       ([],     rho) -> let    -- There may be overloading despite no type variables;
+                               --      (?x :: Int) => Int -> Int
                           (theta, tau) = tcSplitPhiTy rho
                         in
-                        returnM ([], theta, tau)
+                        return ([], theta, tau)
 
-       (tyvars, rho) -> tcSkolTyVars info tyvars       `thenM` \ tyvars' ->
-                        let
-                          tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
-                          (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}
 
 
@@ -266,8 +294,7 @@ We return Nothing iff the original box was unbound.
 
 \begin{code}
 data LookupTyVarResult -- The result of a lookupTcTyVar call
-  = FlexiTv
-  | RigidTv
+  = DoneTv TcTyVarDetails      -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv
   | IndirectTv Bool TcType
        --      True  => This is a non-wobbly type refinement, 
        --               gotten from GADT match unification
@@ -277,34 +304,48 @@ data LookupTyVarResult    -- The result of a lookupTcTyVar call
 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 
-  = case tcTyVarDetails tyvar of
+  = 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 RigidTv
-                       }
-      MetaTv ref -> do         { details <- readMutVar ref
-                       ; case details of
-                           Indirect ty -> return (IndirectTv False ty)
-                           Flexi       -> return FlexiTv
+                           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 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
+      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
@@ -394,13 +435,13 @@ zonkTcPredType (IParam n t)
 \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.
 --
--- 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, 
@@ -486,11 +527,7 @@ zonkType unbound_var_fn rflag ty
     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 (NoteTy _ ty2)            = go ty2      -- Discard free-tyvar annotations
 
     go (PredTy p)                = go_pred p           `thenM` \ p' ->
                                    returnM (PredTy p')
@@ -522,9 +559,8 @@ zonkTyVar :: (TcTyVar -> TcM Type)          -- What to do for an unbound mutable variabl
           -> Bool                               -- Consult the type refinement?
          -> TcTyVar -> TcM TcType
 zonkTyVar unbound_var_fn rflag tyvar 
-  | not (isTcTyVar tyvar)      -- This can happen when
-                               -- zonking a forall type, when the bound type variable
-                               -- needn't be mutable
+  | not (isTcTyVar tyvar)      -- When zonking (forall a.  ...a...), the occurrences of 
+                               -- the quantified variable 'a' are TyVars not TcTyVars
   = returnM (TyVarTy tyvar)
 
   | otherwise
@@ -533,9 +569,9 @@ zonkTyVar unbound_var_fn rflag tyvar
           -- 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
+         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}
 
 
@@ -549,8 +585,8 @@ zonkTyVar unbound_var_fn rflag tyvar
 \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
@@ -615,6 +651,7 @@ This might not necessarily show up in kind checking.
 \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
@@ -627,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
+  | SpecInstCtxt       -- SPECIALISE instance pragma
 
 -- Notes re TySynCtxt
 -- We allow type synonyms that aren't types; e.g.  type List = []
@@ -653,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 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}
@@ -678,6 +717,7 @@ checkValidType ctxt ty
                                                -- constructor, hence rank 1
                 ForSigCtxt _   -> Rank 1
                 RuleSigCtxt _  -> Rank 1
+                SpecInstCtxt   -> Rank 1
 
        actual_kind = typeKind ty
 
@@ -687,7 +727,7 @@ checkValidType ctxt ty
                        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
@@ -762,9 +802,17 @@ check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
 
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (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_`
@@ -773,29 +821,6 @@ 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 (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
 
@@ -804,8 +829,31 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
   =    -- 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 ->
@@ -820,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 }
 
-    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
 
@@ -832,7 +875,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     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
@@ -931,15 +974,20 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 -------------------------
 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
-       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
 
 -------------------------
+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
@@ -1030,7 +1078,8 @@ checkThetaCtxt ctxt theta
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+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
@@ -1081,20 +1130,16 @@ check_inst_head 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,
-    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
-    (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")