[project @ 2001-11-05 14:16:48 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index c535684..ca4629a 100644 (file)
@@ -4,61 +4,68 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
-                   tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
-                   tcExtendTyVarScope, tcExtendTopTyVarScope,
+module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, 
+                   UserTypeCtxt(..),
+
+                       -- Kind checking
+                   kcHsTyVar, kcHsTyVars, mkTyClTyVars,
+                   kcHsType, kcHsSigType, kcHsSigTypes, 
+                   kcHsLiftedSigType, kcHsContext,
+                   tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
+
                    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
                  ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVarBndr(..), HsUsageAnn(..),
-                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..) )
-import RnHsSyn         ( RenamedHsType, RenamedContext, RenamedSig )
+import HsSyn           ( HsType(..), HsTyVarBndr(..),
+                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
+import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
 import TcHsSyn         ( TcId )
 
 import TcMonad
-import TcEnv           ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
-                          tcExtendUVarEnv, tcLookupUVar,
-                         tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
+import TcEnv           ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
+                         tcGetGlobalTyVars, tcLEnvElts, tcInLocalScope,
+                         TyThing(..), TcTyThing(..), tcExtendKindEnv
                        )
-import TcType          ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
-                         typeToTcType, kindToTcKind,
-                         newKindVar, tcInstSigVar,
-                         zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
+import TcMType         ( newKindVar, tcInstSigTyVars, 
+                         zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
+                         unifyKind, unifyOpenTypeKind,
+                         checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
-                         instFunDeps, instFunDepsOfTheta )
-import FunDeps         ( tyVarFunDep, oclose )
-import TcUnify         ( unifyKind, unifyKinds, unifyTypeKind )
-import Type            ( Type, PredType(..), ThetaType, UsageAnn(..),
-                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
-                          mkUsForAllTy, zipFunTys, hoistForAllTys,
-                         mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
-                         mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
-                         boxedTypeKind, unboxedTypeKind, 
-                         mkArrowKinds, getTyVar_maybe, getTyVar,
-                         tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys
+import TcType          ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
+                         TcTyVar, TcTyVarSet, TcType, TcKind, TcThetaType, TcTauType,
+                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
+                         tcSplitForAllTys, tcSplitRhoTy, 
+                         hoistForAllTys, allDistinctTyVars, zipFunTys, 
+                         mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, mkRhoTy,
+                         liftedTypeKind, unliftedTypeKind, mkArrowKind,
+                         mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
+                         tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
+                         tyVarsOfType, mkForAllTys
                        )
-import PprType         ( pprConstraint, pprType, pprPred )
+import qualified Type  ( getTyVar_maybe )
+
+import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
+import PprType         ( pprType )
 import Subst           ( mkTopTyVarSubst, substTy )
-import Id              ( mkVanillaId, idName, idType, idFreeTyVars )
-import Var             ( TyVar, mkTyVar, mkNamedUVar, varName )
+import CoreFVs         ( idFreeTyVars )
+import Id              ( mkLocalId, idName, idType )
+import Var             ( Id, Var, TyVar, mkTyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
 import VarEnv
 import VarSet
-import Bag             ( bagToList )
 import ErrUtils                ( Message )
-import TyCon           ( TyCon )
-import Name            ( Name, OccName, isLocallyDefined )
-import TysWiredIn      ( mkListTy, mkTupleTy )
-import UniqFM          ( elemUFM, foldUFM )
+import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind )
+import Class           ( classTyCon )
+import Name            ( Name, getSrcLoc )
+import NameSet
+import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
-import Unique          ( Unique, Uniquable(..) )
-import Util            ( mapAccumL, isSingleton, removeDups )
+import Util            ( isSingleton, lengthIs )
 import Outputable
+
 \end{code}
 
 
@@ -68,292 +75,424 @@ import Outputable
 %*                                                                     *
 %************************************************************************
 
-tcHsType and tcHsTypeKind
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking we now type-check types in three phases
+
+       1.  Kind check the HsType [kcHsType]
+       2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
+       3.  Check the validity of the resulting type [checkValidType]
+
+Often these steps are done one after the othe (tcHsSigType).
+But in mutually recursive groups of type and class decls we do
+       1 kind-check the whole group
+       2 build TyCons/Classes in a knot-tied wa
+       3 check the validity of types in the now-unknotted TyCons/Classes
+
+\begin{code}
+tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
+  -- Do kind checking, and hoist for-alls to the top
+tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
+                       kcTypeType ty           `thenTc_`
+                       tcHsType ty
+                     )                         `thenTc` \ ty' ->
+                     checkValidType ctxt ty'   `thenTc_`
+                     returnTc ty'
+
+checkTypeCtxt ctxt ty
+  = vcat [ptext SLIT("In the type:") <+> ppr ty,
+         ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
+
+tcHsType    :: RenamedHsType -> TcM Type
+  -- Don't do kind checking, nor validity checking, 
+  --   but do hoist for-alls to the top
+  -- This is used in type and class decls, where kinding is
+  -- done in advance, and validity checking is done later
+  -- [Validity checking done later because of knot-tying issues.]
+tcHsType ty = tc_type ty  `thenTc` \ ty' ->  
+             returnTc (hoistForAllTys ty')
+
+tcHsTheta :: RenamedContext -> TcM ThetaType
+-- Used when we are expecting a ClassContext (i.e. no implicit params)
+-- Does not do validity checking, like tcHsType
+tcHsTheta hs_theta = mapTc tc_pred hs_theta
+
+-- In interface files the type is already kinded,
+-- and we definitely don't want to hoist for-alls.
+-- Otherwise we'll change
+--     dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
+-- into 
+--     dmfail :: forall m:(*->*) a:* Monad m => String -> m a
+-- which definitely isn't right!
+tcIfaceType ty = tc_type ty
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Kind checking}
+%*                                                                     *
+%************************************************************************
+
+Kind checking
+~~~~~~~~~~~~~
+When we come across the binding site for some type variables, we
+proceed in two stages
+
+1. Figure out what kind each tyvar has
+
+2. Create suitably-kinded tyvars, 
+   extend the envt, 
+   and typecheck the body
+
+To do step 1, we proceed thus:
+
+1a. Bind each type variable to a kind variable
+1b. Apply the kind checker
+1c. Zonk the resulting kinds
+
+The kind checker is passed to tcHsTyVars as an argument.  
+
+For example, when we find
+       (forall a m. m a -> m a)
+we bind a,m to kind varibles and kind-check (m a -> m a).  This
+makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
+in an environment that binds a and m suitably.
+
+The kind checker passed to tcHsTyVars needs to look at enough to
+establish the kind of the tyvar:
+  * For a group of type and class decls, it's just the group, not
+       the rest of the program
+  * For a tyvar bound in a pattern type signature, its the types
+       mentioned in the other type signatures in that bunch of patterns
+  * For a tyvar bound in a RULE, it's the type signatures on other
+       universally quantified variables in the rule
 
-tcHsType checks that the type really is of kind Type!
+Note that this may occasionally give surprising results.  For example:
+
+       data T a b = MkT (a b)
+
+Here we deduce                 a::*->*, b::*.
+But equally valid would be
+                               a::(*->*)-> *, b::*->*
 
 \begin{code}
-kcHsType :: RenamedHsType -> TcM c ()
-  -- Kind-check the type
-kcHsType ty = tc_type ty       `thenTc_`
-             returnTc ()
-
-tcHsSigType :: RenamedHsType -> TcM s TcType
-  -- Used for type sigs written by the programmer
-  -- Hoist any inner for-alls to the top
-tcHsSigType ty
-  = tcHsType ty                `thenTc` \ ty' ->
-    returnTc (hoistForAllTys ty')
-
-tcHsType :: RenamedHsType -> TcM s TcType
-tcHsType ty
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_type ty
-
-tcHsTypeKind    :: RenamedHsType -> TcM s (TcKind, TcType)
-tcHsTypeKind ty 
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_type_kind ty
-
--- Type-check a type, *and* then lazily zonk it.  The important
--- point is that this zonks all the uncommitted *kind* variables
--- in kinds of any any nested for-all tyvars.
--- There won't be any mutable *type* variables at all.
+-- tcHsTyVars is used for type variables in type signatures
+--     e.g. forall a. a->a
+-- They are immutable, because they scope only over the signature
+-- They may or may not be explicitly-kinded
+tcHsTyVars :: [HsTyVarBndr Name] 
+          -> TcM a                             -- The kind checker
+          -> ([TyVar] -> TcM b)
+          -> TcM b
+
+tcHsTyVars [] kind_check thing_inside = thing_inside []
+       -- A useful short cut for a common case!
+  
+tcHsTyVars tv_names kind_check thing_inside
+  = kcHsTyVars tv_names                                `thenNF_Tc` \ tv_names_w_kinds ->
+    tcExtendKindEnv tv_names_w_kinds kind_check                `thenTc_`
+    zonkKindEnv tv_names_w_kinds                       `thenNF_Tc` \ tvs_w_kinds ->
+    let
+       tyvars = mkImmutTyVars tvs_w_kinds
+    in
+    tcExtendTyVarEnv tyvars (thing_inside tyvars)
+
+
+
+tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
+-- tcAddScopedTyVars is used for scoped type variables
+-- added by pattern type signatures
+--     e.g.  \ (x::a) (y::a) -> x+y
+-- They never have explicit kinds (because this is source-code only)
+-- They are mutable (because they can get bound to a more specific type)
+
+-- Find the not-already-in-scope signature type variables,
+-- kind-check them, and bring them into scope
 --
--- NOTE the forkNF_Tc.  This makes the zonking lazy, which is
--- absolutely necessary.  During the type-checking of a recursive
--- group of tycons/classes (TcTyClsDecls.tcGroup) we use an
--- environment in which we aren't allowed to look at the actual
--- tycons/classes returned from a lookup. Because tc_app does
--- look at the tycon to build the type, we can't look at the type
--- either, until we get out of the loop.   The fork delays the
--- zonking till we've completed the loop.  Sigh.
-
-tcHsTopType :: RenamedHsType -> TcM s Type
-tcHsTopType ty
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_type ty                         `thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')   `thenTc` \ ty'' ->
-    returnTc (hoistForAllTys ty'')
-
-tcHsTopBoxedType :: RenamedHsType -> TcM s Type
-tcHsTopBoxedType ty
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_boxed_type ty                   `thenTc` \ ty' ->
-    forkNF_Tc (zonkTcTypeToType ty')   `thenTc` \ ty'' ->
-    returnTc (hoistForAllTys ty'')
-
-tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
-tcHsTopTypeKind ty
-  = -- tcAddErrCtxt (typeCtxt ty)              $
-    tc_type_kind ty                            `thenTc` \ (kind, ty') ->
-    forkNF_Tc (zonkTcTypeToType ty')           `thenTc` \ zonked_ty ->
-    returnNF_Tc (kind, hoistForAllTys zonked_ty)
+-- We no longer specify that these type variables must be univerally 
+-- quantified (lots of email on the subject).  If you want to put that 
+-- back in, you need to
+--     a) Do a checkSigTyVars after thing_inside
+--     b) More insidiously, don't pass in expected_ty, else
+--        we unify with it too early and checkSigTyVars barfs
+--        Instead you have to pass in a fresh ty var, and unify
+--        it with expected_ty afterwards
+tcAddScopedTyVars [] thing_inside
+  = thing_inside       -- Quick get-out for the empty case
+
+tcAddScopedTyVars sig_tys thing_inside
+  = tcGetEnv                                   `thenNF_Tc` \ env ->
+    let
+       all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
+       sig_tvs         = filter not_in_scope (nameSetToList all_sig_tvs)
+       not_in_scope tv = not (tcInLocalScope env tv)
+    in       
+    mapNF_Tc newNamedKindVar sig_tvs                   `thenTc` \ kind_env ->
+    tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)    `thenTc_`
+    zonkKindEnv kind_env                               `thenNF_Tc` \ tvs_w_kinds ->
+    listTc [ tcNewMutTyVar name kind PatSigTv
+          | (name, kind) <- tvs_w_kinds]               `thenNF_Tc` \ tyvars ->
+    tcExtendTyVarEnv tyvars thing_inside
+\end{code}
+    
+
+\begin{code}
+kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
+kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
+
+kcHsTyVar (UserTyVar name)       = newNamedKindVar name
+kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
+
+kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
+
+newNamedKindVar name = newKindVar      `thenNF_Tc` \ kind ->
+                      returnNF_Tc (name, kind)
+
+---------------------------
+kcLiftedType :: RenamedHsType -> TcM ()
+       -- The type ty must be a *lifted* *type*
+kcLiftedType ty
+  = kcHsType ty                                `thenTc` \ kind ->
+    tcAddErrCtxt (typeKindCtxt ty)     $
+    unifyKind liftedTypeKind kind
+    
+---------------------------
+kcTypeType :: RenamedHsType -> TcM ()
+       -- The type ty must be a *type*, but it can be lifted or unlifted.
+kcTypeType ty
+  = kcHsType ty                                `thenTc` \ kind ->
+    tcAddErrCtxt (typeKindCtxt ty)     $
+    unifyOpenTypeKind kind
+
+---------------------------
+kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
+       -- Used for type signatures
+kcHsSigType      = kcTypeType
+kcHsSigTypes tys  = mapTc_ kcHsSigType tys
+kcHsLiftedSigType = kcLiftedType
+
+---------------------------
+kcHsType :: RenamedHsType -> TcM TcKind
+kcHsType (HsTyVar name)              = kcTyVar name
+
+kcHsType (HsListTy ty)
+  = kcLiftedType ty            `thenTc` \ tau_ty ->
+    returnTc liftedTypeKind
+
+kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
+  = mapTc kcTypeType tys       `thenTc_`
+    returnTc (case boxity of
+                 Boxed   -> liftedTypeKind
+                 Unboxed -> unliftedTypeKind)
+
+kcHsType (HsFunTy ty1 ty2)
+  = kcTypeType ty1     `thenTc_`
+    kcTypeType ty2     `thenTc_`
+    returnTc liftedTypeKind
+
+kcHsType (HsNumTy _)           -- The unit type for generics
+  = returnTc liftedTypeKind
+
+kcHsType ty@(HsOpTy ty1 op ty2)
+  = kcTyVar op                         `thenTc` \ op_kind ->
+    kcHsType ty1                       `thenTc` \ ty1_kind ->
+    kcHsType ty2                       `thenTc` \ ty2_kind ->
+    tcAddErrCtxt (appKindCtxt (ppr ty))        $
+    kcAppKind op_kind  ty1_kind                `thenTc` \ op_kind' ->
+    kcAppKind op_kind' ty2_kind
+   
+kcHsType (HsPredTy pred)
+  = kcHsPred pred              `thenTc_`
+    returnTc liftedTypeKind
+
+kcHsType ty@(HsAppTy ty1 ty2)
+  = kcHsType ty1                       `thenTc` \ tc_kind ->
+    kcHsType ty2                       `thenTc` \ arg_kind ->
+    tcAddErrCtxt (appKindCtxt (ppr ty))        $
+    kcAppKind tc_kind arg_kind
+
+kcHsType (HsForAllTy (Just tv_names) context ty)
+  = kcHsTyVars tv_names                `thenNF_Tc` \ kind_env ->
+    tcExtendKindEnv kind_env   $
+    kcHsContext context                `thenTc_`
+    kcHsType ty                        `thenTc_`
+    returnTc liftedTypeKind
+
+---------------------------
+kcAppKind fun_kind arg_kind
+  = case tcSplitFunTy_maybe fun_kind of 
+       Just (arg_kind', res_kind)
+               -> unifyKind arg_kind arg_kind' `thenTc_`
+                  returnTc res_kind
+
+       Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
+                  unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
+                  returnTc res_kind
+
+
+---------------------------
+kcHsContext ctxt = mapTc_ kcHsPred ctxt
+
+kcHsPred :: RenamedHsPred -> TcM ()
+kcHsPred pred@(HsIParam name ty)
+  = tcAddErrCtxt (appKindCtxt (ppr pred))      $
+    kcLiftedType ty
+
+kcHsPred pred@(HsClassP cls tys)
+  = tcAddErrCtxt (appKindCtxt (ppr pred))      $
+    kcClass cls                                        `thenTc` \ kind ->
+    mapTc kcHsType tys                         `thenTc` \ arg_kinds ->
+    unifyKind kind (mkArrowKinds arg_kinds liftedTypeKind)
+
+ ---------------------------
+kcTyVar name   -- Could be a tyvar or a tycon
+  = tcLookup name      `thenTc` \ thing ->
+    case thing of 
+       AThing kind         -> returnTc kind
+       ATyVar tv           -> returnTc (tyVarKind tv)
+       AGlobal (ATyCon tc) -> returnTc (tyConKind tc) 
+       other               -> failWithTc (wrongThingErr "type" thing name)
+
+kcClass cls    -- Must be a class
+  = tcLookup cls                               `thenNF_Tc` \ thing -> 
+    case thing of
+       AThing kind           -> returnTc kind
+       AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
+       other                 -> failWithTc (wrongThingErr "class" thing cls)
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+\subsection{tc_type}
+%*                                                                     *
+%************************************************************************
+
+tc_type, the main work horse
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+       -------------------
+       *** BIG WARNING ***
+       -------------------
+
+tc_type is used to typecheck the types in the RHS of data
+constructors.  In the case of recursive data types, that means that
+the type constructors themselves are (partly) black holes.  e.g.
+
+       data T a = MkT a [T a]
+
+While typechecking the [T a] on the RHS, T itself is not yet fully
+defined.  That in turn places restrictions on what you can check in
+tcHsType; if you poke on too much you get a black hole.  I keep
+forgetting this, hence this warning!
+
+So tc_type does no validity-checking.  Instead that's all done
+by TcMType.checkValidType
+
+       --------------------------
+       *** END OF BIG WARNING ***
+       --------------------------
 
-The main work horse
-~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-tc_boxed_type :: RenamedHsType -> TcM s Type
-tc_boxed_type ty
-  = tc_type_kind ty                                    `thenTc` \ (actual_kind, tc_ty) ->
-    tcAddErrCtxt (typeKindCtxt ty)
-                (unifyKind boxedTypeKind actual_kind)  `thenTc_`
-    returnTc tc_ty
-
-tc_type :: RenamedHsType -> TcM s Type
-tc_type ty
-       -- The type ty must be a *type*, but it can be boxed
-       -- or unboxed.  So we check that is is of form (Type bv)
-       -- using unifyTypeKind
-  = tc_type_kind ty                            `thenTc` \ (actual_kind, tc_ty) ->
-    tcAddErrCtxt (typeKindCtxt ty)
-                (unifyTypeKind actual_kind)    `thenTc_`
-    returnTc tc_ty
-
-tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
-tc_type_kind ty@(HsTyVar name)
+tc_type :: RenamedHsType -> TcM Type
+
+tc_type ty@(HsTyVar name)
   = tc_app ty []
 
-tc_type_kind (HsListTy ty)
-  = tc_boxed_type ty           `thenTc` \ tau_ty ->
-    returnTc (boxedTypeKind, mkListTy tau_ty)
+tc_type (HsListTy ty)
+  = tc_type ty `thenTc` \ tau_ty ->
+    returnTc (mkListTy tau_ty)
 
-tc_type_kind (HsTupleTy (HsTupCon _ Boxed) tys)
-  = mapTc tc_boxed_type tys    `thenTc` \ tau_tys ->
-    returnTc (boxedTypeKind, mkTupleTy Boxed (length tys) tau_tys)
+tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
+  = ASSERT( tys `lengthIs` arity )
+    tc_types tys       `thenTc` \ tau_tys ->
+    returnTc (mkTupleTy boxity arity tau_tys)
 
-tc_type_kind (HsTupleTy (HsTupCon _ Unboxed) tys)
-  = mapTc tc_type tys                  `thenTc` \ tau_tys ->
-    returnTc (unboxedTypeKind, mkTupleTy Unboxed (length tys) tau_tys)
+tc_type (HsFunTy ty1 ty2)
+  = tc_type ty1                        `thenTc` \ tau_ty1 ->
+    tc_type ty2                        `thenTc` \ tau_ty2 ->
+    returnTc (mkFunTy tau_ty1 tau_ty2)
 
-tc_type_kind (HsFunTy ty1 ty2)
-  = tc_type ty1        `thenTc` \ tau_ty1 ->
-    tc_type ty2        `thenTc` \ tau_ty2 ->
-    returnTc (boxedTypeKind, mkFunTy tau_ty1 tau_ty2)
+tc_type (HsNumTy n)
+  = ASSERT(n== 1)
+    returnTc (mkTyConApp genUnitTyCon [])
 
-tc_type_kind (HsAppTy ty1 ty2)
-  = tc_app ty1 [ty2]
+tc_type (HsOpTy ty1 op ty2)
+  = tc_type ty1 `thenTc` \ tau_ty1 ->
+    tc_type ty2 `thenTc` \ tau_ty2 ->
+    tc_fun_type op [tau_ty1,tau_ty2]
 
-tc_type_kind (HsPredTy pred)
-  = tcClassAssertion True pred `thenTc` \ pred' ->
-    returnTc (boxedTypeKind, mkPredTy pred')
+tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 
-tc_type_kind (HsUsgTy usg ty)
-  = newUsg usg                          `thenTc` \ usg' ->
-    tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
-    returnTc (kind, mkUsgTy usg' tc_ty)
-  where
-    newUsg usg = case usg of
-                   HsUsOnce        -> returnTc UsOnce
-                   HsUsMany        -> returnTc UsMany
-                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
-                                        returnTc (UsVar uv)
+tc_type (HsPredTy pred)
+  = tc_pred pred       `thenTc` \ pred' ->
+    returnTc (mkPredTy pred')
 
-tc_type_kind (HsUsgForAllTy uv_name ty)
+tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
   = let
-        uv = mkNamedUVar uv_name
+       kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
     in
-    tcExtendUVarEnv uv_name uv $
-      tc_type_kind ty                     `thenTc` \ (kind, tc_ty) ->
-      returnTc (kind, mkUsForAllTy uv tc_ty)
-
-tc_type_kind full_ty@(HsForAllTy (Just tv_names) context ty)
-  = tcExtendTyVarScope tv_names                $ \ forall_tyvars ->
-    tcContext context                  `thenTc` \ theta ->
-    tc_type_kind ty                    `thenTc` \ (kind, tau) ->
-    let
-       body_kind | null theta = kind
-                 | otherwise  = boxedTypeKind
-               -- Context behaves like a function type
-               -- This matters.  Return-unboxed-tuple analysis can
-               -- give overloaded functions like
-               --      f :: forall a. Num a => (# a->a, a->a #)
-               -- And we want these to get through the type checker
-
-       -- Check for ambiguity
-       --   forall V. P => tau
-       -- is ambiguous if P contains generic variables
-       -- (i.e. one of the Vs) that are not mentioned in tau
-       --
-       -- However, we need to take account of functional dependencies
-       -- when we speak of 'mentioned in tau'.  Example:
-       --      class C a b | a -> b where ...
-       -- Then the type
-       --      forall x y. (C x y) => x
-       -- is not ambiguous because x is mentioned and x determines y
-       --
-       -- NOTE: In addition, GHC insists that at least one type variable
-       -- in each constraint is in V.  So we disallow a type like
-       --      forall a. Eq b => b -> b
-       -- even in a scope where b is in scope.
-       -- This is the is_free test below.
-
-       tau_vars            = tyVarsOfType tau
-       fds                 = instFunDepsOfTheta theta
-       tvFundep            = tyVarFunDep fds
-       extended_tau_vars   = oclose tvFundep tau_vars
-       is_ambig ct_var     = (ct_var `elem` forall_tyvars) &&
-                             not (ct_var `elemUFM` extended_tau_vars)
-       is_free ct_var      = not (ct_var `elem` forall_tyvars)
-
-       check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
-                         checkTc (not all_free)  (freeErr  pred full_ty)
-             where 
-               ct_vars   = varSetElems (tyVarsOfPred pred)
-               any_ambig = is_source_polytype && any is_ambig ct_vars
-               all_free  = all is_free  ct_vars
-
-       -- Check ambiguity only for source-program types, not
-       -- for types coming from inteface files.  The latter can
-       -- legitimately have ambiguous types. Example
-       --    class S a where s :: a -> (Int,Int)
-       --    instance S Char where s _ = (1,1)
-       --    f:: S a => [a] -> Int -> (Int,Int)
-       --    f (_::[a]) x = (a*x,b)
-       --      where (a,b) = s (undefined::a)
-       -- Here the worker for f gets the type
-       --      fw :: forall a. S a => Int -> (# Int, Int #)
-       --
-       -- If the list of tv_names is empty, we have a monotype,
-       -- and then we don't need to check for ambiguity either,
-       -- because the test can't fail (see is_ambig).
-       is_source_polytype = case tv_names of
-                               (UserTyVar _ : _) -> True
-                               other             -> False
-    in
-    mapTc check_pred theta             `thenTc_`
-    returnTc (body_kind, mkSigmaTy forall_tyvars theta tau)
+    tcHsTyVars tv_names kind_check     $ \ tyvars ->
+    mapTc tc_pred ctxt                 `thenTc` \ theta ->
+    tc_type ty                         `thenTc` \ tau ->
+    returnTc (mkSigmaTy tyvars theta tau)
+
+tc_types arg_tys = mapTc tc_type arg_tys
 \end{code}
 
 Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
+tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
 tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
-  | null tys
-  = tc_fun_type ty []
-
-  | otherwise
   = tcAddErrCtxt (appKindCtxt pp_app)  $
-    mapAndUnzipTc tc_type_kind tys     `thenTc` \ (arg_kinds, arg_tys) ->
-    tc_fun_type ty arg_tys             `thenTc` \ (fun_kind, result_ty) ->
-
-       -- Check argument compatibility
-    newKindVar                                 `thenNF_Tc` \ result_kind ->
-    unifyKind fun_kind (mkArrowKinds arg_kinds result_kind)
-                                       `thenTc_`
-    returnTc (result_kind, result_ty)
+    tc_types tys                       `thenTc` \ arg_tys ->
+    case ty of
+       HsTyVar fun -> tc_fun_type fun arg_tys
+       other       -> tc_type ty               `thenTc` \ fun_ty ->
+                      returnNF_Tc (mkAppTys fun_ty arg_tys)
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
--- (tc_fun_type ty arg_tys) returns (kind-of ty, mkAppTys ty arg_tys)
+-- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 --     hence the rather strange functionality.
 
-tc_fun_type (HsTyVar name) arg_tys
-  = tcLookupTy name                    `thenTc` \ (tycon_kind, thing) ->
+tc_fun_type name arg_tys
+  = tcLookup name                      `thenTc` \ thing ->
     case thing of
-       ATyVar tv     -> returnTc (tycon_kind, mkAppTys (mkTyVarTy tv) arg_tys)
-       AClass clas _ -> failWithTc (classAsTyConErr name)
-
-       ADataTyCon tc ->  -- Data or newtype
-                         returnTc (tycon_kind, mkTyConApp tc arg_tys)
-
-       ASynTyCon tc arity ->   -- Type synonym
-                                 checkTc (arity <= n_args) err_msg     `thenTc_`
-                                 returnTc (tycon_kind, result_ty)
-                          where
-                               -- It's OK to have an *over-applied* type synonym
-                               --      data Tree a b = ...
-                               --      type Foo a = Tree [a]
-                               --      f :: Foo a b -> ...
-                             result_ty = mkAppTys (mkSynTy tc (take arity arg_tys))
-                                                  (drop arity arg_tys)
-                             err_msg = arityErr "type synonym" name arity n_args
-                             n_args  = length arg_tys
-
-tc_fun_type ty arg_tys
-  = tc_type_kind ty            `thenTc` \ (fun_kind, fun_ty) ->
-    returnTc (fun_kind, mkAppTys fun_ty arg_tys)
+       ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
+
+       AGlobal (ATyCon tc)
+               | isSynTyCon tc ->  returnTc (mkSynTy tc arg_tys)
+               | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
+
+       other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
 
 
 Contexts
 ~~~~~~~~
 \begin{code}
-
-tcContext :: RenamedContext -> TcM s ThetaType
-tcContext context = mapTc (tcClassAssertion False) context
-
-tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
+tc_pred assn@(HsClassP class_name tys)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
-    mapAndUnzipTc tc_type_kind tys             `thenTc` \ (arg_kinds, arg_tys) ->
-    tcLookupTy class_name                      `thenTc` \ (kind, thing) ->
+    tc_types tys                       `thenTc` \ arg_tys ->
+    tcLookupGlobal class_name                  `thenTc` \ thing ->
     case thing of
-       AClass clas arity ->
-                       -- Check with kind mis-match
-               checkTc (arity == n_tys) err                            `thenTc_`
-               unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)   `thenTc_`
-               returnTc (Class clas arg_tys)
-           where
-               n_tys = length tys
-               err   = arityErr "Class" class_name arity n_tys
-       other -> failWithTc (tyVarAsClassErr class_name)
-
-tcClassAssertion ccall_ok assn@(HsPIParam name ty)
+       AClass clas -> returnTc (ClassP clas arg_tys)
+       other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
+
+tc_pred assn@(HsIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
-    tc_type_kind ty    `thenTc` \ (arg_kind, arg_ty) ->
+    tc_type ty                                 `thenTc` \ arg_ty ->
     returnTc (IParam name arg_ty)
 \end{code}
 
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Type variables, with knot tying!}
@@ -361,38 +500,16 @@ tcClassAssertion ccall_ok assn@(HsPIParam name ty)
 %************************************************************************
 
 \begin{code}
-tcExtendTopTyVarScope :: TcKind -> [HsTyVarBndr Name]
-                     -> ([TcTyVar] -> TcKind -> TcM s a)
-                     -> TcM s a
-tcExtendTopTyVarScope kind tyvar_names thing_inside
-  = let
-       (tyvars_w_kinds, result_kind) = zipFunTys tyvar_names kind
-       tyvars                        = map mk_tv tyvars_w_kinds
-    in
-    tcExtendTyVarEnv tyvars (thing_inside tyvars result_kind)  
+mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
+mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
+
+mkTyClTyVars :: Kind                   -- Kind of the tycon or class
+            -> [HsTyVarBndr Name]
+            -> [TyVar]
+mkTyClTyVars kind tyvar_names
+  = mkImmutTyVars tyvars_w_kinds
   where
-    mk_tv (UserTyVar name,    kind) = mkTyVar name kind
-    mk_tv (IfaceTyVar name _, kind) = mkTyVar name kind
-       -- NB: immutable tyvars, but perhaps with mutable kinds
-
-tcExtendTyVarScope :: [HsTyVarBndr Name] 
-                  -> ([TcTyVar] -> TcM s a) -> TcM s a
-tcExtendTyVarScope tv_names thing_inside
-  = mapNF_Tc tcHsTyVar tv_names        `thenNF_Tc` \ tyvars ->
-    tcExtendTyVarEnv tyvars            $
-    thing_inside tyvars
-    
-tcHsTyVar :: HsTyVarBndr Name -> NF_TcM s TcTyVar
-tcHsTyVar (UserTyVar name)       = newKindVar          `thenNF_Tc` \ kind ->
-                                  tcNewMutTyVar name kind
-       -- NB: mutable kind => mutable tyvar, so that zonking can bind
-       -- the tyvar to its immutable form
-
-tcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (mkTyVar name (kindToTcKind kind))
-
-kcHsTyVar :: HsTyVarBndr name -> NF_TcM s TcKind
-kcHsTyVar (UserTyVar name)       = newKindVar
-kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (kindToTcKind kind)
+    (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
 \end{code}
 
 
@@ -446,16 +563,15 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 
 
 \begin{code}
-tcTySig :: RenamedSig -> TcM s TcSigInfo
+tcTySig :: RenamedSig -> TcM TcSigInfo
 
 tcTySig (Sig v ty src_loc)
  = tcAddSrcLoc src_loc                         $ 
-   tcAddErrCtxt (tcsigCtxt v)                  $
-   tcHsSigType ty                              `thenTc` \ sigma_tc_ty ->
-   mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig -> 
+   tcHsSigType (FunSigCtxt v) ty               `thenTc` \ sigma_tc_ty ->
+   mkTcSig (mkLocalId v sigma_tc_ty) src_loc   `thenNF_Tc` \ sig -> 
    returnTc sig
 
-mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
+mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
 mkTcSig poly_id src_loc
   =    -- Instantiate this type
        -- It's important to do this even though in the error-free case
@@ -465,16 +581,17 @@ mkTcSig poly_id src_loc
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
    let
-       (tyvars, rho) = splitForAllTys (idType poly_id)
+       (tyvars, rho) = tcSplitForAllTys (idType poly_id)
    in
-   mapNF_Tc tcInstSigVar tyvars                `thenNF_Tc` \ tyvars' ->
+   tcInstSigTyVars SigTv tyvars                        `thenNF_Tc` \ tyvars' ->
        -- Make *signature* type variables
 
    let
      tyvar_tys' = mkTyVarTys tyvars'
      rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
        -- mkTopTyVarSubst because the tyvars' are fresh
-     (theta', tau') = splitRhoTy rho'
+
+     (theta', tau') = tcSplitRhoTy rho'
        -- This splitRhoTy tries hard to make sure that tau' is a type synonym
        -- wherever possible, which can improve interface files.
    in
@@ -483,9 +600,8 @@ mkTcSig poly_id src_loc
                tyvar_tys'
                theta' tau'                     `thenNF_Tc` \ inst ->
        -- We make a Method even if it's not overloaded; no harm
-   instFunDeps SignatureOrigin theta'          `thenNF_Tc` \ fds ->
        
-   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) (inst : fds) src_loc)
+   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
   where
     name = idName poly_id
 \end{code}
@@ -557,114 +673,134 @@ give a helpful message in checkSigTyVars.
 \begin{code}
 checkSigTyVars :: [TcTyVar]            -- Universally-quantified type variables in the signature
               -> TcTyVarSet            -- Tyvars that are free in the type signature
-                                       -- These should *already* be in the global-var set, and are
-                                       -- used here only to improve the error message
-              -> TcM s [TcTyVar]       -- Zonked signature type variables
+                                       --      Not necessarily zonked
+                                       --      These should *already* be in the free-in-env set, 
+                                       --      and are used here only to improve the error message
+              -> TcM [TcTyVar]         -- Zonked signature type variables
 
 checkSigTyVars [] free = returnTc []
-
 checkSigTyVars sig_tyvars free_tyvars
   = zonkTcTyVars sig_tyvars            `thenNF_Tc` \ sig_tys ->
     tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
 
-    checkTcM (all_ok sig_tys globals)
+    checkTcM (allDistinctTyVars sig_tys globals)
             (complain sig_tys globals) `thenTc_`
 
-    returnTc (map (getTyVar "checkSigTyVars") sig_tys)
+    returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
 
   where
-    all_ok []       acc = True
-    all_ok (ty:tys) acc = case getTyVar_maybe ty of
-                           Nothing                       -> False      -- Point (a)
-                           Just tv | tv `elemVarSet` acc -> False      -- Point (b) or (c)
-                                   | otherwise           -> all_ok tys (acc `extendVarSet` tv)
-    
-
     complain sig_tys globals
-      = -- For the in-scope ones, zonk them and construct a map
-       -- from the zonked tyvar to the in-scope one
-       -- If any of the in-scope tyvars zonk to a type, then ignore them;
-       -- that'll be caught later when we back up to their type sig
-       tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
-       zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
-       let
-           in_scope_assoc = [ (zonked_tv, in_scope_tv) 
-                            | (z_ty, in_scope_tv) <- in_scope_tys `zip` in_scope_tvs,
-                              Just zonked_tv <- [getTyVar_maybe z_ty]
-                            ]
-           in_scope_env = mkVarEnv in_scope_assoc
-       in
-
-       -- "check" checks each sig tyvar in turn
+      = -- "check" checks each sig tyvar in turn
         foldlNF_Tc check
-                  (env2, in_scope_env, [])
+                  (env2, emptyVarEnv, [])
                   (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
 
-        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
+        failWithTcM (env3, main_msg $$ vcat msgs)
       where
-       (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
-       (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
+       (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars
+       (env2, tidy_tys) = tidyOpenTypes  env1         sig_tys
 
        main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
 
-       check (env, acc, msgs) (sig_tyvar,ty)
+       check (tidy_env, acc, msgs) (sig_tyvar,ty)
                -- sig_tyvar is from the signature;
                -- ty is what you get if you zonk sig_tyvar and then tidy it
                --
                -- acc maps a zonked type variable back to a signature type variable
-         = case getTyVar_maybe ty of {
+         = case tcGetTyVar_maybe ty of {
              Nothing ->                        -- Error (a)!
-                       returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr ty) : msgs) ;
+                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
 
              Just tv ->
 
            case lookupVarEnv acc tv of {
-               Just sig_tyvar' ->      -- Error (b) or (d)!
-                       returnNF_Tc (env, acc, unify_msg sig_tyvar (ppr sig_tyvar') : msgs) ;
+               Just sig_tyvar' ->      -- Error (b)!
+                       returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
+                   where
+                       thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
 
-               Nothing ->
+             ; Nothing ->
 
-           if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
+           if tv `elemVarSet` globals  -- Error (c) or (d)! Type variable escapes
                                        -- The least comprehensible, so put it last
-           then   tcGetValueEnv                                        `thenNF_Tc` \ ve ->
-                  find_globals tv env  [] (valueEnvIds ve)             `thenNF_Tc` \ (env1, globs) ->
-                  find_frees   tv env1 [] (varSetElems free_tyvars)    `thenNF_Tc` \ (env2, frees) ->
-                  returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
+                       -- Game plan: 
+                       --    a) get the local TcIds and TyVars from the environment,
+                       --       and pass them to find_globals (they might have tv free)
+                       --    b) similarly, find any free_tyvars that mention tv
+           then   tcGetEnv                                                     `thenNF_Tc` \ ve ->
+                  find_globals tv tidy_env  (tcLEnvElts ve)                    `thenNF_Tc` \ (tidy_env1, globs) ->
+                  find_frees   tv tidy_env1 [] (varSetElems free_tyvars)       `thenNF_Tc` \ (tidy_env2, frees) ->
+                  returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 
            else        -- All OK
-           returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
+           returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
            }}
 
+-----------------------
 -- find_globals looks at the value environment and finds values
 -- whose types mention the offending type variable.  It has to be 
 -- careful to zonk the Id's type first, so it has to be in the monad.
 -- We must be careful to pass it a zonked type variable, too.
-find_globals tv tidy_env acc []
-  = returnNF_Tc (tidy_env, acc)
 
-find_globals tv tidy_env acc (id:ids) 
-  | not (isLocallyDefined id) ||
-    isEmptyVarSet (idFreeTyVars id)
-  = find_globals tv tidy_env acc ids
-
-  | otherwise
-  = zonkTcType (idType id)     `thenNF_Tc` \ id_ty ->
-    if tv `elemVarSet` tyVarsOfType id_ty then
-       let 
-          (tidy_env', id_ty') = tidyOpenType tidy_env id_ty
-          acc'                = (idName id, id_ty') : acc
-       in
-       find_globals tv tidy_env' acc' ids
-    else
-       find_globals tv tidy_env  acc  ids
+find_globals :: Var 
+             -> TidyEnv 
+             -> [TcTyThing] 
+             -> NF_TcM (TidyEnv, [SDoc])
+
+find_globals tv tidy_env things
+  = go tidy_env [] things
+  where
+    go tidy_env acc [] = returnNF_Tc (tidy_env, acc)
+    go tidy_env acc (thing : things)
+      = find_thing ignore_it tidy_env thing    `thenNF_Tc` \ (tidy_env1, maybe_doc) ->
+       case maybe_doc of
+         Just d  -> go tidy_env1 (d:acc) things
+         Nothing -> go tidy_env1 acc     things
+
+    ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty)
+
+-----------------------
+find_thing ignore_it tidy_env (ATcId id)
+  = zonkTcType  (idType id)    `thenNF_Tc` \ id_ty ->
+    if ignore_it id_ty then
+       returnNF_Tc (tidy_env, Nothing)
+    else let
+       (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty
+       msg = sep [ppr id <+> dcolon <+> ppr tidy_ty, 
+                  nest 2 (parens (ptext SLIT("bound at") <+>
+                                  ppr (getSrcLoc id)))]
+    in
+    returnNF_Tc (tidy_env', Just msg)
+
+find_thing ignore_it tidy_env (ATyVar tv)
+  = zonkTcTyVar tv             `thenNF_Tc` \ tv_ty ->
+    if ignore_it tv_ty then
+       returnNF_Tc (tidy_env, Nothing)
+    else let
+       (tidy_env1, tv1)     = tidyOpenTyVar tidy_env  tv
+       (tidy_env2, tidy_ty) = tidyOpenType  tidy_env1 tv_ty
+       msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at]
+
+       eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty
+                | otherwise                                        = equals <+> ppr tv_ty
+               -- It's ok to use Type.getTyVar_maybe because ty is zonked by now
+       
+       bound_at | isMutTyVar tv = mut_info     -- The expected case
+                | otherwise     = empty
+       
+       mut_info = sep [ptext SLIT("is bound by the") <+> ppr (mutTyVarDetails tv),
+                       ptext SLIT("at") <+> ppr (getSrcLoc tv)]
+    in
+    returnNF_Tc (tidy_env2, Just msg)
 
+-----------------------
 find_frees tv tidy_env acc []
   = returnNF_Tc (tidy_env, acc)
 find_frees tv tidy_env acc (ftv:ftvs)
   = zonkTcTyVar ftv    `thenNF_Tc` \ ty ->
     if tv `elemVarSet` tyVarsOfType ty then
        let
-           (tidy_env', ftv') = tidyTyVar tidy_env ftv
+           (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv
        in
        find_frees tv tidy_env' (ftv':acc) ftvs
     else
@@ -674,10 +810,8 @@ find_frees tv tidy_env acc (ftv:ftvs)
 escape_msg sig_tv tv globs frees
   = mk_msg sig_tv <+> ptext SLIT("escapes") $$
     if not (null globs) then
-       vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
-             ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
-             nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
-       ]
+       vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), 
+             nest 2 (vcat globs)]
      else if not (null frees) then
        vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
              nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
@@ -696,7 +830,8 @@ escape_msg sig_tv tv globs frees
     vcat_first 0 (x:xs) = text "...others omitted..."
     vcat_first n (x:xs) = x $$ vcat_first (n-1) xs
 
-unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> quotes thing
+
+unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
 mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
 \end{code}
 
@@ -704,13 +839,13 @@ These two context are used with checkSigTyVars
     
 \begin{code}
 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
-       -> TidyEnv -> NF_TcM s (TidyEnv, Message)
+       -> TidyEnv -> NF_TcM (TidyEnv, Message)
 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
   = zonkTcType sig_tau         `thenNF_Tc` \ actual_tau ->
     let
-       (env1, tidy_sig_tyvars)  = tidyTyVars tidy_env sig_tyvars
+       (env1, tidy_sig_tyvars)  = tidyOpenTyVars tidy_env sig_tyvars
        (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
-       (env3, tidy_actual_tau)  = tidyOpenType env1 actual_tau
+       (env3, tidy_actual_tau)  = tidyOpenType env2 actual_tau
        msg = vcat [ptext SLIT("Signature type:    ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
                    ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
                    when
@@ -739,10 +874,6 @@ sigPatCtxt bound_tvs bound_ids tidy_env
 %************************************************************************
 
 \begin{code}
-tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
-
-typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
-
 typeKindCtxt :: RenamedHsType -> Message
 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
                       nest 2 (quotes (ppr ty)),
@@ -751,23 +882,13 @@ typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 appKindCtxt :: SDoc -> Message
 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 
-classAsTyConErr name
-  = ptext SLIT("Class used as a type constructor:") <+> ppr name
-
-tyConAsClassErr name
-  = ptext SLIT("Type constructor used as a class:") <+> ppr name
-
-tyVarAsClassErr name
-  = ptext SLIT("Type variable used as a class:") <+> ppr name
-
-ambigErr pred ty
-  = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
-        nest 4 (ptext SLIT("for the type:") <+> ppr ty),
-        nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>"))]
-
-freeErr pred ty
-  = sep [ptext SLIT("The constraint") <+> quotes (pprPred pred) <+>
-                  ptext SLIT("does not mention any of the universally quantified type variables"),
-        nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
-    ]
+wrongThingErr expected thing name
+  = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
+  where
+    pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
+    pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
+    pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
+    pp_thing (ATyVar _)          = ptext SLIT("Type variable")
+    pp_thing (ATcId _)           = ptext SLIT("Local identifier")
+    pp_thing (AThing _)          = ptext SLIT("Utterly bogus")
 \end{code}