[project @ 2002-11-19 09:37:08 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index d57b53b..fb575ab 100644 (file)
@@ -4,66 +4,58 @@
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
 
 \begin{code}
-module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, 
+module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred,
                    UserTypeCtxt(..),
 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsSigTypes, 
                    kcHsLiftedSigType, kcHsContext,
                    UserTypeCtxt(..),
 
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsSigTypes, 
                    kcHsLiftedSigType, kcHsContext,
-                   tcScopedTyVars, tcHsTyVars, mkImmutTyVars,
+                   tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
 
-                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
-                   checkSigTyVars, sigCtxt, sigPatCtxt
+                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
                  ) where
 
 #include "HsVersions.h"
 
                  ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVarBndr(..),
+import HsSyn           ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
                           Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
-import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
+import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
 import TcHsSyn         ( TcId )
 
 import TcHsSyn         ( TcId )
 
-import TcMonad
+import TcRnMonad
 import TcEnv           ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
 import TcEnv           ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
-                         tcGetGlobalTyVars, tcEnvTcIds, tcEnvTyVars,
-                         TyThing(..), TcTyThing(..), tcExtendKindEnv
+                         TyThing(..), TcTyThing(..), tcExtendKindEnv,
+                         getInLocalScope
                        )
                        )
-import TcMType         ( newKindVar, tcInstSigVars, 
-                         zonkKindEnv, zonkTcType, zonkTcTyVars, zonkTcTyVar,
-                         unifyKind, unifyOpenTypeKind,
+import TcMType         ( newMutTyVar, newKindVar, zonkKindEnv, tcInstType,
                          checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
                        )
                          checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
                        )
-import TcType          ( Type, Kind, SourceType(..), ThetaType,
-                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
-                         tcSplitForAllTys, tcSplitRhoTy,
-                         hoistForAllTys, allDistinctTyVars,
-                          zipFunTys, 
-                         mkSigmaTy, mkPredTy, mkTyConApp,
-                         mkAppTys, mkRhoTy,
+import TcUnify         ( unifyKind, unifyOpenTypeKind )
+import TcType          ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
+                         TcTyVar, TcKind, TcThetaType, TcTauType,
+                         mkTyVarTy, mkTyVarTys, mkFunTy, 
+                         zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
+                         mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
                          liftedTypeKind, unliftedTypeKind, mkArrowKind,
                          liftedTypeKind, unliftedTypeKind, mkArrowKind,
-                         mkArrowKinds, tcGetTyVar_maybe, tcGetTyVar, tcSplitFunTy_maybe,
-                         tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-                         tyVarsOfType, mkForAllTys
+                         mkArrowKinds, tcSplitFunTy_maybe, tcSplitForAllTys
                        )
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
-import PprType         ( pprType )
-import Subst           ( mkTopTyVarSubst, substTy )
-import CoreFVs         ( idFreeTyVars )
+import Inst            ( Inst, InstOrigin(..), newMethodWith, instToId )
+
 import Id              ( mkLocalId, idName, idType )
 import Id              ( mkLocalId, idName, idType )
-import Var             ( Id, Var, TyVar, mkTyVar, tyVarKind )
-import VarEnv
-import VarSet
+import Var             ( TyVar, mkTyVar, tyVarKind )
 import ErrUtils                ( Message )
 import ErrUtils                ( Message )
-import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind )
+import TyCon           ( TyCon, tyConKind )
 import Class           ( classTyCon )
 import Name            ( Name )
 import Class           ( classTyCon )
 import Name            ( Name )
-import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
+import NameSet
+import Subst           ( deShadowTy )
+import TysWiredIn      ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
-import Util            ( mapAccumL, isSingleton )
+import Util            ( lengthIs )
 import Outputable
 import Outputable
-
+import List            ( nubBy )
 \end{code}
 
 
 \end{code}
 
 
@@ -77,7 +69,7 @@ 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]
 
        1.  Kind check the HsType [kcHsType]
        2.  Convert from HsType to Type, and hoist the foralls [tcHsType]
-       3.  Check the validity of the resultint type [checkValidType]
+       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
 
 Often these steps are done one after the othe (tcHsSigType).
 But in mutually recursive groups of type and class decls we do
@@ -88,12 +80,12 @@ But in mutually recursive groups of type and class decls we do
 \begin{code}
 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
   -- Do kind checking, and hoist for-alls to the top
 \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_`
+tcHsSigType ctxt ty = addErrCtxt (checkTypeCtxt ctxt ty) (
+                       kcTypeType ty           `thenM_`
                        tcHsType ty
                        tcHsType ty
-                     )                         `thenTc` \ ty' ->
-                     checkValidType ctxt ty'   `thenTc_`
-                     returnTc ty'
+                     )                         `thenM` \ ty' ->
+                     checkValidType ctxt ty'   `thenM_`
+                     returnM ty'
 
 checkTypeCtxt ctxt ty
   = vcat [ptext SLIT("In the type:") <+> ppr ty,
 
 checkTypeCtxt ctxt ty
   = vcat [ptext SLIT("In the type:") <+> ppr ty,
@@ -105,13 +97,13 @@ tcHsType    :: RenamedHsType -> TcM Type
   -- 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.]
   -- 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')
+tcHsType ty = tc_type ty  `thenM` \ ty' ->  
+             returnM (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 :: 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
+tcHsTheta hs_theta = mappM tc_pred hs_theta
 
 -- In interface files the type is already kinded,
 -- and we definitely don't want to hoist for-alls.
 
 -- In interface files the type is already kinded,
 -- and we definitely don't want to hoist for-alls.
@@ -186,155 +178,203 @@ tcHsTyVars [] kind_check thing_inside = thing_inside []
        -- A useful short cut for a common case!
   
 tcHsTyVars tv_names kind_check 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 ->
+  = kcHsTyVars tv_names                                `thenM` \ tv_names_w_kinds ->
+    tcExtendKindEnv tv_names_w_kinds kind_check                `thenM_`
+    zonkKindEnv tv_names_w_kinds                       `thenM` \ tvs_w_kinds ->
     let
        tyvars = mkImmutTyVars tvs_w_kinds
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
     let
        tyvars = mkImmutTyVars tvs_w_kinds
     in
     tcExtendTyVarEnv tyvars (thing_inside tyvars)
 
--- tcScopedTyVars is used for scoped type variables
+
+
+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)
 --     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)
-tcScopedTyVars :: [Name] 
-              -> TcM a                         -- The kind checker
-              -> TcM b
-              -> TcM b
-tcScopedTyVars [] kind_check thing_inside = thing_inside
-
-tcScopedTyVars tv_names kind_check thing_inside
-  = mapNF_Tc newNamedKindVar tv_names          `thenTc` \ kind_env ->
-    tcExtendKindEnv kind_env kind_check                `thenTc_`
-    zonkKindEnv kind_env                       `thenNF_Tc` \ tvs_w_kinds ->
-    listTc [tcNewMutTyVar name kind | (name, kind) <- tvs_w_kinds]     `thenNF_Tc` \ tyvars ->
+
+-- Find the not-already-in-scope signature type variables,
+-- kind-check them, and bring them into scope
+--
+-- 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
+  = getInLocalScope                    `thenM` \ in_scope ->
+    let
+       all_sig_tvs     = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
+       sig_tvs         = filter (not . in_scope) (nameSetToList all_sig_tvs)
+    in       
+    mappM newNamedKindVar sig_tvs                      `thenM` \ kind_env ->
+    tcExtendKindEnv kind_env (kcHsSigTypes sig_tys)    `thenM_`
+    zonkKindEnv kind_env                               `thenM` \ tvs_w_kinds ->
+    sequenceM [ newMutTyVar name kind PatSigTv
+             | (name, kind) <- tvs_w_kinds]            `thenM` \ tyvars ->
     tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
 
 \begin{code}
     tcExtendTyVarEnv tyvars thing_inside
 \end{code}
     
 
 \begin{code}
-kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
-kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
+kcHsTyVar  :: HsTyVarBndr name   -> TcM (name, TcKind)
+kcHsTyVars :: [HsTyVarBndr name] -> TcM [(name, TcKind)]
 
 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
 
 kcHsTyVar (UserTyVar name)       = newNamedKindVar name
-kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
+kcHsTyVar (IfaceTyVar name kind) = returnM (name, kind)
 
 
-kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
+kcHsTyVars tvs = mappM kcHsTyVar tvs
 
 
-newNamedKindVar name = newKindVar      `thenNF_Tc` \ kind ->
-                      returnNF_Tc (name, kind)
+newNamedKindVar name = newKindVar      `thenM` \ kind ->
+                      returnM (name, kind)
 
 ---------------------------
 kcLiftedType :: RenamedHsType -> TcM ()
        -- The type ty must be a *lifted* *type*
 kcLiftedType ty
 
 ---------------------------
 kcLiftedType :: RenamedHsType -> TcM ()
        -- The type ty must be a *lifted* *type*
 kcLiftedType ty
-  = kcHsType ty                                `thenTc` \ kind ->
-    tcAddErrCtxt (typeKindCtxt ty)     $
+  = kcHsType ty                                `thenM` \ kind ->
+    addErrCtxt (typeKindCtxt ty)       $
     unifyKind liftedTypeKind kind
     
 ---------------------------
 kcTypeType :: RenamedHsType -> TcM ()
        -- The type ty must be a *type*, but it can be lifted or unlifted.
 kcTypeType 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)     $
+  = kcHsType ty                                `thenM` \ kind ->
+    addErrCtxt (typeKindCtxt ty)       $
     unifyOpenTypeKind kind
 
 ---------------------------
 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
        -- Used for type signatures
 kcHsSigType      = kcTypeType
     unifyOpenTypeKind kind
 
 ---------------------------
 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
        -- Used for type signatures
 kcHsSigType      = kcTypeType
-kcHsSigTypes tys  = mapTc_ kcHsSigType tys
+kcHsSigTypes tys  = mappM_ kcHsSigType tys
 kcHsLiftedSigType = kcLiftedType
 
 ---------------------------
 kcHsType :: RenamedHsType -> TcM TcKind
 kcHsType (HsTyVar name)              = kcTyVar name
 
 kcHsLiftedSigType = kcLiftedType
 
 ---------------------------
 kcHsType :: RenamedHsType -> TcM TcKind
 kcHsType (HsTyVar name)              = kcTyVar name
 
+kcHsType (HsKindSig ty k)
+  = kcHsType ty                        `thenM` \ k' ->
+    unifyKind k k'             `thenM_`
+    returnM k
+
 kcHsType (HsListTy ty)
 kcHsType (HsListTy ty)
-  = kcLiftedType ty            `thenTc` \ tau_ty ->
-    returnTc liftedTypeKind
+  = kcLiftedType ty            `thenM` \ tau_ty ->
+    returnM liftedTypeKind
 
 
-kcHsType (HsTupleTy (HsTupCon _ boxity _) tys)
-  = mapTc kcTypeType tys       `thenTc_`
-    returnTc (case boxity of
+kcHsType (HsPArrTy ty)
+  = kcLiftedType ty            `thenM` \ tau_ty ->
+    returnM liftedTypeKind
+
+kcHsType (HsTupleTy (HsTupCon boxity _) tys)
+  = mappM kcTypeType tys       `thenM_`
+    returnM (case boxity of
                  Boxed   -> liftedTypeKind
                  Unboxed -> unliftedTypeKind)
 
 kcHsType (HsFunTy ty1 ty2)
                  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' ->
+  = kcTypeType ty1     `thenM_`
+    kcTypeType ty2     `thenM_`
+    returnM liftedTypeKind
+
+kcHsType (HsOpTy ty1 HsArrow ty2)
+  = kcTypeType ty1     `thenM_`
+    kcTypeType ty2     `thenM_`
+    returnM liftedTypeKind
+
+kcHsType ty@(HsOpTy ty1 (HsTyOp op) ty2)
+  = kcTyVar op                         `thenM` \ op_kind ->
+    kcHsType ty1                       `thenM` \ ty1_kind ->
+    kcHsType ty2                       `thenM` \ ty2_kind ->
+    addErrCtxt (appKindCtxt (ppr ty))  $
+    kcAppKind op_kind  ty1_kind                `thenM` \ op_kind' ->
     kcAppKind op_kind' ty2_kind
     kcAppKind op_kind' ty2_kind
+
+kcHsType (HsParTy ty)          -- Skip parentheses markers
+  = kcHsType ty
    
    
+kcHsType (HsNumTy _)           -- The unit type for generics
+  = returnM liftedTypeKind
+
 kcHsType (HsPredTy pred)
 kcHsType (HsPredTy pred)
-  = kcHsPred pred              `thenTc_`
-    returnTc liftedTypeKind
+  = kcHsPred pred              `thenM_`
+    returnM liftedTypeKind
 
 kcHsType ty@(HsAppTy ty1 ty2)
 
 kcHsType ty@(HsAppTy ty1 ty2)
-  = kcHsType ty1                       `thenTc` \ tc_kind ->
-    kcHsType ty2                       `thenTc` \ arg_kind ->
-    tcAddErrCtxt (appKindCtxt (ppr ty))        $
+  = kcHsType ty1                       `thenM` \ tc_kind ->
+    kcHsType ty2                       `thenM` \ arg_kind ->
+    addErrCtxt (appKindCtxt (ppr ty))  $
     kcAppKind tc_kind arg_kind
 
 kcHsType (HsForAllTy (Just tv_names) context ty)
     kcAppKind tc_kind arg_kind
 
 kcHsType (HsForAllTy (Just tv_names) context ty)
-  = kcHsTyVars tv_names                `thenNF_Tc` \ kind_env ->
+  = kcHsTyVars tv_names                `thenM` \ kind_env ->
     tcExtendKindEnv kind_env   $
     tcExtendKindEnv kind_env   $
-    kcHsContext context                `thenTc_`
-    kcHsType ty                        `thenTc_`
-    returnTc liftedTypeKind
+    kcHsContext context                `thenM_`
+    kcLiftedType ty            `thenM_`
+       -- The body of a forall must be of kind *
+       -- In principle, I suppose, we could allow unlifted types,
+       -- but it seems simpler to stick to lifted types for now.
+    returnM liftedTypeKind
 
 ---------------------------
 kcAppKind fun_kind arg_kind
   = case tcSplitFunTy_maybe fun_kind of 
        Just (arg_kind', res_kind)
 
 ---------------------------
 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
+               -> unifyKind arg_kind arg_kind' `thenM_`
+                  returnM res_kind
 
 
-       Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
-                  unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
-                  returnTc res_kind
+       Nothing -> newKindVar                                           `thenM` \ res_kind ->
+                  unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenM_`
+                  returnM res_kind
 
 
 ---------------------------
 
 
 ---------------------------
-kcHsContext ctxt = mapTc_ kcHsPred ctxt
+kc_pred :: RenamedHsPred -> TcM TcKind -- Does *not* check for a saturated
+                                       -- application (reason: used from TcDeriv)
+kc_pred pred@(HsIParam name ty)
+  = kcHsType ty
+
+kc_pred pred@(HsClassP cls tys)
+  = kcClass cls                                `thenM` \ kind ->
+    mappM kcHsType tys                 `thenM` \ arg_kinds ->
+    newKindVar                                 `thenM` \ kv -> 
+    unifyKind kind (mkArrowKinds arg_kinds kv) `thenM_` 
+    returnM kv
 
 
-kcHsPred :: RenamedHsPred -> TcM ()
-kcHsPred pred@(HsIParam name ty)
-  = tcAddErrCtxt (appKindCtxt (ppr pred))      $
-    kcLiftedType ty
+---------------------------
+kcHsContext ctxt = mappM_ kcHsPred ctxt
 
 
-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)
+kcHsPred pred          -- Checks that the result is of kind liftedType
+  = addErrCtxt (appKindCtxt (ppr pred))        $
+    kc_pred pred                               `thenM` \ kind ->
+    unifyKind liftedTypeKind kind              `thenM_`
+    returnM ()
+    
 
  ---------------------------
 kcTyVar name   -- Could be a tyvar or a tycon
 
  ---------------------------
 kcTyVar name   -- Could be a tyvar or a tycon
-  = tcLookup name      `thenTc` \ thing ->
+  = tcLookup name      `thenM` \ thing ->
     case thing of 
     case thing of 
-       AThing kind         -> returnTc kind
-       ATyVar tv           -> returnTc (tyVarKind tv)
-       AGlobal (ATyCon tc) -> returnTc (tyConKind tc) 
+       AThing kind         -> returnM kind
+       ATyVar tv           -> returnM (tyVarKind tv)
+       AGlobal (ATyCon tc) -> returnM (tyConKind tc) 
        other               -> failWithTc (wrongThingErr "type" thing name)
 
 kcClass cls    -- Must be a class
        other               -> failWithTc (wrongThingErr "type" thing name)
 
 kcClass cls    -- Must be a class
-  = tcLookup cls                               `thenNF_Tc` \ thing -> 
+  = tcLookup cls                               `thenM` \ thing -> 
     case thing of
     case thing of
-       AThing kind           -> returnTc kind
-       AGlobal (AClass cls)  -> returnTc (tyConKind (classTyCon cls))
+       AThing kind           -> returnM kind
+       AGlobal (AClass cls)  -> returnM (tyConKind (classTyCon cls))
        other                 -> failWithTc (wrongThingErr "class" thing cls)
 \end{code}
 
        other                 -> failWithTc (wrongThingErr "class" thing cls)
 \end{code}
 
@@ -376,45 +416,60 @@ tc_type :: RenamedHsType -> TcM Type
 tc_type ty@(HsTyVar name)
   = tc_app ty []
 
 tc_type ty@(HsTyVar name)
   = tc_app ty []
 
+tc_type (HsKindSig ty k)
+  = tc_type ty -- Kind checking done already
+
 tc_type (HsListTy ty)
 tc_type (HsListTy ty)
-  = tc_type ty `thenTc` \ tau_ty ->
-    returnTc (mkListTy tau_ty)
+  = tc_type ty `thenM` \ tau_ty ->
+    returnM (mkListTy tau_ty)
 
 
-tc_type (HsTupleTy (HsTupCon _ boxity arity) tys)
-  = ASSERT( arity == length tys )
-    tc_types tys       `thenTc` \ tau_tys ->
-    returnTc (mkTupleTy boxity arity tau_tys)
+tc_type (HsPArrTy ty)
+  = tc_type ty `thenM` \ tau_ty ->
+    returnM (mkPArrTy tau_ty)
+
+tc_type (HsTupleTy (HsTupCon boxity arity) tys)
+  = ASSERT( tys `lengthIs` arity )
+    tc_types tys       `thenM` \ tau_tys ->
+    returnM (mkTupleTy boxity arity tau_tys)
 
 tc_type (HsFunTy ty1 ty2)
 
 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 ty1                        `thenM` \ tau_ty1 ->
+    tc_type ty2                        `thenM` \ tau_ty2 ->
+    returnM (mkFunTy tau_ty1 tau_ty2)
+
+tc_type (HsOpTy ty1 HsArrow ty2)
+  = tc_type ty1 `thenM` \ tau_ty1 ->
+    tc_type ty2 `thenM` \ tau_ty2 ->
+    returnM (mkFunTy tau_ty1 tau_ty2)
+
+tc_type (HsOpTy ty1 (HsTyOp op) ty2)
+  = tc_type ty1 `thenM` \ tau_ty1 ->
+    tc_type ty2 `thenM` \ tau_ty2 ->
+    tc_fun_type op [tau_ty1,tau_ty2]
+
+tc_type (HsParTy ty)           -- Remove the parentheses markers
+  = tc_type ty
 
 tc_type (HsNumTy n)
   = ASSERT(n== 1)
 
 tc_type (HsNumTy n)
   = ASSERT(n== 1)
-    returnTc (mkTyConApp genUnitTyCon [])
-
-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]
+    returnM (mkTyConApp genUnitTyCon [])
 
 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 
 tc_type (HsPredTy pred)
 
 tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
 
 tc_type (HsPredTy pred)
-  = tc_pred pred       `thenTc` \ pred' ->
-    returnTc (mkPredTy pred')
+  = tc_pred pred       `thenM` \ pred' ->
+    returnM (mkPredTy pred')
 
 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
   = let
 
 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
   = let
-       kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
+       kind_check = kcHsContext ctxt `thenM_` kcHsType ty
     in
     tcHsTyVars tv_names kind_check     $ \ tyvars ->
     in
     tcHsTyVars tv_names kind_check     $ \ tyvars ->
-    mapTc tc_pred ctxt                 `thenTc` \ theta ->
-    tc_type ty                         `thenTc` \ tau ->
-    returnTc (mkSigmaTy tyvars theta tau)
+    mappM tc_pred ctxt                 `thenM` \ theta ->
+    tc_type ty                         `thenM` \ tau ->
+    returnM (mkSigmaTy tyvars theta tau)
 
 
-tc_types arg_tys = mapTc tc_type arg_tys
+tc_types arg_tys = mappM tc_type arg_tys
 \end{code}
 
 Help functions for type applications
 \end{code}
 
 Help functions for type applications
@@ -426,12 +481,12 @@ tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
-  = tcAddErrCtxt (appKindCtxt pp_app)  $
-    tc_types tys                       `thenTc` \ arg_tys ->
+  = addErrCtxt (appKindCtxt pp_app)    $
+    tc_types tys                       `thenM` \ arg_tys ->
     case ty of
        HsTyVar fun -> tc_fun_type fun 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)
+       other       -> tc_type ty               `thenM` \ fun_ty ->
+                      returnM (mkAppTys fun_ty arg_tys)
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
@@ -440,17 +495,11 @@ tc_app ty tys
 --     hence the rather strange functionality.
 
 tc_fun_type name arg_tys
 --     hence the rather strange functionality.
 
 tc_fun_type name arg_tys
-  = tcLookup name                      `thenTc` \ thing ->
+  = tcLookup name                      `thenM` \ thing ->
     case thing of
     case thing of
-       ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
-
-       AGlobal (ATyCon tc)
-               | isSynTyCon tc ->  returnTc (mkAppTys (mkSynTy tc (take arity arg_tys))
-                                                      (drop arity arg_tys))
-               | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
-               where
-                   arity = tyConArity tc
+       ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
 
 
+       AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
 
        other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
 
        other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
@@ -459,18 +508,22 @@ tc_fun_type name arg_tys
 Contexts
 ~~~~~~~~
 \begin{code}
 Contexts
 ~~~~~~~~
 \begin{code}
+tcHsPred pred = kc_pred pred `thenM_`  tc_pred pred
+       -- Is happy with a partial application, e.g. (ST s)
+       -- Used from TcDeriv
+
 tc_pred assn@(HsClassP class_name tys)
 tc_pred assn@(HsClassP class_name tys)
-  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
-    tc_types tys                       `thenTc` \ arg_tys ->
-    tcLookupGlobal class_name                  `thenTc` \ thing ->
+  = addErrCtxt (appKindCtxt (ppr assn))        $
+    tc_types tys                       `thenM` \ arg_tys ->
+    tcLookupGlobal class_name                  `thenM` \ thing ->
     case thing of
     case thing of
-       AClass clas -> returnTc (ClassP clas arg_tys)
+       AClass clas -> returnM (ClassP clas arg_tys)
        other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 
 tc_pred assn@(HsIParam name ty)
        other       -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
 
 tc_pred assn@(HsIParam name ty)
-  = tcAddErrCtxt (appKindCtxt (ppr assn))      $
-    tc_type ty                                 `thenTc` \ arg_ty ->
-    returnTc (IParam name arg_ty)
+  = addErrCtxt (appKindCtxt (ppr assn))        $
+    tc_type ty                                 `thenM` \ arg_ty ->
+    returnM (IParam name arg_ty)
 \end{code}
 
 
 \end{code}
 
 
@@ -513,8 +566,6 @@ been instantiated.
 \begin{code}
 data TcSigInfo
   = TySigInfo      
 \begin{code}
 data TcSigInfo
   = TySigInfo      
-       Name                    -- N, the Name in corresponding binding
-
        TcId                    -- *Polymorphic* binder for this value...
                                -- Has name = N
 
        TcId                    -- *Polymorphic* binder for this value...
                                -- Has name = N
 
@@ -532,15 +583,21 @@ data TcSigInfo
        SrcLoc                  -- Of the signature
 
 instance Outputable TcSigInfo where
        SrcLoc                  -- Of the signature
 
 instance Outputable TcSigInfo where
-    ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
-       ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+    ppr (TySigInfo id tyvars theta tau _ inst loc) =
+       ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+
+tcSigPolyId :: TcSigInfo -> TcId
+tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
+
+tcSigMonoId :: TcSigInfo -> TcId
+tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
 
 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
        -- Search for a particular signature
 maybeSig [] name = Nothing
 
 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
        -- Search for a particular signature
 maybeSig [] name = Nothing
-maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
-  | name == sig_name = Just sig
-  | otherwise       = maybeSig sigs name
+maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
+  | name == idName sig_id = Just sig
+  | otherwise            = maybeSig sigs name
 \end{code}
 
 
 \end{code}
 
 
@@ -548,12 +605,12 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 tcTySig :: RenamedSig -> TcM TcSigInfo
 
 tcTySig (Sig v ty src_loc)
 tcTySig :: RenamedSig -> TcM TcSigInfo
 
 tcTySig (Sig v ty src_loc)
- = tcAddSrcLoc src_loc                         $ 
-   tcHsSigType (FunSigCtxt v) ty               `thenTc` \ sigma_tc_ty ->
-   mkTcSig (mkLocalId v sigma_tc_ty) src_loc   `thenNF_Tc` \ sig -> 
-   returnTc sig
+ = addSrcLoc src_loc                           $ 
+   tcHsSigType (FunSigCtxt v) ty               `thenM` \ sigma_tc_ty ->
+   mkTcSig (mkLocalId v sigma_tc_ty) src_loc   `thenM` \ sig -> 
+   returnM sig
 
 
-mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
+mkTcSig :: TcId -> SrcLoc -> TcM TcSigInfo
 mkTcSig poly_id src_loc
   =    -- Instantiate this type
        -- It's important to do this even though in the error-free case
 mkTcSig poly_id src_loc
   =    -- Instantiate this type
        -- It's important to do this even though in the error-free case
@@ -562,279 +619,78 @@ mkTcSig poly_id src_loc
        -- the tyvars *do* get unified with something, we want to carry on
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
        -- the tyvars *do* get unified with something, we want to carry on
        -- typechecking the rest of the program with the function bound
        -- to a pristine type, namely sigma_tc_ty
-   let
-       (tyvars, rho) = tcSplitForAllTys (idType poly_id)
-   in
-   tcInstSigVars 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') = tcSplitRhoTy rho'
-       -- This splitRhoTy tries hard to make sure that tau' is a type synonym
-       -- wherever possible, which can improve interface files.
-   in
-   newMethodWithGivenTy SignatureOrigin 
-               poly_id
-               tyvar_tys'
-               theta' tau'                     `thenNF_Tc` \ inst ->
+   tcInstType SigTv (idType poly_id)           `thenM` \ (tyvars', theta', tau') ->
+
+   getInstLoc SignatureOrigin                  `thenM` \ inst_loc ->
+   newMethodWith inst_loc poly_id
+                (mkTyVarTys tyvars')
+                theta' tau'                    `thenM` \ inst ->
        -- We make a Method even if it's not overloaded; no harm
        -- We make a Method even if it's not overloaded; no harm
+       -- But do not extend the LIE!  We're just making an Id.
        
        
-   returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToId inst) [inst] src_loc)
-  where
-    name = idName poly_id
+   returnM (TySigInfo poly_id tyvars' theta' tau' 
+                         (instToId inst) [inst] src_loc)
 \end{code}
 
 
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 %************************************************************************
 %*                                                                     *
-\subsection{Checking signature type variables}
+\subsection{Errors and contexts}
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 
-@checkSigTyVars@ is used after the type in a type signature has been unified with
-the actual type found.  It then checks that the type variables of the type signature
-are
-       (a) Still all type variables
-               eg matching signature [a] against inferred type [(p,q)]
-               [then a will be unified to a non-type variable]
-
-       (b) Still all distinct
-               eg matching signature [(a,b)] against inferred type [(p,p)]
-               [then a and b will be unified together]
-
-       (c) Not mentioned in the environment
-               eg the signature for f in this:
-
-                       g x = ... where
-                                       f :: a->[a]
-                                       f y = [x,y]
-
-               Here, f is forced to be monorphic by the free occurence of x.
-
-       (d) Not (unified with another type variable that is) in scope.
-               eg f x :: (r->r) = (\y->y) :: forall a. a->r
-           when checking the expression type signature, we find that
-           even though there is nothing in scope whose type mentions r,
-           nevertheless the type signature for the expression isn't right.
-
-           Another example is in a class or instance declaration:
-               class C a where
-                  op :: forall b. a -> b
-                  op x = x
-           Here, b gets unified with a
-
-Before doing this, the substitution is applied to the signature type variable.
-
-We used to have the notion of a "DontBind" type variable, which would
-only be bound to itself or nothing.  Then points (a) and (b) were 
-self-checking.  But it gave rise to bogus consequential error messages.
-For example:
-
-   f = (*)     -- Monomorphic
-
-   g :: Num a => a -> a
-   g x = f x x
-
-Here, we get a complaint when checking the type signature for g,
-that g isn't polymorphic enough; but then we get another one when
-dealing with the (Num x) context arising from f's definition;
-we try to unify x with Int (to default it), but find that x has already
-been unified with the DontBind variable "a" from g's signature.
-This is really a problem with side-effecting unification; we'd like to
-undo g's effects when its type signature fails, but unification is done
-by side effect, so we can't (easily).
-
-So we revert to ordinary type variables for signatures, and try to
-give a helpful message in checkSigTyVars.
 
 \begin{code}
 
 \begin{code}
-checkSigTyVars :: [TcTyVar]            -- Universally-quantified type variables in the signature
-              -> TcTyVarSet            -- Tyvars that are free in the type signature
-                                       --      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 (allDistinctTyVars sig_tys globals)
-            (complain sig_tys globals) `thenTc_`
-
-    returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys)
-
-  where
-    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
-       tcGetEnv                                `thenNF_Tc` \ env ->
-       let
-          in_scope_tvs = tcEnvTyVars env
-       in
-       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 <- [tcGetTyVar_maybe z_ty]
-                            ]
-           in_scope_env = mkVarEnv in_scope_assoc
-       in
-
-       -- "check" checks each sig tyvar in turn
-        foldlNF_Tc check
-                  (env2, in_scope_env, [])
-                  (tidy_tvs `zip` tidy_tys)    `thenNF_Tc` \ (env3, _, msgs) ->
-
-        failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
-      where
-       (env1, tidy_tvs) = mapAccumL tidyTyVar emptyTidyEnv sig_tyvars
-       (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
-
-       main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
-
-       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 tcGetTyVar_maybe ty of {
-             Nothing ->                        -- Error (a)!
-                       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 (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
-                   where
-                       thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
-
-             ; Nothing ->
-
-           if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
-                                       -- The least comprehensible, so put it last
-                       -- Game plan: 
-                       --    a) get the local TcIds 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  [] (tcEnvTcIds 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 (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 :: Var 
-             -> TidyEnv 
-             -> [(Name,Type)] 
-             -> [Id] 
-             -> NF_TcM (TidyEnv,[(Name,Type)])
-
-find_globals tv tidy_env acc []
-  = returnNF_Tc (tidy_env, acc)
-
-find_globals tv tidy_env acc (id:ids) 
-  | 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_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
-       in
-       find_frees tv tidy_env' (ftv':acc) ftvs
-    else
-       find_frees tv tidy_env  acc        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])
-       ]
-     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"))
-       ]
-     else
-       empty   -- Sigh.  It's really hard to give a good error message
-               -- all the time.   One bad case is an existential pattern match
-  where
-    is_are | isSingleton frees = ptext SLIT("is")
-          | otherwise         = ptext SLIT("are")
-    pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
-         | otherwise    = ptext SLIT("It")
-
-    vcat_first :: Int -> [SDoc] -> SDoc
-    vcat_first n []     = empty
-    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") <+> thing
-mk_msg tv          = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
-\end{code}
-
-These two context are used with checkSigTyVars
-    
-\begin{code}
-sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
-       -> 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
-       (env2, tidy_sig_rho)     = tidyOpenType env1 (mkRhoTy sig_theta sig_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
-                  ]
+hoistForAllTys :: Type -> Type
+-- Used for user-written type signatures only
+-- Move all the foralls and constraints to the top
+-- e.g.  T -> forall a. a        ==>   forall a. T -> a
+--      T -> (?x::Int) -> Int   ==>   (?x::Int) -> T -> Int
+--
+-- Also: eliminate duplicate constraints.  These can show up
+-- when hoisting constraints, notably implicit parameters.
+--
+-- We want to 'look through' type synonyms when doing this
+-- so it's better done on the Type than the HsType
+
+hoistForAllTys ty
+  = let
+       no_shadow_ty = deShadowTy ty
+       -- Running over ty with an empty substitution gives it the
+       -- no-shadowing property.  This is important.  For example:
+       --      type Foo r = forall a. a -> r
+       --      foo :: Foo (Foo ())
+       -- Here the hoisting should give
+       --      foo :: forall a a1. a -> a1 -> ()
+       --
+       -- What about type vars that are lexically in scope in the envt?
+       -- We simply rely on them having a different unique to any
+       -- binder in 'ty'.  Otherwise we'd have to slurp the in-scope-tyvars
+       -- out of the envt, which is boring and (I think) not necessary.
     in
     in
-    returnNF_Tc (env3, msg)
-
-sigPatCtxt bound_tvs bound_ids tidy_env
-  = returnNF_Tc (env1,
-                sep [ptext SLIT("When checking a pattern that binds"),
-                     nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))])
+    case hoist no_shadow_ty of 
+       (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
+               -- The 'nubBy' eliminates duplicate constraints,
+               -- notably implicit parameters
   where
   where
-    show_ids = filter is_interesting bound_ids
-    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
-
-    (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids)
-    ppr_id id ty     = ppr id <+> dcolon <+> ppr ty
-       -- Don't zonk the types so we get the separate, un-unified versions
+    hoist ty
+       | (tvs1, body_ty) <- tcSplitForAllTys ty,
+         not (null tvs1)
+       = case hoist body_ty of
+               (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
+
+       | Just (arg, res) <- tcSplitFunTy_maybe ty
+       = let
+             arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
+         in                            -- to the argument type
+         if (isPredTy arg') then
+           case hoist res of
+               (tvs,theta,tau) -> (tvs, arg':theta, tau)
+         else
+            case hoist res of
+               (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
+
+       | otherwise = ([], [], ty)
 \end{code}
 
 
 \end{code}
 
 
@@ -860,6 +716,6 @@ wrongThingErr expected thing name
     pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
     pp_thing (AGlobal (AnId   _)) = ptext SLIT("Identifier")
     pp_thing (ATyVar _)          = ptext SLIT("Type variable")
     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 (ATcId _ _)         = ptext SLIT("Local identifier")
     pp_thing (AThing _)          = ptext SLIT("Utterly bogus")
 \end{code}
     pp_thing (AThing _)          = ptext SLIT("Utterly bogus")
 \end{code}