[project @ 2004-03-11 14:34:22 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 291cf84..3c0ac28 100644 (file)
@@ -21,7 +21,7 @@ module TcSimplify (
 
 import {-# SOURCE #-} TcUnify( unifyTauTy )
 import TcEnv           -- temp
-import HsSyn           ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr )
+import HsSyn           ( HsBind(..), LHsBinds, HsExpr(..), LHsExpr, pprLHsBinds )
 import TcHsSyn         ( TcId, TcDictBinds, mkHsApp, mkHsTyApp, mkHsDictApp )
 
 import TcRnMonad
@@ -35,8 +35,8 @@ import Inst           ( lookupInst, LookupInstResult(..),
                          newDictsFromOld, tcInstClassOp,
                          getDictClassTys, isTyVarDict,
                          instLoc, zonkInst, tidyInsts, tidyMoreInsts,
-                         Inst, pprInsts, pprInstsInFull, tcGetInstEnvs,
-                         isIPDict, isInheritableInst, pprDFuns
+                         Inst, pprInsts, pprDictsInFull, tcGetInstEnvs,
+                         isIPDict, isInheritableInst, pprDFuns, pprDictsTheta
                        )
 import TcEnv           ( tcGetGlobalTyVars, tcLookupId, findGlobals )
 import InstEnv         ( lookupInstEnv, classInstEnv )
@@ -44,7 +44,7 @@ import TcMType                ( zonkTcTyVarsAndFV, tcInstTyVars, checkAmbiguity )
 import TcType          ( TcTyVar, TcTyVarSet, ThetaType, TyVarDetails(VanillaTv),
                          mkClassPred, isOverloadedTy, mkTyConApp,
                          mkTyVarTy, tcGetTyVar, isTyVarClassPred, mkTyVarTys,
-                         tyVarsOfPred )
+                         tyVarsOfPred, tcEqType, pprPred )
 import Id              ( idType, mkUserLocal )
 import Var             ( TyVar )
 import Name            ( getOccName, getSrcLoc )
@@ -77,6 +77,60 @@ import CmdLineOpts
 %************************************************************************
 
        --------------------------------------
+       Notes on functional dependencies (a bug)
+       --------------------------------------
+
+| > class Foo a b | a->b
+| >
+| > class Bar a b | a->b
+| >
+| > data Obj = Obj
+| >
+| > instance Bar Obj Obj
+| >
+| > instance (Bar a b) => Foo a b
+| >
+| > foo:: (Foo a b) => a -> String
+| > foo _ = "works"
+| >
+| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+| > runFoo f = f Obj
+| 
+| *Test> runFoo foo
+| 
+| <interactive>:1:
+|     Could not deduce (Bar a b) from the context (Foo a b)
+|       arising from use of `foo' at <interactive>:1
+|     Probable fix:
+|         Add (Bar a b) to the expected type of an expression
+|     In the first argument of `runFoo', namely `foo'
+|     In the definition of `it': it = runFoo foo
+| 
+| Why all of the sudden does GHC need the constraint Bar a b? The
+| function foo didn't ask for that... 
+
+The trouble is that to type (runFoo foo), GHC has to solve the problem:
+
+       Given constraint        Foo a b
+       Solve constraint        Foo a b'
+
+Notice that b and b' aren't the same.  To solve this, just do
+improvement and then they are the same.  But GHC currently does
+       simplify constraints
+       apply improvement
+       and loop
+
+That is usually fine, but it isn't here, because it sees that Foo a b is
+not the same as Foo a b', and so instead applies the instance decl for
+instance Bar a b => Foo a b.  And that's where the Bar constraint comes
+from.
+
+The Right Thing is to improve whenever the constraint set changes at
+all.  Not hard in principle, but it'll take a bit of fiddling to do.  
+
+
+
+       --------------------------------------
                Notes on quantification
        --------------------------------------
 
@@ -306,6 +360,36 @@ but we'll produce the non-principal type
 
 
        --------------------------------------
+       The need for forall's in constraints
+       --------------------------------------
+
+[Exchange on Haskell Cafe 5/6 Dec 2000]
+
+  class C t where op :: t -> Bool
+  instance C [t] where op x = True
+
+  p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
+  q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
+
+The definitions of p and q differ only in the order of the components in
+the pair on their right-hand sides.  And yet:
+
+  ghc and "Typing Haskell in Haskell" reject p, but accept q;
+  Hugs rejects q, but accepts p;
+  hbc rejects both p and q;
+  nhc98 ... (Malcolm, can you fill in the blank for us!).
+
+The type signature for f forces context reduction to take place, and
+the results of this depend on whether or not the type of y is known,
+which in turn depends on which component of the pair the type checker
+analyzes first.  
+
+Solution: if y::m a, float out the constraints
+       Monad m, forall c. C (m c)
+When m is later unified with [], we can solve both constraints.
+
+
+       --------------------------------------
                Notes on implicit parameters
        --------------------------------------
 
@@ -771,6 +855,64 @@ tcSimplCheck doc get_qtvs givens wanted_lie
 %*                                                                     *
 %************************************************************************
 
+tcSimplifyRestricted infers which type variables to quantify for a 
+group of restricted bindings.  This isn't trivial.
+
+Eg1:   id = \x -> x
+       We want to quantify over a to get id :: forall a. a->a
+       
+Eg2:   eq = (==)
+       We do not want to quantify over a, because there's an Eq a 
+       constraint, so we get eq :: a->a->Bool  (notice no forall)
+
+So, assume:
+       RHS has type 'tau', whose free tyvars are tau_tvs
+       RHS has constraints 'wanteds'
+
+Plan A (simple)
+  Quantify over (tau_tvs \ ftvs(wanteds))
+  This is bad. The constraints may contain (Monad (ST s))
+  where we have        instance Monad (ST s) where...
+  so there's no need to be monomorphic in s!
+
+  Also the constraint might be a method constraint,
+  whose type mentions a perfectly innocent tyvar:
+         op :: Num a => a -> b -> a
+  Here, b is unconstrained.  A good example would be
+       foo = op (3::Int)
+  We want to infer the polymorphic type
+       foo :: forall b. b -> b
+
+
+Plan B (cunning, used for a long time up to and including GHC 6.2)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem).  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 reasons for this is to maximise sharing.
+
+  This fails for a very subtle reason.  Suppose that in the Step 2
+  a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
+  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.
+
+  Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
+  the problem.
+
+
+Plan C (brutal)
+  Step 1: Simplify the constraints as much as possible (to deal 
+  with Plan A's problem).  Then set
+       qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
+  Return the bindings from Step 1.
+  
+
+
 \begin{code}
 tcSimplifyRestricted   -- Used for restricted binding groups
                        -- i.e. ones subject to the monomorphism restriction
@@ -779,72 +921,37 @@ tcSimplifyRestricted      -- Used for restricted binding groups
        -> [Inst]               -- Free in the RHSs
        -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
                TcDictBinds)    -- Bindings
+       -- tcSimpifyRestricted returns no constraints to
+       -- quantify over; by definition there are none.
+       -- They are all thrown back in the LIE
 
 tcSimplifyRestricted doc tau_tvs wanteds
-  =    -- First squash out all methods, to find the constrained tyvars
-       -- We can't just take the free vars of wanted_lie because that'll
-       -- have methods that may incidentally mention entirely unconstrained variables
-       --      e.g. a call to  f :: Eq a => a -> b -> b
-       -- Here, b is unconstrained.  A good example would be
-       --      foo = f (3::Int)
-       -- We want to infer the polymorphic type
-       --      foo :: forall b. b -> b
-
        -- '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` \ (foo_frees, foo_binds, constrained_dicts) ->
+  = simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, binds, irreds) ->
+    ASSERT( null frees )
 
        -- Next, figure out the tyvars we will quantify over
     zonkTcTyVarsAndFV (varSetElems tau_tvs)    `thenM` \ tau_tvs' ->
     tcGetGlobalTyVars                          `thenM` \ gbl_tvs ->
     let
-       constrained_tvs = tyVarsOfInsts constrained_dicts
-       qtvs = (tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs)
-                        `minusVarSet` constrained_tvs
+       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
     in
     traceTc (text "tcSimplifyRestricted" <+> vcat [
-               pprInsts wanteds, pprInsts foo_frees, pprInsts constrained_dicts,
-               ppr foo_binds,
+               pprInsts wanteds, pprInsts frees, pprInsts irreds,
+               pprLHsBinds binds,
                ppr constrained_tvs, ppr tau_tvs', ppr qtvs ])  `thenM_`
 
-       -- The first step may have squashed more methods than
-       -- necessary, so try again, this time 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
-    restrict_loop doc qtvs wanteds
-       -- We still need a loop because improvement can take place
-       -- E.g. if we have (C (T a)) and the instance decl
-       --      instance D Int b => C (T a) where ...
-       -- and there's a functional dependency for D.   Then we may improve
-       -- the tyep variable 'b'.
-
-restrict_loop doc qtvs wanteds
-  = mappM zonkInst wanteds                     `thenM` \ wanteds' ->
-    zonkTcTyVarsAndFV (varSetElems qtvs)       `thenM` \ qtvs' ->
-    let
-        try_me inst | isFreeWrtTyVars qtvs' inst = Free
-                   | otherwise                  = ReduceMe
-    in
-    reduceContext doc try_me [] wanteds'       `thenM` \ (no_improvement, frees, binds, irreds) ->
-    if no_improvement then
-       ASSERT( null irreds )
-       extendLIEs frees                        `thenM_`
-       returnM (varSetElems qtvs', binds)
-    else
-       restrict_loop doc qtvs' (irreds ++ frees)       `thenM` \ (qtvs1, binds1) ->
-       returnM (qtvs1, binds `unionBags` binds1)
+    extendLIEs irreds                                          `thenM_`
+    returnM (varSetElems qtvs, binds)
 \end{code}
 
 
@@ -907,7 +1014,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
+    try_me inst        | isDict inst = DontReduce NoSCs        -- See notes above for why NoSCs
                | otherwise   = ReduceMe
 \end{code}
 
@@ -1412,19 +1519,19 @@ reduceList (n,stack) try_me wanteds state
                      go ws state'
 
     -- Base case: we're done!
-reduce stack try_me wanted state
+reduce stack try_me wanted avails
     -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- isAvailable state wanted
+  | Just avail <- isAvailable avails wanted
   = if isLinearInst wanted then
-       addLinearAvailable state avail wanted   `thenM` \ (state', wanteds') ->
-       reduceList stack try_me wanteds' state'
+       addLinearAvailable avails avail wanted  `thenM` \ (avails', wanteds') ->
+       reduceList stack try_me wanteds' avails'
     else
-       returnM state           -- No op for non-linear things
+       returnM avails          -- No op for non-linear things
 
   | otherwise
   = case try_me wanted of {
 
-      DontReduce want_scs -> addIrred want_scs state wanted
+      DontReduce want_scs -> addIrred want_scs 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
@@ -1437,26 +1544,30 @@ reduce stack try_me wanted state
     ; ReduceMe ->              -- It should be reduced
        lookupInst wanted             `thenM` \ lookup_result ->
        case lookup_result of
-           GenInst wanteds' rhs -> addWanted state wanted rhs wanteds'         `thenM` \ state' ->
-                                   reduceList stack try_me wanteds' state'
-               -- Experiment with doing addWanted *before* the reduceList, 
+           GenInst wanteds' rhs -> addIrred NoSCs avails wanted                `thenM` \ avails1 ->
+                                   reduceList stack try_me wanteds' avails1    `thenM` \ avails2 ->
+                                   addWanted avails2 wanted rhs wanteds'
+               -- Experiment with temporarily doing addIrred *before* the reduceList, 
                -- which has the effect of adding the thing we are trying
                -- to prove to the database before trying to prove the things it
                -- needs.  See note [RECURSIVE DICTIONARIES]
+               -- NB: we must not do an addWanted before, because that adds the
+               --     superclasses too, and thaat can lead to a spurious loop; see
+               --     the examples in [SUPERCLASS-LOOP]
+               -- So we do an addIrred before, and then overwrite it afterwards with addWanted
 
-           SimpleInst rhs       -> addWanted state wanted rhs []
+           SimpleInst rhs       -> addWanted avails wanted rhs []
 
            NoInstance ->    -- No such instance!
                             -- Add it and its superclasses
-                            addIrred AddSCs state wanted
-
+                            addIrred AddSCs avails wanted
     }
   where
     try_simple do_this_otherwise
       = lookupInst wanted        `thenM` \ lookup_result ->
        case lookup_result of
-           SimpleInst rhs -> addWanted state wanted rhs []
-           other          -> do_this_otherwise state wanted
+           SimpleInst rhs -> addWanted avails wanted rhs []
+           other          -> do_this_otherwise avails wanted
 \end{code}
 
 
@@ -1512,14 +1623,13 @@ addFree avails free = returnM (addToFM avails free IsFree)
 
 addWanted :: Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
 addWanted avails wanted rhs_expr wanteds
-  = ASSERT2( not (wanted `elemFM` avails), ppr wanted $$ ppr avails )
-    addAvailAndSCs avails wanted avail
+  = addAvailAndSCs avails wanted avail
   where
     avail | instBindingRequired wanted = Rhs rhs_expr wanteds
          | otherwise                  = ASSERT( null wanteds ) NoRhs
 
 addGiven :: Avails -> Inst -> TcM Avails
-addGiven state given = addAvailAndSCs state given (Given (instToId given) False)
+addGiven avails given = addAvailAndSCs avails given (Given (instToId given) False)
        -- No ASSERT( not (given `elemFM` avails) ) because in an instance
        -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
        -- so the assert isn't true
@@ -1535,21 +1645,23 @@ addAvailAndSCs avails inst avail
   | otherwise             = traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps]) `thenM_`
                             addSCs is_loop avails1 inst 
   where
-    avails1 = addToFM avails inst avail
-    is_loop inst = inst `elem` deps    -- Note: this compares by *type*, not by Unique
-    deps         = findAllDeps avails avail
-
-findAllDeps :: Avails -> Avail -> [Inst]
--- Find all the Insts that this one depends on
--- See Note [SUPERCLASS-LOOP]
-findAllDeps avails (Rhs _ kids) = kids ++ concat (map (find_all_deps_help avails) kids)
-findAllDeps avails other       = []
-
-find_all_deps_help :: Avails -> Inst -> [Inst]
-find_all_deps_help avails inst
-  = case lookupFM avails inst of
-       Just avail -> findAllDeps avails avail
-       Nothing    -> []
+    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
+    dep_tys     = map idType (varSetElems deps)
+
+    findAllDeps :: IdSet -> Avail -> IdSet
+    -- Find all the Insts that this one depends on
+    -- 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
+
 
 addSCs :: (Inst -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to Avails
@@ -1566,17 +1678,18 @@ addSCs is_loop avails dict
     sc_theta' = substTheta (mkTopTyVarSubst tyvars tys) sc_theta
 
     add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
-      | is_loop sc_dict
-      = returnM avails -- See Note [SUPERCLASS-LOOP]
-      | otherwise
-      = case lookupFM avails sc_dict of
-         Just (Given _ _) -> returnM avails    -- Given is cheaper than superclass selection
-         Just other       -> returnM avails'   -- SCs already added
-         Nothing          -> addSCs is_loop avails' sc_dict
+      | add_me sc_dict = addSCs is_loop avails' sc_dict
+      | otherwise      = returnM avails
       where
        sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
-       avail      = Rhs sc_sel_rhs [dict]
-       avails'    = addToFM avails sc_dict avail
+       avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
+
+    add_me :: Inst -> Bool
+    add_me sc_dict
+       | is_loop sc_dict = False       -- See Note [SUPERCLASS-LOOP]
+       | otherwise       = case lookupFM avails sc_dict of
+                               Just (Given _ _) -> False       -- Given is cheaper than superclass selection
+                               other            -> True        
 \end{code}
 
 Note [SUPERCLASS-LOOP]: Checking for loops
@@ -1643,13 +1756,13 @@ by instance decl, holds if
 
 by instance decl of Eq, holds if
        d3 : D []
-       where   d2 = dfEqList d2
+       where   d2 = dfEqList d3
                d1 = dfEqD d2
 
 But now we can "tie the knot" to give
 
        d3 = d1
-       d2 = dfEqList d2
+       d2 = dfEqList d3
        d1 = dfEqD d2
 
 and it'll even run!  The trick is to put the thing we are trying to prove
@@ -1917,43 +2030,39 @@ tcSimplifyDeriv tyvars theta
     doptM Opt_AllowUndecidableInstances                `thenM` \ undecidable_ok ->
     let
        tv_set      = mkVarSet tvs
-       simpl_theta = map dictPred irreds       -- reduceMe squashes all non-dicts
-
-       check_pred pred
-         | isEmptyVarSet pred_tyvars   -- Things like (Eq T) should be rejected
-         = addErrTc (noInstErr pred)
-
-         | not undecidable_ok && not (isTyVarClassPred pred)
-         -- Check that the returned dictionaries are all of form (C a b)
-         --    (where a, b are type variables).  
-         -- We allow this if we had -fallow-undecidable-instances,
-         -- but note that risks non-termination in the 'deriving' context-inference
-         -- fixpoint loop.   It is useful for situations like
-         --    data Min h a = E | M a (h a)
-         -- which gives the instance decl
-         --    instance (Eq a, Eq (h a)) => Eq (Min h a)
-          = addErrTc (noInstErr pred)
+
+       (bad_insts, ok_insts) = partition is_bad_inst irreds
+       is_bad_inst dict 
+          = let pred = dictPred dict   -- reduceMe squashes all non-dicts
+            in isEmptyVarSet (tyVarsOfPred pred)
+                 -- Things like (Eq T) are bad
+            || (not undecidable_ok && not (isTyVarClassPred pred))
+                 -- The returned dictionaries should be of form (C a b)
+                 --    (where a, b are type variables).  
+                 -- We allow non-tyvar dicts if we had -fallow-undecidable-instances,
+                 -- but note that risks non-termination in the 'deriving' context-inference
+                 -- fixpoint loop.   It is useful for situations like
+                 --    data Min h a = E | M a (h a)
+                 -- which gives the instance decl
+                 --    instance (Eq a, Eq (h a)) => Eq (Min h a)
   
-         | not (pred_tyvars `subVarSet` tv_set) 
+       simpl_theta = map dictPred ok_insts
+       weird_preds = [pred | pred <- simpl_theta
+                           , not (tyVarsOfPred pred `subVarSet` tv_set)]  
          -- Check for a bizarre corner case, when the derived instance decl should
          -- have form  instance C a b => D (T a) where ...
          -- Note that 'b' isn't a parameter of T.  This gives rise to all sorts
          -- of problems; in particular, it's hard to compare solutions for
          -- equality when finding the fixpoint.  So I just rule it out for now.
-         = addErrTc (badDerivedPred pred)
   
-         | otherwise
-         = returnM ()
-         where
-           pred_tyvars = tyVarsOfPred pred
-
        rev_env = mkTopTyVarSubst tvs (mkTyVarTys tyvars)
                -- This reverse-mapping is a Royal Pain, 
                -- but the result should mention TyVars not TcTyVars
     in
    
-    mappM check_pred simpl_theta               `thenM_`
-    checkAmbiguity tvs simpl_theta tv_set      `thenM_`
+    addNoInstanceErrs Nothing [] bad_insts             `thenM_`
+    mapM_ (addErrTc . badDerivedPred) weird_preds      `thenM_`
+    checkAmbiguity tvs simpl_theta tv_set              `thenM_`
     returnM (substTheta rev_env simpl_theta)
   where
     doc    = ptext SLIT("deriving classes for a data type")
@@ -1971,7 +2080,7 @@ tcSimplifyDefault theta
   = newDicts DataDeclOrigin theta              `thenM` \ wanteds ->
     simpleReduceLoop doc reduceMe wanteds      `thenM` \ (frees, _, irreds) ->
     ASSERT( null frees )       -- try_me never returns Free
-    mappM (addErrTc . noInstErr) irreds        `thenM_`
+    addNoInstanceErrs Nothing []  irreds       `thenM_`
     if null irreds then
        returnM ()
     else
@@ -2027,7 +2136,7 @@ addTopIPErrs dicts
     (tidy_env, tidy_dicts) = tidyInsts dicts
     report dicts = addErrTcM (tidy_env, mk_msg dicts)
     mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> 
-                                    plural tidy_dicts <+> pprInsts tidy_dicts)
+                                    plural tidy_dicts <+> pprDictsTheta tidy_dicts)
 
 addNoInstanceErrs :: Maybe SDoc        -- Nothing => top level
                                -- Just d => d describes the construct
@@ -2071,15 +2180,16 @@ addNoInstanceErrs mb_what givens dicts
        no_inst_doc | null no_inst_dicts = empty
                    | otherwise = vcat [addInstLoc no_inst_dicts heading, probable_fix]
        heading | null givens = ptext SLIT("No instance") <> plural no_inst_dicts <+> 
-                               ptext SLIT("for") <+> pprInsts no_inst_dicts
-               | otherwise   = sep [ptext SLIT("Could not deduce") <+> pprInsts no_inst_dicts,
-                                    nest 2 $ ptext SLIT("from the context") <+> pprInsts tidy_givens]
+                               ptext SLIT("for") <+> pprDictsTheta no_inst_dicts
+               | otherwise   = sep [ptext SLIT("Could not deduce") <+> pprDictsTheta no_inst_dicts,
+                                    nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta tidy_givens]
     in
     addErrTcM (tidy_env3, no_inst_doc $$ overlap_doc)
  
   where
     mk_overlap_msg dict (matches, unifiers)
-      = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") <+> ppr dict)),
+      = 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 
@@ -2094,12 +2204,12 @@ addNoInstanceErrs mb_what givens 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])
       where
-       fix1 = sep [ptext SLIT("Add") <+> pprInsts dicts,
+       fix1 = sep [ptext SLIT("Add") <+> pprDictsTheta dicts,
                    ptext SLIT("to the") <+> what]
 
        fix2 | null instance_dicts = empty
             | otherwise           = ptext SLIT("Or add an instance declaration for")
-                                    <+> pprInsts instance_dicts
+                                    <+> 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
@@ -2125,7 +2235,7 @@ addTopAmbigErrs dicts
          dicts = map fst pairs
          msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
                             pprQuotedList tvs <+> in_msg,
-                    nest 2 (pprInstsInFull dicts)]
+                    nest 2 (pprDictsInFull dicts)]
          in_msg | isSingleton dicts = text "in the top-level constraint:"
                 | otherwise         = text "in these top-level constraints:"
 
@@ -2160,11 +2270,9 @@ warnDefault dicts default_ty
     (_, tidy_dicts) = tidyInsts dicts
     warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
                                quotes (ppr default_ty),
-                     pprInstsInFull tidy_dicts]
+                     pprDictsInFull tidy_dicts]
 
 -- Used for the ...Thetas variants; all top level
-noInstErr pred = ptext SLIT("No instance for") <+> quotes (ppr pred)
-
 badDerivedPred pred
   = vcat [ptext SLIT("Can't derive instances where the instance context mentions"),
          ptext SLIT("type variables that are not data type parameters"),
@@ -2173,7 +2281,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 (pprInstsInFull stack)]
+         nest 4 (pprDictsInFull stack)]
 
-reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+reduceDepthMsg n stack = nest 4 (pprDictsInFull stack)
 \end{code}