[project @ 2002-11-21 11:31:34 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index cd1ba2b..b45acab 100644 (file)
@@ -23,24 +23,24 @@ import HsSyn                ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
 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, tcInstType,
+import TcMType         ( newMutTyVar, newKindVar, zonkKindEnv, tcInstType,
                          checkValidType, UserTypeCtxt(..), pprUserTypeCtxt
                        )
 import TcUnify         ( unifyKind, unifyOpenTypeKind )
 import TcType          ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
                          TcTyVar, TcKind, TcThetaType, TcTauType,
                          mkTyVarTy, mkTyVarTys, mkFunTy, 
-                         hoistForAllTys, zipFunTys, 
+                         zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
                          mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys, 
                          liftedTypeKind, unliftedTypeKind, mkArrowKind,
-                         mkArrowKinds, tcSplitFunTy_maybe
+                         mkArrowKinds, tcSplitFunTy_maybe, tcSplitForAllTys
                        )
-import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToId )
+import Inst            ( Inst, InstOrigin(..), newMethod, instToId )
 
 import Id              ( mkLocalId, idName, idType )
 import Var             ( TyVar, mkTyVar, tyVarKind )
@@ -49,12 +49,13 @@ import TyCon                ( TyCon, tyConKind )
 import Class           ( classTyCon )
 import Name            ( Name )
 import NameSet
+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 +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
-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 +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.]
-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 +178,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,54 +210,53 @@ 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 ()
        -- 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
-  = 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
-kcHsSigTypes tys  = mapTc_ kcHsSigType tys
+kcHsSigTypes tys  = mappM_ kcHsSigType tys
 kcHsLiftedSigType = kcLiftedType
 
 ---------------------------
@@ -264,72 +264,78 @@ kcHsType :: RenamedHsType -> TcM TcKind
 kcHsType (HsTyVar name)              = kcTyVar name
 
 kcHsType (HsKindSig ty k)
-  = kcHsType ty                        `thenTc` \ k' ->
-    unifyKind k k'             `thenTc_`
-    returnTc k
+  = kcHsType ty                        `thenM` \ k' ->
+    unifyKind k k'             `thenM_`
+    returnM k
 
 kcHsType (HsListTy ty)
-  = kcLiftedType ty            `thenTc` \ tau_ty ->
-    returnTc liftedTypeKind
+  = kcLiftedType ty            `thenM` \ tau_ty ->
+    returnM liftedTypeKind
 
 kcHsType (HsPArrTy 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 (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
+  = kcTypeType ty1     `thenM_`
+    kcTypeType ty2     `thenM_`
+    returnM liftedTypeKind
 
 kcHsType (HsOpTy ty1 HsArrow ty2)
-  = kcTypeType ty1     `thenTc_`
-    kcTypeType ty2     `thenTc_`
-    returnTc liftedTypeKind
+  = kcTypeType ty1     `thenM_`
+    kcTypeType ty2     `thenM_`
+    returnM liftedTypeKind
 
 kcHsType ty@(HsOpTy ty1 (HsTyOp 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' ->
+  = 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
+
+kcHsType (HsParTy ty)          -- Skip parentheses markers
+  = kcHsType ty
    
 kcHsType (HsNumTy _)           -- The unit type for generics
-  = returnTc liftedTypeKind
+  = returnM liftedTypeKind
 
 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))        $
+  = 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)
-  = 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            `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)
-               -> 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
 
 
 ---------------------------
@@ -339,36 +345,36 @@ 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 ->
+    mappM kcHsType tys                 `thenM` \ arg_kinds ->
+    newKindVar                                 `thenM` \ kv -> 
+    unifyKind kind (mkArrowKinds arg_kinds kv) `thenM_` 
+    returnM kv
 
 ---------------------------
-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 ->
+    unifyKind liftedTypeKind kind              `thenM_`
+    returnM ()
     
 
  ---------------------------
 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}
 
@@ -414,53 +420,56 @@ 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 `thenTc` \ tau_ty ->
-    returnTc (mkPArrTy tau_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 `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 (HsTyOp op) ty2)
-  = tc_type ty1 `thenTc` \ tau_ty1 ->
-    tc_type ty2 `thenTc` \ tau_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 (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
-       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
@@ -472,12 +481,12 @@ 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 ->
+  = addErrCtxt (appKindCtxt pp_app)    $
+    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)
+       other       -> tc_type ty               `thenM` \ fun_ty ->
+                      returnM (mkAppTys fun_ty arg_tys)
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
@@ -486,11 +495,11 @@ tc_app ty tys
 --     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) -> returnTc (mkGenTyConApp tc arg_tys)
+       AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
 
        other -> failWithTc (wrongThingErr "type constructor" thing name)
 \end{code}
@@ -499,22 +508,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}
 
 
@@ -596,12 +605,12 @@ maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : 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) 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
@@ -610,19 +619,80 @@ 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
-   tcInstType 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 poly_id tyvars' theta' tau' 
+   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}
+
 
 %************************************************************************
 %*                                                                     *
@@ -646,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 (ATcId _)           = ptext SLIT("Local identifier")
+    pp_thing (ATcId _ _)         = ptext SLIT("Local identifier")
     pp_thing (AThing _)          = ptext SLIT("Utterly bogus")
 \end{code}