Another round of External Core fixes

[ghc-hetmet.git] / compiler / typecheck / TcBinds.lhs

diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 36c71a1..d9f5587 100644 (file)
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -1,9 +1,17 @@
 %
 %

+% (c) The University of Glasgow 2006

 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcBinds]{TcBinds}
 
 \begin{code}
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcBinds]{TcBinds}
 
 \begin{code}

+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+

 module TcBinds ( tcLocalBinds, tcTopBinds, 
                 tcHsBootSigs, tcMonoBinds, 
                 TcPragFun, tcSpecPrag, tcPrags, mkPragFun, 
 module TcBinds ( tcLocalBinds, tcTopBinds, 
                 tcHsBootSigs, tcMonoBinds, 
                 TcPragFun, tcSpecPrag, tcPrags, mkPragFun, 

@@ -15,59 +23,42 @@ module TcBinds ( tcLocalBinds, tcTopBinds,
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 

-import DynFlags                ( dopt, DynFlags,
-                         DynFlag(Opt_MonomorphismRestriction, Opt_MonoPatBinds, Opt_GlasgowExts) )
-import HsSyn           ( HsExpr(..), HsBind(..), LHsBinds, LHsBind, Sig(..),
-                         HsLocalBinds(..), HsValBinds(..), HsIPBinds(..),
-                         LSig, Match(..), IPBind(..), Prag(..),
-                         HsType(..), LHsType, HsExplicitForAll(..), hsLTyVarNames, 
-                         isVanillaLSig, sigName, placeHolderNames, isPragLSig,
-                         LPat, GRHSs, MatchGroup(..), pprLHsBinds, mkHsCoerce,
-                         collectHsBindBinders, collectPatBinders, pprPatBind, isBangHsBind
-                       )
-import TcHsSyn         ( zonkId )
+import DynFlags
+import HsSyn
+import TcHsSyn

 
 import TcRnMonad
 
 import TcRnMonad

-import Inst            ( newDictsAtLoc, newIPDict, instToId )
-import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
-                         pprBinders, tcLookupLocalId_maybe, tcLookupId,
-                         tcGetGlobalTyVars )
-import TcUnify         ( tcInfer, tcSubExp, unifyTheta, 
-                         bleatEscapedTvs, sigCtxt )
-import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, 
-                         tcSimplifyRestricted, tcSimplifyIPs )
-import TcHsType                ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat           ( tcPat, PatCtxt(..) )
-import TcSimplify      ( bindInstsOfLocalFuns )
-import TcMType         ( newFlexiTyVarTy, zonkQuantifiedTyVar, zonkSigTyVar,
-                         tcInstSigTyVars, tcInstSkolTyVars, tcInstType, 
-                         zonkTcType, zonkTcTypes, zonkTcTyVars )
-import TcType          ( TcType, TcTyVar, TcThetaType, 
-                         SkolemInfo(SigSkol), UserTypeCtxt(FunSigCtxt), 
-                         TcTauType, TcSigmaType, isUnboxedTupleType,
-                         mkTyVarTy, mkForAllTys, mkFunTys, exactTyVarsOfType, 
-                         mkForAllTy, isUnLiftedType, tcGetTyVar, 
-                         mkTyVarTys, tidyOpenTyVar )
-import Kind            ( argTypeKind )
-import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv ) 
-import TysWiredIn      ( unitTy )
-import TysPrim         ( alphaTyVar )
-import Id              ( Id, mkLocalId, mkVanillaGlobal )
-import IdInfo          ( vanillaIdInfo )
-import Var             ( TyVar, idType, idName )
-import Name            ( Name )
+import Inst
+import TcEnv
+import TcUnify
+import TcSimplify
+import TcHsType
+import TcPat
+import TcMType
+import TcType
+import {- Kind parts of -} Type
+import Coercion
+import VarEnv
+import TysPrim
+import Id
+import IdInfo
+import Var ( TyVar, varType )
+import Name

 import NameSet
 import NameEnv
 import VarSet
 import NameSet
 import NameEnv
 import VarSet

-import SrcLoc          ( Located(..), unLoc, getLoc )
+import SrcLoc

 import Bag
 import Bag

-import ErrUtils                ( Message )
-import Digraph         ( SCC(..), stronglyConnComp )
-import Maybes          ( expectJust, isJust, isNothing, orElse )
-import Util            ( singleton )
-import BasicTypes      ( TopLevelFlag(..), isTopLevel, isNotTopLevel,
-                         RecFlag(..), isNonRec, InlineSpec, defaultInlineSpec )
+import ErrUtils
+import Digraph
+import Maybes
+import List
+import Util
+import BasicTypes

 import Outputable
 import Outputable

+import FastString
+
+import Control.Monad

 \end{code}
 
 
 \end{code}
 
 

@@ -153,11 +144,11 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
        -- I wonder if we should do these one at at time
        -- Consider     ?x = 4
        --              ?y = ?x + 1
        -- I wonder if we should do these one at at time
        -- Consider     ?x = 4
        --              ?y = ?x + 1

-    tc_ip_bind (IPBind ip expr)
-      = newFlexiTyVarTy argTypeKind            `thenM` \ ty ->
-       newIPDict (IPBindOrigin ip) ip ty       `thenM` \ (ip', ip_inst) ->
-       tcMonoExpr expr ty                      `thenM` \ expr' ->
-       returnM (ip_inst, (IPBind ip' expr'))
+    tc_ip_bind (IPBind ip expr) = do
+        ty <- newFlexiTyVarTy argTypeKind
+        (ip', ip_inst) <- newIPDict (IPBindOrigin ip) ip ty
+        expr' <- tcMonoExpr expr ty
+        return (ip_inst, (IPBind ip' expr'))

 
 ------------------------
 tcValBinds :: TopLevelFlag 
 
 ------------------------
 tcValBinds :: TopLevelFlag 

@@ -182,9 +173,9 @@ tcValBinds top_lvl (ValBindsOut binds sigs) thing_inside
 
                -- Extend the envt right away with all 
                -- the Ids declared with type signatures
 
                -- Extend the envt right away with all 
                -- the Ids declared with type signatures

-       ; gla_exts     <- doptM Opt_GlasgowExts
+       ; poly_rec <- doptM Opt_RelaxedPolyRec

        ; (binds', thing) <- tcExtendIdEnv poly_ids $
        ; (binds', thing) <- tcExtendIdEnv poly_ids $

-                            tc_val_binds gla_exts top_lvl sig_fn prag_fn 
+                            tc_val_binds poly_rec top_lvl sig_fn prag_fn 

                                          binds thing_inside
 
        ; return (ValBindsOut binds' sigs, thing) }
                                          binds thing_inside
 
        ; return (ValBindsOut binds' sigs, thing) }

@@ -196,14 +187,14 @@ tc_val_binds :: Bool -> TopLevelFlag -> TcSigFun -> TcPragFun
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 

-tc_val_binds gla_exts top_lvl sig_fn prag_fn [] thing_inside
+tc_val_binds poly_rec top_lvl sig_fn prag_fn [] thing_inside

   = do { thing <- thing_inside
        ; return ([], thing) }
 
   = do { thing <- thing_inside
        ; return ([], thing) }
 

-tc_val_binds gla_exts top_lvl sig_fn prag_fn (group : groups) thing_inside
+tc_val_binds poly_rec top_lvl sig_fn prag_fn (group : groups) thing_inside

   = do { (group', (groups', thing))
   = do { (group', (groups', thing))

-               <- tc_group gla_exts top_lvl sig_fn prag_fn group $ 
-                  tc_val_binds gla_exts top_lvl sig_fn prag_fn groups thing_inside
+               <- tc_group poly_rec top_lvl sig_fn prag_fn group $ 
+                  tc_val_binds poly_rec top_lvl sig_fn prag_fn groups thing_inside

        ; return (group' ++ groups', thing) }
 
 ------------------------
        ; return (group' ++ groups', thing) }
 
 ------------------------

@@ -215,15 +206,15 @@ tc_group :: Bool -> TopLevelFlag -> TcSigFun -> TcPragFun
 -- We get a list of groups back, because there may 
 -- be specialisations etc as well
 
 -- We get a list of groups back, because there may 
 -- be specialisations etc as well
 

-tc_group gla_exts top_lvl sig_fn prag_fn (NonRecursive, binds) thing_inside
+tc_group poly_rec top_lvl sig_fn prag_fn (NonRecursive, binds) thing_inside

        -- A single non-recursive binding
        -- We want to keep non-recursive things non-recursive
         -- so that we desugar unlifted bindings correctly
  =  do { (binds, thing) <- tc_haskell98 top_lvl sig_fn prag_fn NonRecursive binds thing_inside
        ; return ([(NonRecursive, b) | b <- binds], thing) }
 
        -- A single non-recursive binding
        -- We want to keep non-recursive things non-recursive
         -- so that we desugar unlifted bindings correctly
  =  do { (binds, thing) <- tc_haskell98 top_lvl sig_fn prag_fn NonRecursive binds thing_inside
        ; return ([(NonRecursive, b) | b <- binds], thing) }
 

-tc_group gla_exts top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
-  | not gla_exts       -- Recursive group, normal Haskell 98 route
+tc_group poly_rec top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
+  | not poly_rec       -- Recursive group, normal Haskell 98 route

   = do { (binds1, thing) <- tc_haskell98 top_lvl sig_fn prag_fn Recursive binds thing_inside
        ; return ([(Recursive, unionManyBags binds1)], thing) }
 
   = do { (binds1, thing) <- tc_haskell98 top_lvl sig_fn prag_fn Recursive binds thing_inside
        ; return ([(Recursive, unionManyBags binds1)], thing) }
 

@@ -261,7 +252,7 @@ tc_haskell98 top_lvl sig_fn prag_fn rec_flag binds thing_inside
 bindLocalInsts :: TopLevelFlag -> TcM ([LHsBinds TcId], [TcId], a) -> TcM ([LHsBinds TcId], a)
 bindLocalInsts top_lvl thing_inside
   | isTopLevel top_lvl = do { (binds, ids, thing) <- thing_inside; return (binds, thing) }
 bindLocalInsts :: TopLevelFlag -> TcM ([LHsBinds TcId], [TcId], a) -> TcM ([LHsBinds TcId], a)
 bindLocalInsts top_lvl thing_inside
   | isTopLevel top_lvl = do { (binds, ids, thing) <- thing_inside; return (binds, thing) }

-       -- For the top level don't bother will all this bindInstsOfLocalFuns stuff. 
+       -- For the top level don't bother with all this bindInstsOfLocalFuns stuff. 

        -- All the top level things are rec'd together anyway, so it's fine to
        -- leave them to the tcSimplifyTop, and quite a bit faster too
 
        -- All the top level things are rec'd together anyway, so it's fine to
        -- leave them to the tcSimplifyTop, and quite a bit faster too
 

@@ -323,7 +314,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
     in
        -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
     setSrcSpan loc                             $
     in
        -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
     setSrcSpan loc                             $

-    recoverM (recoveryCode binder_names)       $ do 
+    recoverM (recoveryCode binder_names sig_fn)        $ do 

 
   { traceTc (ptext SLIT("------------------------------------------------"))
   ; traceTc (ptext SLIT("Bindings for") <+> ppr binder_names)
 
   { traceTc (ptext SLIT("------------------------------------------------"))
   ; traceTc (ptext SLIT("Bindings for") <+> ppr binder_names)

@@ -331,6 +322,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
        -- TYPECHECK THE BINDINGS
   ; ((binds', mono_bind_infos), lie_req) 
        <- getLIE (tcMonoBinds bind_list sig_fn rec_tc)
        -- TYPECHECK THE BINDINGS
   ; ((binds', mono_bind_infos), lie_req) 
        <- getLIE (tcMonoBinds bind_list sig_fn rec_tc)

+  ; traceTc (text "temp" <+> (ppr binds' $$ ppr lie_req))

 
        -- CHECK FOR UNLIFTED BINDINGS
        -- These must be non-recursive etc, and are not generalised
 
        -- CHECK FOR UNLIFTED BINDINGS
        -- These must be non-recursive etc, and are not generalised

@@ -350,57 +342,61 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
 
     else do    -- The normal lifted case: GENERALISE
   { dflags <- getDOpts 
 
     else do    -- The normal lifted case: GENERALISE
   { dflags <- getDOpts 

-  ; (tyvars_to_gen, dict_binds, dict_ids)
+  ; (tyvars_to_gen, dicts, dict_binds)

        <- addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
           generalise dflags top_lvl bind_list sig_fn mono_bind_infos lie_req
 
        <- addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
           generalise dflags top_lvl bind_list sig_fn mono_bind_infos lie_req
 

-       -- FINALISE THE QUANTIFIED TYPE VARIABLES
-       -- The quantified type variables often include meta type variables
-       -- we want to freeze them into ordinary type variables, and
-       -- default their kind (e.g. from OpenTypeKind to TypeKind)
-  ; tyvars_to_gen' <- mappM zonkQuantifiedTyVar tyvars_to_gen
-

        -- BUILD THE POLYMORPHIC RESULT IDs
        -- BUILD THE POLYMORPHIC RESULT IDs

-  ; exports <- mapM (mkExport prag_fn tyvars_to_gen' (map idType dict_ids))
+  ; let dict_vars = map instToVar dicts        -- May include equality constraints
+  ; exports <- mapM (mkExport top_lvl prag_fn tyvars_to_gen (map varType dict_vars))

                    mono_bind_infos
 
                    mono_bind_infos
 

-       -- ZONK THE poly_ids, because they are used to extend the type 
-       -- environment; see the invariant on TcEnv.tcExtendIdEnv 

   ; let        poly_ids = [poly_id | (_, poly_id, _, _) <- exports]
   ; let        poly_ids = [poly_id | (_, poly_id, _, _) <- exports]

-  ; zonked_poly_ids <- mappM zonkId poly_ids
+  ; traceTc (text "binding:" <+> ppr (poly_ids `zip` map idType poly_ids))

 
 

-  ; traceTc (text "binding:" <+> ppr (zonked_poly_ids `zip` map idType zonked_poly_ids))
-
-  ; let abs_bind = L loc $ AbsBinds tyvars_to_gen'
-                                   dict_ids exports
+  ; let abs_bind = L loc $ AbsBinds tyvars_to_gen
+                                   dict_vars exports

                                    (dict_binds `unionBags` binds')
 
                                    (dict_binds `unionBags` binds')
 

-  ; return ([unitBag abs_bind], zonked_poly_ids)
+  ; return ([unitBag abs_bind], poly_ids)      -- poly_ids are guaranteed zonked by mkExport

   } }
 
 
 --------------
   } }
 
 
 --------------

-mkExport :: TcPragFun -> [TyVar] -> [TcType] -> MonoBindInfo
-        -> TcM ([TyVar], Id, Id, [Prag])
-mkExport prag_fn inferred_tvs dict_tys (poly_name, mb_sig, mono_id)
-  = case mb_sig of
-      Nothing  -> do { prags <- tcPrags poly_id (prag_fn poly_name)
-                    ; return (inferred_tvs, poly_id, mono_id, prags) }
-         where
-           poly_id = mkLocalId poly_name poly_ty
-           poly_ty = mkForAllTys inferred_tvs
-                                      $ mkFunTys dict_tys 
-                                      $ idType mono_id
-
-      Just sig -> do { let poly_id = sig_id sig
-                    ; prags <- tcPrags poly_id (prag_fn poly_name)
-                    ; sig_tys <- zonkTcTyVars (sig_tvs sig)
-                    ; let sig_tvs' = map (tcGetTyVar "mkExport") sig_tys
-                    ; return (sig_tvs', poly_id, mono_id, prags) }
-               -- We zonk the sig_tvs here so that the export triple
-               -- always has zonked type variables; 
-               -- a convenient invariant
+mkExport :: TopLevelFlag -> TcPragFun -> [TyVar] -> [TcType]
+        -> MonoBindInfo
+        -> TcM ([TyVar], Id, Id, [LPrag])
+-- mkExport generates exports with 
+--     zonked type variables, 
+--     zonked poly_ids
+-- The former is just because no further unifications will change
+-- the quantified type variables, so we can fix their final form
+-- right now.
+-- The latter is needed because the poly_ids are used to extend the
+-- type environment; see the invariant on TcEnv.tcExtendIdEnv 
+
+-- Pre-condition: the inferred_tvs are already zonked
+
+mkExport top_lvl prag_fn inferred_tvs dict_tys (poly_name, mb_sig, mono_id)
+  = do { warn_missing_sigs <- doptM Opt_WarnMissingSigs
+       ; let warn = isTopLevel top_lvl && warn_missing_sigs
+       ; (tvs, poly_id) <- mk_poly_id warn mb_sig
+               -- poly_id has a zonked type
+
+       ; prags <- tcPrags poly_id (prag_fn poly_name)
+               -- tcPrags requires a zonked poly_id
+
+       ; return (tvs, poly_id, mono_id, prags) }
+  where
+    poly_ty = mkForAllTys inferred_tvs (mkFunTys dict_tys (idType mono_id))
+
+    mk_poly_id warn Nothing    = do { poly_ty' <- zonkTcType poly_ty
+                                   ; missingSigWarn warn poly_name poly_ty'
+                                   ; return (inferred_tvs, mkLocalId poly_name poly_ty') }
+    mk_poly_id warn (Just sig) = do { tvs <- mapM zonk_tv (sig_tvs sig)
+                                   ; return (tvs,  sig_id sig) }

 
 

+    zonk_tv tv = do { ty <- zonkTcTyVar tv; return (tcGetTyVar "mkExport" ty) }

 
 ------------------------
 type TcPragFun = Name -> [LSig Name]
 
 ------------------------
 type TcPragFun = Name -> [LSig Name]

@@ -413,16 +409,17 @@ mkPragFun sigs = \n -> lookupNameEnv env n `orElse` []
          env = foldl add emptyNameEnv prs
          add env (n,p) = extendNameEnv_Acc (:) singleton env n p
 
          env = foldl add emptyNameEnv prs
          add env (n,p) = extendNameEnv_Acc (:) singleton env n p
 

-tcPrags :: Id -> [LSig Name] -> TcM [Prag]
-tcPrags poly_id prags = mapM tc_prag prags
+tcPrags :: Id -> [LSig Name] -> TcM [LPrag]
+tcPrags poly_id prags = mapM (wrapLocM tc_prag) prags

   where
   where

-    tc_prag (L loc prag) = setSrcSpan loc $ 
-                          addErrCtxt (pragSigCtxt prag) $ 
-                          tcPrag poly_id prag
+    tc_prag prag = addErrCtxt (pragSigCtxt prag) $ 
+                  tcPrag poly_id prag

 
 pragSigCtxt prag = hang (ptext SLIT("In the pragma")) 2 (ppr prag)
 
 tcPrag :: TcId -> Sig Name -> TcM Prag
 
 pragSigCtxt prag = hang (ptext SLIT("In the pragma")) 2 (ppr prag)
 
 tcPrag :: TcId -> Sig Name -> TcM Prag

+-- Pre-condition: the poly_id is zonked
+-- Reason: required by tcSubExp

 tcPrag poly_id (SpecSig orig_name hs_ty inl) = tcSpecPrag poly_id hs_ty inl
 tcPrag poly_id (SpecInstSig hs_ty)          = tcSpecPrag poly_id hs_ty defaultInlineSpec
 tcPrag poly_id (InlineSig v inl)             = return (InlinePrag inl)
 tcPrag poly_id (SpecSig orig_name hs_ty inl) = tcSpecPrag poly_id hs_ty inl
 tcPrag poly_id (SpecInstSig hs_ty)          = tcSpecPrag poly_id hs_ty defaultInlineSpec
 tcPrag poly_id (InlineSig v inl)             = return (InlinePrag inl)

@@ -430,11 +427,10 @@ tcPrag poly_id (InlineSig v inl)             = return (InlinePrag inl)
 
 tcSpecPrag :: TcId -> LHsType Name -> InlineSpec -> TcM Prag
 tcSpecPrag poly_id hs_ty inl
 
 tcSpecPrag :: TcId -> LHsType Name -> InlineSpec -> TcM Prag
 tcSpecPrag poly_id hs_ty inl

-  = do { spec_ty <- tcHsSigType (FunSigCtxt (idName poly_id)) hs_ty
-       ; (co_fn, lie) <- getLIE (tcSubExp (idType poly_id) spec_ty)
-       ; extendLIEs lie
-       ; let const_dicts = map instToId lie
-       ; return (SpecPrag (mkHsCoerce co_fn (HsVar poly_id)) spec_ty const_dicts inl) }
+  = do { let name = idName poly_id
+       ; spec_ty <- tcHsSigType (FunSigCtxt name) hs_ty
+       ; co_fn <- tcSubExp (SpecPragOrigin name) (idType poly_id) spec_ty
+       ; return (SpecPrag (mkHsWrap co_fn (HsVar poly_id)) spec_ty inl) }

        -- Most of the work of specialisation is done by 
        -- the desugarer, guided by the SpecPrag
   
        -- Most of the work of specialisation is done by 
        -- the desugarer, guided by the SpecPrag
   

@@ -442,15 +438,14 @@ tcSpecPrag poly_id hs_ty inl
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise 
 -- subsequent error messages
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise 
 -- subsequent error messages

-recoveryCode binder_names
+recoveryCode binder_names sig_fn

   = do { traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)
        ; poly_ids <- mapM mk_dummy binder_names
        ; return ([], poly_ids) }
   where
   = do { traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)
        ; poly_ids <- mapM mk_dummy binder_names
        ; return ([], poly_ids) }
   where

-    mk_dummy name = do { mb_id <- tcLookupLocalId_maybe name
-                       ; case mb_id of
-                             Just id -> return id              -- Had signature, was in envt
-                             Nothing -> return (mkLocalId name forall_a_a) }    -- No signature
+    mk_dummy name 
+       | isJust (sig_fn name) = tcLookupId name        -- Had signature; look it up
+       | otherwise            = return (mkLocalId name forall_a_a)    -- No signature

 
 forall_a_a :: TcType
 forall_a_a = mkForAllTy alphaTyVar (mkTyVarTy alphaTyVar)
 
 forall_a_a :: TcType
 forall_a_a = mkForAllTy alphaTyVar (mkTyVarTy alphaTyVar)

@@ -527,7 +522,7 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
        -- e.g.         f = \(x::forall a. a->a) -> <body>
        --      We want to infer a higher-rank type for f
     setSrcSpan b_loc   $
        -- e.g.         f = \(x::forall a. a->a) -> <body>
        --      We want to infer a higher-rank type for f
     setSrcSpan b_loc   $

-    do { ((co_fn, matches'), rhs_ty) <- tcInfer (tcMatchesFun name matches)
+    do { ((co_fn, matches'), rhs_ty) <- tcInfer (tcMatchesFun name inf matches)

 
                -- Check for an unboxed tuple type
                --      f = (# True, False #)
 
                -- Check for an unboxed tuple type
                --      f = (# True, False #)

@@ -542,7 +537,7 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
        ; let mono_id = mkLocalId mono_name zonked_rhs_ty
        ; return (unitBag (L b_loc (FunBind { fun_id = L nm_loc mono_id, fun_infix = inf,
                                              fun_matches = matches', bind_fvs = fvs,
        ; let mono_id = mkLocalId mono_name zonked_rhs_ty
        ; return (unitBag (L b_loc (FunBind { fun_id = L nm_loc mono_id, fun_infix = inf,
                                              fun_matches = matches', bind_fvs = fvs,

-                                             fun_co_fn = co_fn })),
+                                             fun_co_fn = co_fn, fun_tick = Nothing })),

                  [(name, Nothing, mono_id)]) }
 
 tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf, 
                  [(name, Nothing, mono_id)]) }
 
 tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf, 

@@ -554,19 +549,23 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
        -- we can (a) use genuine, rigid skolem constants for the type variables
        --        (b) bring (rigid) scoped type variables into scope
     setSrcSpan b_loc   $
        -- we can (a) use genuine, rigid skolem constants for the type variables
        --        (b) bring (rigid) scoped type variables into scope
     setSrcSpan b_loc   $

-    do { tc_sig <- tcInstSig True name scoped_tvs
+    do { tc_sig <- tcInstSig True name

        ; mono_name <- newLocalName name
        ; let mono_ty = sig_tau tc_sig
              mono_id = mkLocalId mono_name mono_ty
              rhs_tvs = [ (name, mkTyVarTy tv)
        ; mono_name <- newLocalName name
        ; let mono_ty = sig_tau tc_sig
              mono_id = mkLocalId mono_name mono_ty
              rhs_tvs = [ (name, mkTyVarTy tv)

-                       | (name, tv) <- sig_scoped tc_sig `zip` sig_tvs tc_sig ]
+                       | (name, tv) <- scoped_tvs `zip` sig_tvs tc_sig ]
+                       -- See Note [More instantiated than scoped]
+                       -- Note that the scoped_tvs and the (sig_tvs sig) 
+                       -- may have different Names. That's quite ok.

 
 

-       ; (co_fn, matches') <- tcExtendTyVarEnv2 rhs_tvs    $
-                              tcMatchesFun mono_name matches mono_ty
+       ; (co_fn, matches') <- tcExtendTyVarEnv2 rhs_tvs $
+                              tcMatchesFun mono_name inf matches mono_ty

 
        ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, 
                                    fun_infix = inf, fun_matches = matches',
 
        ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, 
                                    fun_infix = inf, fun_matches = matches',

-                                   bind_fvs = placeHolderNames, fun_co_fn = co_fn }
+                                   bind_fvs = placeHolderNames, fun_co_fn = co_fn, 
+                                   fun_tick = Nothing }

        ; return (unitBag (L b_loc fun_bind'),
                  [(name, Just tc_sig, mono_id)]) }
 
        ; return (unitBag (L b_loc fun_bind'),
                  [(name, Just tc_sig, mono_id)]) }
 

@@ -579,9 +578,9 @@ tcMonoBinds binds sig_fn non_rec
                                -- A monomorphic binding for each term variable that lacks 
                                -- a type sig.  (Ones with a sig are already in scope.)
 
                                -- A monomorphic binding for each term variable that lacks 
                                -- a type sig.  (Ones with a sig are already in scope.)
 

-       ; binds' <- tcExtendIdEnv2    rhs_id_env $
+       ; binds' <- tcExtendIdEnv2 rhs_id_env $ do

                    traceTc (text "tcMonoBinds" <+> vcat [ ppr n <+> ppr id <+> ppr (idType id) 
                    traceTc (text "tcMonoBinds" <+> vcat [ ppr n <+> ppr id <+> ppr (idType id) 

-                                                        | (n,id) <- rhs_id_env]) `thenM_`
+                                                        | (n,id) <- rhs_id_env])

                    mapM (wrapLocM tcRhs) tc_binds
        ; return (listToBag binds', mono_info) }
 
                    mapM (wrapLocM tcRhs) tc_binds
        ; return (listToBag binds', mono_info) }
 

@@ -645,9 +644,8 @@ tcLhs sig_fn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss })
                                      | (name, Just sig) <- nm_sig_prs]
              sig_tau_fn  = lookupNameEnv tau_sig_env
 
                                      | (name, Just sig) <- nm_sig_prs]
              sig_tau_fn  = lookupNameEnv tau_sig_env
 

-             tc_pat exp_ty = tcPat (LetPat sig_tau_fn) pat exp_ty unitTy $ \ _ ->
+             tc_pat exp_ty = tcLetPat sig_tau_fn pat exp_ty $

                              mapM lookup_info nm_sig_prs
                              mapM lookup_info nm_sig_prs

-               -- The unitTy is a bit bogus; it's the "result type" for lookup_info.  

 
                -- After typechecking the pattern, look up the binder
                -- names, which the pattern has brought into scope.
 
                -- After typechecking the pattern, look up the binder
                -- names, which the pattern has brought into scope.

@@ -668,11 +666,16 @@ tcLhs sig_fn other_bind = pprPanic "tcLhs" (ppr other_bind)
 
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind TcId)
 
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind TcId)

-tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches)
-  = do { (co_fn, matches') <- tcMatchesFun (idName mono_id) matches 
-                                           (idType mono_id)
+-- When we are doing pattern bindings, or multiple function bindings at a time
+-- we *don't* bring any scoped type variables into scope
+-- Wny not?  They are not completely rigid.
+-- That's why we have the special case for a single FunBind in tcMonoBinds
+tcRhs (TcFunBind (_,_,mono_id) fun' inf matches)
+  = do { (co_fn, matches') <- tcMatchesFun (idName mono_id) inf 
+                                           matches (idType mono_id)

        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',
        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',

-                           bind_fvs = placeHolderNames, fun_co_fn = co_fn }) }
+                           bind_fvs = placeHolderNames, fun_co_fn = co_fn,
+                           fun_tick = Nothing }) }

 
 tcRhs bind@(TcPatBind _ pat' grhss pat_ty)
   = do { grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
 
 tcRhs bind@(TcPatBind _ pat' grhss pat_ty)
   = do { grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $

@@ -701,10 +704,13 @@ getMonoBindInfo tc_binds
 generalise :: DynFlags -> TopLevelFlag 
           -> [LHsBind Name] -> TcSigFun 
           -> [MonoBindInfo] -> [Inst]
 generalise :: DynFlags -> TopLevelFlag 
           -> [LHsBind Name] -> TcSigFun 
           -> [MonoBindInfo] -> [Inst]

-          -> TcM ([TcTyVar], TcDictBinds, [TcId])
+          -> TcM ([TyVar], [Inst], TcDictBinds)
+-- The returned [TyVar] are all ready to quantify
+

 generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
   | isMonoGroup dflags bind_list
 generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
   | isMonoGroup dflags bind_list

-  = do { extendLIEs lie_req; return ([], emptyBag, []) }
+  = do { extendLIEs lie_req
+       ; return ([], [], emptyBag) }

 
   | isRestrictedGroup dflags bind_list sig_fn  -- RESTRICTED CASE
   =    -- Check signature contexts are empty 
 
   | isRestrictedGroup dflags bind_list sig_fn  -- RESTRICTED CASE
   =    -- Check signature contexts are empty 

@@ -719,39 +725,41 @@ generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
        -- Check that signature type variables are OK
        ; final_qtvs <- checkSigsTyVars qtvs sigs
 
        -- Check that signature type variables are OK
        ; final_qtvs <- checkSigsTyVars qtvs sigs
 

-       ; return (final_qtvs, binds, []) }
+       ; return (final_qtvs, [], binds) }

 
   | null sigs  -- UNRESTRICTED CASE, NO TYPE SIGS
   = tcSimplifyInfer doc tau_tvs lie_req
 
   | otherwise  -- UNRESTRICTED CASE, WITH TYPE SIGS
 
   | null sigs  -- UNRESTRICTED CASE, NO TYPE SIGS
   = tcSimplifyInfer doc tau_tvs lie_req
 
   | otherwise  -- UNRESTRICTED CASE, WITH TYPE SIGS

-  = do { sig_lie <- unifyCtxts sigs    -- sigs is non-empty
+  = do { sig_lie <- unifyCtxts sigs    -- sigs is non-empty; sig_lie is zonked

        ; let   -- The "sig_avails" is the stuff available.  We get that from
                -- the context of the type signature, BUT ALSO the lie_avail
                -- so that polymorphic recursion works right (see Note [Polymorphic recursion])
                local_meths = [mkMethInst sig mono_id | (_, Just sig, mono_id) <- mono_infos]
                sig_avails = sig_lie ++ local_meths
        ; let   -- The "sig_avails" is the stuff available.  We get that from
                -- the context of the type signature, BUT ALSO the lie_avail
                -- so that polymorphic recursion works right (see Note [Polymorphic recursion])
                local_meths = [mkMethInst sig mono_id | (_, Just sig, mono_id) <- mono_infos]
                sig_avails = sig_lie ++ local_meths

+               loc = sig_loc (head sigs)

 
        -- Check that the needed dicts can be
        -- expressed in terms of the signature ones
 
        -- Check that the needed dicts can be
        -- expressed in terms of the signature ones

-       ; (forall_tvs, dict_binds) <- tcSimplifyInferCheck doc tau_tvs sig_avails lie_req
+       ; (qtvs, binds) <- tcSimplifyInferCheck loc tau_tvs sig_avails lie_req

        
        -- Check that signature type variables are OK
        
        -- Check that signature type variables are OK

-       ; final_qtvs <- checkSigsTyVars forall_tvs sigs
+       ; final_qtvs <- checkSigsTyVars qtvs sigs

 
 

-       ; returnM (final_qtvs, dict_binds, map instToId sig_lie) }
+       ; return (final_qtvs, sig_lie, binds) }

   where
     bndrs   = bndrNames mono_infos
     sigs    = [sig | (_, Just sig, _) <- mono_infos]
   where
     bndrs   = bndrNames mono_infos
     sigs    = [sig | (_, Just sig, _) <- mono_infos]

-    tau_tvs = foldr (unionVarSet . exactTyVarsOfType . getMonoType) emptyVarSet mono_infos
-               -- NB: exactTyVarsOfType; see Note [Silly type synonym] 
-               --     near defn of TcType.exactTyVarsOfType
+    get_tvs | isTopLevel top_lvl = tyVarsOfType         -- See Note [Silly type synonym] in TcType
+           | otherwise          = exactTyVarsOfType
+    tau_tvs = foldr (unionVarSet . get_tvs . getMonoType) emptyVarSet mono_infos

     is_mono_sig sig = null (sig_theta sig)
     doc = ptext SLIT("type signature(s) for") <+> pprBinders bndrs
 
     mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
                            sig_theta = theta, sig_loc = loc }) mono_id
     is_mono_sig sig = null (sig_theta sig)
     doc = ptext SLIT("type signature(s) for") <+> pprBinders bndrs
 
     mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
                            sig_theta = theta, sig_loc = loc }) mono_id

-      = Method mono_id poly_id (mkTyVarTys tvs) theta loc
+      = Method {tci_id = mono_id, tci_oid = poly_id, tci_tys = mkTyVarTys tvs,
+               tci_theta = theta, tci_loc = loc}

 \end{code}
 
 unifyCtxts checks that all the signature contexts are the same
 \end{code}
 
 unifyCtxts checks that all the signature contexts are the same

@@ -768,21 +776,33 @@ might not otherwise be related.  This is a rather subtle issue.
 
 \begin{code}
 unifyCtxts :: [TcSigInfo] -> TcM [Inst]
 
 \begin{code}
 unifyCtxts :: [TcSigInfo] -> TcM [Inst]

+-- Post-condition: the returned Insts are full zonked

 unifyCtxts (sig1 : sigs)       -- Argument is always non-empty
   = do { mapM unify_ctxt sigs
 unifyCtxts (sig1 : sigs)       -- Argument is always non-empty
   = do { mapM unify_ctxt sigs

-       ; newDictsAtLoc (sig_loc sig1) (sig_theta sig1) }
+       ; theta <- zonkTcThetaType (sig_theta sig1)
+       ; newDictBndrs (sig_loc sig1) theta }

   where
     theta1 = sig_theta sig1
     unify_ctxt :: TcSigInfo -> TcM ()
     unify_ctxt sig@(TcSigInfo { sig_theta = theta })
   where
     theta1 = sig_theta sig1
     unify_ctxt :: TcSigInfo -> TcM ()
     unify_ctxt sig@(TcSigInfo { sig_theta = theta })

-       = setSrcSpan (instLocSrcSpan (sig_loc sig))     $
+       = setSrcSpan (instLocSpan (sig_loc sig))        $

          addErrCtxt (sigContextsCtxt sig1 sig)         $
          addErrCtxt (sigContextsCtxt sig1 sig)         $

-         unifyTheta theta1 theta
+         do { cois <- unifyTheta theta1 theta
+            ; -- Check whether all coercions are identity coercions
+              -- That can happen if we have, say
+              --         f :: C [a]   => ...
+              --         g :: C (F a) => ...
+              -- where F is a type function and (F a ~ [a])
+              -- Then unification might succeed with a coercion.  But it's much
+              -- much simpler to require that such signatures have identical contexts
+              checkTc (all isIdentityCoercion cois)
+                      (ptext SLIT("Mutually dependent functions have syntactically distinct contexts"))
+            }

 
 checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
 checkSigsTyVars qtvs sigs 
   = do { gbl_tvs <- tcGetGlobalTyVars
 
 checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
 checkSigsTyVars qtvs sigs 
   = do { gbl_tvs <- tcGetGlobalTyVars

-       ; sig_tvs_s <- mappM (check_sig gbl_tvs) sigs
+       ; sig_tvs_s <- mapM (check_sig gbl_tvs) sigs

 
        ; let   -- Sigh.  Make sure that all the tyvars in the type sigs
                -- appear in the returned ty var list, which is what we are
 
        ; let   -- Sigh.  Make sure that all the tyvars in the type sigs
                -- appear in the returned ty var list, which is what we are

@@ -794,15 +814,15 @@ checkSigsTyVars qtvs sigs
                -- Here, 'a' won't appear in qtvs, so we have to add it
                sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
                all_tvs = varSetElems (extendVarSetList sig_tvs qtvs)
                -- Here, 'a' won't appear in qtvs, so we have to add it
                sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
                all_tvs = varSetElems (extendVarSetList sig_tvs qtvs)

-       ; returnM all_tvs }
+       ; return all_tvs }

   where
     check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs, 
                                  sig_theta = theta, sig_tau = tau})
       = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id))       $
        addErrCtxtM (sigCtxt id tvs theta tau)                                          $
        do { tvs' <- checkDistinctTyVars tvs
   where
     check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs, 
                                  sig_theta = theta, sig_tau = tau})
       = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id))       $
        addErrCtxtM (sigCtxt id tvs theta tau)                                          $
        do { tvs' <- checkDistinctTyVars tvs

-          ; ifM (any (`elemVarSet` gbl_tvs) tvs')
-                (bleatEscapedTvs gbl_tvs tvs tvs') 
+          ; when (any (`elemVarSet` gbl_tvs) tvs')
+                 (bleatEscapedTvs gbl_tvs tvs tvs')

           ; return tvs' }
 
 checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar]
           ; return tvs' }
 
 checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar]

@@ -838,7 +858,7 @@ checkDistinctTyVars sig_tvs
                         <+> quotes (ppr tidy_tv2)
            ; failWithTcM (env2, msg) }
        where
                         <+> quotes (ppr tidy_tv2)
            ; failWithTcM (env2, msg) }
        where

-\end{code}    
+\end{code}

 
 
 @getTyVarsToGen@ decides what type variables to generalise over.
 
 
 @getTyVarsToGen@ decides what type variables to generalise over.

@@ -958,6 +978,44 @@ The @TcSigInfo@ contains @TcTypes@ because they are unified with
 the variable's type, and after that checked to see whether they've
 been instantiated.
 
 the variable's type, and after that checked to see whether they've
 been instantiated.
 

+Note [Scoped tyvars]
+~~~~~~~~~~~~~~~~~~~~
+The -XScopedTypeVariables flag brings lexically-scoped type variables
+into scope for any explicitly forall-quantified type variables:
+       f :: forall a. a -> a
+       f x = e
+Then 'a' is in scope inside 'e'.
+
+However, we do *not* support this 
+  - For pattern bindings e.g
+       f :: forall a. a->a
+       (f,g) = e
+
+  - For multiple function bindings, unless Opt_RelaxedPolyRec is on
+       f :: forall a. a -> a
+       f = g
+       g :: forall b. b -> b
+       g = ...f...
+    Reason: we use mutable variables for 'a' and 'b', since they may
+    unify to each other, and that means the scoped type variable would
+    not stand for a completely rigid variable.
+
+    Currently, we simply make Opt_ScopedTypeVariables imply Opt_RelaxedPolyRec
+
+
+Note [More instantiated than scoped]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There may be more instantiated type variables than lexically-scoped 
+ones.  For example:
+       type T a = forall b. b -> (a,b)
+       f :: forall c. T c
+Here, the signature for f will have one scoped type variable, c,
+but two instantiated type variables, c' and b'.  
+
+We assume that the scoped ones are at the *front* of sig_tvs,
+and remember the names from the original HsForAllTy in the TcSigFun.
+
+

 \begin{code}
 type TcSigFun = Name -> Maybe [Name]   -- Maps a let-binder to the list of
                                        -- type variables brought into scope
 \begin{code}
 type TcSigFun = Name -> Maybe [Name]   -- Maps a let-binder to the list of
                                        -- type variables brought into scope

@@ -970,23 +1028,18 @@ mkTcSigFun :: [LSig Name] -> TcSigFun
 -- Precondition: no duplicates
 mkTcSigFun sigs = lookupNameEnv env
   where
 -- Precondition: no duplicates
 mkTcSigFun sigs = lookupNameEnv env
   where

-    env = mkNameEnv [(name, scoped_tyvars hs_ty)
-                   | L span (TypeSig (L _ name) (L _ hs_ty)) <- sigs]
-    scoped_tyvars (HsForAllTy Explicit tvs _ _) = hsLTyVarNames tvs
-    scoped_tyvars other                                = []
+    env = mkNameEnv [(name, hsExplicitTvs lhs_ty)
+                   | L span (TypeSig (L _ name) lhs_ty) <- sigs]

        -- The scoped names are the ones explicitly mentioned
        -- in the HsForAll.  (There may be more in sigma_ty, because
        -- The scoped names are the ones explicitly mentioned
        -- in the HsForAll.  (There may be more in sigma_ty, because

-       -- of nested type synonyms.  See Note [Scoped] with TcSigInfo.)
+       -- of nested type synonyms.  See Note [More instantiated than scoped].)
+       -- See Note [Only scoped tyvars are in the TyVarEnv]

 
 ---------------
 data TcSigInfo
   = TcSigInfo {
        sig_id     :: TcId,             --  *Polymorphic* binder for this value...
 
 
 ---------------
 data TcSigInfo
   = TcSigInfo {
        sig_id     :: TcId,             --  *Polymorphic* binder for this value...
 

-       sig_scoped :: [Name],           -- Names for any scoped type variables
-                                       -- Invariant: correspond 1-1 with an initial
-                                       -- segment of sig_tvs (see Note [Scoped])
-

        sig_tvs    :: [TcTyVar],        -- Instantiated type variables
                                        -- See Note [Instantiate sig]
 
        sig_tvs    :: [TcTyVar],        -- Instantiated type variables
                                        -- See Note [Instantiate sig]
 

@@ -995,19 +1048,21 @@ data TcSigInfo
        sig_loc    :: InstLoc           -- The location of the signature
     }
 
        sig_loc    :: InstLoc           -- The location of the signature
     }
 

---     Note [Scoped]
--- There may be more instantiated type variables than scoped 
--- ones.  For example:
---     type T a = forall b. b -> (a,b)
---     f :: forall c. T c
--- Here, the signature for f will have one scoped type variable, c,
--- but two instantiated type variables, c' and b'.  
+
+--     Note [Only scoped tyvars are in the TyVarEnv]
+-- We are careful to keep only the *lexically scoped* type variables in
+-- the type environment.  Why?  After all, the renamer has ensured
+-- that only legal occurrences occur, so we could put all type variables
+-- into the type env.

 --
 --

--- We assume that the scoped ones are at the *front* of sig_tvs,
--- and remember the names from the original HsForAllTy in sig_scoped
+-- But we want to check that two distinct lexically scoped type variables
+-- do not map to the same internal type variable.  So we need to know which
+-- the lexically-scoped ones are... and at the moment we do that by putting
+-- only the lexically scoped ones into the environment.
+

 
 --     Note [Instantiate sig]
 
 --     Note [Instantiate sig]

--- It's vital to instantiate a type signature with fresh variable.
+-- It's vital to instantiate a type signature with fresh variables.

 -- For example:
 --     type S = forall a. a->a
 --     f,g :: S
 -- For example:
 --     type S = forall a. a->a
 --     f,g :: S

@@ -1036,14 +1091,16 @@ tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo)
 tcInstSig_maybe sig_fn name 
   = case sig_fn name of
        Nothing  -> return Nothing
 tcInstSig_maybe sig_fn name 
   = case sig_fn name of
        Nothing  -> return Nothing

-       Just tvs -> do  { tc_sig <- tcInstSig False name tvs
-                       ; return (Just tc_sig) }
+       Just scoped_tvs -> do   { tc_sig <- tcInstSig False name
+                               ; return (Just tc_sig) }
+       -- NB: the scoped_tvs may be non-empty, but we can 
+       -- just ignore them.  See Note [Scoped tyvars].

 
 

-tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo
+tcInstSig :: Bool -> Name -> TcM TcSigInfo

 -- Instantiate the signature, with either skolems or meta-type variables
 -- depending on the use_skols boolean.  This variable is set True
 -- when we are typechecking a single function binding; and False for
 -- Instantiate the signature, with either skolems or meta-type variables
 -- depending on the use_skols boolean.  This variable is set True
 -- when we are typechecking a single function binding; and False for

--- pattern bindigs and a group of several function bindings.
+-- pattern bindings and a group of several function bindings.

 -- Reason: in the latter cases, the "skolems" can be unified together, 
 --        so they aren't properly rigid in the type-refinement sense.
 -- NB: unless we are doing H98, each function with a sig will be done
 -- Reason: in the latter cases, the "skolems" can be unified together, 
 --        so they aren't properly rigid in the type-refinement sense.
 -- NB: unless we are doing H98, each function with a sig will be done

@@ -1058,25 +1115,16 @@ tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo
 --
 -- We must not use the same 'a' from the defn of T at both places!!
 
 --
 -- We must not use the same 'a' from the defn of T at both places!!
 

-tcInstSig use_skols name scoped_names
+tcInstSig use_skols name

   = do { poly_id <- tcLookupId name    -- Cannot fail; the poly ids are put into 
                                        -- scope when starting the binding group
        ; let skol_info = SigSkol (FunSigCtxt name)
   = do { poly_id <- tcLookupId name    -- Cannot fail; the poly ids are put into 
                                        -- scope when starting the binding group
        ; let skol_info = SigSkol (FunSigCtxt name)

-             inst_tyvars | use_skols = tcInstSkolTyVars skol_info
-                         | otherwise = tcInstSigTyVars  skol_info
+             inst_tyvars = tcInstSigTyVars use_skols skol_info

        ; (tvs, theta, tau) <- tcInstType inst_tyvars (idType poly_id)
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
        ; (tvs, theta, tau) <- tcInstType inst_tyvars (idType poly_id)
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 

-                             sig_scoped = final_scoped_names, sig_loc = loc }) }
-               -- Note that the scoped_names and the sig_tvs will have
-               -- different Names. That's quite ok; when we bring the 
-               -- scoped_names into scope, we just bind them to the sig_tvs
-  where
-       -- We also only have scoped type variables when we are instantiating
-       -- with true skolems
-    final_scoped_names | use_skols = scoped_names
-                      | otherwise = []
+                             sig_loc = loc }) }

 
 -------------------
 isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool
 
 -------------------
 isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool

@@ -1145,4 +1193,13 @@ restrictedBindCtxtErr binder_names
 
 genCtxt binder_names
   = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
 
 genCtxt binder_names
   = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names

+
+missingSigWarn False name ty = return ()
+missingSigWarn True  name ty
+  = do         { env0 <- tcInitTidyEnv
+       ; let (env1, tidy_ty) = tidyOpenType env0 ty
+       ; addWarnTcM (env1, mk_msg tidy_ty) }
+  where
+    mk_msg ty = vcat [ptext SLIT("Definition but no type signature for") <+> quotes (ppr name),
+                     sep [ptext SLIT("Inferred type:") <+> pprHsVar name <+> dcolon <+> ppr ty]]

 \end{code}
 \end{code}