[project @ 2003-06-27 21:17:24 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index 21d554d..c257251 100644 (file)
@@ -13,48 +13,50 @@ module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred,
                    kcHsLiftedSigType, kcHsContext,
                    tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
 
-                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig
+                   TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
                  ) where
 
 #include "HsVersions.h"
 
-import HsSyn           ( HsType(..), HsTyVarBndr(..),
-                          Sig(..), HsPred(..), pprParendHsType, HsTupCon(..), hsTyVarNames )
+import HsSyn           ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
+                          Sig(..), HsPred(..), HsTupCon(..), hsTyVarNames )
 import RnHsSyn         ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
 import TcHsSyn         ( TcId )
 
-import TcMonad
+import TcRnMonad
 import TcEnv           ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
-                         tcInLocalScope,
-                         TyThing(..), TcTyThing(..), tcExtendKindEnv
+                         TyThing(..), TcTyThing(..), tcExtendKindEnv,
+                         getInLocalScope
                        )
-import TcMType         ( newKindVar, zonkKindEnv, tcInstSigType,
-                         checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
+import TcMType         ( newMutTyVar, newKindVar, zonkKindEnv, tcInstType, zonkTcType,
+                         checkValidType, UserTypeCtxt(..), pprUserTypeCtxt, newOpenTypeKind
                        )
-import TcUnify         ( unifyKind, unifyOpenTypeKind )
+import TcUnify         ( unifyKind, unifyFunKind )
 import TcType          ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
                          TcTyVar, TcKind, TcThetaType, TcTauType,
-                         mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy,
-                         hoistForAllTys, zipFunTys, 
-                         mkSigmaTy, mkPredTy, mkTyConApp, mkAppTys, 
-                         liftedTypeKind, unliftedTypeKind, mkArrowKind,
-                         mkArrowKinds, tcSplitFunTy_maybe
+                         mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
+                         zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
+                         mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
+                         liftedTypeKind, unliftedTypeKind, eqKind,
+                         tcSplitFunTy_maybe, tcSplitForAllTys
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
+import qualified Type  ( splitFunTys )
+import Inst            ( Inst, InstOrigin(..), newMethod, instToId )
 
 import Id              ( mkLocalId, idName, idType )
 import Var             ( TyVar, mkTyVar, tyVarKind )
 import ErrUtils                ( Message )
-import TyCon           ( TyCon, isSynTyCon, tyConKind )
+import TyCon           ( TyCon, tyConKind )
 import Class           ( classTyCon )
 import Name            ( Name )
 import NameSet
-import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
+import Subst           ( deShadowTy )
+import TysWiredIn      ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
 import Util            ( lengthIs )
 import Outputable
-
+import List            ( nubBy )
 \end{code}
 
 
@@ -79,12 +81,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
-tcHsSigType ctxt ty = tcAddErrCtxt (checkTypeCtxt ctxt ty) (
-                       kcTypeType ty           `thenTc_`
+tcHsSigType ctxt ty = addErrCtxt (checkTypeCtxt ctxt ty) (
+                       kcTypeType ty           `thenM_`
                        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,
@@ -96,13 +98,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.]
-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 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.
@@ -177,9 +179,9 @@ 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 ->
+  = 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
@@ -209,114 +211,186 @@ tcAddScopedTyVars [] thing_inside
   = thing_inside       -- Quick get-out for the empty case
 
 tcAddScopedTyVars sig_tys thing_inside
-  = tcGetEnv                                   `thenNF_Tc` \ env ->
+  = getInLocalScope                    `thenM` \ in_scope ->
     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)
+       sig_tvs         = filter (not . in_scope) (nameSetToList all_sig_tvs)
     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 ->
+    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}
-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 (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 ()
+kcLiftedType :: RenamedHsType -> TcM Kind
        -- The type ty must be a *lifted* *type*
-kcLiftedType ty
-  = kcHsType ty                                `thenTc` \ kind ->
-    tcAddErrCtxt (typeKindCtxt ty)     $
-    unifyKind liftedTypeKind kind
+kcLiftedType ty = kcHsType ty  `thenM` \ act_kind ->
+                 checkExpectedKind (ppr ty) act_kind liftedTypeKind
     
 ---------------------------
 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
+  = kcHsType ty                        `thenM` \ kind ->
+    if isTypeKind kind then
+       return ()
+    else
+    newOpenTypeKind                            `thenM` \ exp_kind ->
+    checkExpectedKind (ppr ty) kind exp_kind   `thenM_`
+    returnM ()
 
 ---------------------------
 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
        -- Used for type signatures
-kcHsSigType      = kcTypeType
-kcHsSigTypes tys  = mapTc_ kcHsSigType tys
-kcHsLiftedSigType = kcLiftedType
+kcHsSigType ty              = kcTypeType ty
+kcHsSigTypes tys     = mappM_ kcHsSigType tys
+kcHsLiftedSigType ty = kcLiftedType ty `thenM_` returnM ()
 
 ---------------------------
 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
+-- kcHsType *returns* the kind of the type, rather than taking an expected
+-- kind as argument as tcExpr does.  Reason: the kind of (->) is
+--     forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
+-- so we'd need to generate huge numbers of bx variables.
+
+kcHsType (HsTyVar name)   = kcTyVar name
+kcHsType (HsListTy ty)    = kcLiftedType ty
+kcHsType (HsPArrTy ty)    = kcLiftedType ty
+kcHsType (HsParTy ty)    = kcHsType ty             -- Skip parentheses markers
+kcHsType (HsNumTy _)      = returnM liftedTypeKind  -- The unit type for generics
+kcHsType (HsKindSig ty k) = kcHsType ty                `thenM` \ act_kind ->
+                           checkExpectedKind (ppr ty) act_kind k
+
+kcHsType (HsTupleTy (HsTupCon boxity _) tys)
+  = mappM kcTypeType tys       `thenM_`
+    returnM (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
-   
+  = 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 op_ty@(HsTyOp op) ty2)
+  = addErrCtxt (appKindCtxt (ppr ty))  $
+    kcTyVar op                         `thenM` \ op_kind ->
+    kcApps (ppr op_ty) op_kind [ty1,ty2]
+
 kcHsType (HsPredTy pred)
-  = kcHsPred pred              `thenTc_`
-    returnTc liftedTypeKind
+  = kcHsPred pred              `thenM_`
+    returnM 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
+  = addErrCtxt (appKindCtxt (ppr ty))  $
+    kc_app ty []
+  where
+    kc_app (HsAppTy f a) as = kc_app f (a:as)
+    kc_app f            as = kcHsType f        `thenM` \ fk ->
+                             kcApps (ppr f) fk as
 
 kcHsType (HsForAllTy (Just tv_names) context ty)
-  = kcHsTyVars tv_names                `thenNF_Tc` \ kind_env ->
+  = kcHsTyVars tv_names                `thenM` \ kind_env ->
     tcExtendKindEnv kind_env   $
-    kcHsContext context                `thenTc_`
-    kcHsType ty                        `thenTc_`
-    returnTc liftedTypeKind
+    kcHsContext context                `thenM_`
+    kcLiftedType ty
+       -- 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.
 
 ---------------------------
-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
+kcApps :: SDoc                         -- The function
+       -> TcKind               -- Function kind
+       -> [RenamedHsType]      -- Arg types
+       -> TcM TcKind           -- Result kind
+kcApps pp_fun fun_kind args
+  = go fun_kind args
+  where
+    go fk []       = returnM fk
+    go fk (ty:tys) = unifyFunKind fk   `thenM` \ mb_fk ->
+                    case mb_fk of {
+                       Nothing       -> failWithTc too_few_args ;
+                       Just (ak',fk') -> 
+                    kcHsType ty                        `thenM` \ ak ->
+                    checkExpectedKind (ppr ty) ak ak'  `thenM_`
+                    go fk' tys }
+
+    too_few_args = ptext SLIT("Kind error:") <+> quotes pp_fun <+>
+                       ptext SLIT("is applied to too many type arguments")
 
-       Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
-                  unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
-                  returnTc res_kind
+---------------------------
+-- We would like to get a decent error message from
+--   (a) Under-applied type constructors
+--             f :: (Maybe, Maybe)
+--   (b) Over-applied type constructors
+--             f :: Int x -> Int x
+--
 
+checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
+-- A fancy wrapper for 'unifyKind', which tries to give 
+-- decent error messages.
+-- Returns the same kind that it is passed, exp_kind
+checkExpectedKind pp_ty act_kind exp_kind
+  | act_kind `eqKind` exp_kind -- Short cut for a very common case
+  = returnM exp_kind   
+  | otherwise
+  = tryTc (unifyKind exp_kind act_kind)        `thenM` \ (errs, mb_r) ->
+    case mb_r of {
+       Just _  -> returnM exp_kind ;   -- Unification succeeded
+       Nothing ->
+
+       -- So there's definitely an error
+       -- Now to find out what sort
+    zonkTcType exp_kind                `thenM` \ exp_kind ->
+    zonkTcType act_kind                `thenM` \ act_kind ->
+
+    let (exp_as, _) = Type.splitFunTys exp_kind
+        (act_as, _) = Type.splitFunTys act_kind
+               -- Use the Type versions for kinds      
+       n_exp_as = length exp_as
+       n_act_as = length act_as
+
+       err | n_exp_as < n_act_as       -- E.g. [Maybe]
+           = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
+
+               -- Now n_exp_as >= n_act_as. In the next two cases, 
+               -- n_exp_as == 0, and hence so is n_act_as
+           | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
+           = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty 
+               <+> ptext SLIT("is unlifted")
+
+           | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
+           = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty 
+               <+> ptext SLIT("is lifted")
+
+           | otherwise                 -- E.g. Monad [Int]
+           = sep [ ptext SLIT("Expecting kind") <+> quotes (ppr exp_kind) <> comma,
+                   ptext SLIT("but") <+> quotes pp_ty <+> 
+                       ptext SLIT("has kind") <+> quotes (ppr act_kind)]
+   in
+   failWithTc (ptext SLIT("Kind error:") <+> err) 
+   }
 
 ---------------------------
 kc_pred :: RenamedHsPred -> TcM TcKind -- Does *not* check for a saturated
@@ -325,36 +399,32 @@ kc_pred pred@(HsIParam name ty)
   = kcHsType ty
 
 kc_pred pred@(HsClassP cls tys)
-  = kcClass cls                                `thenTc` \ kind ->
-    mapTc kcHsType tys                 `thenTc` \ arg_kinds ->
-    newKindVar                                 `thenNF_Tc` \ kv -> 
-    unifyKind kind (mkArrowKinds arg_kinds kv) `thenTc_` 
-    returnTc kv
+  = kcClass cls                `thenM` \ kind ->
+    kcApps (ppr cls) kind tys
 
 ---------------------------
-kcHsContext ctxt = mapTc_ kcHsPred ctxt
+kcHsContext ctxt = mappM_ kcHsPred ctxt
 
 kcHsPred pred          -- Checks that the result is of kind liftedType
-  = tcAddErrCtxt (appKindCtxt (ppr pred))      $
-    kc_pred pred                               `thenTc` \ kind ->
-    unifyKind liftedTypeKind kind              `thenTc_`
-    returnTc ()
+  = addErrCtxt (appKindCtxt (ppr pred))        $
+    kc_pred pred                       `thenM` \ kind ->
+    checkExpectedKind (ppr pred) kind liftedTypeKind
     
 
  ---------------------------
 kcTyVar name   -- Could be a tyvar or a tycon
-  = tcLookup name      `thenTc` \ thing ->
+  = tcLookup name      `thenM` \ thing ->
     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
-  = tcLookup cls                               `thenNF_Tc` \ thing -> 
+  = tcLookup cls                               `thenM` \ thing -> 
     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}
 
@@ -396,45 +466,62 @@ tc_type :: RenamedHsType -> TcM Type
 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 ty `thenTc` \ tau_ty ->
-    returnTc (mkListTy tau_ty)
+  = tc_type ty `thenM` \ tau_ty ->
+    returnM (mkListTy tau_ty)
+
+tc_type (HsPArrTy ty)
+  = tc_type ty `thenM` \ tau_ty ->
+    returnM (mkPArrTy tau_ty)
 
-tc_type (HsTupleTy (HsTupCon _ boxity arity) 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_types tys       `thenM` \ tau_tys ->
+    returnM (mkTupleTy boxity arity 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 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)
-    returnTc (mkTyConApp genUnitTyCon [])
+    returnM (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]
-
-tc_type (HsAppTy ty1 ty2) = tc_app ty1 [ty2]
+tc_type ty@(HsAppTy ty1 ty2) 
+  = addErrCtxt (appKindCtxt (ppr ty))  $
+    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
-       kind_check = kcHsContext ctxt `thenTc_` kcHsType ty
+       kind_check = kcHsContext ctxt `thenM_` kcHsType ty
     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
@@ -446,27 +533,22 @@ tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
-  = tcAddErrCtxt (appKindCtxt pp_app)  $
-    tc_types tys                       `thenTc` \ arg_tys ->
+  = tc_types tys                       `thenM` \ 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)
+       other       -> tc_type ty               `thenM` \ fun_ty ->
+                      returnM (mkAppTys fun_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 name arg_tys
-  = tcLookup name                      `thenTc` \ thing ->
+  = tcLookup name                      `thenM` \ thing ->
     case thing of
-       ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
+       ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
 
-       AGlobal (ATyCon tc)
-               | isSynTyCon tc ->  returnTc (mkSynTy tc arg_tys)
-               | otherwise     ->  returnTc (mkTyConApp tc arg_tys)
+       AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
 
        other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
@@ -475,22 +557,22 @@ tc_fun_type name arg_tys
 Contexts
 ~~~~~~~~
 \begin{code}
-tcHsPred pred = kc_pred pred `thenTc_`  tc_pred pred
+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)
-  = 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
-       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)
-  = 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}
 
 
@@ -533,8 +615,6 @@ been instantiated.
 \begin{code}
 data TcSigInfo
   = TySigInfo      
-       Name                    -- N, the Name in corresponding binding
-
        TcId                    -- *Polymorphic* binder for this value...
                                -- Has name = N
 
@@ -552,15 +632,21 @@ data TcSigInfo
        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 (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}
 
 
@@ -568,13 +654,13 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 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)   `thenM` \ sig -> 
+   returnM sig
 
-mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
-mkTcSig poly_id src_loc
+mkTcSig :: TcId -> TcM TcSigInfo
+mkTcSig poly_id
   =    -- Instantiate this type
        -- It's important to do this even though in the error-free case
        -- we could just split the sigma_tc_ty (since the tyvars don't
@@ -582,19 +668,81 @@ 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
-   tcInstSigType SigTv (idType poly_id)                `thenNF_Tc` \ (tyvars', theta', tau') ->
+   tcInstType SigTv (idType poly_id)           `thenM` \ (tyvars', theta', tau') ->
 
-   newMethodWithGivenTy SignatureOrigin 
-                       poly_id
-                       (mkTyVarTys tyvars')
-                       theta' tau'             `thenNF_Tc` \ inst ->
+   getInstLoc SignatureOrigin                  `thenM` \ inst_loc ->
+   newMethod inst_loc poly_id
+            (mkTyVarTys tyvars')
+            theta' tau'                        `thenM` \ inst ->
        -- 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 (idName poly_id) poly_id tyvars' theta' tau' 
+   getSrcLocM                                  `thenM` \ src_loc ->
+   returnM (TySigInfo poly_id tyvars' theta' tau' 
                          (instToId inst) [inst] src_loc)
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+\subsection{Errors and contexts}
+%*                                                                     *
+%************************************************************************
+
+
+\begin{code}
+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
+    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
+    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}
+
 
 %************************************************************************
 %*                                                                     *
@@ -614,10 +762,11 @@ appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 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 (AGlobal (ATyCon _))   = ptext SLIT("Type constructor")
+    pp_thing (AGlobal (AClass _))   = ptext SLIT("Class")
+    pp_thing (AGlobal (AnId   _))   = ptext SLIT("Identifier")
+    pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
     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}