[project @ 2005-02-09 14:02:31 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 3c0ac28..4c0ca4b 100644 (file)
@@ -21,42 +21,43 @@ module TcSimplify (
 
 import {-# SOURCE #-} TcUnify( unifyTauTy )
 import TcEnv           -- temp
-import HsSyn           ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr, pprLHsBinds )
+import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
 import TcHsSyn         ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
 
 import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
-                         tyVarsOfInst, fdPredsOfInsts, fdPredsOfInst, newDicts,
+                         tyVarsOfInst, fdPredsOfInsts, newDicts, 
                          isDict, isClassDict, isLinearInst, linearInstType,
                          isStdClassTyVarDict, isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         instBindingRequired,
+                         instBindingRequired, fdPredsOfInst,
                          newDictsFromOld, tcInstClassOp,
                          getDictClassTys, isTyVarDict,
                          instLoc, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, pprInsts, pprDictsInFull, tcGetInstEnvs,
-                         isIPDict, isInheritableInst, pprDFuns, pprDictsTheta
+                         Inst, pprInsts, pprDictsInFull, pprInstInFull, tcGetInstEnvs,
+                         isInheritableInst, pprDFuns, pprDictsTheta
                        )
-import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals )
-import InstEnv         ( lookupInstEnv, classInstEnv )
+import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals, pprBinders )
+import InstEnv         ( lookupInstEnv, classInstances )
 import TcMType         ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
-import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
-                         mkClassPred, isOverloadedTy, mkTyConApp,
+import TcType          ( TcTyVar, TcTyVarSet, ThetaType, 
+                          mkClassPred, isOverloadedTy, mkTyConApp,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
                          tyVarsOfPred, tcEqType, pprPred )
 import Id              ( idType, mkUserLocal )
 import Var             ( TyVar )
-import Name            ( getOccName, getSrcLoc )
+import Name            ( Name, getOccName, getSrcLoc )
 import NameSet         ( NameSet, mkNameSet, elemNameSet )
 import Class           ( classBigSig, classKey )
 import FunDeps         ( oclose, grow, improve, pprEquationDoc )
 import PrelInfo                ( isNumericClass ) 
 import PrelNames       ( splitName, fstName, sndName, integerTyConName,
                          showClassKey, eqClassKey, ordClassKey )
-import Subst           ( mkTopTyVarSubst, substTheta, substTy )
+import Type            ( zipTopTvSubst, substTheta, substTy )
 import TysWiredIn      ( pairTyCon, doubleTy )
 import ErrUtils                ( Message )
+import BasicTypes      ( TopLevelFlag, isNotTopLevel )
 import VarSet
 import VarEnv          ( TidyEnv )
 import FiniteMap
@@ -508,6 +509,21 @@ you might not expect the addition to be done twice --- but it will if
 we follow the argument of Question 2 and generalise over ?y.
 
 
+Question 4: top level
+~~~~~~~~~~~~~~~~~~~~~
+At the top level, monomorhism makes no sense at all.
+
+    module Main where
+       main = let ?x = 5 in print foo
+
+       foo = woggle 3
+
+       woggle :: (?x :: Int) => Int -> Int
+       woggle y = ?x + y
+
+We definitely don't want (foo :: Int) with a top-level implicit parameter
+(?x::Int) becuase there is no way to bind it.  
+
 
 Possible choices
 ~~~~~~~~~~~~~~~~
@@ -651,7 +667,8 @@ inferLoop doc tau_tvs wanteds
          | isClassDict inst              = DontReduceUnlessConstant    -- Dicts
          | otherwise                     = ReduceMe                    -- Lits and Methods
     in
-    traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, ppr (grow preds tau_tvs'), ppr qtvs])     `thenM_`
+    traceTc (text "infloop" <+> vcat [ppr tau_tvs', ppr wanteds', ppr preds, 
+                                     ppr (grow preds tau_tvs'), ppr qtvs])     `thenM_`
                -- Step 2
     reduceContext doc try_me [] wanteds'    `thenM` \ (no_improvement, frees, binds, irreds) ->
 
@@ -765,7 +782,8 @@ tcSimplifyCheck doc qtvs givens wanted_lie
                 givens wanted_lie      `thenM` \ (qtvs', binds) ->
     returnM binds
   where
-    get_qtvs = zonkTcTyVarsAndFV qtvs
+--    get_qtvs = zonkTcTyVarsAndFV qtvs
+    get_qtvs = return (mkVarSet qtvs)
 
 
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
@@ -898,8 +916,8 @@ Plan B (cunning, used for a long time up to and including GHC 6.2)
   In the Step 1 this constraint might have been simplified, perhaps to
   (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
   This won't happen in Step 2... but that in turn might prevent some other
-  constraint mentioning 'b' from being simplified... and that in turn
-  breaks the invariant that no constraints are quantified over.
+  constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) 
+  and that in turn breaks the invariant that no constraints are quantified over.
 
   Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
   the problem.
@@ -912,11 +930,49 @@ Plan C (brutal)
   Return the bindings from Step 1.
   
 
+A note about Plan C (arising from "bug" reported by George Russel March 2004)
+Consider this:
+
+      instance (HasBinary ty IO) => HasCodedValue ty
+
+      foo :: HasCodedValue a => String -> IO a
+
+      doDecodeIO :: HasCodedValue a => () -> () -> IO a
+      doDecodeIO codedValue view  
+        = let { act = foo "foo" } in  act
+
+You might think this should work becuase the call to foo gives rise to a constraint
+(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO.  But the
+restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
+constraint using the (rather bogus) instance declaration, and now we are stuffed.
+
+I claim this is not really a bug -- but it bit Sergey as well as George.  So here's
+plan D
+
+
+Plan D (a variant of plan B)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem), BUT DO NO IMPROVEMENT.  Then set
+       qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
+
+  Step 2: Now simplify again, treating the constraint as 'free' if 
+  it does not mention qtvs, and trying to reduce it otherwise.
+
+  The point here is that it's generally OK to have too few qtvs; that is,
+  to make the thing more monomorphic than it could be.  We don't want to
+  do that in the common cases, but in wierd cases it's ok: the programmer
+  can always add a signature.  
+
+  Too few qtvs => too many wanteds, which is what happens if you do less
+  improvement.
+
 
 \begin{code}
 tcSimplifyRestricted   -- Used for restricted binding groups
                        -- i.e. ones subject to the monomorphism restriction
        :: SDoc
+       -> TopLevelFlag
+       -> [Name]               -- Things bound in this group
        -> TcTyVarSet           -- Free in the type of the RHSs
        -> [Inst]               -- Free in the RHSs
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
@@ -925,33 +981,70 @@ tcSimplifyRestricted      -- Used for restricted binding groups
        -- quantify over; by definition there are none.
        -- They are all thrown back in the LIE
 
-tcSimplifyRestricted doc tau_tvs wanteds
-       -- 'reduceMe': Reduce as far as we can.  Don't stop at
+tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
+       -- Zonk everything in sight
+  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
+    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
+    tcGetGlobalTyVars                          `thenM` \ gbl_tvs' ->
+
+       -- 'reduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
        -- variables as possible, and we don't want to stop
        -- at (say) Monad (ST s), because that reduces
        -- immediately, with no constraint on s.
-  = simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, binds, irreds) ->
-    ASSERT( null frees )
+       --
+       -- BUT do no improvement!  See Plan D above
+    reduceContextWithoutImprovement 
+       doc reduceMe wanteds'           `thenM` \ (_frees, _binds, constrained_dicts) ->
 
        -- Next, figure out the tyvars we will quantify over
-    zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
-    tcGetGlobalTyVars                          `thenM` \ gbl_tvs ->
     let
-       constrained_tvs = tyVarsOfInsts irreds
-       qtvs = (tau_tvs' `minusVarSet` constrained_tvs)
-                        `minusVarSet` oclose (fdPredsOfInsts irreds) gbl_tvs
-               -- The second minusVarSet arranges not to quantify over
-               -- any tyvars that are functionally determined by ones in
-               -- the environment
+       constrained_tvs = tyVarsOfInsts constrained_dicts
+       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs')
+                        `minusVarSet` constrained_tvs
     in
     traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts frees, pprInsts irreds,
-               pprLHsBinds binds,
+               pprInsts wanteds, pprInsts _frees, pprInsts constrained_dicts,
+               ppr _binds,
                ppr constrained_tvs, ppr tau_tvs', ppr qtvs ])  `thenM_`
 
-    extendLIEs irreds                                          `thenM_`
-    returnM (varSetElems qtvs, binds)
+       -- The first step may have squashed more methods than
+       -- necessary, so try again, this time more gently, knowing the exact
+       -- set of type variables to quantify over.
+       --
+       -- We quantify only over constraints that are captured by qtvs;
+       -- these will just be a subset of non-dicts.  This in contrast
+       -- to normal inference (using isFreeWhenInferring) in which we quantify over
+       -- all *non-inheritable* constraints too.  This implements choice
+       -- (B) under "implicit parameter and monomorphism" above.
+       --
+       -- Remember that we may need to do *some* simplification, to
+       -- (for example) squash {Monad (ST s)} into {}.  It's not enough
+       -- just to float all constraints
+       --
+       -- At top level, we *do* squash methods becuase we want to 
+       -- expose implicit parameters to the test that follows
+    let
+       is_nested_group = isNotTopLevel top_lvl
+        try_me inst | isFreeWrtTyVars qtvs inst,
+                     (is_nested_group || isDict inst) = Free
+                   | otherwise                        = ReduceMe
+    in
+    reduceContextWithoutImprovement 
+       doc try_me wanteds'             `thenM` \ (frees, binds, irreds) ->
+    ASSERT( null irreds )
+
+       -- See "Notes on implicit parameters, Question 4: top level"
+    if is_nested_group then
+       extendLIEs frees        `thenM_`
+        returnM (varSetElems qtvs, binds)
+    else
+       let
+           (non_ips, bad_ips) = partition isClassDict frees
+       in    
+       addTopIPErrs bndrs bad_ips      `thenM_`
+       extendLIEs non_ips              `thenM_`
+        returnM (varSetElems qtvs, binds)
 \end{code}
 
 
@@ -998,7 +1091,7 @@ because the scsel will mess up matching.  Instead we want
        forall dIntegralInt, dNumInt.
        fromIntegral Int Int dIntegralInt dNumInt = id Int
 
-Hence "DontReduce NoSCs"
+Hence "WithoutSCs"
 
 \begin{code}
 tcSimplifyToDicts :: [Inst] -> TcM (TcDictBinds)
@@ -1014,7 +1107,7 @@ tcSimplifyToDicts wanteds
     doc = text "tcSimplifyToDicts"
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
-    try_me inst        | isDict inst = DontReduce NoSCs        -- See notes above for why NoSCs
+    try_me inst        | isDict inst = KeepDictWithoutSCs      -- See notes above re "WithoutSCs"
                | otherwise   = ReduceMe
 \end{code}
 
@@ -1114,30 +1207,37 @@ For each method @Inst@ in the @init_lie@ that mentions one of the
 @LIE@), as well as the @HsBinds@ generated.
 
 \begin{code}
-bindInstsOfLocalFuns ::        [Inst] -> [TcId] -> TcM (LHsBinds TcId)
+bindInstsOfLocalFuns ::        [Inst] -> [TcId] -> TcM TcDictBinds
+-- Simlifies only MethodInsts, and generate only bindings of form 
+--     fm = f tys dicts
+-- We're careful not to even generate bindings of the form
+--     d1 = d2
+-- You'd think that'd be fine, but it interacts with what is
+-- arguably a bug in Match.tidyEqnInfo (see notes there)
 
 bindInstsOfLocalFuns wanteds local_ids
   | null overloaded_ids
        -- Common case
   = extendLIEs wanteds         `thenM_`
-    returnM emptyBag
+    returnM emptyLHsBinds
 
   | otherwise
-  = simpleReduceLoop doc try_me wanteds                `thenM` \ (frees, binds, irreds) ->
+  = simpleReduceLoop doc try_me for_me `thenM` \ (frees, binds, irreds) ->
     ASSERT( null irreds )
+    extendLIEs not_for_me      `thenM_`
     extendLIEs frees           `thenM_`
     returnM binds
   where
     doc                     = text "bindInsts" <+> ppr local_ids
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
+    (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
 
     overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
                                                -- so it's worth building a set, so that
                                                -- lookup (in isMethodFor) is faster
-
-    try_me inst | isMethodFor overloaded_set inst = ReduceMe
-               | otherwise                       = Free
+    try_me inst | isMethod inst = ReduceMe
+               | otherwise     = Free
 \end{code}
 
 
@@ -1158,7 +1258,8 @@ data WhatToDo
                        -- produce an error message of any kind.
                        -- It might be quite legitimate such as (Eq a)!
 
- | DontReduce WantSCs          -- Return as irreducible
+ | KeepDictWithoutSCs  -- Return as irreducible; don't add its superclasses
+                       -- Rather specialised: see notes with tcSimplifyToDicts
 
  | DontReduceUnlessConstant    -- Return as irreducible unless it can
                                -- be reduced to a constant in one step
@@ -1176,6 +1277,7 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
 
 \begin{code}
 type Avails = FiniteMap Inst Avail
+emptyAvails = emptyFM
 
 data Avail
   = IsFree             -- Used for free Insts
@@ -1416,7 +1518,7 @@ reduceContext doc try_me givens wanteds
             ]))                                        `thenM_`
 
         -- Build the Avail mapping from "givens"
-    foldlM addGiven emptyFM givens                     `thenM` \ init_state ->
+    foldlM addGiven emptyAvails givens                 `thenM` \ init_state ->
 
         -- Do the real work
     reduceList (0,[]) try_me wanteds init_state                `thenM` \ avails ->
@@ -1441,23 +1543,60 @@ reduceContext doc try_me givens wanteds
 
     returnM (no_improvement, frees, binds, irreds)
 
+-- reduceContextWithoutImprovement differs from reduceContext
+--     (a) no improvement
+--     (b) 'givens' is assumed empty
+reduceContextWithoutImprovement doc try_me wanteds
+  =
+    traceTc (text "reduceContextWithoutImprovement" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----------------------"
+            ]))                                        `thenM_`
+
+        -- Do the real work
+    reduceList (0,[]) try_me wanteds emptyAvails       `thenM` \ avails ->
+    extractResults avails wanteds                      `thenM` \ (binds, irreds, frees) ->
+
+    traceTc (text "reduceContextWithoutImprovement end" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "wanted" <+> ppr wanteds,
+            text "----",
+            text "avails" <+> pprAvails avails,
+            text "frees" <+> ppr frees,
+            text "----------------------"
+            ]))                                        `thenM_`
+
+    returnM (frees, binds, irreds)
+
 tcImprove :: Avails -> TcM Bool                -- False <=> no change
 -- Perform improvement using all the predicates in Avails
 tcImprove avails
- =  tcGetInstEnvs                      `thenM` \ (home_ie, pkg_ie) ->
+ =  tcGetInstEnvs                      `thenM` \ inst_envs -> 
     let
        preds = [ (pred, pp_loc)
-               | inst <- keysFM avails,
-                 let pp_loc = pprInstLoc (instLoc inst),
-                 pred <- fdPredsOfInst inst
+               | (inst, avail) <- fmToList avails,
+                 pred <- get_preds inst avail,
+                 let pp_loc = pprInstLoc (instLoc inst)
                ]
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
                -- NB that (?x::t1) and (?x::t2) will be held separately in avails
                --    so that improve will see them separate
+
+       -- For free Methods, we want to take predicates from their context,
+       -- but for Methods that have been squished their context will already
+       -- be in Avails, and we don't want duplicates.  Hence this rather
+       -- horrid get_preds function
+       get_preds inst IsFree = fdPredsOfInst inst
+       get_preds inst other | isDict inst = [dictPred inst]
+                            | otherwise   = []
+
        eqns = improve get_insts preds
-       get_insts clas = classInstEnv home_ie clas ++ classInstEnv pkg_ie clas
+       get_insts clas = classInstances inst_envs clas
      in
      if null eqns then
        returnM True
@@ -1466,10 +1605,11 @@ tcImprove avails
         mappM_ unify eqns      `thenM_`
        returnM False
   where
-    unify ((qtvs, t1, t2), doc)
-        = addErrCtxt doc                               $
-          tcInstTyVars VanillaTv (varSetElems qtvs)    `thenM` \ (_, _, tenv) ->
-          unifyTauTy (substTy tenv t1) (substTy tenv t2)
+    unify ((qtvs, pairs), doc)
+        = addErrCtxt doc                       $
+          tcInstTyVars (varSetElems qtvs)      `thenM` \ (_, _, tenv) ->
+          mapM_ (unif_pr tenv) pairs
+    unif_pr tenv (ty1,ty2) =  unifyTauTy (substTy tenv ty1) (substTy tenv ty2)
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -1509,7 +1649,8 @@ reduceList (n,stack) try_me wanteds state
   =
 #ifdef DEBUG
    (if n > 8 then
-       pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
+       pprTrace "Interesting! Context reduction stack deeper than 8:" 
+                (nest 2 (pprStack stack))
     else (\x->x))
 #endif
     go wanteds state
@@ -1531,7 +1672,7 @@ reduce stack try_me wanted avails
   | otherwise
   = case try_me wanted of {
 
-      DontReduce want_scs -> addIrred want_scs avails wanted
+      KeepDictWithoutSCs -> addIrred NoSCs avails wanted
 
     ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
                                     -- First, see if the inst can be reduced to a constant in one step
@@ -1648,7 +1789,7 @@ addAvailAndSCs avails inst avail
     avails1     = addToFM avails inst avail
     is_loop inst = any (`tcEqType` idType (instToId inst)) dep_tys
                        -- Note: this compares by *type*, not by Unique
-    deps         = findAllDeps emptyVarSet avail
+    deps         = findAllDeps (unitVarSet (instToId inst)) avail
     dep_tys     = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> Avail -> IdSet
@@ -1656,12 +1797,17 @@ addAvailAndSCs avails inst avail
     -- See Note [SUPERCLASS-LOOP]
     -- Watch out, though.  Since the avails may contain loops 
     -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
-    findAllDeps so_far (Rhs _ kids) 
-      = foldl findAllDeps
-             (extendVarSetList so_far (map instToId kids))     -- Add the kids to so_far
-              [a | Just a <- map (lookupFM avails) kids]       -- Find the kids' Avail
-    findAllDeps so_far other = so_far
-
+    findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
+    findAllDeps so_far other       = so_far
+
+    find_all :: IdSet -> Inst -> IdSet
+    find_all so_far kid
+      | kid_id `elemVarSet` so_far       = so_far
+      | Just avail <- lookupFM avails kid = findAllDeps so_far' avail
+      | otherwise                        = so_far'
+      where
+       so_far' = extendVarSet so_far kid_id    -- Add the new kid to so_far
+       kid_id = instToId kid
 
 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to Avails
@@ -1675,7 +1821,7 @@ addSCs is_loop avails dict
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
+    sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
 
     add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
       | add_me sc_dict = addSCs is_loop avails' sc_dict
@@ -1698,11 +1844,11 @@ We have to be careful here.  If we are *given* d1:Ord a,
 and want to deduce (d2:C [a]) where
 
        class Ord a => C a where
-       instance Ord a => C [a] where ...
+       instance Ord [a] => C [a] where ...
 
-Then we'll use the instance decl to deduce C [a] and then add the
+Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
 superclasses of C [a] to avails.  But we must not overwrite the binding
-for d1:Ord a (which is given) with a superclass selection or we'll just
+for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
 build a loop! 
 
 Here's another variant, immortalised in tcrun020
@@ -1819,20 +1965,23 @@ tc_simplify_top is_interactive wanteds
        non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
 
                -- Collect together all the bad guys
-       bad_guys               = non_stds ++ concat std_bads
-       (bad_ips, non_ips)     = partition isIPDict bad_guys
-       (no_insts, ambigs)     = partition no_inst non_ips
-       no_inst d              = not (isTyVarDict d) 
-       -- Previously, there was a more elaborate no_inst definition:
-       --      no_inst d = not (isTyVarDict d) || tyVarsOfInst d `subVarSet` fixed_tvs
-       --      fixed_tvs = oclose (fdPredsOfInsts tidy_dicts) emptyVarSet
-       -- But that seems over-elaborate to me; it only bites for class decls with
-       -- fundeps like this:           class C a b | -> b where ...
+       bad_guys           = non_stds ++ concat std_bads
+       (non_ips, bad_ips) = partition isClassDict bad_guys
+       (ambigs, no_insts) = partition is_ambig non_ips
+       is_ambig d         = not (tyVarsOfInst d `subVarSet` fixed_tvs)
+       fixed_tvs          = oclose (fdPredsOfInsts irreds) emptyVarSet
+       -- If the dict has free type variables, it's almost certainly ambiguous,
+       -- and that's the first thing to fix.  
+       -- Otherwise, addNoInstanceErrs does the right thing
+       -- I say "almost certain" because we might have
+       --       class C a b | a -> B where ...
+       -- plus an Inst (C Int x).  Then the 'x' isn't ambiguous; it's just that
+       -- there's no instance decl for (C Int ...).  Hence the oclose.
     in
 
        -- Report definite errors
     groupErrs (addNoInstanceErrs Nothing []) no_insts  `thenM_`
-    addTopIPErrs bad_ips                               `thenM_`
+    strangeTopIPErrs bad_ips                           `thenM_`
 
        -- Deal with ambiguity errors, but only if
        -- if there has not been an error so far; errors often
@@ -2019,11 +2168,11 @@ tcSimplifyDeriv :: [TyVar]
                -> TcM ThetaType        -- Needed
 
 tcSimplifyDeriv tyvars theta
-  = tcInstTyVars VanillaTv tyvars                      `thenM` \ (tvs, _, tenv) ->
+  = tcInstTyVars tyvars                        `thenM` \ (tvs, _, tenv) ->
        -- The main loop may do unification, and that may crash if 
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?
-    newDicts DataDeclOrigin (substTheta tenv theta)    `thenM` \ wanteds ->
+    newDicts DerivOrigin (substTheta tenv theta)       `thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds              `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )                       -- reduceMe never returns Free
 
@@ -2055,7 +2204,7 @@ tcSimplifyDeriv tyvars theta
          -- of problems; in particular, it's hard to compare solutions for
          -- equality when finding the fixpoint.  So I just rule it out for now.
   
-       rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
+       rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars
     in
@@ -2077,7 +2226,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
                  -> TcM ()
 
 tcSimplifyDefault theta
-  = newDicts DataDeclOrigin theta              `thenM` \ wanteds ->
+  = newDicts DefaultOrigin theta               `thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )       -- try_me never returns Free
     addNoInstanceErrs Nothing []  irreds       `thenM_`
@@ -2130,7 +2279,21 @@ addInstLoc insts msg = msg $$ nest 2 (pprInstLoc (instLoc (head insts)))
 plural [x] = empty
 plural xs  = char 's'
 
-addTopIPErrs dicts
+addTopIPErrs :: [Name] -> [Inst] -> TcM ()
+addTopIPErrs bndrs [] 
+  = return ()
+addTopIPErrs bndrs ips
+  = addErrTcM (tidy_env, mk_msg tidy_ips)
+  where
+    (tidy_env, tidy_ips) = tidyInsts ips
+    mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from the monomorphic top-level binding(s) of"),
+                           pprBinders bndrs <> colon],
+                      nest 2 (vcat (map ppr_ip ips)),
+                      monomorphism_fix]
+    ppr_ip ip = pprPred (dictPred ip) <+> pprInstLoc (instLoc ip)
+
+strangeTopIPErrs :: [Inst] -> TcM ()
+strangeTopIPErrs dicts -- Strange, becuase addTopIPErrs should have caught them all
   = groupErrs report tidy_dicts
   where
     (tidy_env, tidy_dicts) = tidyInsts dicts
@@ -2148,7 +2311,6 @@ addNoInstanceErrs mb_what givens []
 addNoInstanceErrs mb_what givens dicts
   =    -- Some of the dicts are here because there is no instances
        -- and some because there are too many instances (overlap)
-       -- The first thing we do is separate them
     getDOpts           `thenM` \ dflags ->
     tcGetInstEnvs      `thenM` \ inst_envs ->
     let
@@ -2163,19 +2325,20 @@ addNoInstanceErrs mb_what givens dicts
          | not (isClassDict dict) = (overlap_doc, dict : no_inst_dicts)
          | otherwise
          = case lookupInstEnv dflags inst_envs clas tys of
-               res@(ms, _) 
-                 | length ms > 1 -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
-                 | otherwise     -> (overlap_doc, dict : no_inst_dicts)        -- No match
-               -- NB: there can be exactly one match, in the case where we have
-               --      instance C a where ...
-               -- (In this case, lookupInst doesn't bother to look up, 
-               --  unless -fallow-undecidable-instances is set.)
-               -- So we report this as "no instance" rather than "overlap"; the fix is
-               -- to specify -fallow-undecidable-instances, but we leave that to the programmer!
+               -- The case of exactly one match and no unifiers means
+               -- a successful lookup.  That can't happen here, becuase
+               -- dicts only end up here if they didn't match in Inst.lookupInst
+#ifdef DEBUG
+               ([m],[]) -> pprPanic "addNoInstanceErrs" (ppr dict)
+#endif
+               ([], _)  -> (overlap_doc, dict : no_inst_dicts)         -- No match
+               res      -> (mk_overlap_msg dict res $$ overlap_doc, no_inst_dicts)
          where
            (clas,tys) = getDictClassTys dict
     in
-    mk_probable_fix tidy_env2 mb_what no_inst_dicts    `thenM` \ (tidy_env3, probable_fix) ->
+       
+       -- Now generate a good message for the no-instance bunch
+    mk_probable_fix tidy_env2 no_inst_dicts    `thenM` \ (tidy_env3, probable_fix) ->
     let
        no_inst_doc | null no_inst_dicts = empty
                    | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
@@ -2184,36 +2347,46 @@ addNoInstanceErrs mb_what givens dicts
                | otherwise   = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
                                     nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
     in
+       -- And emit both the non-instance and overlap messages
     addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
   where
     mk_overlap_msg dict (matches, unifiers)
       = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
                                        <+> pprPred (dictPred dict))),
                sep [ptext SLIT("Matching instances") <> colon,
-                    nest 2 (pprDFuns (dfuns ++ unifiers))],
-               if null unifiers 
-               then empty
-               else parens (ptext SLIT("The choice depends on the instantiation of") <+>
-                            quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))))]
+                    nest 2 (vcat [pprDFuns dfuns, pprDFuns unifiers])],
+               ASSERT( not (null matches) )
+               if not (isSingleton matches)
+               then    -- Two or more matches
+                    empty
+               else    -- One match, plus some unifiers
+               ASSERT( not (null unifiers) )
+               parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
+                                quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
+                             ptext SLIT("Use -fallow-incoherent-instances to use the first choice above")])]
       where
        dfuns = [df | (_, (_,_,df)) <- matches]
 
-    mk_probable_fix tidy_env Nothing dicts     -- Top level
-      = mkMonomorphismMsg tidy_env dicts
-    mk_probable_fix tidy_env (Just what) dicts -- Nested (type signatures, instance decls)
-      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 fix1, nest 2 fix2])
+    mk_probable_fix tidy_env dicts     
+      = returnM (tidy_env, sep [ptext SLIT("Probable fix:"), nest 2 (vcat fixes)])
       where
-       fix1 = sep [ptext SLIT("Add") <+> pprDictsTheta dicts,
-                   ptext SLIT("to the") <+> what]
+       fixes = add_ors (fix1 ++ fix2)
 
-       fix2 | null instance_dicts = empty
-            | otherwise           = ptext SLIT("Or add an instance declaration for")
-                                    <+> pprDictsTheta instance_dicts
+       fix1 = case mb_what of
+                Nothing   -> []        -- Top level
+                Just what -> -- Nested (type signatures, instance decls)
+                             [ sep [ ptext SLIT("add") <+> pprDictsTheta dicts,
+                               ptext SLIT("to the") <+> what] ]
+
+       fix2 | null instance_dicts = []
+            | otherwise           = [ ptext SLIT("add an instance declaration for")
+                                      <+> pprDictsTheta instance_dicts ]
        instance_dicts = [d | d <- dicts, isClassDict d, not (isTyVarDict d)]
                -- Insts for which it is worth suggesting an adding an instance declaration
                -- Exclude implicit parameters, and tyvar dicts
 
+       add_ors :: [SDoc] -> [SDoc]
+       add_ors (f1:fs) = f1 : map (ptext SLIT("or") <+>) fs
 
 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
@@ -2227,40 +2400,39 @@ addTopAmbigErrs dicts
     
     report :: [(Inst,[TcTyVar])] -> TcM ()
     report pairs@((inst,tvs) : _)      -- The pairs share a common set of ambiguous tyvars
-       = mkMonomorphismMsg tidy_env dicts      `thenM` \ (tidy_env, mono_msg) ->
-         addSrcSpan (instLocSrcSpan (instLoc inst)) $
+       = mkMonomorphismMsg tidy_env tvs        `thenM` \ (tidy_env, mono_msg) ->
+         setSrcSpan (instLocSrcSpan (instLoc inst)) $
                -- the location of the first one will do for the err message
          addErrTcM (tidy_env, msg $$ mono_msg)
        where
          dicts = map fst pairs
          msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
-                            pprQuotedList tvs <+> in_msg,
+                         pprQuotedList tvs <+> in_msg,
                     nest 2 (pprDictsInFull dicts)]
-         in_msg | isSingleton dicts = text "in the top-level constraint:"
-                | otherwise         = text "in these top-level constraints:"
+         in_msg = text "in the constraint" <> plural dicts <> colon
 
 
-mkMonomorphismMsg :: TidyEnv -> [Inst] -> TcM (TidyEnv, Message)
+mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
 -- There's an error with these Insts; if they have free type variables
 -- it's probably caused by the monomorphism restriction. 
 -- Try to identify the offending variable
 -- ASSUMPTION: the Insts are fully zonked
-mkMonomorphismMsg tidy_env insts
-  | isEmptyVarSet inst_tvs
-  = returnM (tidy_env, empty)
-  | otherwise
-  = findGlobals inst_tvs tidy_env      `thenM` \ (tidy_env, docs) ->
+mkMonomorphismMsg tidy_env inst_tvs
+  = findGlobals (mkVarSet inst_tvs) tidy_env   `thenM` \ (tidy_env, docs) ->
     returnM (tidy_env, mk_msg docs)
-
   where
-    inst_tvs = tyVarsOfInsts insts
-
-    mk_msg []   = empty                -- This happens in things like
-                               --      f x = show (read "foo")
-                               -- whre monomorphism doesn't play any role
+    mk_msg []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+                       -- This happens in things like
+                       --      f x = show (read "foo")
+                       -- whre monomorphism doesn't play any role
     mk_msg docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
                        nest 2 (vcat docs),
-                       ptext SLIT("Probable fix: give these definition(s) an explicit type signature")]
+                       monomorphism_fix
+                      ]
+monomorphism_fix :: SDoc
+monomorphism_fix = ptext SLIT("Probable fix:") <+> 
+                  (ptext SLIT("give these definition(s) an explicit type signature")
+                   $$ ptext SLIT("or use -fno-monomorphism-restriction"))
     
 warnDefault dicts default_ty
   = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
@@ -2281,7 +2453,7 @@ badDerivedPred pred
 reduceDepthErr n stack
   = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
          ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
-         nest 4 (pprDictsInFull stack)]
+         nest 4 (pprStack stack)]
 
-reduceDepthMsg n stack = nest 4 (pprDictsInFull stack)
+pprStack stack = vcat (map pprInstInFull stack)
 \end{code}