Don't import FastString in HsVersions.h

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

diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 9e0b583..d9f5587 100644 (file)
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -5,6 +5,13 @@
 \section[TcBinds]{TcBinds}
 
 \begin{code}
 \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, 

@@ -30,11 +37,12 @@ import TcPat
 import TcMType
 import TcType
 import {- Kind parts of -} Type
 import TcMType
 import TcType
 import {- Kind parts of -} Type

+import Coercion

 import VarEnv
 import TysPrim
 import Id
 import IdInfo
 import VarEnv
 import TysPrim
 import Id
 import IdInfo

-import Var ( TyVar )
+import Var ( TyVar, varType )

 import Name
 import NameSet
 import NameEnv
 import Name
 import NameSet
 import NameEnv

@@ -44,9 +52,13 @@ import Bag
 import ErrUtils
 import Digraph
 import Maybes
 import ErrUtils
 import Digraph
 import Maybes

+import List

 import Util
 import BasicTypes
 import Outputable
 import Util
 import BasicTypes
 import Outputable

+import FastString
+
+import Control.Monad

 \end{code}
 
 
 \end{code}
 
 

@@ -132,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 

@@ -161,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) }

@@ -175,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) }
 
 ------------------------

@@ -194,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) }
 

@@ -240,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
 

@@ -310,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

@@ -329,25 +342,20 @@ 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
 
   ; let        poly_ids = [poly_id | (_, poly_id, _, _) <- exports]
   ; traceTc (text "binding:" <+> ppr (poly_ids `zip` map idType poly_ids))
 
                    mono_bind_infos
 
   ; let        poly_ids = [poly_id | (_, poly_id, _, _) <- exports]
   ; traceTc (text "binding:" <+> ppr (poly_ids `zip` map idType 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')
 
   ; return ([unitBag abs_bind], poly_ids)      -- poly_ids are guaranteed zonked by mkExport
                                    (dict_binds `unionBags` binds')
 
   ; return ([unitBag abs_bind], poly_ids)      -- poly_ids are guaranteed zonked by mkExport

@@ -355,8 +363,9 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
 
 
 --------------
 
 
 --------------

-mkExport :: TcPragFun -> [TyVar] -> [TcType] -> MonoBindInfo
-        -> TcM ([TyVar], Id, Id, [Prag])
+mkExport :: TopLevelFlag -> TcPragFun -> [TyVar] -> [TcType]
+        -> MonoBindInfo
+        -> TcM ([TyVar], Id, Id, [LPrag])

 -- mkExport generates exports with 
 --     zonked type variables, 
 --     zonked poly_ids
 -- mkExport generates exports with 
 --     zonked type variables, 
 --     zonked poly_ids

@@ -368,20 +377,24 @@ mkExport :: TcPragFun -> [TyVar] -> [TcType] -> MonoBindInfo
 
 -- Pre-condition: the inferred_tvs are already zonked
 
 
 -- Pre-condition: the inferred_tvs are already zonked
 

-mkExport prag_fn inferred_tvs dict_tys (poly_name, mb_sig, mono_id)
-  = do { (tvs, poly_id) <- mk_poly_id mb_sig
+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

 
 

-       ; poly_id' <- zonkId poly_id
-       ; prags <- tcPrags poly_id' (prag_fn poly_name)
+       ; prags <- tcPrags poly_id (prag_fn poly_name)

                -- tcPrags requires a zonked poly_id
 
                -- tcPrags requires a zonked poly_id
 

-       ; return (tvs, poly_id', mono_id, prags) }
+       ; return (tvs, poly_id, mono_id, prags) }

   where
     poly_ty = mkForAllTys inferred_tvs (mkFunTys dict_tys (idType mono_id))
 
   where
     poly_ty = mkForAllTys inferred_tvs (mkFunTys dict_tys (idType mono_id))
 

-    mk_poly_id Nothing    = return (inferred_tvs, mkLocalId poly_name poly_ty)
-    mk_poly_id (Just sig) = do { tvs <- mapM zonk_tv (sig_tvs sig)
-                              ; return (tvs,  sig_id sig) }
+    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) }
 
 
     zonk_tv tv = do { ty <- zonkTcTyVar tv; return (tcGetTyVar "mkExport" ty) }
 

@@ -396,12 +409,11 @@ 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)
 
 
 pragSigCtxt prag = hang (ptext SLIT("In the pragma")) 2 (ppr prag)
 

@@ -415,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 (mkHsWrap 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
   

@@ -511,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 #)

@@ -538,15 +549,18 @@ 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',

@@ -564,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) }
 

@@ -652,9 +666,13 @@ 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',
                            bind_fvs = placeHolderNames, fun_co_fn = co_fn,
                            fun_tick = Nothing }) }
        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',
                            bind_fvs = placeHolderNames, fun_co_fn = co_fn,
                            fun_tick = Nothing }) }

@@ -686,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 

@@ -704,7 +725,7 @@ 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
 
   | null sigs  -- UNRESTRICTED CASE, NO TYPE SIGS
   = tcSimplifyInfer doc tau_tvs lie_req

@@ -720,18 +741,18 @@ generalise dflags top_lvl bind_list sig_fn mono_infos lie_req
 
        -- 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 loc 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
 
     is_mono_sig sig = null (sig_theta sig)
     doc = ptext SLIT("type signature(s) for") <+> pprBinders bndrs
 

@@ -766,12 +787,22 @@ unifyCtxts (sig1 : sigs)  -- Argument is always non-empty
     unify_ctxt sig@(TcSigInfo { sig_theta = theta })
        = setSrcSpan (instLocSpan (sig_loc sig))        $
          addErrCtxt (sigContextsCtxt sig1 sig)         $
     unify_ctxt sig@(TcSigInfo { sig_theta = theta })
        = setSrcSpan (instLocSpan (sig_loc 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

@@ -783,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]

@@ -827,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.

@@ -947,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

@@ -963,7 +1032,7 @@ mkTcSigFun sigs = lookupNameEnv env
                    | 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
                    | 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

-       -- 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]
 
 ---------------
        -- See Note [Only scoped tyvars are in the TyVarEnv]
 
 ---------------

@@ -971,10 +1040,6 @@ data TcSigInfo
   = TcSigInfo {
        sig_id     :: TcId,             --  *Polymorphic* binder for this value...
 
   = 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]
 

@@ -996,17 +1061,6 @@ data TcSigInfo
 -- only the lexically scoped ones into the environment.
 
 
 -- only the lexically scoped ones into the environment.
 
 

---     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'.  
---
--- We assume that the scoped ones are at the *front* of sig_tvs,
--- and remember the names from the original HsForAllTy in sig_scoped
-

 --     Note [Instantiate sig]
 -- It's vital to instantiate a type signature with fresh variables.
 -- For example:
 --     Note [Instantiate sig]
 -- It's vital to instantiate a type signature with fresh variables.
 -- For example:

@@ -1037,10 +1091,12 @@ 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

@@ -1059,7 +1115,7 @@ 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)

@@ -1068,15 +1124,7 @@ tcInstSig use_skols name scoped_names
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
        ; 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}