Major improvement to pattern bindings

This patch makes a number of related improvements

a) Implements the Haskell Prime semantics for pattern bindings
   (Trac #2357).  That is, a pattern binding p = e is typed
   just as if it had been written
        t = e
        f = case t of p -> f
        g = case t of p -> g
        ... etc ...
   where f,g are the variables bound by p. In paricular it's
   ok to say
      (f,g) = (\x -> x, \y -> True)
   and f and g will get propertly inferred types
      f :: a -> a
      g :: a -> Int

b) Eliminates the MonoPatBinds flag altogether.  (For the moment
   it is deprecated and has no effect.)  Pattern bindings are now
   generalised as per (a).  Fixes Trac #2187 and #4940, in the
   way the users wanted!

c) Improves the OutsideIn algorithm generalisation decision.
   Given a definition without a type signature (implying "infer
   the type"), the published algorithm rule is this:
      - generalise *top-level* functions, and
      - do not generalise *nested* functions
   The new rule is
      - generalise a binding whose free variables have
        Guaranteed Closed Types
      - do not generalise other bindings

   Generally, a top-level let-bound function has a Guaranteed
   Closed Type, and so does a nested function whose free vaiables
   are top-level functions, and so on. (However a top-level
   function that is bitten by the Monomorphism Restriction does
   not have a GCT.)

   Example:
     f x = let { foo y = y } in ...
   Here 'foo' has no free variables, so it is generalised despite
   being nested.

d) When inferring a type f :: ty for a definition f = e, check that
   the compiler would accept f :: ty as a type signature for that
   same definition.  The type is rejected precisely when the type
   is ambiguous.

   Example:
      class Wob a b where
        to :: a -> b
        from :: b -> a

      foo x = [x, to (from x)]
   GHC 7.0 would infer the ambiguous type
      foo :: forall a b. Wob a b => b -> [b]
   but that type would give an error whenever it is called; and
   GHC 7.0 would reject that signature if given by the
   programmer.  The new type checker rejects it up front.

   Similarly, with the advent of type families, ambiguous types are
   easy to write by mistake.  See Trac #1897 and linked tickets for
   many examples.  Eg
      type family F a :: *
      f ::: F a -> Int
      f x = 3
   This is rejected because (F a ~ F b) does not imply a~b.  Previously
   GHC would *infer* the above type for f, but was unable to check it.
   Now even the inferred type is rejected -- correctly.

The main implemenation mechanism is to generalise the abe_wrap
field of ABExport (in HsBinds), from [TyVar] to HsWrapper. This
beautiful generalisation turned out to make everything work nicely
with minimal programming effort.  All the work was fiddling around
the edges; the core change was easy!

19 files changed, 439 insertions, 306 deletions

diff --git a/compiler/deSugar/DsBinds.lhs b/compiler/deSugar/DsBinds.lhs
index 36dc4eefb2..7eceeb247f 100644
--- a/compiler/deSugar/DsBinds.lhs
+++ b/compiler/deSugar/DsBinds.lhs
@@ -37,7 +37,6 @@ import Digraph
 import TcType
 import Type
 import Coercion
-import TysPrim  ( anyTypeOfKind )
 import CostCentre
 import Module
 import Id
@@ -122,15 +121,17 @@ dsHsBind auto_scc (PatBind { pat_lhs = pat, pat_rhs = grhss, pat_rhs_ty = ty })
 	-- Non-recursive bindings come through this way
 	-- So do self-recursive bindings, and recursive bindings
 	-- that have been chopped up with type signatures
-dsHsBind auto_scc (AbsBinds { abs_tvs = all_tyvars, abs_ev_vars = dicts
-               		    , abs_exports = [(tyvars, global, local, prags)]
+dsHsBind auto_scc (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
+               		    , abs_exports = [export]
                		    , abs_ev_binds = ev_binds, abs_binds = binds })
-  = ASSERT( all (`elem` tyvars) all_tyvars )
-    do	{ bind_prs    <- ds_lhs_binds NoSccs binds
+  | ABE { abe_wrap = wrap, abe_poly = global
+        , abe_mono = local, abe_prags = prags } <- export
+  = do	{ bind_prs    <- ds_lhs_binds NoSccs binds
         ; ds_ev_binds <- dsTcEvBinds ev_binds
-
+        ; wrap_fn <- dsHsWrapper wrap
 	; let	core_bind = Rec (fromOL bind_prs)
 	        rhs       = addAutoScc auto_scc global $
+			    wrap_fn $  -- Usually the identity
 			    mkLams tyvars $ mkLams dicts $ 
 	                    wrapDsEvBinds ds_ev_binds $
                             Let core_bind $
@@ -144,14 +145,14 @@ dsHsBind auto_scc (AbsBinds { abs_tvs = all_tyvars, abs_ev_vars = dicts
     
 	; return (main_bind `consOL` spec_binds) }
 
-dsHsBind auto_scc (AbsBinds { abs_tvs = all_tyvars, abs_ev_vars = dicts
+dsHsBind auto_scc (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts
                             , abs_exports = exports, abs_ev_binds = ev_binds
                        	    , abs_binds = binds })
   = do	{ bind_prs    <- ds_lhs_binds NoSccs binds
         ; ds_ev_binds <- dsTcEvBinds ev_binds
 	; let env = mkABEnv exports
-	      do_one (lcl_id,rhs) | Just (_, gbl_id, _, _prags) <- lookupVarEnv env lcl_id
-			          = (lcl_id, addAutoScc auto_scc gbl_id rhs)
+	      do_one (lcl_id,rhs) | Just export <- lookupVarEnv env lcl_id
+			          = (lcl_id, addAutoScc auto_scc (abe_poly export) rhs)
 				  | otherwise = (lcl_id,rhs)
 	       
 	      core_bind = Rec (map do_one (fromOL bind_prs))
@@ -159,37 +160,27 @@ dsHsBind auto_scc (AbsBinds { abs_tvs = all_tyvars, abs_ev_vars = dicts
 
 	      tup_expr     = mkBigCoreVarTup locals
 	      tup_ty	   = exprType tup_expr
-	      poly_tup_rhs = mkLams all_tyvars $ mkLams dicts $
+	      poly_tup_rhs = mkLams tyvars $ mkLams dicts $
 	      		     wrapDsEvBinds ds_ev_binds $
 			     Let core_bind $
 	 	     	     tup_expr
-	      locals       = [local | (_, _, local, _) <- exports]
-	      local_tys    = map idType locals
+	      locals       = map abe_mono exports
 
 	; poly_tup_id <- newSysLocalDs (exprType poly_tup_rhs)
 
-	; let mk_bind ((tyvars, global, _, spec_prags), n)  -- locals!!n == local
-	        = 	-- Need to make fresh locals to bind in the selector,
-		      	-- because some of the tyvars will be bound to 'Any'
-		  do { let ty_args = map mk_ty_arg all_tyvars
-		           substitute = substTyWith all_tyvars ty_args
-		     ; locals' <- newSysLocalsDs (map substitute local_tys)
-		     ; tup_id  <- newSysLocalDs  (substitute tup_ty)
-	             ; let rhs = mkLams tyvars $ mkLams dicts $
-	      	     		 mkTupleSelector locals' (locals' !! n) tup_id $
-			         mkVarApps (mkTyApps (Var poly_tup_id) ty_args)
-			 		   dicts
-                           full_rhs = Let (NonRec poly_tup_id poly_tup_rhs) rhs
-		     ; (spec_binds, rules) <- dsSpecs full_rhs spec_prags
-				                      
+	; let mk_bind (ABE { abe_wrap = wrap, abe_poly = global
+                           , abe_mono = local, abe_prags = spec_prags })
+	        = do { wrap_fn <- dsHsWrapper wrap
+		     ; tup_id  <- newSysLocalDs tup_ty
+	             ; let rhs = wrap_fn $ mkLams tyvars $ mkLams dicts $
+	      	     		 mkTupleSelector locals local tup_id $
+			         mkVarApps (Var poly_tup_id) (tyvars ++ dicts)
+                           rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs
+		     ; (spec_binds, rules) <- dsSpecs rhs_for_spec spec_prags
 		     ; let global' = addIdSpecialisations global rules
 		     ; return ((global', rhs) `consOL` spec_binds) }
-	        where
-	          mk_ty_arg all_tyvar
-			| all_tyvar `elem` tyvars = mkTyVarTy all_tyvar
-	      		| otherwise		  = dsMkArbitraryType all_tyvar
 
-	; export_binds_s <- mapM mk_bind (exports `zip` [0..])
+	; export_binds_s <- mapM mk_bind exports
 	     -- Don't scc (auto-)annotate the tuple itself.
 
 	; return ((poly_tup_id, poly_tup_rhs) `consOL` 
@@ -311,14 +302,14 @@ dictArity dicts = count isId dicts
 
 
 ------------------------
-type AbsBindEnv = VarEnv ([TyVar], Id, Id, TcSpecPrags)
+type AbsBindEnv = VarEnv (ABExport Id)
 	-- Maps the "lcl_id" for an AbsBind to
 	-- its "gbl_id" and associated pragmas, if any
 
-mkABEnv :: [([TyVar], Id, Id, TcSpecPrags)] -> AbsBindEnv
+mkABEnv :: [ABExport Id] -> AbsBindEnv
 -- Takes the exports of a AbsBinds, and returns a mapping
 --	lcl_id -> (tyvars, gbl_id, lcl_id, prags)
-mkABEnv exports = mkVarEnv [ (lcl_id, export) | export@(_, _, lcl_id, _) <- exports]
+mkABEnv exports = mkVarEnv [ (abe_mono export, export) | export <- exports]
 \end{code}
 
 Note [Rules and inlining]
@@ -560,9 +551,6 @@ specUnfolding wrap_fn spec_ty (DFunUnfolding _ _ ops)
 -}
 specUnfolding _ _ _
   = return (noUnfolding, nilOL)
-
-dsMkArbitraryType :: TcTyVar -> Type
-dsMkArbitraryType tv = anyTypeOfKind (tyVarKind tv)
 \end{code}
 
 %************************************************************************
diff --git a/compiler/deSugar/DsExpr.lhs b/compiler/deSugar/DsExpr.lhs
index a68214d1b1..743874d8e4 100644
--- a/compiler/deSugar/DsExpr.lhs
+++ b/compiler/deSugar/DsExpr.lhs
@@ -136,7 +136,7 @@ dsStrictBind (AbsBinds { abs_tvs = [], abs_ev_vars = []
                , abs_binds = binds }) body
   = do { ds_ev_binds <- dsTcEvBinds ev_binds
        ; let body1 = foldr bind_export body exports
-             bind_export (_, g, l, _) b = bindNonRec g (Var l) b
+             bind_export export b = bindNonRec (abe_poly export) (Var (abe_mono export)) b
        ; body2 <- foldlBagM (\body bind -> dsStrictBind (unLoc bind) body) 
                             body1 binds 
        ; return (wrapDsEvBinds ds_ev_binds body2) }
@@ -542,8 +542,8 @@ dsExpr expr@(RecordUpd record_expr (HsRecFields { rec_flds = fields })
                      = nlHsVar (lookupNameEnv upd_fld_env field_name `orElse` pat_arg_id)
 		 inst_con = noLoc $ HsWrap wrap (HsVar (dataConWrapId con))
 			-- Reconstruct with the WrapId so that unpacking happens
-		 wrap = mkWpEvVarApps theta_vars          `WpCompose` 
-			mkWpTyApps    (mkTyVarTys ex_tvs) `WpCompose`
+		 wrap = mkWpEvVarApps theta_vars          <.>
+			mkWpTyApps    (mkTyVarTys ex_tvs) <.>
 			mkWpTyApps [ty | (tv, ty) <- univ_tvs `zip` out_inst_tys
 				       , not (tv `elemVarEnv` wrap_subst) ]
     	         rhs = foldl (\a b -> nlHsApp a b) inst_con val_args
diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index fcba55af81..4b06737d6e 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -150,7 +150,7 @@ data HsBindLR idL idR
        -- AbsBinds only gets used when idL = idR after renaming,
        -- but these need to be idL's for the collect... code in HsUtil 
        -- to have the right type
-	abs_exports :: [([TyVar], idL, idL, TcSpecPrags)],	-- (tvs, poly_id, mono_id, prags)
+	abs_exports :: [ABExport idL],
 
         abs_ev_binds :: TcEvBinds,     -- Evidence bindings
 	abs_binds    :: LHsBinds idL   -- Typechecked user bindings
@@ -171,6 +171,14 @@ data HsBindLR idL idR
 	-- (You can get a PhD for explaining the True Meaning
 	--  of this last construct.)
 
+data ABExport id 
+  = ABE { abe_poly  :: id 
+        , abe_mono  :: id 
+        , abe_wrap  :: HsWrapper  -- See Note [AbsBinds wrappers]
+             -- Shape: (forall abs_tvs. abs_ev_vars => abe_mono) ~ abe_poly
+        , abe_prags :: TcSpecPrags }
+  deriving (Data, Typeable)
+
 placeHolderNames :: NameSet
 -- Used for the NameSet in FunBind and PatBind prior to the renamer
 placeHolderNames = panic "placeHolderNames"
@@ -306,17 +314,19 @@ ppr_monobind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dictvars
   = sep [ptext (sLit "AbsBinds"),
   	 brackets (interpp'SP tyvars),
   	 brackets (interpp'SP dictvars),
-  	 brackets (sep (punctuate comma (map ppr_exp exports)))]
+  	 brackets (sep (punctuate comma (map ppr exports)))]
     $$
-    nest 2 ( vcat [pprBndr LetBind x | (_,x,_,_) <- exports]
+    nest 2 ( vcat [pprBndr LetBind (abe_poly ex) | ex <- exports]
   			-- Print type signatures
   	     $$ pprLHsBinds val_binds )
     $$
     ifPprDebug (ppr ev_binds)
-  where
-    ppr_exp (tvs, gbl, lcl, prags)
-	= vcat [ppr gbl <+> ptext (sLit "<=") <+> ppr tvs <+> ppr lcl,
-	  	nest 2 (pprTcSpecPrags prags)]
+
+instance (OutputableBndr id) => Outputable (ABExport id) where
+  ppr (ABE { abe_wrap = wrap, abe_poly = gbl, abe_mono = lcl, abe_prags = prags })
+    = vcat [ ppr gbl <+> ptext (sLit "<=") <+> ppr lcl
+	   , nest 2 (pprTcSpecPrags prags)
+           , nest 2 (ppr wrap)]
 \end{code}
 
 
@@ -513,12 +523,12 @@ mkWpLet (EvBinds b) | isEmptyBag b = WpHole
 mkWpLet ev_binds                   = WpLet ev_binds
 
 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
-mk_co_lam_fn f as = foldr (\x wrap -> f x `WpCompose` wrap) WpHole as
+mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
 
 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
 -- For applications, the *first* argument must
 -- come *last* in the composition sequence
-mk_co_app_fn f as = foldr (\x wrap -> wrap `WpCompose` f x) WpHole as
+mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
 
 idHsWrapper :: HsWrapper
 idHsWrapper = WpHole
diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs
index 33d800d66a..cd95571964 100644
--- a/compiler/hsSyn/HsUtils.lhs
+++ b/compiler/hsSyn/HsUtils.lhs
@@ -29,7 +29,7 @@ module HsUtils(
   mkLHsTupleExpr, mkLHsVarTuple, missingTupArg,
 
   -- Bindings
-  mkFunBind, mkVarBind, mkHsVarBind, mk_easy_FunBind, 
+  mkFunBind, mkVarBind, mkHsVarBind, mk_easy_FunBind, mkTopFunBind,
 
   -- Literals
   mkHsIntegral, mkHsFractional, mkHsIsString, mkHsString, 
@@ -407,14 +407,23 @@ missingTupArg = Missing placeHolderType
 %************************************************************************
 
 \begin{code}
-mkFunBind :: Located id -> [LMatch id] -> HsBind id
+mkFunBind :: Located RdrName -> [LMatch RdrName] -> HsBind RdrName
 -- Not infix, with place holders for coercion and free vars
-mkFunBind fn ms = FunBind { fun_id = fn, fun_infix = False, fun_matches = mkMatchGroup ms,
-			    fun_co_fn = idHsWrapper, bind_fvs = placeHolderNames,
-			    fun_tick = Nothing }
-
-
-mkHsVarBind :: SrcSpan -> id -> LHsExpr id -> LHsBind id
+mkFunBind fn ms = FunBind { fun_id = fn, fun_infix = False
+                          , fun_matches = mkMatchGroup ms
+			  , fun_co_fn = idHsWrapper
+                          , bind_fvs = placeHolderNames
+			  , fun_tick = Nothing }
+
+mkTopFunBind :: Located Name -> [LMatch Name] -> HsBind Name
+-- In Name-land, with empty bind_fvs
+mkTopFunBind fn ms = FunBind { fun_id = fn, fun_infix = False
+                             , fun_matches = mkMatchGroup ms
+			     , fun_co_fn = idHsWrapper
+                             , bind_fvs = emptyNameSet	-- NB: closed binding
+			     , fun_tick = Nothing }
+
+mkHsVarBind :: SrcSpan -> RdrName -> LHsExpr RdrName -> LHsBind RdrName
 mkHsVarBind loc var rhs = mk_easy_FunBind loc var [] rhs
 
 mkVarBind :: id -> LHsExpr id -> LHsBind id
@@ -422,9 +431,8 @@ mkVarBind var rhs = L (getLoc rhs) $
 		    VarBind { var_id = var, var_rhs = rhs, var_inline = False }
 
 ------------
-mk_easy_FunBind :: SrcSpan -> id -> [LPat id]
-		-> LHsExpr id -> LHsBind id
-
+mk_easy_FunBind :: SrcSpan -> RdrName -> [LPat RdrName]
+		-> LHsExpr RdrName -> LHsBind RdrName
 mk_easy_FunBind loc fun pats expr
   = L loc $ mkFunBind (L loc fun) [mkMatch pats expr emptyLocalBinds]
 
@@ -483,7 +491,7 @@ collect_bind (PatBind { pat_lhs = p })    acc = collect_lpat p acc
 collect_bind (FunBind { fun_id = L _ f }) acc = f : acc
 collect_bind (VarBind { var_id = f })     acc = f : acc
 collect_bind (AbsBinds { abs_exports = dbinds, abs_binds = _binds }) acc
-  = [dp | (_,dp,_,_) <- dbinds] ++ acc 
+  = map abe_poly dbinds ++ acc 
 	-- ++ foldr collect_bind acc binds
 	-- I don't think we want the binders from the nested binds
 	-- The only time we collect binders from a typechecked 
diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 68410cdb64..d850ac7657 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -910,19 +910,15 @@ languageExtensions :: Maybe Language -> [ExtensionFlag]
 
 languageExtensions Nothing
     -- Nothing => the default case
-    = Opt_MonoPatBinds   -- Experimentally, I'm making this non-standard
-                         -- behaviour the default, to see if anyone notices
-                         -- SLPJ July 06
-      -- In due course I'd like Opt_MonoLocalBinds to be on by default
-      -- But NB it's implied by GADTs etc
-      -- SLPJ September 2010
-    : Opt_NondecreasingIndentation -- This has been on by default for some time
+    = Opt_NondecreasingIndentation -- This has been on by default for some time
     : delete Opt_DatatypeContexts  -- The Haskell' committee decided to
                                    -- remove datatype contexts from the
                                    -- language:
    -- http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
       (languageExtensions (Just Haskell2010))
 
+   -- NB: MonoPatBinds is no longer the default
+
 languageExtensions (Just Haskell98)
     = [Opt_ImplicitPrelude,
        Opt_MonomorphismRestriction,
@@ -1863,7 +1859,8 @@ xFlags = [
   ( "NPlusKPatterns",                   AlwaysAllowed, Opt_NPlusKPatterns, nop ),
   ( "DoAndIfThenElse",                  AlwaysAllowed, Opt_DoAndIfThenElse, nop ),
   ( "RebindableSyntax",                 AlwaysAllowed, Opt_RebindableSyntax, nop ),
-  ( "MonoPatBinds",                     AlwaysAllowed, Opt_MonoPatBinds, nop ),
+  ( "MonoPatBinds",                     AlwaysAllowed, Opt_MonoPatBinds, 
+    \ turn_on -> when turn_on $ deprecate "Experimental feature now removed; has no effect" ),
   ( "ExplicitForAll",                   AlwaysAllowed, Opt_ExplicitForAll, nop ),
   ( "AlternativeLayoutRule",            AlwaysAllowed, Opt_AlternativeLayoutRule, nop ),
   ( "AlternativeLayoutRuleTransitional",AlwaysAllowed, Opt_AlternativeLayoutRuleTransitional, nop ),
diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs
index 2a1330370a..a833c83b01 100644
--- a/compiler/rename/RnBinds.lhs
+++ b/compiler/rename/RnBinds.lhs
@@ -334,8 +334,10 @@ rnLocalValBindsRHS :: NameSet  -- names bound by the LHSes
 rnLocalValBindsRHS bound_names binds
   = rnValBindsRHS trim (Just bound_names) binds
   where
-    trim fvs = intersectNameSet bound_names fvs 
-	-- Only keep the names the names from this group
+    trim fvs = filterNameSet isInternalName fvs
+     -- Keep Internal Names; these are the non-top-level ones
+     -- As well as dependency analysis, we need these for the
+     -- MonoLocalBinds test in TcBinds.decideGeneralisationPlan
 
 -- for local binds
 -- wrapper that does both the left- and right-hand sides 
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index ce40f56e24..0f404c6923 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -25,10 +25,11 @@ import TcHsType
 import TcPat
 import TcMType
 import TcType
-import Coercion
+-- import Coercion
 import TysPrim
 import Id
 import Var
+import VarSet
 import Name
 import NameSet
 import NameEnv
@@ -158,7 +159,7 @@ but rather because we otherwise end up with constraints like this
     Num alpha, Implic { wanted = alpha ~ Int }
 The constraint solver solves alpha~Int by unification, but then
 doesn't float that solved constraint out (it's not an unsolved 
-wanted.  Result disaster: the (Num alpha) is again solved, this
+wanted).  Result disaster: the (Num alpha) is again solved, this
 time by defaulting.  No no no.
 
 However [Oct 10] this is all handled automatically by the 
@@ -227,9 +228,10 @@ tc_group 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 { (binds1, ids) <- tcPolyBinds top_lvl sig_fn prag_fn NonRecursive NonRecursive
-                                      (bagToList binds)
-       ; thing <- tcExtendIdEnv ids thing_inside
+ =  do { (binds1, ids, closed) <- tcPolyBinds top_lvl sig_fn prag_fn 
+       	 	       	       	  	      NonRecursive NonRecursive
+                                             (bagToList binds)
+       ; thing <- tcExtendLetEnv closed ids thing_inside
        ; return ( [(NonRecursive, binds1)], thing) }
 
 tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
@@ -247,8 +249,8 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
     sccs = stronglyConnCompFromEdgedVertices (mkEdges sig_fn binds)
 
     go :: [SCC (LHsBind Name)] -> TcM (LHsBinds TcId, [TcId], thing)
-    go (scc:sccs) = do  { (binds1, ids1)        <- tc_scc scc
-                        ; (binds2, ids2, thing) <- tcExtendIdEnv ids1 $ go sccs
+    go (scc:sccs) = do  { (binds1, ids1, closed) <- tc_scc scc
+                        ; (binds2, ids2, thing)  <- tcExtendLetEnv closed ids1 $ go sccs
                         ; return (binds1 `unionBags` binds2, ids1 ++ ids2, thing) }
     go []         = do  { thing <- thing_inside; return (emptyBag, [], thing) }
 
@@ -257,25 +259,6 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
 
     tc_sub_group = tcPolyBinds top_lvl sig_fn prag_fn Recursive
 
-
-------------------------
-{-
-bindLocalInsts :: TopLevelFlag
-	       -> TcM (LHsBinds TcId, [TcId],    a)
-	       -> TcM (LHsBinds TcId, TcEvBinds, a)
-bindLocalInsts top_lvl thing_inside
-  | isTopLevel top_lvl
-  = do { (binds, _, thing) <- thing_inside; return (binds, emptyBag, 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) <- captureConstraints thing_inside
-        ; lie_binds <- bindLocalMethods lie ids
-        ; return (binds, lie_binds, thing) }
--}
-
 ------------------------
 mkEdges :: SigFun -> LHsBinds Name
         -> [(LHsBind Name, BKey, [BKey])]
@@ -309,7 +292,7 @@ tcPolyBinds :: TopLevelFlag -> SigFun -> PragFun
   	    -> RecFlag       -- Whether it's recursive after breaking
   	                     -- dependencies based on type signatures
   	    -> [LHsBind Name]
-  	    -> TcM (LHsBinds TcId, [TcId])
+  	    -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 
 -- Typechecks a single bunch of bindings all together, 
 -- and generalises them.  The bunch may be only part of a recursive
@@ -333,20 +316,22 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc bind_list
     -- (as determined by sig_fn), returning a TcSigInfo for each
     ; tc_sig_fn <- tcInstSigs sig_fn binder_names
 
-    ; dflags <- getDOpts
-    ; let plan = decideGeneralisationPlan dflags top_lvl binder_names bind_list tc_sig_fn
+    ; dflags   <- getDOpts
+    ; type_env <- getLclTypeEnv
+    ; let plan = decideGeneralisationPlan dflags type_env 
+                         binder_names bind_list tc_sig_fn
     ; traceTc "Generalisation plan" (ppr plan)
-    ; (binds, poly_ids) <- case plan of
-         NoGen         -> tcPolyNoGen tc_sig_fn prag_fn rec_tc bind_list
-         InferGen mono -> tcPolyInfer top_lvl mono tc_sig_fn prag_fn rec_tc bind_list
-         CheckGen sig  -> tcPolyCheck sig prag_fn rec_tc bind_list
+    ; result@(_, poly_ids, _) <- case plan of
+         NoGen          -> tcPolyNoGen tc_sig_fn prag_fn rec_tc bind_list
+         InferGen mn cl -> tcPolyInfer mn cl tc_sig_fn prag_fn rec_tc bind_list
+         CheckGen sig   -> tcPolyCheck sig prag_fn rec_tc bind_list
 
 	-- Check whether strict bindings are ok
         -- These must be non-recursive etc, and are not generalised
         -- They desugar to a case expression in the end
     ; checkStrictBinds top_lvl rec_group bind_list poly_ids
 
-    ; return (binds, poly_ids) }
+    ; return result }
   where
     binder_names = collectHsBindListBinders bind_list
     loc = foldr1 combineSrcSpans (map getLoc bind_list)
@@ -360,14 +345,14 @@ tcPolyNoGen
   -> RecFlag       -- Whether it's recursive after breaking
                    -- dependencies based on type signatures
   -> [LHsBind Name]
-  -> TcM (LHsBinds TcId, [TcId])
+  -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 -- No generalisation whatsoever
 
 tcPolyNoGen tc_sig_fn prag_fn rec_tc bind_list
   = do { (binds', mono_infos) <- tcMonoBinds tc_sig_fn (LetGblBndr prag_fn) 
                                              rec_tc bind_list
        ; mono_ids' <- mapM tc_mono_info mono_infos
-       ; return (binds', mono_ids') }
+       ; return (binds', mono_ids', NotTopLevel) }
   where
     tc_mono_info (name, _, mono_id)
       = do { mono_ty' <- zonkTcTypeCarefully (idType mono_id)
@@ -385,68 +370,78 @@ tcPolyCheck :: TcSigInfo -> PragFun
   	    -> RecFlag       -- Whether it's recursive after breaking
   	                     -- dependencies based on type signatures
   	    -> [LHsBind Name]
-  	    -> TcM (LHsBinds TcId, [TcId])
+  	    -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 -- There is just one binding, 
 --   it binds a single variable,
 --   it has a signature,
-tcPolyCheck sig@(TcSigInfo { sig_id = id, sig_tvs = tvs, sig_scoped = scoped
+tcPolyCheck sig@(TcSigInfo { sig_id = poly_id, sig_tvs = tvs, sig_scoped = scoped
                            , sig_theta = theta, sig_tau = tau })
     prag_fn rec_tc bind_list
-  = do { ev_vars <- newEvVars theta
-       ; let skol_info = SigSkol (FunSigCtxt (idName id)) (mkPhiTy theta tau)
+  = do { loc <- getSrcSpanM
+       ; ev_vars <- newEvVars theta
+       ; let skol_info = SigSkol (FunSigCtxt (idName poly_id)) (mkPhiTy theta tau)
+             prag_sigs = prag_fn (idName poly_id)
        ; (ev_binds, (binds', [mono_info])) 
             <- checkConstraints skol_info tvs ev_vars $
                tcExtendTyVarEnv2 (scoped `zip` mkTyVarTys tvs)    $
                tcMonoBinds (\_ -> Just sig) LetLclBndr rec_tc bind_list
 
-       ; export <- mkExport prag_fn tvs theta mono_info
+       ; spec_prags <- tcSpecPrags poly_id prag_sigs
+       ; poly_id    <- addInlinePrags poly_id prag_sigs
 
-       ; loc <- getSrcSpanM
-       ; let (_, poly_id, _, _) = export
+       ; let (_, _, mono_id) = mono_info
+             export = ABE { abe_wrap = idHsWrapper
+                          , abe_poly = poly_id
+                          , abe_mono = mono_id
+                          , abe_prags = SpecPrags spec_prags }
              abs_bind = L loc $ AbsBinds 
                         { abs_tvs = tvs
                         , abs_ev_vars = ev_vars, abs_ev_binds = ev_binds
                         , abs_exports = [export], abs_binds = binds' }
-       ; return (unitBag abs_bind, [poly_id]) }
+             closed | isEmptyVarSet (tyVarsOfType (idType poly_id)) = TopLevel
+                    | otherwise                                     = NotTopLevel
+       ; return (unitBag abs_bind, [poly_id], closed) }
 
 ------------------
 tcPolyInfer 
-  :: TopLevelFlag 
-  -> Bool	  -- True <=> apply the monomorphism restriction
+  :: Bool	  -- True <=> apply the monomorphism restriction
+  -> Bool	  -- True <=> free vars have closed types
   -> TcSigFun -> PragFun
   -> RecFlag       -- Whether it's recursive after breaking
                    -- dependencies based on type signatures
   -> [LHsBind Name]
-  -> TcM (LHsBinds TcId, [TcId])
-tcPolyInfer top_lvl mono tc_sig_fn prag_fn rec_tc bind_list
+  -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
+tcPolyInfer mono closed tc_sig_fn prag_fn rec_tc bind_list
   = do { ((binds', mono_infos), wanted) 
              <- captureConstraints $
                 tcMonoBinds tc_sig_fn LetLclBndr rec_tc bind_list
 
-       ; unifyCtxts [sig | (_, Just sig, _) <- mono_infos] 
-
        ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos]
-       ; (qtvs, givens, ev_binds) <- simplifyInfer top_lvl mono name_taus wanted
-
-       ; exports <- mapM (mkExport prag_fn qtvs (map evVarPred givens))
-                    mono_infos
+       ; (qtvs, givens, mr_bites, ev_binds) <- simplifyInfer closed mono name_taus wanted
 
-       ; let poly_ids = [poly_id | (_, poly_id, _, _) <- exports]
-       ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
+       ; theta <- zonkTcThetaType (map evVarPred givens)
+       ; exports <- checkNoErrs $ mapM (mkExport prag_fn qtvs theta) mono_infos
 
        ; loc <- getSrcSpanM
-       ; let abs_bind = L loc $ AbsBinds { abs_tvs = qtvs
-                                         , abs_ev_vars = givens, abs_ev_binds = ev_binds
-                                         , abs_exports = exports, abs_binds = binds' }
+       ; let poly_ids = map abe_poly exports
+       	     final_closed | closed && not mr_bites = TopLevel
+	     		  | otherwise              = NotTopLevel
+             abs_bind = L loc $ 
+                        AbsBinds { abs_tvs = qtvs
+                                 , abs_ev_vars = givens, abs_ev_binds = ev_binds
+                                 , abs_exports = exports, abs_binds = binds' }
 
-       ; return (unitBag abs_bind, poly_ids)   -- poly_ids are guaranteed zonked by mkExport
+       ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
+       ; return (unitBag abs_bind, poly_ids, final_closed)   
+         -- poly_ids are guaranteed zonked by mkExport
   }
 
 
 --------------
-mkExport :: PragFun -> [TyVar] -> TcThetaType
+mkExport :: PragFun 
+         -> [TyVar] -> TcThetaType	-- Both already zonked
          -> MonoBindInfo
-         -> TcM ([TyVar], Id, Id, TcSpecPrags)
+         -> TcM (ABExport Id)
 -- mkExport generates exports with 
 --      zonked type variables, 
 --      zonked poly_ids
@@ -456,29 +451,61 @@ mkExport :: PragFun -> [TyVar] -> TcThetaType
 -- 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
+-- Pre-condition: the qtvs and theta are already zonked
 
-mkExport prag_fn inferred_tvs theta
-         (poly_name, mb_sig, mono_id)
-  = do  { (tvs, poly_id) <- mk_poly_id mb_sig
-                -- poly_id has a zonked type
+mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
+  = do  { mono_ty <- zonkTcTypeCarefully (idType mono_id)
+        ; let inferred_poly_ty = mkSigmaTy my_tvs theta mono_ty
+              my_tvs   = filter (`elemVarSet` used_tvs) qtvs
+              used_tvs = tyVarsOfTheta theta `unionVarSet` tyVarsOfType mono_ty
 
-        ; poly_id' <- addInlinePrags poly_id prag_sigs
+              poly_id  = case mb_sig of
+                           Nothing  -> mkLocalId poly_name inferred_poly_ty
+                           Just sig -> sig_id sig
+                -- poly_id has a zonked type
 
+        ; poly_id <- addInlinePrags poly_id prag_sigs
         ; spec_prags <- tcSpecPrags poly_id prag_sigs
                 -- tcPrags requires a zonked poly_id
 
-        ; return (tvs, poly_id', mono_id, SpecPrags spec_prags) }
+        ; let sel_poly_ty = mkSigmaTy qtvs theta mono_ty
+        ; traceTc "mkExport: check sig" 
+                  (ppr poly_name $$ ppr sel_poly_ty $$ ppr (idType poly_id)) 
+
+	-- Perform the impedence-matching and ambiguity check
+	-- right away.  If it fails, we want to fail now (and recover
+	-- in tcPolyBinds).  If we delay checking, we get an error cascade.
+	-- Remember we are in the tcPolyInfer case, so the type envt is 
+	-- closed (unless we are doing NoMonoLocalBinds in which case all bets
+	-- are off)
+        ; (wrap, wanted) <- addErrCtxtM (mk_msg poly_id) $
+                            captureConstraints $
+                            tcSubType origin sig_ctxt sel_poly_ty (idType poly_id)
+	; ev_binds <- simplifyAmbiguityCheck poly_name wanted
+
+        ; return (ABE { abe_wrap = mkWpLet (EvBinds ev_binds) <.> wrap
+                      , abe_poly = poly_id
+                      , abe_mono = mono_id
+                      , abe_prags = SpecPrags spec_prags }) }
   where
-    prag_sigs = prag_fn poly_name
-    poly_ty = mkSigmaTy inferred_tvs theta (idType mono_id)
+    inferred = isNothing mb_sig
 
-    mk_poly_id Nothing    = do { poly_ty' <- zonkTcTypeCarefully poly_ty
-                               ; 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_msg poly_id tidy_env
+      = return (tidy_env', msg)
+      where
+        msg | inferred  = hang (ptext (sLit "When checking that") <+> pp_name)
+                             2 (ptext (sLit "has the inferred type") <+> pp_ty)
+                          $$ ptext (sLit "Probable cause: the inferred type is ambiguous")
+            | otherwise = hang (ptext (sLit "When checking that") <+> pp_name)
+                             2 (ptext (sLit "has the specified type") <+> pp_ty)
+        pp_name = quotes (ppr poly_name)
+        pp_ty   = quotes (ppr tidy_ty)
+        (tidy_env', tidy_ty) = tidyOpenType tidy_env (idType poly_id)
+        
 
-    zonk_tv tv = do { ty <- zonkTcTyVar tv; return (tcGetTyVar "mkExport" ty) }
+    prag_sigs = prag_fn poly_name
+    origin    = AmbigOrigin poly_name
+    sig_ctxt  = InfSigCtxt poly_name
 
 ------------------------
 type PragFun = Name -> [LSig Name]
@@ -627,12 +654,12 @@ tcVect (HsVect name@(L loc _) (Just rhs))
     do { _id <- wrapLocM tcLookupId name     -- need to ensure that the name is already defined
 
          -- turn the vectorisation declaration into a single non-recursive binding
-       ; let bind    = L loc $ mkFunBind name [mkSimpleMatch [] rhs] 
+       ; let bind    = L loc $ mkTopFunBind name [mkSimpleMatch [] rhs] 
              sigFun  = const Nothing
              pragFun = mkPragFun [] (unitBag bind)
 
          -- perform type inference (including generalisation)
-       ; (binds, [id']) <- tcPolyInfer TopLevel False sigFun pragFun NonRecursive [bind]
+       ; (binds, [id'], _) <- tcPolyInfer False True sigFun pragFun NonRecursive [bind]
 
        ; traceTc "tcVect inferred type" $ ppr (varType id')
        ; traceTc "tcVect bindings"      $ ppr binds
@@ -663,11 +690,11 @@ vectCtxt name = ptext (sLit "When checking the vectorisation declaration for") <
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise 
 -- subsequent error messages
-recoveryCode :: [Name] -> SigFun -> TcM (LHsBinds TcId, [Id])
+recoveryCode :: [Name] -> SigFun -> TcM (LHsBinds TcId, [Id], TopLevelFlag)
 recoveryCode binder_names sig_fn
   = do  { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
         ; poly_ids <- mapM mk_dummy binder_names
-        ; return (emptyBag, poly_ids) }
+        ; return (emptyBag, poly_ids, TopLevel) }
   where
     mk_dummy name 
         | isJust (sig_fn name) = tcLookupId name        -- Had signature; look it up
@@ -711,7 +738,7 @@ The signatures have been dealt with already.
 tcMonoBinds :: TcSigFun -> LetBndrSpec 
             -> RecFlag  -- Whether the binding is recursive for typechecking purposes
                         -- i.e. the binders are mentioned in their RHSs, and
-                        --      we are not resuced by a type signature
+                        --      we are not rescued by a type signature
             -> [LHsBind Name]
             -> TcM (LHsBinds TcId, [MonoBindInfo])
 
@@ -809,7 +836,8 @@ tcRhs :: TcMonoBind -> TcM (HsBind TcId)
 -- 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) loc inf matches)
-  = do  { (co_fn, matches') <- tcMatchesFun (idName mono_id) inf 
+  = do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
+        ; (co_fn, matches') <- tcMatchesFun (idName mono_id) inf 
                                             matches (idType mono_id)
         ; return (FunBind { fun_id = L loc mono_id, fun_infix = inf
                           , fun_matches = matches'
@@ -817,7 +845,8 @@ tcRhs (TcFunBind (_,_,mono_id) loc inf matches)
                           , bind_fvs = placeHolderNames, fun_tick = Nothing }) }
 
 tcRhs (TcPatBind _ pat' grhss pat_ty)
-  = do  { grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
+  = do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
+        ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
                     tcGRHSsPat grhss pat_ty
         ; return (PatBind { pat_lhs = pat', pat_rhs = grhss', pat_rhs_ty = pat_ty 
                           , bind_fvs = placeHolderNames }) }
@@ -852,6 +881,7 @@ We unify them because, with polymorphic recursion, their types
 might not otherwise be related.  This is a rather subtle issue.
 
 \begin{code}
+{-
 unifyCtxts :: [TcSigInfo] -> TcM ()
 -- Post-condition: the returned Insts are full zonked
 unifyCtxts [] = return ()
@@ -875,6 +905,18 @@ unifyCtxts (sig1 : sigs)
                checkTc (all isReflCo cois)
                        (ptext (sLit "Mutually dependent functions have syntactically distinct contexts"))
              }
+
+-----------------------------------------------
+sigContextsCtxt :: TcSigInfo -> TcSigInfo -> SDoc
+sigContextsCtxt sig1 sig2
+  = 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)]),
+          ptext (sLit "The signature contexts in a mutually recursive group should all be identical")]
+  where
+    id1 = sig_id sig1
+    id2 = sig_id sig2
+-}
 \end{code}
 
 
@@ -1138,48 +1180,70 @@ tcInstSig sig_fn use_skols name
 -------------------------------
 data GeneralisationPlan 
   = NoGen		-- No generalisation, no AbsBinds
-  | InferGen Bool	-- Implicit generalisation; there is an AbsBinds
-    	     		--   True <=> apply the MR; generalise only unconstrained type vars
+  | InferGen 	        -- Implicit generalisation; there is an AbsBinds
+       Bool    		--   True <=> apply the MR; generalise only unconstrained type vars
+       Bool             --   True <=> bindings mention only variables with closed types
   | CheckGen TcSigInfo	-- Explicit generalisation; there is an AbsBinds
 
 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
 
 instance Outputable GeneralisationPlan where
-  ppr NoGen        = ptext (sLit "NoGen")
-  ppr (InferGen b) = ptext (sLit "InferGen") <+> ppr b
-  ppr (CheckGen s) = ptext (sLit "CheckGen") <+> ppr s
+  ppr NoGen          = ptext (sLit "NoGen")
+  ppr (InferGen b c) = ptext (sLit "InferGen") <+> ppr b <+> ppr c
+  ppr (CheckGen s)   = ptext (sLit "CheckGen") <+> ppr s
 
 decideGeneralisationPlan 
-   :: DynFlags -> TopLevelFlag -> [Name] -> [LHsBind Name] -> TcSigFun -> GeneralisationPlan
-decideGeneralisationPlan dflags top_lvl _bndrs binds sig_fn
+   :: DynFlags -> TcTypeEnv -> [Name]
+   -> [LHsBind Name] -> TcSigFun -> GeneralisationPlan
+decideGeneralisationPlan dflags type_env bndr_names lbinds sig_fn
   | bang_pat_binds                         = NoGen
-  | mono_pat_binds                         = NoGen
   | Just sig <- one_funbind_with_sig binds = if null (sig_tvs sig) && null (sig_theta sig)
                                              then NoGen	      -- Optimise common case
                                              else CheckGen sig
-  | (xopt Opt_MonoLocalBinds dflags 
-      && isNotTopLevel top_lvl)      	   = NoGen
-  | otherwise                              = InferGen mono_restriction
+  | mono_local_binds      	           = NoGen
+  | otherwise                              = InferGen mono_restriction closed_flag
 
   where
-    bang_pat_binds = any (isBangHsBind . unLoc) binds
+    bndr_set = mkNameSet bndr_names
+    binds = map unLoc lbinds
+
+    bang_pat_binds = any isBangHsBind binds
        -- Bang patterns must not be polymorphic,
        -- because we are going to force them
        -- See Trac #4498
 
-    mono_pat_binds = xopt Opt_MonoPatBinds dflags
-                  && any (is_pat_bind . unLoc) binds
-
-    mono_restriction = xopt Opt_MonomorphismRestriction dflags 
-                    && any (restricted . unLoc) binds
+    mono_restriction  = xopt Opt_MonomorphismRestriction dflags 
+                     && any restricted binds
+
+    is_closed_ns :: NameSet -> Bool -> Bool
+    is_closed_ns ns b = foldNameSet ((&&) . is_closed_id) b ns
+	-- ns are the Names referred to from the RHS of this bind
+
+    is_closed_id :: Name -> Bool
+    is_closed_id name 
+      | name `elemNameSet` bndr_set
+      = True 		  -- Ignore binders in this groups, of course
+      | Just (ATcId { tct_closed = cl }) <- lookupNameEnv type_env name
+      = isTopLevel cl 	  -- This is the key line
+      | otherwise
+      = WARN( isInternalName name, ppr name ) True
+      	-- The free-var set for a top level binding mentions
+	-- imported things too, so that we can report unused imports
+	-- These won't be in the local type env.  
+	-- Ditto class method etc from the current module
+    
+    closed_flag = foldr (is_closed_ns . bind_fvs) True binds
+
+    mono_local_binds = xopt Opt_MonoLocalBinds dflags 
+                    && not closed_flag
 
     no_sig n = isNothing (sig_fn n)
 
     -- With OutsideIn, all nested bindings are monomorphic
     -- except a single function binding with a signature
-    one_funbind_with_sig [L _ FunBind { fun_id = v }] = sig_fn (unLoc v)
-    one_funbind_with_sig _                            = Nothing
+    one_funbind_with_sig [FunBind { fun_id = v }] = sig_fn (unLoc v)
+    one_funbind_with_sig _                        = Nothing
 
     -- The Haskell 98 monomorphism resetriction
     restricted (PatBind {})                              = True
@@ -1193,9 +1257,6 @@ decideGeneralisationPlan dflags top_lvl _bndrs binds sig_fn
         -- No args => like a pattern binding
         -- Some args => a function binding
 
-    is_pat_bind (PatBind {}) = True
-    is_pat_bind _            = False
-
 -------------------
 checkStrictBinds :: TopLevelFlag -> RecFlag
                  -> [LHsBind Name] -> [Id]
@@ -1264,15 +1325,4 @@ pprBindList binds = vcat (map ppr binds)
 patMonoBindsCtxt :: OutputableBndr id => LPat id -> GRHSs Name -> SDoc
 patMonoBindsCtxt pat grhss
   = hang (ptext (sLit "In a pattern binding:")) 2 (pprPatBind pat grhss)
-
------------------------------------------------
-sigContextsCtxt :: TcSigInfo -> TcSigInfo -> SDoc
-sigContextsCtxt sig1 sig2
-  = 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)]),
-          ptext (sLit "The signature contexts in a mutually recursive group should all be identical")]
-  where
-    id1 = sig_id sig1
-    id2 = sig_id sig2
 \end{code}
diff --git a/compiler/typecheck/TcClassDcl.lhs b/compiler/typecheck/TcClassDcl.lhs
index 2663895443..0dca868084 100644
--- a/compiler/typecheck/TcClassDcl.lhs
+++ b/compiler/typecheck/TcClassDcl.lhs
@@ -235,15 +235,17 @@ tcInstanceMethodBody skol_info tyvars dfun_ev_vars
                              -- Substitute the local_meth_name for the binder
 			     -- NB: the binding is always a FunBind
         ; traceTc "TIM" (ppr local_meth_id $$ ppr (meth_sig_fn (idName local_meth_id))) 
-	; (ev_binds, (tc_bind, _)) 
+	; (ev_binds, (tc_bind, _, _)) 
                <- checkConstraints skol_info tyvars dfun_ev_vars $
 		  tcExtendIdEnv [local_meth_id] $
 	          tcPolyBinds TopLevel meth_sig_fn no_prag_fn 
 		  	     NonRecursive NonRecursive
 		  	     [lm_bind]
 
-        ; let full_bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
-                                   , abs_exports = [(tyvars, meth_id, local_meth_id, specs)]
+        ; let export = ABE { abe_wrap = idHsWrapper, abe_poly = meth_id
+                           , abe_mono = local_meth_id, abe_prags = specs }
+              full_bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
+                                   , abs_exports = [export]
                                    , abs_ev_binds = ev_binds
                                    , abs_binds = tc_bind }
 
@@ -357,8 +359,8 @@ mkGenericDefMethBind clas inst_tys sel_id dm_name
 		   (vcat [ppr clas <+> ppr inst_tys,
 			  nest 2 (ppr sel_id <+> equals <+> ppr rhs)]))
 
-        ; return (noLoc $ mkFunBind (noLoc (idName sel_id))
-                                    [mkSimpleMatch [] rhs]) }
+        ; return (noLoc $ mkTopFunBind (noLoc (idName sel_id))
+                                       [mkSimpleMatch [] rhs]) }
   where
     rhs = nlHsVar dm_name
 \end{code}
diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs
index 52096b6948..9550232805 100644
--- a/compiler/typecheck/TcEnv.lhs
+++ b/compiler/typecheck/TcEnv.lhs
@@ -23,7 +23,7 @@ module TcEnv(
 	-- Local environment
 	tcExtendKindEnv, tcExtendKindEnvTvs,
 	tcExtendTyVarEnv, tcExtendTyVarEnv2, 
-	tcExtendGhciEnv,
+	tcExtendGhciEnv, tcExtendLetEnv,
 	tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, 
 	tcLookup, tcLookupLocated, tcLookupLocalIds, 
 	tcLookupId, tcLookupTyVar, getScopedTyVarBinds,
@@ -76,6 +76,7 @@ import NameEnv
 import HscTypes
 import DynFlags
 import SrcLoc
+import BasicTypes
 import Outputable
 import Unique
 import FastString
@@ -371,23 +372,8 @@ tcExtendTyVarEnv tvs thing_inside
   = tcExtendTyVarEnv2 [(tyVarName tv, mkTyVarTy tv) | tv <- tvs] thing_inside
 
 tcExtendTyVarEnv2 :: [(Name,TcType)] -> TcM r -> TcM r
-tcExtendTyVarEnv2 binds thing_inside = do
-    env@(TcLclEnv {tcl_env = le,
-                   tcl_tyvars = gtvs,
-                   tcl_rdr = rdr_env}) <- getLclEnv
-    let
-	rdr_env'   = extendLocalRdrEnvList rdr_env (map fst binds)
-	new_tv_set = tcTyVarsOfTypes (map snd binds)
- 	le'        = extendNameEnvList le [(name, ATyVar name ty) | (name, ty) <- binds]
-
-	-- It's important to add the in-scope tyvars to the global tyvar set
-	-- as well.  Consider
-	--	f (_::r) = let g y = y::r in ...
-	-- Here, g mustn't be generalised.  This is also important during
-	-- class and instance decls, when we mustn't generalise the class tyvars
-	-- when typechecking the methods.
-    gtvs' <- tcExtendGlobalTyVars gtvs new_tv_set
-    setLclEnv (env {tcl_env = le', tcl_tyvars = gtvs', tcl_rdr = rdr_env'}) thing_inside
+tcExtendTyVarEnv2 binds thing_inside 
+  = tc_extend_local_env [(name, ATyVar name ty) | (name, ty) <- binds] thing_inside
 
 getScopedTyVarBinds :: TcM [(Name, TcType)]
 getScopedTyVarBinds
@@ -397,32 +383,54 @@ getScopedTyVarBinds
 
 
 \begin{code}
+tcExtendLetEnv :: TopLevelFlag -> [TcId] -> TcM a -> TcM a
+tcExtendLetEnv closed ids thing_inside 
+  = do	{ stage <- getStage
+	; tc_extend_local_env [ (idName id, ATcId { tct_id = id 
+    	         	                          , tct_closed = closed
+    	       		                          , tct_level = thLevel stage })
+                 	         | id <- ids]
+          thing_inside }
+
 tcExtendIdEnv :: [TcId] -> TcM a -> TcM a
-tcExtendIdEnv ids thing_inside = tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
+tcExtendIdEnv ids thing_inside 
+  = tcExtendIdEnv2 [(idName id, id) | id <- ids] thing_inside
 
 tcExtendIdEnv1 :: Name -> TcId -> TcM a -> TcM a
-tcExtendIdEnv1 name id thing_inside = tcExtendIdEnv2 [(name,id)] thing_inside
+tcExtendIdEnv1 name id thing_inside 
+  = tcExtendIdEnv2 [(name,id)] thing_inside
 
 tcExtendIdEnv2 :: [(Name,TcId)] -> TcM a -> TcM a
 -- Invariant: the TcIds are fully zonked (see tcExtendIdEnv above)
 tcExtendIdEnv2 names_w_ids thing_inside
-  = do	{ env <- getLclEnv
-	; tc_extend_local_id_env env (thLevel (tcl_th_ctxt env)) names_w_ids thing_inside }
+  = do	{ stage <- getStage
+	; tc_extend_local_env [ (name, ATcId { tct_id = id 
+    	         	                     , tct_closed = NotTopLevel
+    	       		                     , tct_level = thLevel stage })
+                 	         | (name,id) <- names_w_ids]
+          thing_inside }
 
 tcExtendGhciEnv :: [TcId] -> TcM a -> TcM a
 -- Used to bind Ids for GHCi identifiers bound earlier in the user interaction
--- Note especially that we bind them at TH level 'impLevel'.  That's because it's
--- OK to use a variable bound earlier in the interaction in a splice, becuase
--- GHCi has already compiled it to bytecode
+-- Note especially that we bind them at 
+--  * TH level 'impLevel'.  That's because it's OK to use a variable bound
+--    earlier in the interaction in a splice, because
+--    GHCi has already compiled it to bytecode
+--  * Closedness flag is TopLevel.  The thing's type is closed
+
 tcExtendGhciEnv ids thing_inside
-  = do	{ env <- getLclEnv
-	; tc_extend_local_id_env env impLevel [(idName id, id) | id <- ids] thing_inside }
-
-tc_extend_local_id_env		-- This is the guy who does the work
-	:: TcLclEnv
-	-> ThLevel
-	-> [(Name,TcId)]
-	-> TcM a -> TcM a
+  = tc_extend_local_env [ (idName id, ATcId { tct_id     = id 
+    	         	     	            , tct_closed = is_top id
+    	       		     	  	    , tct_level  = impLevel })
+                        | id <- ids]
+    thing_inside
+  where
+    is_top id | isEmptyVarSet (tcTyVarsOfType (idType id)) = TopLevel
+              | otherwise                                  = NotTopLevel
+
+
+tc_extend_local_env :: [(Name, TcTyThing)] -> TcM a -> TcM a
+-- This is the guy who does the work
 -- Invariant: the TcIds are fully zonked. Reasons:
 --	(a) The kinds of the forall'd type variables are defaulted
 --	    (see Kind.defaultKind, done in zonkQuantifiedTyVar)
@@ -430,18 +438,41 @@ tc_extend_local_id_env		-- This is the guy who does the work
 --	    in the types, because instantiation does not look through such things
 --	(c) The call to tyVarsOfTypes is ok without looking through refs
 
-tc_extend_local_id_env env th_lvl names_w_ids thing_inside
+tc_extend_local_env extra_env thing_inside
   = do	{ traceTc "env2" (ppr extra_env)
-	; gtvs' <- tcExtendGlobalTyVars (tcl_tyvars env) extra_global_tyvars
-	; let env' = env {tcl_env = le', tcl_tyvars = gtvs', tcl_rdr = rdr_env'}
-	; setLclEnv env' thing_inside }
+        ; env1 <- getLclEnv
+        ; let le'      = extendNameEnvList     (tcl_env env1) extra_env
+              rdr_env' = extendLocalRdrEnvList (tcl_rdr env1) (map fst extra_env)
+	      env2     = env1 {tcl_env = le', tcl_rdr = rdr_env'}
+	; env3 <- extend_gtvs env2
+	; setLclEnv env3 thing_inside }
   where
-    extra_global_tyvars = tcTyVarsOfTypes [idType id | (_,id) <- names_w_ids]
-    extra_env	    = [ (name, ATcId { tct_id = id, 
-    				       tct_level = th_lvl })
-    		      | (name,id) <- names_w_ids]
-    le'		    = extendNameEnvList (tcl_env env) extra_env
-    rdr_env'	    = extendLocalRdrEnvList (tcl_rdr env) [name | (name,_) <- names_w_ids]
+    extend_gtvs env 
+      | isEmptyVarSet extra_tvs 
+      = return env
+      | otherwise               
+      = do { g_var <- tcExtendGlobalTyVars (tcl_tyvars env) extra_tvs
+           ; return (env { tcl_tyvars = g_var }) }
+
+    extra_tvs = foldr (unionVarSet . get_tvs) emptyVarSet extra_env
+
+    get_tvs (_, ATcId { tct_id = id, tct_closed = closed })
+      = case closed of
+          TopLevel    -> ASSERT2( isEmptyVarSet id_tvs, ppr id $$ ppr (idType id) ) 
+                         emptyVarSet
+          NotTopLevel -> id_tvs
+      where
+        id_tvs = tcTyVarsOfType (idType id)
+    get_tvs (_, ATyVar _ ty) = tcTyVarsOfType ty	-- See Note [Global TyVars]
+    get_tvs other = pprPanic "get_tvs" (ppr other)
+        
+	-- Note [Global TyVars]
+	-- It's important to add the in-scope tyvars to the global tyvar set
+	-- as well.  Consider
+	--	f (_::r) = let g y = y::r in ...
+	-- Here, g mustn't be generalised.  This is also important during
+	-- class and instance decls, when we mustn't generalise the class tyvars
+	-- when typechecking the methods.
 
 tcExtendGlobalTyVars :: IORef VarSet -> VarSet -> TcM (IORef VarSet)
 tcExtendGlobalTyVars gtv_var extra_global_tvs
diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs
index 2f258340c9..254f132d54 100644
--- a/compiler/typecheck/TcErrors.lhs
+++ b/compiler/typecheck/TcErrors.lhs
@@ -226,16 +226,6 @@ pprWithArising ev_vars
 addErrorReport :: ReportErrCtxt -> SDoc -> TcM ()
 addErrorReport ctxt msg = addErrTcM (cec_tidy ctxt, msg $$ cec_extra ctxt)
 
-pprErrCtxtLoc :: ReportErrCtxt -> SDoc
-pprErrCtxtLoc ctxt 
-  = case map (ctLocOrigin . ic_loc) (cec_encl ctxt) of
-       []           -> ptext (sLit "the top level")	-- Should not happen
-       (orig:origs) -> ppr_skol orig $$ 
-                       vcat [ ptext (sLit "or") <+> ppr_skol orig | orig <- origs ]
-  where
-    ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
-    ppr_skol skol_info      = ppr skol_info
-
 getUserGivens :: ReportErrCtxt -> [([EvVar], GivenLoc)]
 -- One item for each enclosing implication
 getUserGivens (CEC {cec_encl = ctxt})
@@ -514,13 +504,10 @@ reportDictErrs ctxt wanteds orig
 
       | otherwise
       = vcat [ couldNotDeduce givens (min_wanteds, orig)
-             , show_fixes (fix1 : (fixes2 ++ fixes3)) ]
+             , show_fixes (fixes1 ++ fixes2 ++ fixes3) ]
       where
         givens = getUserGivens ctxt
         min_wanteds = mkMinimalBySCs wanteds
-        fix1 = sep [ ptext (sLit "add") <+> pprTheta min_wanteds
-                          <+> ptext (sLit "to the context of")
-	           , nest 2 $ pprErrCtxtLoc ctxt ]
 
         fixes2 = case instance_dicts of
                    []  -> []
@@ -544,6 +531,23 @@ reportDictErrs ctxt wanteds orig
 	show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
 				 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 
+        fixes1 | (orig:origs) <- mapCatMaybes get_good_orig (cec_encl ctxt)
+               = [sep [ ptext (sLit "add") <+> pprTheta min_wanteds
+                        <+> ptext (sLit "to the context of")
+	              , nest 2 $ ppr_skol orig $$ 
+                                 vcat [ ptext (sLit "or") <+> ppr_skol orig 
+                                      | orig <- origs ]
+                 ]    ]
+               | otherwise = []
+
+        ppr_skol (PatSkol dc _) = ptext (sLit "the data constructor") <+> quotes (ppr dc)
+        ppr_skol skol_info      = ppr skol_info
+
+	-- Do not suggest adding constraints to an *inferred* type signature!
+        get_good_orig ic = case ctLocOrigin (ic_loc ic) of 
+                             SigSkol (InfSigCtxt {}) _ -> Nothing
+                             origin                    -> Just origin
+
 reportOverlap :: ReportErrCtxt -> (InstEnv,InstEnv) -> CtOrigin
               -> PredType -> TcM (Maybe PredType)
 -- Report an overlap error if this class constraint results
diff --git a/compiler/typecheck/TcHsSyn.lhs b/compiler/typecheck/TcHsSyn.lhs
index 5887fb57e2..699869c824 100644
--- a/compiler/typecheck/TcHsSyn.lhs
+++ b/compiler/typecheck/TcHsSyn.lhs
@@ -425,15 +425,17 @@ zonk_bind env sig_warn (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs
     	    ; new_val_binds <- zonkMonoBinds env3 noSigWarn val_binds
     	    ; new_exports   <- mapM (zonkExport env3) exports
     	    ; return (new_val_binds, new_exports) } 
-       ; sig_warn True [b | (_,b,_,_) <- new_exports]
+       ; sig_warn True (map abe_poly new_exports)
        ; return (AbsBinds { abs_tvs = tyvars, abs_ev_vars = new_evs, abs_ev_binds = new_ev_binds
 			  , abs_exports = new_exports, abs_binds = new_val_bind }) }
   where
-    zonkExport env (tyvars, global, local, prags)
-	-- The tyvars are already zonked
-	= zonkIdBndr env global			`thenM` \ new_global ->
-	  zonkSpecPrags env prags		`thenM` \ new_prags -> 
-	  returnM (tyvars, new_global, zonkIdOcc env local, new_prags)
+    zonkExport env (ABE{ abe_wrap = wrap, abe_poly = poly_id
+                       , abe_mono = mono_id, abe_prags = prags })
+	= zonkIdBndr env poly_id		`thenM` \ new_poly_id ->
+	  zonkCoFn env wrap                     `thenM` \ (_, new_wrap) ->
+          zonkSpecPrags env prags		`thenM` \ new_prags -> 
+	  returnM (ABE{ abe_wrap = new_wrap, abe_poly = new_poly_id
+                      , abe_mono = zonkIdOcc env mono_id, abe_prags = new_prags })
 
 zonkSpecPrags :: ZonkEnv -> TcSpecPrags -> TcM TcSpecPrags
 zonkSpecPrags _   IsDefaultMethod = return IsDefaultMethod
diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index a0a5a503eb..3070ee9cb4 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -781,7 +781,7 @@ tcInstDecls2 tycl_decls inst_decls
         ; let dm_ids = collectHsBindsBinders dm_binds
               -- Add the default method Ids (again)
               -- See Note [Default methods and instances]
-        ; inst_binds_s <- tcExtendIdEnv dm_ids $
+        ; inst_binds_s <- tcExtendLetEnv TopLevel dm_ids $
                           mapM tcInstDecl2 inst_decls
 
           -- Done
@@ -884,10 +884,11 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
              dfun_args = map varToCoreExpr sc_args ++
                          map Var           meth_ids
 
+             export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id_w_fun
+                          , abe_mono = self_dict, abe_prags = SpecPrags spec_inst_prags }
              main_bind = AbsBinds { abs_tvs = inst_tyvars
                                   , abs_ev_vars = dfun_ev_vars
-                                  , abs_exports = [(inst_tyvars, dfun_id_w_fun, self_dict,
-                                                    SpecPrags spec_inst_prags)]
+                                  , abs_exports = [export]
                                   , abs_ev_binds = emptyTcEvBinds
                                   , abs_binds = unitBag dict_bind }
 
@@ -1119,9 +1120,12 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                         -- Copy the inline pragma (if any) from the default
                         -- method to this version. Note [INLINE and default methods]
 
+                  
+                 export = ABE { abe_wrap = idHsWrapper, abe_poly = meth_id1
+                              , abe_mono = local_meth_id
+                              , abe_prags = mk_meth_spec_prags meth_id1 [] }
                  bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
-                                 , abs_exports = [( tyvars, meth_id1, local_meth_id
-                                                  , mk_meth_spec_prags meth_id1 [])]
+                                 , abs_exports = [export]
                                  , abs_ev_binds = EvBinds (unitBag self_ev_bind)
                                  , abs_binds    = unitBag meth_bind }
              -- Default methods in an instance declaration can't have their own
@@ -1215,9 +1219,10 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
 
             ; let meth_rhs  = wrapId (mk_op_wrapper sel_id rep_d) sel_id
                   meth_bind = mkVarBind local_meth_id (L loc meth_rhs)
+                  export = ABE { abe_wrap = idHsWrapper, abe_poly = meth_id
+                               , abe_mono = local_meth_id, abe_prags = noSpecPrags }
                   bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars
-                                   , abs_exports = [(tyvars, meth_id,
-                                                     local_meth_id, noSpecPrags)]
+                                   , abs_exports = [export]
                                    , abs_ev_binds = rep_ev_binds
                                    , abs_binds = unitBag $ meth_bind }
 
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 6962a19dbc..063eff79e1 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -438,7 +438,9 @@ zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvar
 -----------------  Types
 zonkTcTypeCarefully :: TcType -> TcM TcType
 -- Do not zonk type variables free in the environment
-zonkTcTypeCarefully ty
+zonkTcTypeCarefully ty = zonkTcType ty   -- I think this function is out of date
+
+{-
   = do { env_tvs <- tcGetGlobalTyVars
        ; zonkType (zonk_tv env_tvs) ty }
   where
@@ -455,6 +457,7 @@ zonkTcTypeCarefully ty
                               ; case cts of
 			           Flexi       -> return (TyVarTy tv)
 			           Indirect ty -> zonkType (zonk_tv env_tvs) ty }
+-}
 
 zonkTcType :: TcType -> TcM TcType
 -- Simply look through all Flexis
@@ -836,6 +839,7 @@ checkValidType ctxt ty = do
 
 		 ExprSigCtxt 	-> gen_rank 1
 		 FunSigCtxt _   -> gen_rank 1
+		 InfSigCtxt _   -> ArbitraryRank	-- Inferred type
 		 ConArgCtxt _   | polycomp -> gen_rank 2
                                 -- We are given the type of the entire
                                 -- constructor, hence rank 1
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 403a3aa847..706690d502 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -1222,9 +1222,10 @@ mkPlan :: LStmt Name -> TcM PlanResult
 mkPlan (L loc (ExprStmt expr _ _ _))	-- An expression typed at the prompt 
   = do	{ uniq <- newUnique		-- is treated very specially
 	; let fresh_it  = itName uniq
-	      the_bind  = L loc $ mkFunBind (L loc fresh_it) matches
+	      the_bind  = L loc $ mkTopFunBind (L loc fresh_it) matches
 	      matches   = [mkMatch [] expr emptyLocalBinds]
-	      let_stmt  = L loc $ LetStmt (HsValBinds (ValBindsOut [(NonRecursive,unitBag the_bind)] []))
+	      let_stmt  = L loc $ LetStmt $ HsValBinds $
+                          ValBindsOut [(NonRecursive,unitBag the_bind)] []
 	      bind_stmt = L loc $ BindStmt (nlVarPat fresh_it) expr
 					   (HsVar bindIOName) noSyntaxExpr 
 	      print_it  = L loc $ ExprStmt (nlHsApp (nlHsVar printName) (nlHsVar fresh_it))
@@ -1343,10 +1344,11 @@ tcRnExpr hsc_env ictxt rdr_expr
     uniq <- newUnique ;
     let { fresh_it  = itName uniq } ;
     ((_tc_expr, res_ty), lie)	<- captureConstraints (tcInferRho rn_expr) ;
-    ((qtvs, dicts, _), lie_top) <- captureConstraints $ 
-                                   simplifyInfer TopLevel False {- No MR for now -}
-                                                 [(fresh_it, res_ty)]
-                                                 lie  ;
+    ((qtvs, dicts, _, _), lie_top) <- captureConstraints $ 
+                                      simplifyInfer True {- Free vars are closed -}
+                                                    False {- No MR for now -}
+                                                    [(fresh_it, res_ty)]
+                                                    lie  ;
     _ <- simplifyInteractive lie_top ;       -- Ignore the dicionary bindings
 
     let { all_expr_ty = mkForAllTys qtvs (mkPiTypes dicts res_ty) } ;
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index 1935883cee..01389a92db 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -1015,7 +1015,7 @@ isUntouchable :: TcTyVar -> TcM Bool
 isUntouchable tv = do { env <- getLclEnv
                       ; return (varUnique tv < tcl_untch env) }
 
-getLclTypeEnv :: TcM (NameEnv TcTyThing)
+getLclTypeEnv :: TcM TcTypeEnv
 getLclTypeEnv = do { env <- getLclEnv; return (tcl_env env) }
 
 setLclTypeEnv :: TcLclEnv -> TcM a -> TcM a
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index 9ddb36b8c3..90603464b6 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -516,8 +516,9 @@ data TcTyThing
   = AGlobal TyThing		-- Used only in the return type of a lookup
 
   | ATcId   {		-- Ids defined in this module; may not be fully zonked
-	tct_id    :: TcId,		
-	tct_level :: ThLevel }
+	tct_id     :: TcId,		
+	tct_closed :: TopLevelFlag,   -- See Note [Bindings with closed types]
+	tct_level  :: ThLevel }
 
   | ATyVar  Name TcType		-- The type to which the lexically scoped type vaiable
 				-- is currently refined. We only need the Name
@@ -543,6 +544,10 @@ pprTcTyThingCategory (ATcId {})      = ptext (sLit "Local identifier")
 pprTcTyThingCategory (AThing {})     = ptext (sLit "Kinded thing")
 \end{code}
 
+Note [Bindings with closed types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+TODO: write me.  This is all to do with OutsideIn
+
 \begin{code}
 type ErrCtxt = (Bool, TidyEnv -> TcM (TidyEnv, Message))
 	-- Monadic so that we have a chance
@@ -1139,6 +1144,7 @@ data CtOrigin
   | PArrSeqOrigin  (ArithSeqInfo Name) -- [:x..y:] and [:x,y..z:]
   | SectionOrigin
   | TupleOrigin			       -- (..,..)
+  | AmbigOrigin Name	-- f :: ty
   | ExprSigOrigin	-- e :: ty
   | PatSigOrigin	-- p :: ty
   | PatOrigin	        -- Instantiating a polytyped pattern at a constructor
@@ -1170,6 +1176,7 @@ pprO AppOrigin             = ptext (sLit "an application")
 pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
 pprO (IPOccOrigin name)    = hsep [ptext (sLit "a use of implicit parameter"), quotes (ppr name)]
 pprO RecordUpdOrigin       = ptext (sLit "a record update")
+pprO (AmbigOrigin name)    = ptext (sLit "the ambiguity check for") <+> quotes (ppr name)
 pprO ExprSigOrigin         = ptext (sLit "an expression type signature")
 pprO PatSigOrigin          = ptext (sLit "a pattern type signature")
 pprO PatOrigin             = ptext (sLit "a pattern")
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index eb5578eb15..636e7481fb 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,6 +1,6 @@
 \begin{code}
 module TcSimplify( 
-       simplifyInfer,
+       simplifyInfer, simplifyAmbiguityCheck,
        simplifyDefault, simplifyDeriv, 
        simplifyRule, simplifyTop, simplifyInteractive
   ) where
@@ -30,7 +30,7 @@ import Util
 import PrelInfo
 import PrelNames
 import Class		( classKey )
-import BasicTypes       ( RuleName, TopLevelFlag, isTopLevel )
+import BasicTypes       ( RuleName )
 import Control.Monad    ( when )
 import Outputable
 import FastString
@@ -53,6 +53,11 @@ simplifyTop wanteds
   = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
 
 ------------------
+simplifyAmbiguityCheck :: Name -> WantedConstraints -> TcM (Bag EvBind)
+simplifyAmbiguityCheck name wanteds
+  = simplifyCheck (SimplCheck (ptext (sLit "ambiguity check for") <+> ppr name)) wanteds
+
+------------------
 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
 simplifyInteractive wanteds 
   = simplifyCheck SimplInteractive wanteds
@@ -199,21 +204,24 @@ Allow constraints which consist only of type variables, with no repeats.
 ***********************************************************************************
 
 \begin{code}
-simplifyInfer :: TopLevelFlag
+simplifyInfer :: Bool
               -> Bool                  -- Apply monomorphism restriction
               -> [(Name, TcTauType)]   -- Variables to be generalised,
                                        -- and their tau-types
               -> WantedConstraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints
+		      Bool,	    -- The monomorphism restriction did something
+		      		    --   so the results type is not as general as
+				    --   it could be
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer top_lvl apply_mr name_taus wanteds
+simplifyInfer _top_lvl apply_mr name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
        ; zonked_taus <- zonkTcTypes (map snd name_taus)
        ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
        ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
-       ; return (qtvs, [], emptyTcEvBinds) }
+       ; return (qtvs, [], False, emptyTcEvBinds) }
 
   | otherwise
   = do { zonked_wanteds <- zonkWC wanteds
@@ -221,8 +229,11 @@ simplifyInfer top_lvl apply_mr name_taus wanteds
        ; gbl_tvs        <- tcGetGlobalTyVars
 
        ; traceTc "simplifyInfer {"  $ vcat
-             [ ptext (sLit "apply_mr =") <+> ppr apply_mr
-             , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
+             [ ptext (sLit "names =") <+> ppr (map fst name_taus)
+             , ptext (sLit "taus (zonked) =") <+> ppr zonked_taus
+             , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
+             , ptext (sLit "closed =") <+> ppr _top_lvl
+             , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
              ]
 
@@ -265,32 +276,36 @@ simplifyInfer top_lvl apply_mr name_taus wanteds
        ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
        ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
        ; let init_tvs 	     = zonked_tau_tvs `minusVarSet` gbl_tvs
+             poly_qtvs       = growWantedEVs gbl_tvs zonked_simples init_tvs
+	     (pbound, pfree) = partitionBag (quantifyMe poly_qtvs) zonked_simples
+
+	     -- Monomorphism restriction
              mr_qtvs  	     = init_tvs `minusVarSet` constrained_tvs
              constrained_tvs = tyVarsOfEvVarXs zonked_simples
-             qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
-             (final_qtvs, (bound, free))
-                | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
-                | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
+	     mr_bites        = apply_mr && not (isEmptyBag pbound)
+
+             (qtvs, (bound, free))
+                | mr_bites  = (mr_qtvs,   (emptyBag, zonked_simples))
+                | otherwise = (poly_qtvs, (pbound,   pfree))
        ; emitFlats free
 
-       ; if isEmptyVarSet final_qtvs && isEmptyBag bound
+       ; if isEmptyVarSet qtvs && isEmptyBag bound
          then ASSERT( isEmptyBag (wc_insol simpl_results) )
               do { traceTc "} simplifyInfer/no quantification" empty
                  ; emitImplications (wc_impl simpl_results)
-                 ; return ([], [], EvBinds tc_binds0) }
+                 ; return ([], [], mr_bites, EvBinds tc_binds0) }
          else do
 
             -- Step 4, zonk quantified variables 
        { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
-       ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
-                        | (name, ty) <- name_taus ]
+             skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
+                                   | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
                         -- they are also bound in ic_skols and we want them to be
                         -- tidied uniformly
-             skol_info = InferSkol poly_ids
 
        ; gloc <- getCtLoc skol_info
-       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
+       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
 
             -- Step 5
             -- Minimize `bound' and emit an implication
@@ -310,17 +325,21 @@ simplifyInfer top_lvl apply_mr name_taus wanteds
        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
              vcat [ ptext (sLit "implic =") <+> ppr implic
                        -- ic_skols, ic_given give rest of result
-                  , ptext (sLit "qtvs =") <+> ppr final_qtvs
+                  , ptext (sLit "qtvs =") <+> ppr qtvs_to_return
                   , ptext (sLit "spb =") <+> ppr zonked_simples
                   , ptext (sLit "bound =") <+> ppr bound ]
 
 
 
-       ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
+       ; return ( qtvs_to_return, minimal_bound_ev_vars
+                , mr_bites,  TcEvBinds ev_binds_var) } }
   where
+    get_tau_tvs = tyVarsOfTypes	-- I think this stuff is out of date
+{-
     get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
                 | otherwise          = exactTyVarsOfTypes
      -- See Note [Silly type synonym] in TcType
+-}
 \end{code}
 
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index c0998de4f0..11c29308de 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -1098,8 +1098,8 @@ mkRecSelBind (tycon, sel_name)
     -- Make the binding: sel (C2 { fld = x }) = x
     --                   sel (C7 { fld = x }) = x
     --    where cons_w_field = [C2,C7]
-    sel_bind | is_naughty = mkFunBind sel_lname [mkSimpleMatch [] unit_rhs]
-             | otherwise  = mkFunBind sel_lname (map mk_match cons_w_field ++ deflt)
+    sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
+             | otherwise  = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
     mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)] 
                                  (L loc (HsVar field_var))
     mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 1313bdd310..134ab54d83 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -336,6 +336,7 @@ data MetaInfo
 data UserTypeCtxt
   = FunSigCtxt Name	-- Function type signature
 			-- Also used for types in SPECIALISE pragmas
+  | InfSigCtxt Name	-- Inferred type for function
   | ExprSigCtxt		-- Expression type signature
   | ConArgCtxt Name	-- Data constructor argument
   | TySynCtxt Name	-- RHS of a type synonym decl
@@ -410,19 +411,20 @@ pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs")
 pprTcTyVarDetails (MetaTv SigTv _) = ptext (sLit "sig")
 
 pprUserTypeCtxt :: UserTypeCtxt -> SDoc
-pprUserTypeCtxt (FunSigCtxt n)  = ptext (sLit "the type signature for") <+> quotes (ppr n)
-pprUserTypeCtxt ExprSigCtxt     = ptext (sLit "an expression type signature")
-pprUserTypeCtxt (ConArgCtxt c)  = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
-pprUserTypeCtxt (TySynCtxt c)   = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
-pprUserTypeCtxt GenPatCtxt      = ptext (sLit "the type pattern of a generic definition")
-pprUserTypeCtxt ThBrackCtxt     = ptext (sLit "a Template Haskell quotation [t|...|]")
-pprUserTypeCtxt LamPatSigCtxt   = ptext (sLit "a pattern type signature")
-pprUserTypeCtxt BindPatSigCtxt  = ptext (sLit "a pattern type signature")
-pprUserTypeCtxt ResSigCtxt      = ptext (sLit "a result type signature")
-pprUserTypeCtxt (ForSigCtxt n)  = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
-pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
-pprUserTypeCtxt SpecInstCtxt    = ptext (sLit "a SPECIALISE instance pragma")
-pprUserTypeCtxt GenSigCtxt      = ptext (sLit "a type expected by the context")
+pprUserTypeCtxt (InfSigCtxt n)   = ptext (sLit "the inferred type for") <+> quotes (ppr n)
+pprUserTypeCtxt (FunSigCtxt n)   = ptext (sLit "the type signature for") <+> quotes (ppr n)
+pprUserTypeCtxt ExprSigCtxt      = ptext (sLit "an expression type signature")
+pprUserTypeCtxt (ConArgCtxt c)   = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
+pprUserTypeCtxt (TySynCtxt c)    = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
+pprUserTypeCtxt GenPatCtxt       = ptext (sLit "the type pattern of a generic definition")
+pprUserTypeCtxt ThBrackCtxt      = ptext (sLit "a Template Haskell quotation [t|...|]")
+pprUserTypeCtxt LamPatSigCtxt    = ptext (sLit "a pattern type signature")
+pprUserTypeCtxt BindPatSigCtxt   = ptext (sLit "a pattern type signature")
+pprUserTypeCtxt ResSigCtxt       = ptext (sLit "a result type signature")
+pprUserTypeCtxt (ForSigCtxt n)   = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
+pprUserTypeCtxt DefaultDeclCtxt  = ptext (sLit "a type in a `default' declaration")
+pprUserTypeCtxt SpecInstCtxt     = ptext (sLit "a SPECIALISE instance pragma")
+pprUserTypeCtxt GenSigCtxt       = ptext (sLit "a type expected by the context")
 \end{code}