projects / ghc-hetmet.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Make FamInst warning-free
[ghc-hetmet.git] / compiler / typecheck / TcBinds.lhs
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index e71d920..3b9a496 100644 (file)
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -1,72 +1,62 @@
 %
 %
+% (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, 
 module TcBinds ( tcLocalBinds, tcTopBinds, 
                 tcHsBootSigs, tcMonoBinds, 
-                TcPragFun, tcSpecPrag, tcPrags, mkPragFun,
-                TcSigInfo(..),
+                TcPragFun, tcSpecPrag, tcPrags, mkPragFun, 
+                TcSigInfo(..), TcSigFun, mkTcSigFun,
                 badBootDeclErr ) where
 
                 badBootDeclErr ) where
 
-#include "HsVersions.h"
-
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 
-import DynFlags                ( DynFlag(Opt_MonomorphismRestriction, 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}
 
 
@@ -126,7 +116,7 @@ tcHsBootSigs (ValBindsOut binds sigs)
 tcHsBootSigs groups = pprPanic "tcHsBootSigs" (ppr groups)
 
 badBootDeclErr :: Message
 tcHsBootSigs groups = pprPanic "tcHsBootSigs" (ppr groups)
 
 badBootDeclErr :: Message
-badBootDeclErr = ptext SLIT("Illegal declarations in an hs-boot file")
+badBootDeclErr = ptext (sLit "Illegal declarations in an hs-boot file")
 
 ------------------------
 tcLocalBinds :: HsLocalBinds Name -> TcM thing
 
 ------------------------
 tcLocalBinds :: HsLocalBinds Name -> TcM thing
@@ -152,11 +142,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 
@@ -170,7 +160,7 @@ tcValBinds top_lvl (ValBindsOut binds sigs) thing_inside
   = do         {       -- Typecheck the signature
        ; let { prag_fn = mkPragFun sigs
              ; ty_sigs = filter isVanillaLSig sigs
   = do         {       -- Typecheck the signature
        ; let { prag_fn = mkPragFun sigs
              ; ty_sigs = filter isVanillaLSig sigs
-             ; sig_fn  = mkSigFun ty_sigs }
+             ; sig_fn  = mkTcSigFun ty_sigs }
 
        ; poly_ids <- mapM tcTySig ty_sigs
                -- No recovery from bad signatures, because the type sigs
 
        ; poly_ids <- mapM tcTySig ty_sigs
                -- No recovery from bad signatures, because the type sigs
@@ -181,31 +171,32 @@ 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
+       ; poly_rec <- doptM Opt_RelaxedPolyRec
        ; (binds', thing) <- tcExtendIdEnv poly_ids $
        ; (binds', thing) <- tcExtendIdEnv poly_ids $
-                            tc_val_binds 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) }
 
 ------------------------
-tc_val_binds :: TopLevelFlag -> TcSigFun -> TcPragFun
+tc_val_binds :: Bool -> TopLevelFlag -> TcSigFun -> TcPragFun
             -> [(RecFlag, LHsBinds Name)] -> TcM thing
             -> TcM ([(RecFlag, LHsBinds TcId)], thing)
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 
             -> [(RecFlag, LHsBinds Name)] -> TcM thing
             -> TcM ([(RecFlag, LHsBinds TcId)], thing)
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 
-tc_val_binds 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 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 top_lvl sig_fn prag_fn group $ 
-                  tc_val_binds 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) }
 
 ------------------------
-tc_group :: TopLevelFlag -> TcSigFun -> TcPragFun
+tc_group :: Bool -> TopLevelFlag -> TcSigFun -> TcPragFun
         -> (RecFlag, LHsBinds Name) -> TcM thing
         -> TcM ([(RecFlag, LHsBinds TcId)], thing)
 
         -> (RecFlag, LHsBinds Name) -> TcM thing
         -> TcM ([(RecFlag, LHsBinds TcId)], thing)
 
@@ -213,41 +204,60 @@ tc_group :: 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 top_lvl sig_fn prag_fn (NonRecursive, binds) thing_inside
-  =    -- A single non-recursive binding
+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
        -- We want to keep non-recursive things non-recursive
         -- so that we desugar unlifted bindings correctly
-    do { (binds, thing) <- tcPolyBinds top_lvl NonRecursive NonRecursive
-                                       sig_fn prag_fn binds thing_inside
+ =  do { (binds, thing) <- tc_haskell98 top_lvl sig_fn prag_fn NonRecursive binds thing_inside
        ; return ([(NonRecursive, b) | b <- binds], thing) }
 
        ; return ([(NonRecursive, b) | b <- binds], thing) }
 
-tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
-  =    -- A recursive strongly-connected component
-       -- To maximise polymorphism (with -fglasgow-exts), we do a new 
+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) }
+
+  | otherwise          -- Recursive group, with gla-exts
+  =    -- To maximise polymorphism (with -fglasgow-exts), we do a new 
        -- strongly-connected-component analysis, this time omitting 
        -- any references to variables with type signatures.
        --
        -- strongly-connected-component analysis, this time omitting 
        -- any references to variables with type signatures.
        --
-       -- Then we bring into scope all the variables with type signatures
+       -- Notice that the bindInsts thing covers *all* the bindings in the original
+       -- group at once; an earlier one may use a later one!
     do { traceTc (text "tc_group rec" <+> pprLHsBinds binds)
     do { traceTc (text "tc_group rec" <+> pprLHsBinds binds)
-       ; gla_exts     <- doptM Opt_GlasgowExts
-       ; (binds,thing) <- if gla_exts 
-                          then go new_sccs
-                          else tc_binds Recursive binds thing_inside
-       ; return ([(Recursive, unionManyBags binds)], thing) }
+       ; (binds1,thing) <- bindLocalInsts top_lvl $
+                           go (stronglyConnComp (mkEdges sig_fn binds))
+       ; return ([(Recursive, unionManyBags binds1)], thing) }
                -- Rec them all together
   where
                -- Rec them all together
   where
-    new_sccs :: [SCC (LHsBind Name)]
-    new_sccs = stronglyConnComp (mkEdges sig_fn binds)
+--  go :: SCC (LHsBind Name) -> TcM ([LHsBind TcId], [TcId], thing)
+    go (scc:sccs) = do { (binds1, ids1) <- tc_scc scc
+                       ; (binds2, ids2, thing) <- tcExtendIdEnv ids1 $ go sccs
+                       ; return (binds1 ++ binds2, ids1 ++ ids2, thing) }
+    go []        = do  { thing <- thing_inside; return ([], [], thing) }
+
+    tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive (unitBag bind)
+    tc_scc (CyclicSCC binds) = tc_sub_group Recursive    (listToBag binds)
 
 
---  go :: SCC (LHsBind Name) -> TcM ([LHsBind TcId], thing)
-    go (scc:sccs) = do { (binds1, (binds2, thing)) <- go1 scc (go sccs)
-                       ; return (binds1 ++ binds2, thing) }
-    go []        = do  { thing <- thing_inside; return ([], thing) }
+    tc_sub_group = tcPolyBinds top_lvl sig_fn prag_fn Recursive
 
 
-    go1 (AcyclicSCC bind) = tc_binds NonRecursive (unitBag bind)
-    go1 (CyclicSCC binds) = tc_binds Recursive    (listToBag binds)
+tc_haskell98 top_lvl sig_fn prag_fn rec_flag binds thing_inside
+  = bindLocalInsts top_lvl $ do
+    { (binds1, ids) <- tcPolyBinds top_lvl sig_fn prag_fn rec_flag rec_flag binds
+    ; thing <- tcExtendIdEnv ids thing_inside
+    ; return (binds1, ids, thing) }
 
 
-    tc_binds rec_tc binds = tcPolyBinds top_lvl Recursive rec_tc sig_fn prag_fn binds
+------------------------
+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 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
+
+  | otherwise  -- Nested case
+  = do { ((binds, ids, thing), lie) <- getLIE thing_inside
+       ; lie_binds <- bindInstsOfLocalFuns lie ids
+       ; return (binds ++ [lie_binds], thing) }
 
 ------------------------
 mkEdges :: TcSigFun -> LHsBinds Name
 
 ------------------------
 mkEdges :: TcSigFun -> LHsBinds Name
@@ -275,76 +285,42 @@ bindersOfHsBind (PatBind { pat_lhs = pat })  = collectPatBinders pat
 bindersOfHsBind (FunBind { fun_id = L _ f }) = [f]
 
 ------------------------
 bindersOfHsBind (FunBind { fun_id = L _ f }) = [f]
 
 ------------------------
-tcPolyBinds :: TopLevelFlag 
+tcPolyBinds :: TopLevelFlag -> TcSigFun -> TcPragFun
            -> RecFlag                  -- Whether the group is really recursive
            -> RecFlag                  -- Whether the group is really recursive
-           -> RecFlag                  -- Whether it's recursive for typechecking purposes
-           -> TcSigFun -> TcPragFun
+           -> RecFlag                  -- Whether it's recursive after breaking
+                                       -- dependencies based on type signatures
            -> LHsBinds Name
            -> LHsBinds Name
-           -> TcM thing
-           -> TcM ([LHsBinds TcId], thing)
+           -> TcM ([LHsBinds TcId], [TcId])
 
 -- Typechecks a single bunch of bindings all together, 
 -- and generalises them.  The bunch may be only part of a recursive
 -- group, because we use type signatures to maximise polymorphism
 --
 
 -- Typechecks a single bunch of bindings all together, 
 -- and generalises them.  The bunch may be only part of a recursive
 -- group, because we use type signatures to maximise polymorphism
 --
--- Deals with the bindInstsOfLocalFuns thing too
---
 -- Returns a list because the input may be a single non-recursive binding,
 -- in which case the dependency order of the resulting bindings is
 -- important.  
 -- Returns a list because the input may be a single non-recursive binding,
 -- in which case the dependency order of the resulting bindings is
 -- important.  
-
-tcPolyBinds top_lvl rec_group rec_tc sig_fn prag_fn scc thing_inside
-  =    -- NB: polymorphic recursion means that a function
-       -- may use an instance of itself, we must look at the LIE arising
-       -- from the function's own right hand side.  Hence the getLIE
-       -- encloses the tc_poly_binds. 
-    do { traceTc (text "tcPolyBinds" <+> ppr scc)
-       ; ((binds1, poly_ids, thing), lie) <- getLIE $ 
-               do { (binds1, poly_ids) <- tc_poly_binds top_lvl rec_group rec_tc
-                                                        sig_fn prag_fn scc
-                  ; thing <- tcExtendIdEnv poly_ids thing_inside
-                  ; return (binds1, poly_ids, thing) }
-
-       ; if isTopLevel top_lvl 
-         then          -- For the top level don't bother will 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
-               do { extendLIEs lie; return (binds1, thing) }
-
-         else do       -- Nested case
-               { lie_binds <- bindInstsOfLocalFuns lie poly_ids
-               ; return (binds1 ++ [lie_binds], thing) }}
-
-------------------------
-tc_poly_binds :: TopLevelFlag          -- See comments on tcPolyBinds
-             -> RecFlag -> RecFlag
-             -> TcSigFun -> TcPragFun
-             -> LHsBinds Name
-             -> TcM ([LHsBinds TcId], [TcId])
--- Typechecks the bindings themselves
+-- 
 -- Knows nothing about the scope of the bindings
 
 -- Knows nothing about the scope of the bindings
 
-tc_poly_binds top_lvl rec_group rec_tc sig_fn prag_fn binds
+tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
   = let 
   = let 
-        binder_names = collectHsBindBinders binds
        bind_list    = bagToList binds
        bind_list    = bagToList binds
-
-       loc = getLoc (head bind_list)
+        binder_names = collectHsBindBinders binds
+       loc          = getLoc (head bind_list)
                -- TODO: location a bit awkward, but the mbinds have been
                --       dependency analysed and may no longer be adjacent
     in
        -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
     setSrcSpan loc                             $
                -- TODO: location a bit awkward, but the mbinds have been
                --       dependency analysed and may no longer be adjacent
     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)
 
        -- 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
@@ -363,58 +339,62 @@ tc_poly_binds top_lvl rec_group rec_tc sig_fn prag_fn binds
                   [poly_id | (_, poly_id, _, _) <- exports]) } -- Guaranteed zonked
 
     else do    -- The normal lifted case: GENERALISE
                   [poly_id | (_, poly_id, _, _) <- exports]) } -- Guaranteed zonked
 
     else do    -- The normal lifted case: GENERALISE
-  { is_unres <- isUnRestrictedGroup bind_list sig_fn
-  ; (tyvars_to_gen, dict_binds, dict_ids)
+  { dflags <- getDOpts 
+  ; (tyvars_to_gen, dicts, dict_binds)
        <- addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
        <- addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
-          generalise top_lvl is_unres 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
+          generalise dflags top_lvl bind_list sig_fn mono_bind_infos lie_req
 
        -- 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 (zonked_poly_ids `zip` map idType zonked_poly_ids))
+  ; 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')
 
                                    (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]
@@ -427,16 +407,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)
+pragSigCtxt prag = hang (ptext (sLit "In the pragma")) 2 (ppr prag)
 
 tcPrag :: TcId -> Sig Name -> TcM 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)
@@ -444,25 +425,25 @@ 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
   
 --------------
 -- 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)
@@ -496,17 +477,18 @@ checkStrictBinds top_lvl rec_group mbind mono_tys infos
     check_sig other           = return ()
 
 strictBindErr flavour unlifted mbind
     check_sig other           = return ()
 
 strictBindErr flavour unlifted mbind
-  = hang (text flavour <+> msg <+> ptext SLIT("aren't allowed:")) 4 (ppr mbind)
+  = hang (text flavour <+> msg <+> ptext (sLit "aren't allowed:")) 
+        4 (pprLHsBinds mbind)
   where
   where
-    msg | unlifted  = ptext SLIT("bindings for unlifted types")
-       | otherwise = ptext SLIT("bang-pattern bindings")
+    msg | unlifted  = ptext (sLit "bindings for unlifted types")
+       | otherwise = ptext (sLit "bang-pattern bindings")
 
 badStrictSig unlifted sig
 
 badStrictSig unlifted sig
-  = hang (ptext SLIT("Illegal polymorphic signature in") <+> msg)
+  = hang (ptext (sLit "Illegal polymorphic signature in") <+> msg)
         4 (ppr sig)
   where
         4 (ppr sig)
   where
-    msg | unlifted  = ptext SLIT("an unlifted binding")
-       | otherwise = ptext SLIT("a bang-pattern binding")
+    msg | unlifted  = ptext (sLit "an unlifted binding")
+       | otherwise = ptext (sLit "a bang-pattern binding")
 \end{code}
 
 
 \end{code}
 
 
@@ -538,7 +520,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 #)
@@ -553,31 +535,35 @@ 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, 
                                fun_matches = matches, bind_fvs = fvs })]
            sig_fn              -- Single function binding
            non_rec     
                  [(name, Nothing, mono_id)]) }
 
 tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf, 
                                fun_matches = matches, bind_fvs = fvs })]
            sig_fn              -- Single function binding
            non_rec     
-  | Just sig <- sig_fn name    -- ...with a type signature
+  | Just scoped_tvs <- sig_fn name     -- ...with a type signature
   =    -- When we have a single function binding, with a type signature
        -- we can (a) use genuine, rigid skolem constants for the type variables
        --        (b) bring (rigid) scoped type variables into scope
     setSrcSpan b_loc   $
   =    -- When we have a single function binding, with a type signature
        -- 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 sig
+    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)]) }
 
@@ -590,9 +576,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) }
 
@@ -628,7 +614,7 @@ getMonoType (_,_,mono_id) = idType mono_id
 
 tcLhs :: TcSigFun -> HsBind Name -> TcM TcMonoBind
 tcLhs sig_fn (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = matches })
 
 tcLhs :: TcSigFun -> HsBind Name -> TcM TcMonoBind
 tcLhs sig_fn (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = matches })
-  = do { mb_sig <- tcInstSig_maybe (sig_fn name)
+  = do { mb_sig <- tcInstSig_maybe sig_fn name
        ; mono_name <- newLocalName name
        ; mono_ty   <- mk_mono_ty mb_sig
        ; let mono_id = mkLocalId mono_name mono_ty
        ; mono_name <- newLocalName name
        ; mono_ty   <- mk_mono_ty mb_sig
        ; let mono_id = mkLocalId mono_name mono_ty
@@ -638,15 +624,26 @@ tcLhs sig_fn (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = m
     mk_mono_ty Nothing    = newFlexiTyVarTy argTypeKind
 
 tcLhs sig_fn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss })
     mk_mono_ty Nothing    = newFlexiTyVarTy argTypeKind
 
 tcLhs sig_fn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss })
-  = do { mb_sigs <- mapM (tcInstSig_maybe . sig_fn) names
+  = do { mb_sigs <- mapM (tcInstSig_maybe sig_fn) names
+       ; mono_pat_binds <- doptM Opt_MonoPatBinds
+               -- With -fmono-pat-binds, we do no generalisation of pattern bindings
+               -- But the signature can still be polymoprhic!
+               --      data T = MkT (forall a. a->a)
+               --      x :: forall a. a->a
+               --      MkT x = <rhs>
+               -- The function get_sig_ty decides whether the pattern-bound variables
+               -- should have exactly the type in the type signature (-fmono-pat-binds), 
+               -- or the instantiated version (-fmono-pat-binds)
 
        ; let nm_sig_prs  = names `zip` mb_sigs
 
        ; let nm_sig_prs  = names `zip` mb_sigs
-             tau_sig_env = mkNameEnv [ (name, sig_tau sig) | (name, Just sig) <- nm_sig_prs]
+             get_sig_ty | mono_pat_binds = idType . sig_id
+                        | otherwise      = sig_tau
+             tau_sig_env = mkNameEnv [ (name, get_sig_ty sig) 
+                                     | (name, Just sig) <- nm_sig_prs]
              sig_tau_fn  = lookupNameEnv tau_sig_env
 
              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.
@@ -667,11 +664,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) $
@@ -697,11 +699,18 @@ getMonoBindInfo tc_binds
 %************************************************************************
 
 \begin{code}
 %************************************************************************
 
 \begin{code}
-generalise :: TopLevelFlag -> Bool 
+generalise :: DynFlags -> TopLevelFlag 
+          -> [LHsBind Name] -> TcSigFun 
           -> [MonoBindInfo] -> [Inst]
           -> [MonoBindInfo] -> [Inst]
-          -> TcM ([TcTyVar], TcDictBinds, [TcId])
-generalise top_lvl is_unrestricted mono_infos lie_req
-  | not is_unrestricted        -- RESTRICTED CASE
+          -> 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
+  = do { extendLIEs lie_req
+       ; return ([], [], emptyBag) }
+
+  | isRestrictedGroup dflags bind_list sig_fn  -- RESTRICTED CASE
   =    -- Check signature contexts are empty 
     do { checkTc (all is_mono_sig sigs)
                  (restrictedBindCtxtErr bndrs)
   =    -- Check signature contexts are empty 
     do { checkTc (all is_mono_sig sigs)
                  (restrictedBindCtxtErr bndrs)
@@ -714,39 +723,41 @@ generalise top_lvl is_unrestricted 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)
     is_mono_sig sig = null (sig_theta sig)
-    doc = ptext SLIT("type signature(s) for") <+> pprBinders bndrs
+    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
 
     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
@@ -763,21 +774,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
@@ -789,15 +812,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})
   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))       $
+      = addErrCtxt (ptext (sLit "In the type signature for") <+> quotes (ppr id))      $
        addErrCtxtM (sigCtxt id tvs theta tau)                                          $
        do { tvs' <- checkDistinctTyVars tvs
        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]
@@ -828,12 +851,12 @@ checkDistinctTyVars sig_tvs
        = do { env0 <- tcInitTidyEnv
            ; let (env1, tidy_tv1) = tidyOpenTyVar env0 sig_tv1
                  (env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2
        = do { env0 <- tcInitTidyEnv
            ; let (env1, tidy_tv1) = tidyOpenTyVar env0 sig_tv1
                  (env2, tidy_tv2) = tidyOpenTyVar env1 sig_tv2
-                 msg = ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1) 
-                        <+> ptext SLIT("is unified with another quantified type variable") 
+                 msg = ptext (sLit "Quantified type variable") <+> quotes (ppr tidy_tv1) 
+                        <+> ptext (sLit "is unified with another quantified type variable") 
                         <+> 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.
@@ -953,26 +976,68 @@ 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}
 \begin{code}
-type TcSigFun = Name -> Maybe (LSig Name)
+type TcSigFun = Name -> Maybe [Name]   -- Maps a let-binder to the list of
+                                       -- type variables brought into scope
+                                       -- by its type signature.
+                                       -- Nothing => no type signature
 
 
-mkSigFun :: [LSig Name] -> TcSigFun
+mkTcSigFun :: [LSig Name] -> TcSigFun
 -- Search for a particular type signature
 -- Precondition: the sigs are all type sigs
 -- Precondition: no duplicates
 -- Search for a particular type signature
 -- Precondition: the sigs are all type sigs
 -- Precondition: no duplicates
-mkSigFun sigs = lookupNameEnv env
+mkTcSigFun sigs = lookupNameEnv env
   where
   where
-    env = mkNameEnv [(expectJust "mkSigFun" (sigName sig), sig) | sig <- sigs]
+    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
+       -- 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]
 
@@ -981,19 +1046,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
@@ -1005,7 +1072,7 @@ data TcSigInfo
 
 instance Outputable TcSigInfo where
     ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
 
 instance Outputable TcSigInfo where
     ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
-       = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
+       = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> ppr theta <+> ptext (sLit "=>") <+> ppr tau
 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}
@@ -1016,18 +1083,28 @@ tcTySig (L span (TypeSig (L _ name) ty))
        ; return (mkLocalId name sigma_ty) }
 
 -------------------
        ; return (mkLocalId name sigma_ty) }
 
 -------------------
-tcInstSig_maybe :: Maybe (LSig Name) -> TcM (Maybe TcSigInfo)
+tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo)
 -- Instantiate with *meta* type variables; 
 -- this signature is part of a multi-signature group
 -- Instantiate with *meta* type variables; 
 -- this signature is part of a multi-signature group
-tcInstSig_maybe Nothing    = return Nothing
-tcInstSig_maybe (Just sig) = do { tc_sig <- tcInstSig False sig
+tcInstSig_maybe sig_fn name 
+  = case sig_fn name of
+       Nothing  -> return Nothing
+       Just scoped_tvs -> do   { tc_sig <- tcInstSig False name
                                ; return (Just tc_sig) }
                                ; return (Just tc_sig) }
+       -- NB: the scoped_tvs may be non-empty, but we can 
+       -- just ignore them.  See Note [Scoped tyvars].
 
 
-tcInstSig :: Bool -> LSig Name -> TcM TcSigInfo
+tcInstSig :: Bool -> Name -> TcM TcSigInfo
 -- Instantiate the signature, with either skolems or meta-type variables
 -- Instantiate the signature, with either skolems or meta-type variables
--- depending on the use_skols boolean
+-- depending on the use_skols boolean.  This variable is set True
+-- when we are typechecking a single function binding; and False for
+-- 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
+--     separately, even if it's mutually recursive, so use_skols will be True
 --
 --
--- We always instantiate with freshs uniques,
+-- We always instantiate with fresh uniques,
 -- although we keep the same print-name
 --     
 --     type T = forall a. [a] -> [a]
 -- although we keep the same print-name
 --     
 --     type T = forall a. [a] -> [a]
@@ -1036,37 +1113,32 @@ tcInstSig :: Bool -> LSig 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 (L loc (TypeSig (L _ name) hs_ty))
-  = setSrcSpan loc $
-    do { poly_id <- tcLookupId name    -- Cannot fail; the poly ids are put into 
+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)
                                        -- 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 = 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
+                             sig_loc = loc }) }
+
+-------------------
+isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool
+-- No generalisation at all
+isMonoGroup dflags binds
+  = dopt Opt_MonoPatBinds dflags && any is_pat_bind binds
   where
   where
-       -- 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.)
-       -- We also only have scoped type variables when we are instantiating
-       -- with true skolems
-    scoped_names = case (use_skols, hs_ty) of
-                    (True, L _ (HsForAllTy Explicit tvs _ _)) -> hsLTyVarNames tvs
-                    other                                     -> []
+    is_pat_bind (L _ (PatBind {})) = True
+    is_pat_bind other             = False
 
 -------------------
 
 -------------------
-isUnRestrictedGroup :: [LHsBind Name] -> TcSigFun -> TcM Bool
-isUnRestrictedGroup binds sig_fn
-  = do { mono_restriction <- doptM Opt_MonomorphismRestriction
-       ; return (not mono_restriction || all_unrestricted) }
+isRestrictedGroup :: DynFlags -> [LHsBind Name] -> TcSigFun -> Bool
+isRestrictedGroup dflags binds sig_fn
+  = mono_restriction && not all_unrestricted
   where 
   where 
+    mono_restriction = dopt Opt_MonomorphismRestriction dflags
     all_unrestricted = all (unrestricted . unLoc) binds
     has_sig n = isJust (sig_fn n)
 
     all_unrestricted = all (unrestricted . unLoc) binds
     has_sig n = isJust (sig_fn n)
 
@@ -1093,14 +1165,14 @@ isUnRestrictedGroup binds sig_fn
 -- This one is called on LHS, when pat and grhss are both Name 
 -- and on RHS, when pat is TcId and grhss is still Name
 patMonoBindsCtxt pat grhss
 -- This one is called on LHS, when pat and grhss are both Name 
 -- and on RHS, when pat is TcId and grhss is still Name
 patMonoBindsCtxt pat grhss
-  = hang (ptext SLIT("In a pattern binding:")) 4 (pprPatBind pat grhss)
+  = hang (ptext (sLit "In a pattern binding:")) 4 (pprPatBind pat grhss)
 
 -----------------------------------------------
 sigContextsCtxt sig1 sig2
 
 -----------------------------------------------
 sigContextsCtxt sig1 sig2
-  = vcat [ptext SLIT("When matching the contexts of the signatures for"), 
+  = vcat [ptext (sLit "When matching the contexts of the signatures for"), 
          nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
                        ppr id2 <+> dcolon <+> ppr (idType id2)]),
          nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
                        ppr id2 <+> dcolon <+> ppr (idType id2)]),
-         ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
+         ptext (sLit "The signature contexts in a mutually recursive group should all be identical")]
   where
     id1 = sig_id sig1
     id2 = sig_id sig2
   where
     id1 = sig_id sig1
     id2 = sig_id sig2
@@ -1108,15 +1180,24 @@ sigContextsCtxt sig1 sig2
 
 -----------------------------------------------
 unboxedTupleErr name ty
 
 -----------------------------------------------
 unboxedTupleErr name ty
-  = hang (ptext SLIT("Illegal binding of unboxed tuple"))
+  = hang (ptext (sLit "Illegal binding of unboxed tuple"))
         4 (ppr name <+> dcolon <+> ppr ty)
 
 -----------------------------------------------
 restrictedBindCtxtErr binder_names
         4 (ppr name <+> dcolon <+> ppr ty)
 
 -----------------------------------------------
 restrictedBindCtxtErr binder_names
-  = hang (ptext SLIT("Illegal overloaded type signature(s)"))
-       4 (vcat [ptext SLIT("in a binding group for") <+> pprBinders binder_names,
-               ptext SLIT("that falls under the monomorphism restriction")])
+  = hang (ptext (sLit "Illegal overloaded type signature(s)"))
+       4 (vcat [ptext (sLit "in a binding group for") <+> pprBinders binder_names,
+               ptext (sLit "that falls under the monomorphism restriction")])
 
 genCtxt binder_names
 
 genCtxt binder_names
-  = ptext SLIT("When generalising the type(s) for") <+> pprBinders 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}
Glasgow Haskell Compiler with heterogeneous metaprogramming (generalized arrows and modal types)