[project @ 2000-10-24 10:36:08 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 5053862..5d430e6 100644 (file)
@@ -116,14 +116,13 @@ and hence the default mechanism would resolve the "a".
 
 \begin{code}
 module TcSimplify (
-       tcSimplify, tcSimplifyAndCheck, tcSimplifyRuleLhs, 
+       tcSimplify, tcSimplifyAndCheck, tcSimplifyToDicts, 
        tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas,
-       bindInstsOfLocalFuns
+       bindInstsOfLocalFuns, partitionPredsOfLIE
     ) where
 
 #include "HsVersions.h"
 
-import CmdLineOpts     ( opt_MaxContextReductionDepth, opt_GlasgowExts, opt_WarnTypeDefaults )
 import HsSyn           ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
 import TcHsSyn         ( TcExpr, TcId, 
                          TcMonoBinds, TcDictBinds
@@ -132,36 +131,42 @@ import TcHsSyn            ( TcExpr, TcId,
 import TcMonad
 import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
                          tyVarsOfInst, 
-                         isDict, isStdClassTyVarDict, isMethodFor,
+                         isDict, isClassDict, isMethod, notFunDep,
+                         isStdClassTyVarDict, isMethodFor,
                          instToId, instBindingRequired, instCanBeGeneralised,
-                         newDictFromOld,
-                         instLoc, getDictClassTys,
-                         pprInst, zonkInst, tidyInst, tidyInsts,
-                         Inst, LIE, pprInsts, pprInstsInFull, mkLIE, emptyLIE, 
-                         plusLIE, pprOrigin
+                         newDictFromOld, newFunDepFromDict,
+                         getDictClassTys, getIPs, isTyVarDict,
+                         getDictPred_maybe, getMethodTheta_maybe,
+                         instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
+                         Inst, LIE, pprInsts, pprInstsInFull,
+                         mkLIE, emptyLIE, unitLIE, consLIE, plusLIE,
+                         lieToList 
                        )
-import TcEnv           ( tcGetGlobalTyVars )
-import TcType          ( TcType, TcTyVarSet, typeToTcType )
+import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
+import InstEnv         ( lookupInstEnv, InstLookupResult(..) )
+
+import TcType          ( TcTyVarSet )
 import TcUnify         ( unifyTauTy )
 import Id              ( idType )
-import Bag             ( bagToList )
-import Class           ( Class, classBigSig, classInstEnv )
+import Class           ( Class, classBigSig )
 import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
 
-import Type            ( Type, ThetaType, TauType, mkTyVarTy, getTyVar,
+import Type            ( Type, ClassContext,
+                         mkTyVarTy, getTyVar,
                          isTyVarTy, splitSigmaTy, tyVarsOfTypes
                        )
-import InstEnv         ( InstEnv )
-import Subst           ( mkTopTyVarSubst, substTheta )
+import Subst           ( mkTopTyVarSubst, substClasses )
 import PprType         ( pprConstraint )
 import TysWiredIn      ( unitTy )
 import VarSet
 import FiniteMap
-import BasicTypes      ( TopLevelFlag(..) )
-import CmdLineOpts     ( opt_GlasgowExts )
 import Outputable
-import Util
+import ListSetOps      ( equivClasses )
+import Util            ( zipEqual, mapAccumL )
 import List            ( partition )
+import Maybe           ( fromJust )
+import Maybes          ( maybeToBool )
+import CmdLineOpts
 \end{code}
 
 
@@ -181,19 +186,21 @@ float them out if poss, after inlinings are sorted out.
 \begin{code}
 tcSimplify
        :: SDoc 
-       -> TopLevelFlag
        -> TcTyVarSet                   -- ``Local''  type variables
                                        -- ASSERT: this tyvar set is already zonked
        -> LIE                          -- Wanted
-       -> TcM s (LIE,                  -- Free
+       -> TcM (LIE,                    -- Free
                  TcDictBinds,          -- Bindings
                  LIE)                  -- Remaining wanteds; no dups
 
-tcSimplify str top_lvl local_tvs wanted_lie
+tcSimplify str local_tvs wanted_lie
+{- this is just an optimization, and interferes with implicit params,
+   disable it for now.  same goes for tcSimplifyAndCheck
   | isEmptyVarSet local_tvs
   = returnTc (wanted_lie, EmptyMonoBinds, emptyLIE)
 
   | otherwise
+-}
   = reduceContext str try_me [] wanteds                `thenTc` \ (binds, frees, irreds) ->
 
        -- Check for non-generalisable insts
@@ -225,11 +232,12 @@ tcSimplify str top_lvl local_tvs wanted_lie
        -- Finished
     returnTc (mkLIE frees, binds, mkLIE irreds')
   where
-    wanteds = bagToList wanted_lie
+    wanteds = lieToList wanted_lie
 
     try_me inst 
       -- Does not constrain a local tyvar
       | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
+        && null (getIPs inst)
       = -- if is_top_level then
        --   FreeIfTautological           -- Special case for inference on 
        --                                -- top-level defns
@@ -238,8 +246,8 @@ tcSimplify str top_lvl local_tvs wanted_lie
 
       -- We're infering (not checking) the type, and 
       -- the inst constrains a local type variable
-      | isDict inst  = DontReduce              -- Dicts
-      | otherwise    = ReduceMe AddToIrreds    -- Lits and Methods
+      | isClassDict inst = DontReduceUnlessConstant    -- Dicts
+      | otherwise       = ReduceMe AddToIrreds         -- Lits and Methods
 \end{code}
 
 @tcSimplifyAndCheck@ is similar to the above, except that it checks
@@ -253,16 +261,18 @@ tcSimplifyAndCheck
                                -- ASSERT: this tyvar set is already zonked
         -> LIE                 -- Given; constrain only local tyvars
         -> LIE                 -- Wanted
-        -> TcM s (LIE,         -- Free
+        -> TcM (LIE,           -- Free
                   TcDictBinds) -- Bindings
 
 tcSimplifyAndCheck str local_tvs given_lie wanted_lie
+{-
   | isEmptyVarSet local_tvs
        -- This can happen quite legitimately; for example in
        --      instance Num Int where ...
   = returnTc (wanted_lie, EmptyMonoBinds)
 
   | otherwise
+-}
   = reduceContext str try_me givens wanteds    `thenTc` \ (binds, frees, irreds) ->
 
        -- Complain about any irreducible ones
@@ -271,13 +281,14 @@ tcSimplifyAndCheck str local_tvs given_lie wanted_lie
        -- Done
     returnTc (mkLIE frees, binds)
   where
-    givens  = bagToList given_lie
-    wanteds = bagToList wanted_lie
-    given_dicts = filter isDict givens
+    givens  = lieToList given_lie
+    wanteds = lieToList wanted_lie
+    given_dicts = filter isClassDict givens
 
     try_me inst 
       -- Does not constrain a local tyvar
       | isEmptyVarSet (tyVarsOfInst inst `intersectVarSet` local_tvs)
+        && (not (isMethod inst) || null (getIPs inst))
       = Free
 
       -- When checking against a given signature we always reduce
@@ -293,20 +304,80 @@ On the LHS of transformation rules we only simplify methods and constants,
 getting dictionaries.  We want to keep all of them unsimplified, to serve
 as the available stuff for the RHS of the rule.
 
+The same thing is used for specialise pragmas. Consider
+       
+       f :: Num a => a -> a
+       {-# SPECIALISE f :: Int -> Int #-}
+       f = ...
+
+The type checker generates a binding like:
+
+       f_spec = (f :: Int -> Int)
+
+and we want to end up with
+
+       f_spec = _inline_me_ (f Int dNumInt)
+
+But that means that we must simplify the Method for f to (f Int dNumInt)! 
+So tcSimplifyToDicts squeezes out all Methods.
+
 \begin{code}
-tcSimplifyRuleLhs :: LIE -> TcM s (LIE, TcDictBinds)
-tcSimplifyRuleLhs wanted_lie
-  = reduceContext (text "tcSimplRuleLhs") try_me [] wanteds    `thenTc` \ (binds, frees, irreds) ->
+tcSimplifyToDicts :: LIE -> TcM (LIE, TcDictBinds)
+tcSimplifyToDicts wanted_lie
+  = reduceContext (text "tcSimplifyToDicts") try_me [] wanteds `thenTc` \ (binds, frees, irreds) ->
     ASSERT( null frees )
     returnTc (mkLIE irreds, binds)
   where
-    wanteds    = bagToList wanted_lie
+    wanteds = lieToList wanted_lie
 
        -- Reduce methods and lits only; stop as soon as we get a dictionary
     try_me inst        | isDict inst = DontReduce
                | otherwise   = ReduceMe AddToIrreds
 \end{code}
 
+The following function partitions a LIE by a predicate defined
+over `Pred'icates (an unfortunate overloading of terminology!).
+This means it sometimes has to split up `Methods', in which case
+a binding is generated.
+
+It is used in `with' bindings to extract from the LIE the implicit
+parameters being bound.
+
+\begin{code}
+partitionPredsOfLIE pred lie
+  = foldlTc (partPreds pred) (emptyLIE, emptyLIE, EmptyMonoBinds) insts
+  where insts = lieToList lie
+
+-- warning: the term `pred' is overloaded here!
+partPreds pred (lie1, lie2, binds) inst
+  | maybeToBool maybe_pred
+  = if pred p then
+       returnTc (consLIE inst lie1, lie2, binds)
+    else
+       returnTc (lie1, consLIE inst lie2, binds)
+    where maybe_pred = getDictPred_maybe inst
+         Just p = maybe_pred
+
+-- the assumption is that those satisfying `pred' are being extracted,
+-- so we leave the method untouched when nothing satisfies `pred'
+partPreds pred (lie1, lie2, binds1) inst
+  | maybeToBool maybe_theta
+  = if any pred theta then
+       zonkInst inst                           `thenTc` \ inst' ->
+       tcSimplifyToDicts (unitLIE inst')       `thenTc` \ (lie3, binds2) ->
+       partitionPredsOfLIE pred lie3           `thenTc` \ (lie1', lie2', EmptyMonoBinds) ->
+       returnTc (lie1 `plusLIE` lie1',
+                 lie2 `plusLIE` lie2',
+                 binds1 `AndMonoBinds` binds2)
+    else
+       returnTc (lie1, consLIE inst lie2, binds1)
+    where maybe_theta = getMethodTheta_maybe inst
+         Just theta = maybe_theta
+
+partPreds pred (lie1, lie2, binds) inst
+  = returnTc (lie1, consLIE inst lie2, binds)
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -321,7 +392,10 @@ data WhatToDo
  = ReduceMe              -- Try to reduce this
        NoInstanceAction  -- What to do if there's no such instance
 
- | DontReduce            -- Return as irreducible
+ | DontReduce                  -- Return as irreducible 
+
+ | DontReduceUnlessConstant    -- Return as irreducible unless it can
+                               -- be reduced to a constant in one step
 
  | Free                          -- Return as free
 
@@ -398,10 +472,13 @@ data RHS
                        -- Invariant: these Insts are already in the finite mapping
 
 
-pprAvails avails = vcat (map pp (eltsFM avails))
-  where
-    pp (Avail main_id rhs ids)
-      = ppr main_id <> colon <+> brackets (ppr ids) <+> pprRhs rhs
+pprAvails avails = vcat (map pprAvail (eltsFM avails))
+
+pprAvail (Avail main_id rhs ids)
+  = ppr main_id <> colon <+> brackets (ppr ids) <+> pprRhs rhs
+
+instance Outputable Avail where
+    ppr = pprAvail
 
 pprRhs NoRhs = text "<no rhs>"
 pprRhs (Rhs rhs b) = ppr rhs
@@ -421,7 +498,7 @@ The main entry point for context reduction is @reduceContext@:
 reduceContext :: SDoc -> (Inst -> WhatToDo)
              -> [Inst] -- Given
              -> [Inst] -- Wanted
-             -> TcM s (TcDictBinds, 
+             -> TcM (TcDictBinds, 
                        [Inst],         -- Free
                        [Inst])         -- Irreducible
 
@@ -429,6 +506,11 @@ reduceContext str try_me givens wanteds
   =     -- Zonking first
     mapNF_Tc zonkInst givens   `thenNF_Tc` \ givens ->
     mapNF_Tc zonkInst wanteds  `thenNF_Tc` \ wanteds ->
+    -- JRL - process fundeps last.  We eliminate fundeps by seeing
+    -- what available classes generate them, so we need to process the
+    -- classes first. (would it be useful to make LIEs ordered in the first place?)
+    let (wantedOther, wantedFds) = partition notFunDep wanteds
+       wanteds'                 = wantedOther ++ wantedFds in
 
 {-
     pprTrace "reduceContext" (vcat [
@@ -440,10 +522,10 @@ reduceContext str try_me givens wanteds
             ]) $
 -}
         -- Build the Avail mapping from "givens"
-    foldlNF_Tc addGiven emptyFM givens         `thenNF_Tc` \ avails ->
+    foldlNF_Tc addGiven emptyFM givens                 `thenNF_Tc` \ avails ->
 
         -- Do the real work
-    reduceList (0,[]) try_me wanteds (avails, [], [])  `thenTc` \ (avails, frees, irreds) ->
+    reduceList (0,[]) try_me wanteds' (avails, [], []) `thenNF_Tc` \ (avails, frees, irreds) ->
 
        -- Extract the bindings from avails
     let
@@ -470,11 +552,12 @@ reduceContext str try_me givens wanteds
             text "wanted" <+> ppr wanteds,
             text "----", 
             text "avails" <+> pprAvails avails,
+            text "frees" <+> ppr frees,
             text "irreds" <+> ppr irreds,
             text "----------------------"
             ]) $
 -}
-    returnTc (binds, frees, irreds)
+    returnNF_Tc (binds, frees, irreds)
 \end{code}
 
 The main context-reduction function is @reduce@.  Here's its game plan.
@@ -485,7 +568,7 @@ reduceList :: (Int,[Inst])          -- Stack (for err msgs)
                   -> (Inst -> WhatToDo)
                   -> [Inst]
                   -> RedState s
-                  -> TcM s (RedState s)
+                  -> TcM (RedState s)
 \end{code}
 
 @reduce@ is passed
@@ -564,7 +647,11 @@ reduce stack try_me wanted state@(avails, frees, irreds)
 
 
     ;
-    DontReduce ->    -- It's irreducible (or at least should not be reduced)
+
+    DontReduce -> add_to_irreds
+    ;
+
+    DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
         -- See if the inst can be reduced to a constant in one step
        lookupInst wanted         `thenNF_Tc` \ lookup_result ->
        case lookup_result of
@@ -622,7 +709,7 @@ activate avails wanted
     
 addWanted avails wanted rhs_expr
   = ASSERT( not (wanted `elemFM` avails) )
-    returnNF_Tc (addToFM avails wanted avail)
+    addFunDeps (addToFM avails wanted avail) wanted
        -- NB: we don't add the thing's superclasses too!
        -- Why not?  Because addWanted is used when we've successfully used an
        -- instance decl to reduce something; e.g.
@@ -667,34 +754,37 @@ addFree avails free
   | isDict free = addToFM avails free (Avail (instToId free) NoRhs [])
   | otherwise   = avails
 
-addGiven :: Avails s -> Inst -> NF_TcM s (Avails s)
+addGiven :: Avails s -> Inst -> NF_TcM (Avails s)
 addGiven avails given
   =     -- ASSERT( not (given `elemFM` avails) )
         -- This assertion isn't necessarily true.  It's permitted
         -- to given a redundant context in a type signature (eg (Ord a, Eq a) => ...)
         -- and when typechecking instance decls we generate redundant "givens" too.
-    addAvail avails given avail
+    -- addAvail avails given avail
+    addAvail avails given avail `thenNF_Tc` \av ->
+    zonkInst given `thenNF_Tc` \given' ->
+    returnNF_Tc av     
   where
     avail = Avail (instToId given) NoRhs []
 
 addAvail avails wanted avail
   = addSuperClasses (addToFM avails wanted avail) wanted
 
-addSuperClasses :: Avails s -> Inst -> NF_TcM s (Avails s)
+addSuperClasses :: Avails s -> Inst -> NF_TcM (Avails s)
                -- Add all the superclasses of the Inst to Avails
                -- Invariant: the Inst is already in Avails.
 
 addSuperClasses avails dict
-  | not (isDict dict)
+  | not (isClassDict dict)
   = returnNF_Tc avails
 
   | otherwise  -- It is a dictionary
-  = foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_theta' sc_sels)
+  = foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_theta' sc_sels) `thenNF_Tc` \ avails' ->
+    addFunDeps avails' dict
   where
     (clas, tys) = getDictClassTys dict
-    
-    (tyvars, sc_theta, sc_sels, _, _) = classBigSig clas
-    sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
+    (tyvars, sc_theta, sc_sels, _) = classBigSig clas
+    sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
 
     add_sc avails ((super_clas, super_tys), sc_sel)
       = newDictFromOld dict super_clas super_tys       `thenNF_Tc` \ super_dict ->
@@ -725,6 +815,16 @@ addSuperClasses avails dict
                  avail   = Avail (instToId super_dict) 
                                  (PassiveScSel sc_sel_rhs [dict])
                                  []
+
+addFunDeps :: Avails s -> Inst -> NF_TcM (Avails s)
+          -- Add in the functional dependencies generated by the inst
+addFunDeps avails inst
+  = newFunDepFromDict inst     `thenNF_Tc` \ fdInst_maybe ->
+    case fdInst_maybe of
+      Nothing -> returnNF_Tc avails
+      Just fdInst ->
+       let fdAvail = Avail (instToId (fromJust fdInst_maybe)) NoRhs [] in
+        addAvail avails fdInst fdAvail
 \end{code}
 
 %************************************************************************
@@ -744,22 +844,22 @@ a,b,c are type variables.  This is required for the context of
 instance declarations.
 
 \begin{code}
-tcSimplifyThetas :: (Class -> InstEnv)         -- How to find the InstEnv
-                -> ThetaType                   -- Wanted
-                -> TcM s ThetaType             -- Needed
+tcSimplifyThetas :: ClassContext               -- Wanted
+                -> TcM ClassContext            -- Needed
 
-tcSimplifyThetas inst_mapper wanteds
-  = reduceSimple inst_mapper [] wanteds                `thenNF_Tc` \ irreds ->
+tcSimplifyThetas wanteds
+  = doptsTc Opt_GlasgowExts            `thenNF_Tc` \ glaExts ->
+    reduceSimple [] wanteds            `thenNF_Tc` \ irreds ->
     let
        -- For multi-param Haskell, check that the returned dictionaries
        -- don't have any of the form (C Int Bool) for which
        -- we expect an instance here
        -- For Haskell 98, check that all the constraints are of the form C a,
        -- where a is a type variable
-       bad_guys | opt_GlasgowExts = [ct | ct@(clas,tys) <- irreds, 
-                                          isEmptyVarSet (tyVarsOfTypes tys)]
-                | otherwise       = [ct | ct@(clas,tys) <- irreds, 
-                                          not (all isTyVarTy tys)]
+       bad_guys | glaExts   = [ct | ct@(clas,tys) <- irreds, 
+                                    isEmptyVarSet (tyVarsOfTypes tys)]
+                | otherwise = [ct | ct@(clas,tys) <- irreds, 
+                                    not (all isTyVarTy tys)]
     in
     if null bad_guys then
        returnTc irreds
@@ -773,12 +873,12 @@ used with \tr{default} declarations.  We are only interested in
 whether it worked or not.
 
 \begin{code}
-tcSimplifyCheckThetas :: ThetaType     -- Given
-                     -> ThetaType      -- Wanted
-                     -> TcM s ()
+tcSimplifyCheckThetas :: ClassContext  -- Given
+                     -> ClassContext   -- Wanted
+                     -> TcM ()
 
 tcSimplifyCheckThetas givens wanteds
-  = reduceSimple classInstEnv givens wanteds    `thenNF_Tc`    \ irreds ->
+  = reduceSimple givens wanteds    `thenNF_Tc` \ irreds ->
     if null irreds then
        returnTc ()
     else
@@ -788,68 +888,67 @@ tcSimplifyCheckThetas givens wanteds
 
 
 \begin{code}
-type AvailsSimple = FiniteMap (Class, [TauType]) Bool
+type AvailsSimple = FiniteMap (Class,[Type]) Bool
                    -- True  => irreducible 
                    -- False => given, or can be derived from a given or from an irreducible
 
-reduceSimple :: (Class -> InstEnv) 
-            -> ThetaType               -- Given
-            -> ThetaType               -- Wanted
-            -> NF_TcM s ThetaType      -- Irreducible
+reduceSimple :: ClassContext                   -- Given
+            -> ClassContext                    -- Wanted
+            -> NF_TcM ClassContext             -- Irreducible
 
-reduceSimple inst_mapper givens wanteds
-  = reduce_simple (0,[]) inst_mapper givens_fm wanteds `thenNF_Tc` \ givens_fm' ->
+reduceSimple givens wanteds
+  = reduce_simple (0,[]) givens_fm wanteds     `thenNF_Tc` \ givens_fm' ->
     returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
   where
     givens_fm     = foldl addNonIrred emptyFM givens
 
-reduce_simple :: (Int,ThetaType)               -- Stack
-             -> (Class -> InstEnv) 
+reduce_simple :: (Int,ClassContext)            -- Stack
              -> AvailsSimple
-             -> ThetaType
-             -> NF_TcM s AvailsSimple
+             -> ClassContext
+             -> NF_TcM AvailsSimple
 
-reduce_simple (n,stack) inst_mapper avails wanteds
+reduce_simple (n,stack) avails wanteds
   = go avails wanteds
   where
     go avails []     = returnNF_Tc avails
-    go avails (w:ws) = reduce_simple_help (n+1,w:stack) inst_mapper avails w   `thenNF_Tc` \ avails' ->
+    go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w       `thenNF_Tc` \ avails' ->
                       go avails' ws
 
-reduce_simple_help stack inst_mapper givens wanted@(clas,tys)
+reduce_simple_help stack givens wanted@(clas,tys)
   | wanted `elemFM` givens
   = returnNF_Tc givens
 
   | otherwise
-  = lookupSimpleInst (inst_mapper clas) clas tys       `thenNF_Tc` \ maybe_theta ->
+  = lookupSimpleInst clas tys  `thenNF_Tc` \ maybe_theta ->
 
     case maybe_theta of
       Nothing ->    returnNF_Tc (addIrred givens wanted)
-      Just theta -> reduce_simple stack inst_mapper (addNonIrred givens wanted) theta
+      Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
 
-addIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
-addIrred givens ct
+addIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addIrred givens ct@(clas,tys)
   = addSCs (addToFM givens ct True) ct
 
-addNonIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
-addNonIrred givens ct
+addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addNonIrred givens ct@(clas,tys)
   = addSCs (addToFM givens ct False) ct
 
 addSCs givens ct@(clas,tys)
  = foldl add givens sc_theta
  where
-   (tyvars, sc_theta_tmpl, _, _, _) = classBigSig clas
-   sc_theta = substTheta (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+   (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
+   sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
 
-   add givens ct = case lookupFM givens ct of
-                          Nothing    -> -- Add it and its superclasses
-                                        addSCs (addToFM givens ct False) ct
+   add givens ct@(clas, tys)
+     = case lookupFM givens ct of
+       Nothing    -> -- Add it and its superclasses
+                    addSCs (addToFM givens ct False) ct
 
-                          Just True  -> -- Set its flag to False; superclasses already done
-                                        addToFM givens ct False
+       Just True  -> -- Set its flag to False; superclasses already done
+                    addToFM givens ct False
 
-                          Just False -> -- Already done
-                                        givens
+       Just False -> -- Already done
+                    givens
                           
 \end{code}
 
@@ -879,7 +978,7 @@ For each method @Inst@ in the @init_lie@ that mentions one of the
 @LIE@), as well as the @HsBinds@ generated.
 
 \begin{code}
-bindInstsOfLocalFuns ::        LIE -> [TcId] -> TcM s (LIE, TcMonoBinds)
+bindInstsOfLocalFuns ::        LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
 
 bindInstsOfLocalFuns init_lie local_ids
   | null overloaded_ids || null lie_for_here
@@ -903,7 +1002,7 @@ bindInstsOfLocalFuns init_lie local_ids
        -- No sense in repeatedly zonking lots of 
        -- constant constraints so filter them out here
     (lie_for_here, lie_not_for_here) = partition (isMethodFor overloaded_set)
-                                                (bagToList init_lie)
+                                                (lieToList init_lie)
     try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
                | otherwise                       = Free
 \end{code}
@@ -950,7 +1049,7 @@ variable, and using @disambigOne@ to do the real business.
 all the constant and ambiguous Insts.
 
 \begin{code}
-tcSimplifyTop :: LIE -> TcM s TcDictBinds
+tcSimplifyTop :: LIE -> TcM TcDictBinds
 tcSimplifyTop wanted_lie
   = reduceContext (text "tcSimplTop") try_me [] wanteds        `thenTc` \ (binds1, frees, irreds) ->
     ASSERT( null frees )
@@ -983,12 +1082,13 @@ tcSimplifyTop wanted_lie
 
     returnTc (binds1 `andMonoBinds` andMonoBindList binds_ambig)
   where
-    wanteds    = bagToList wanted_lie
+    wanteds    = lieToList wanted_lie
     try_me inst        = ReduceMe AddToIrreds
 
     d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
-    complain d | isEmptyVarSet (tyVarsOfInst d) = addTopInstanceErr d
+    complain d | not (null (getIPs d))         = addTopIPErr d
+              | isEmptyVarSet (tyVarsOfInst d) = addTopInstanceErr d
               | otherwise                      = addAmbigErr tyVarsOfInst d
 
 get_tv d   = case getDictClassTys d of
@@ -1011,7 +1111,7 @@ Since we're not using the result of @foo@, the result if (presumably)
 
 \begin{code}
 disambigGroup :: [Inst]        -- All standard classes of form (C a)
-             -> TcM s TcDictBinds
+             -> TcM TcDictBinds
 
 disambigGroup dicts
   |   any isNumericClass classes       -- Guaranteed all standard classes
@@ -1046,10 +1146,7 @@ disambigGroup dicts
     try_default default_tys                    `thenTc` \ chosen_default_ty ->
 
        -- Bind the type variable and reduce the context, for real this time
-    let
-       chosen_default_tc_ty = typeToTcType chosen_default_ty   -- Tiresome!
-    in
-    unifyTauTy chosen_default_tc_ty (mkTyVarTy tyvar)  `thenTc_`
+    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenTc_`
     reduceContext (text "disambig" <+> ppr dicts)
                  try_me [] dicts                       `thenTc` \ (binds, frees, ambigs) ->
     ASSERT( null frees && null ambigs )
@@ -1120,23 +1217,18 @@ genCantGenErr insts     -- Can't generalise these Insts
 addAmbigErrs ambig_tv_fn dicts = mapNF_Tc (addAmbigErr ambig_tv_fn) dicts
 
 addAmbigErr ambig_tv_fn dict
-  = tcAddSrcLoc (instLoc dict) $
-    addErrTcM (tidy_env,
-              sep [text "Ambiguous type variable(s)" <+>
-                       hsep (punctuate comma (map (quotes . ppr) ambig_tvs)),
-                  nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict)),
-                  nest 4 (pprOrigin dict)])
+  = addInstErrTcM (instLoc dict)
+       (tidy_env,
+        sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
+             nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
   where
     ambig_tvs = varSetElems (ambig_tv_fn tidy_dict)
     (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
 
 warnDefault dicts default_ty
-  | not opt_WarnTypeDefaults
-  = returnNF_Tc ()
+  = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn ->
+    if warn then warnTc True msg else returnNF_Tc ()
 
-  | otherwise
-  = tcAddSrcLoc (instLoc (head dicts))         $
-    warnTc True msg
   where
     msg | length dicts > 1 
        = (ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty))
@@ -1147,41 +1239,67 @@ warnDefault dicts default_ty
 
     (_, tidy_dicts) = mapAccumL tidyInst emptyTidyEnv dicts
 
-addRuleLhsErr dict
-  = tcAddSrcLoc (instLoc dict)                 $
-    addErrTcM (tidy_env,
-              vcat [ptext SLIT("Could not deduce") <+> quotes (pprInst tidy_dict),
-                    nest 4 (pprOrigin dict),
-                    ptext SLIT("LHS of a rule must have no overloading")])
+addTopIPErr dict
+  = addInstErrTcM (instLoc dict) 
+       (tidy_env, 
+        ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
   where
     (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
 
 -- Used for top-level irreducibles
 addTopInstanceErr dict
-  = tcAddSrcLoc (instLoc dict)                $
-    addErrTcM (tidy_env, 
-              sep [ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict),
-                  nest 4 $ pprOrigin dict])
+  = addInstErrTcM (instLoc dict) 
+       (tidy_env, 
+        ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
   where
     (tidy_env, tidy_dict) = tidyInst emptyTidyEnv dict
 
+-- The error message when we don't find a suitable instance
+-- is complicated by the fact that sometimes this is because
+-- there is no instance, and sometimes it's because there are
+-- too many instances (overlap).  See the comments in TcEnv.lhs
+-- with the InstEnv stuff.
 addNoInstanceErr str givens dict
-  = tcAddSrcLoc (instLoc dict) $
-    addErrTcM (tidy_env, 
-              sep [sep [ptext SLIT("Could not deduce") <+> quotes (pprInst tidy_dict),
-                       nest 4 $ parens $ pprOrigin dict],
-                  nest 4 $ ptext SLIT("from the context:") <+> pprInsts tidy_givens]
-             $$
-             ptext SLIT("Probable cause:") <+> 
-             vcat [sep [ptext SLIT("missing") <+> quotes (pprInst tidy_dict),
-                        ptext SLIT("in") <+> str],
-                   if all_tyvars then empty else
-                   ptext SLIT("or missing instance declaration for") <+> quotes (pprInst tidy_dict)]
-    )
-  where
-    all_tyvars = all isTyVarTy tys
-    (_, tys)   = getDictClassTys dict
-    (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
+  = tcGetInstEnv       `thenNF_Tc` \ inst_env ->
+    let
+       doc = vcat [herald <+> quotes (pprInst tidy_dict),
+                   nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens,
+                   ambig_doc,
+                   ptext SLIT("Probable fix:"),
+                   nest 4 fix1,
+                   nest 4 fix2]
+    
+       herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
+       unambig_doc | ambig_overlap = ptext SLIT("unambiguously")       
+                   | otherwise     = empty
+    
+       ambig_doc 
+           | not ambig_overlap = empty
+           | otherwise             
+           = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
+                   nest 4 (ptext SLIT("depends on the instantiation of") <+> 
+                           quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
+    
+       fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
+                   ptext SLIT("to the") <+> str]
+    
+       fix2 | isTyVarDict dict || ambig_overlap
+            = empty
+            | otherwise
+            = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
+    
+       (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
+    
+           -- Checks for the ambiguous case when we have overlapping instances
+       ambig_overlap | isClassDict dict
+                     = case lookupInstEnv inst_env clas tys of
+                           NoMatch ambig -> ambig
+                           other         -> False
+                     | otherwise = False
+                     where
+                       (clas,tys) = getDictClassTys dict
+    in
+    addInstErrTcM (instLoc dict) (tidy_env, doc)
 
 -- Used for the ...Thetas variants; all top level
 addNoInstErr (c,ts)