X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=534c5d0601c8e74bd841b1c86da8a845f78ba43d;hp=32fe6cf866ab2166a770aef740222cf62cd3a715;hb=ebec49fed627b7dd17e297ddc79a9c677a2ce538;hpb=5c2ecdff9b9e814c2549da0b3efd61d5107c72d6

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 32fe6cf..534c5d0 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -15,7 +15,9 @@ module TcSimplify (
 	tcSimplifyBracket, tcSimplifyCheckPat,
 
 	tcSimplifyDeriv, tcSimplifyDefault,
-	bindInstsOfLocalFuns, bindIrreds,
+	bindInstsOfLocalFuns, 
+
+        misMatchMsg
     ) where
 
 #include "HsVersions.h"
@@ -24,14 +26,17 @@ import {-# SOURCE #-} TcUnify( unifyType )
 import HsSyn
 
 import TcRnMonad
+import TcHsSyn	( hsLPatType )
 import Inst
 import TcEnv
 import InstEnv
-import TcGadt
 import TcType
 import TcMType
 import TcIface
+import TcTyFuns
+import DsUtils	-- Big-tuple functions
 import Var
+import Id
 import Name
 import NameSet
 import Class
@@ -47,11 +52,13 @@ import VarEnv
 import FiniteMap
 import Bag
 import Outputable
+import Maybes
 import ListSetOps
 import Util
 import SrcLoc
 import DynFlags
-
+import FastString
+import Control.Monad
 import Data.List
 \end{code}
 
@@ -84,34 +91,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1).
 
 Here is a more complicated example:
 
-| > 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... 
+@
+  > 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:
 
@@ -132,14 +141,9 @@ 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
-	--------------------------------------
-
-Suppose we are about to do a generalisation step.
-We have in our hand
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to do a generalisation step.  We have in our hand
 
 	G	the environment
 	T	the type of the RHS
@@ -162,11 +166,12 @@ Here are the things that *must* be true:
  (A)	Q intersect fv(G) = EMPTY			limits how big Q can be
  (B)	Q superset fv(Cq union T) \ oclose(fv(G),C)	limits how small Q can be
 
-(A) says we can't quantify over a variable that's free in the
-environment.  (B) says we must quantify over all the truly free
-variables in T, else we won't get a sufficiently general type.  We do
-not *need* to quantify over any variable that is fixed by the free
-vars of the environment G.
+ (A) says we can't quantify over a variable that's free in the environment. 
+ (B) says we must quantify over all the truly free variables in T, else 
+     we won't get a sufficiently general type.  
+
+We do not *need* to quantify over any variable that is fixed by the
+free vars of the environment G.
 
 	BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
 
@@ -180,38 +185,15 @@ Example:	class H x y | x->y where ...
 
 	So Q can be {c,d}, {b,c,d}
 
+In particular, it's perfectly OK to quantify over more type variables
+than strictly necessary; there is no need to quantify over 'b', since
+it is determined by 'a' which is free in the envt, but it's perfectly
+OK to do so.  However we must not quantify over 'a' itself.
+
 Other things being equal, however, we'd like to quantify over as few
 variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq.
-
-
------------------------------------------
-We will make use of
-
-  fv(T)	 	the free type vars of T
-
-  oclose(vs,C)	The result of extending the set of tyvars vs
-		using the functional dependencies from C
-
-  grow(vs,C)	The result of extend the set of tyvars vs
-		using all conceivable links from C.
-
-		E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
-		Then grow(vs,C) = {a,b,c}
-
-		Note that grow(vs,C) `superset` grow(vs,simplify(C))
-		That is, simplfication can only shrink the result of grow.
-
-Notice that
-   oclose is conservative one way:      v `elem` oclose(vs,C) => v is definitely fixed by vs
-   grow is conservative the other way:  if v might be fixed by vs => v `elem` grow(vs,C)
-
-
------------------------------------------
-
-Note [Choosing which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here's a good way to choose Q:
+constraints can get into Ct instead of Cq.  Here's a good way to
+choose Q:
 
 	Q = grow( fv(T), C ) \ oclose( fv(G), C )
 
@@ -245,9 +227,8 @@ all the functional dependencies yet:
 	T = c->c
 	C = (Eq (T c d))
 
-  Now oclose(fv(T),C) = {c}, because the functional dependency isn't
-  apparent yet, and that's wrong.  We must really quantify over d too.
-
+Now oclose(fv(T),C) = {c}, because the functional dependency isn't
+apparent yet, and that's wrong.  We must really quantify over d too.
 
 There really isn't any point in quantifying over any more than
 grow( fv(T), C ), because the call sites can't possibly influence
@@ -425,14 +406,19 @@ over implicit parameters. See the predicate isFreeWhenInferring.
 
 Note [Implicit parameters and ambiguity] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-What type should we infer for this?
-	f x = (show ?y, x::Int)
-Since we must quantify over the ?y, the most plausible type is
-	f :: (Show a, ?y::a) => Int -> (String, Int)
-But notice that the type of the RHS is (String,Int), with no type 
-varibables mentioned at all!  The type of f looks ambiguous.  But
-it isn't, because at a call site we might have
-	let ?y = 5::Int in f 7
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot.  For example:
+	foo :: (?x :: [a]) => Int
+	foo = length ?x
+is fine.  The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others.  E.g.
+	foo :: (Show a, ?x::[a]) => Int
+	foo = show (?x++?x)
+The type of foo looks ambiguous.  But it isn't, because at a call site
+we might have
+	let ?x = 5::Int in foo
 and all is well.  In effect, implicit parameters are, well, parameters,
 so we can take their type variables into account as part of the
 "tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
@@ -665,54 +651,79 @@ tcSimplifyInfer
 
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted
-  = do	{ tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
-	; wanted' <- mappM zonkInst wanted	-- Zonk before deciding quantified tyvars
+  = do	{ tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
+	; wanted'  <- mapM zonkInst wanted	-- Zonk before deciding quantified tyvars
 	; gbl_tvs  <- tcGetGlobalTyVars
-	; let preds = fdPredsOfInsts wanted'
-	      qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+	; let preds1   = fdPredsOfInsts wanted'
+	      gbl_tvs1 = oclose preds1 gbl_tvs
+	      qtvs     = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
 			-- See Note [Choosing which variables to quantify]
 
 		-- To maximise sharing, remove from consideration any 
 		-- constraints that don't mention qtvs at all
-	; let (free1, bound) = partition (isFreeWhenInferring qtvs) wanted'
-	; extendLIEs free1
+	; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
+	; extendLIEs free
 
 		-- To make types simple, reduce as much as possible
-	; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
-		   ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
+	; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ 
+		   ppr gbl_tvs1 $$ ppr free $$ ppr bound))
 	; (irreds1, binds1) <- tryHardCheckLoop doc bound
 
 		-- Note [Inference and implication constraints]
 	; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
 	; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
 
-		-- By now improvment may have taken place, and we must *not*
-		-- quantify over any variable free in the environment
-		-- tc137 (function h inside g) is an example
-	; gbl_tvs <- tcGetGlobalTyVars
-	; qtvs1 <- zonkTcTyVarsAndFV (varSetElems qtvs)
-	; qtvs2 <- zonkQuantifiedTyVars (varSetElems (qtvs1 `minusVarSet` gbl_tvs))
-
-		-- Do not quantify over constraints that *now* do not
-		-- mention quantified type variables, because they are
-		-- simply ambiguous (or might be bound further out).  Example:
-		-- 	f :: Eq b => a -> (a, b)
-		--	g x = fst (f x)
-		-- From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
-		-- We decide to quantify over 'alpha' alone, but free1 does not include f77
-		-- because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
-		-- constraint (Eq beta), which we dump back into the free set
-		-- See test tcfail181
-	; let (free3, irreds3) = partition (isFreeWhenInferring (mkVarSet qtvs2)) irreds2
-	; extendLIEs free3
-	
+		-- Now work out all over again which type variables to quantify,
+		-- exactly in the same way as before, but starting from irreds2.  Why?
+		-- a) By now improvment may have taken place, and we must *not*
+		--    quantify over any variable free in the environment
+		--    tc137 (function h inside g) is an example
+		--
+		-- b) Do not quantify over constraints that *now* do not
+		--    mention quantified type variables, because they are
+		--    simply ambiguous (or might be bound further out).  Example:
+		--    	f :: Eq b => a -> (a, b)
+		--    	g x = fst (f x)
+		--    From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
+		--    We decide to quantify over 'alpha' alone, but free1 does not include f77
+		--    because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
+		--    constraint (Eq beta), which we dump back into the free set
+		--    See test tcfail181
+		--
+		-- c) irreds may contain type variables not previously mentioned,
+		--    e.g.  instance D a x => Foo [a] 
+		--	    wanteds = Foo [a]
+		--       Then after simplifying we'll get (D a x), and x is fresh
+		-- 	 We must quantify over x else it'll be totally unbound
+	; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
+	; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
+		-- Note that we start from gbl_tvs1
+		-- We use tcGetGlobalTyVars, then oclose wrt preds2, because
+		-- we've already put some of the original preds1 into frees
+		-- E.g. 	wanteds = C a b	  (where a->b)
+		--		gbl_tvs = {a}
+		--		tau_tvs = {b}
+		-- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
+		-- irreds2 will be empty.  But we don't want to generalise over b!
+	; let preds2 = fdPredsOfInsts irreds2	-- irreds2 is zonked
+	      qtvs   = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+	; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
+	; extendLIEs free
+
+		-- Turn the quantified meta-type variables into real type variables
+	; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
+
 		-- We can't abstract over any remaining unsolved 
 		-- implications so instead just float them outwards. Ugh.
-	; let (q_dicts, implics) = partition isDict irreds3
+	; let (q_dicts0, implics) = partition isAbstractableInst irreds3
 	; loc <- getInstLoc (ImplicOrigin doc)
-	; implic_bind <- bindIrreds loc qtvs2 q_dicts implics
+	; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
+
+		-- Prepare equality instances for quantification
+	; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
+	; q_eqs <- mapM finalizeEqInst q_eqs0
 
-	; return (qtvs2, q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
+	; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
 	-- NB: when we are done, we might have some bindings, but
 	-- the final qtvs might be empty.  See Note [NO TYVARS] below.
 
@@ -745,6 +756,8 @@ approximateImplications doc want_dict irreds
 	= [ d | let tv_set = mkVarSet tvs
 	      , d <- get_dicts wanteds 
 	      , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+    get_dict i@(EqInst {}) | want_dict i = [i]
+			   | otherwise   = [] 
     get_dict other = pprPanic "approximateImplications" (ppr other)
 \end{code}
 
@@ -763,7 +776,7 @@ with 'given' implications.
 
 So our best approximation is to make (D [a]) part of the inferred
 context, so we can use that to discharge the implication. Hence
-the strange function getImplicWanteds.
+the strange function get_dicts in approximateImplications.
 
 The common cases are more clear-cut, when we have things like
 	forall a. C a => C b
@@ -787,7 +800,8 @@ tcSimplifyInferCheck
 		 TcDictBinds)	-- Bindings
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do	{ (irreds, binds) <- gentleCheckLoop loc givens wanteds
+  = do	{ traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
+	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
 
 	-- Figure out which type variables to quantify over
 	-- You might think it should just be the signature tyvars,
@@ -811,6 +825,7 @@ tcSimplifyInferCheck loc tau_tvs givens wanteds
 		-- Now we are back to normal (c.f. tcSimplCheck)
 	; implic_bind <- bindIrreds loc qtvs' givens irreds
 
+	; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
 	; return (qtvs', binds `unionBags` implic_bind) }
 \end{code}
 
@@ -868,7 +883,9 @@ isFreeWhenChecking qtvs ips inst
   && isFreeWrtIPs    ips inst
 -}
 
+isFreeWrtTyVars :: VarSet -> Inst -> Bool
 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
+isFreeWrtIPs :: NameSet -> Inst -> Bool
 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 
@@ -893,23 +910,23 @@ tcSimplifyCheck	:: InstLoc
 	 	-> TcM TcDictBinds	-- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do	{ (irreds, binds) <- gentleCheckLoop loc givens wanteds
+    do	{ traceTc (text "tcSimplifyCheck")
+      	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
 	; implic_bind <- bindIrreds loc qtvs givens irreds
 	; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
 -- tcSimplifyCheckPat is used for existential pattern match
 tcSimplifyCheckPat :: InstLoc
-	 	   -> [CoVar] -> Refinement
 	 	   -> [TcTyVar]		-- Quantify over these
 	 	   -> [Inst]		-- Given
 	 	   -> [Inst]		-- Wanted
 	 	   -> TcM TcDictBinds	-- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
+tcSimplifyCheckPat loc qtvs givens wanteds
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do	{ (irreds, binds) <- gentleCheckLoop loc givens wanteds
-	; implic_bind <- bindIrredsR loc qtvs co_vars reft 
-				    givens irreds
+    do	{ traceTc (text "tcSimplifyCheckPat")
+      	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
+	; implic_bind <- bindIrredsR loc qtvs givens irreds
 	; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
@@ -917,26 +934,25 @@ bindIrreds :: InstLoc -> [TcTyVar]
 	   -> [Inst] -> [Inst]
 	   -> TcM TcDictBinds
 bindIrreds loc qtvs givens irreds 
-  = bindIrredsR loc qtvs [] emptyRefinement givens irreds
+  = bindIrredsR loc qtvs givens irreds
 
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
-	    -> Refinement -> [Inst] -> [Inst]
-	    -> TcM TcDictBinds	
+bindIrredsR :: InstLoc -> [TcTyVar] -> [Inst] -> [Inst] -> TcM TcDictBinds	
 -- Make a binding that binds 'irreds', by generating an implication
 -- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs co_vars reft givens irreds
+bindIrredsR loc qtvs givens irreds
   | null irreds
   = return emptyBag
   | otherwise
-  = do	{ let givens' = filter isDict givens
-		-- The givens can include methods
+  = do	{ let givens' = filter isAbstractableInst givens
+		-- The givens can (redundantly) include methods
+		-- We want to retain both EqInsts and Dicts
+		-- There should be no implicadtion constraints
 		-- See Note [Pruning the givens in an implication constraint]
 
-	   -- If there are no 'givens' *and* the refinement is empty
-	   -- (the refinement is like more givens), then it's safe to 
+	   -- If there are no 'givens', then it's safe to 
 	   -- partition the 'wanteds' by their qtvs, thereby trimming irreds
 	   -- See Note [Freeness and implications]
-	; irreds' <- if null givens' && isEmptyRefinement reft
+	; irreds' <- if null givens'
 	     	     then do
 	     	    	{ let qtv_set = mkVarSet qtvs
 	     	    	      (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
@@ -944,53 +960,70 @@ bindIrredsR loc qtvs co_vars reft givens irreds
 	     	    	; return real_irreds }
 	     	     else return irreds
 	
-	; let all_tvs = qtvs ++ co_vars	-- Abstract over all these
-	; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
+	; (implics, bind) <- makeImplicationBind loc qtvs givens' irreds'
 			-- This call does the real work
 			-- If irreds' is empty, it does something sensible
 	; extendLIEs implics
 	; return bind } 
 
 
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
+makeImplicationBind :: InstLoc -> [TcTyVar]
 		    -> [Inst] -> [Inst]
 		    -> TcM ([Inst], TcDictBinds)
 -- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--
 -- The binding looks like
 --	(ir1, .., irn) = f qtvs givens
 -- where f is (evidence for) the new implication constraint
---	f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
+--	f :: forall qtvs. givens => (ir1, .., irn)
+-- qtvs includes coercion variables.
 --
 -- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
-		    givens 	-- Guaranteed all Dicts
+makeImplicationBind loc all_tvs
+		    givens 	-- Guaranteed all Dicts or EqInsts
 		    irreds
  | null irreds			-- If there are no irreds, we are done
  = return ([], emptyBag)
  | otherwise			-- Otherwise we must generate a binding
  = do	{ uniq <- newUnique 
 	; span <- getSrcSpanM
-	; let name = mkInternalName uniq (mkVarOcc "ic") span
-	      implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+	; let (eq_givens, dict_givens) = partition isEqInst givens
+
+                -- extract equality binders
+              eq_cotvs = map eqInstType eq_givens
+
+                -- make the implication constraint instance
+	      name = mkInternalName uniq (mkVarOcc "ic") span
+	      implic_inst = ImplicInst { tci_name = name,
 					 tci_tyvars = all_tvs, 
-					 tci_given = givens,
-					 tci_wanted = irreds, tci_loc = loc }
-
-	; let n_irreds = length irreds
-	      irred_ids = map instToId irreds
-	      tup_ty = mkTupleTy Boxed n_irreds (map idType irred_ids)
-	      pat = TuplePat (map nlVarPat irred_ids) Boxed tup_ty
-	      rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-	      co  = mkWpApps (map instToId givens) <.> mkWpTyApps (mkTyVarTys all_tvs)
-	      bind | n_irreds==1 = VarBind (head irred_ids) rhs
-		   | otherwise   = PatBind { pat_lhs = L span pat, 
-				      	     pat_rhs = unguardedGRHSs rhs, 
-				      	     pat_rhs_ty = tup_ty,
-				      	     bind_fvs = placeHolderNames }
-	; -- pprTrace "Make implic inst" (ppr implic_inst) $
-	  return ([implic_inst], unitBag (L span bind)) }
+					 tci_given = (eq_givens ++ dict_givens),
+                                                       -- same order as binders
+					 tci_wanted = irreds, 
+                                         tci_loc = loc }
+
+	        -- create binders for the irreducible dictionaries
+	      dict_irreds    = filter (not . isEqInst) irreds
+	      dict_irred_ids = map instToId dict_irreds
+	      lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
+
+                -- create the binding
+	      rhs  = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+	      co   =     mkWpApps (map instToId dict_givens)
+		     <.> mkWpTyApps eq_cotvs
+		     <.> mkWpTyApps (mkTyVarTys all_tvs)
+	      bind | [dict_irred_id] <- dict_irred_ids  
+                   = VarBind dict_irred_id rhs
+		   | otherwise        
+                   = PatBind { pat_lhs = lpat
+			     , pat_rhs = unguardedGRHSs rhs 
+			     , pat_rhs_ty = hsLPatType lpat
+			     , bind_fvs = placeHolderNames 
+                             }
+
+	; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+	; return ([implic_inst], unitBag (L span bind)) 
+        }
 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc
@@ -998,9 +1031,11 @@ tryHardCheckLoop :: SDoc
 	     -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
-  = checkLoop (mkRedEnv doc try_me []) wanteds
+  = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
+       ; return (irreds,binds)
+       }
   where
-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe
 	-- Here's the try-hard bit
 
 -----------------------------------------------------------
@@ -1010,14 +1045,26 @@ gentleCheckLoop :: InstLoc
 	       -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
-  = checkLoop env wanteds
+  = do { (irreds,binds) <- checkLoop env wanteds
+       ; return (irreds,binds)
+       }
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+    try_me inst | isMethodOrLit inst = ReduceMe
 		| otherwise	     = Stop
 	-- When checking against a given signature 
 	-- we MUST be very gentle: Note [Check gently]
+
+gentleInferLoop :: SDoc -> [Inst]
+	        -> TcM ([Inst], TcDictBinds)
+gentleInferLoop doc wanteds
+  = do 	{ (irreds, binds) <- checkLoop env wanteds
+	; return (irreds, binds) }
+  where
+    env = mkInferRedEnv doc try_me
+    try_me inst | isMethodOrLit inst = ReduceMe
+		| otherwise	     = Stop
 \end{code}
 
 Note [Check gently]
@@ -1035,7 +1082,7 @@ Inside the pattern match, which binds (a:*, x:a), we know that
 Hence we have a dictionary for Show [a] available; and indeed we 
 need it.  We are going to build an implication contraint
 	forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
+Later, we will solve this constraint using the knowledge (Show b)
 	
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
@@ -1048,28 +1095,66 @@ with tryHardCheckLooop.
 -----------------------------------------------------------
 checkLoop :: RedEnv
 	  -> [Inst]			-- Wanted
-	  -> TcM ([Inst], TcDictBinds)
+	  -> TcM ([Inst], TcDictBinds) 
 -- Precondition: givens are completely rigid
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
-  = do { -- Givens are skolems, so no need to zonk them
-	 wanteds' <- mappM zonkInst wanteds
+  = go env wanteds
+  where go env wanteds
+	  = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+                ; env'     <- zonkRedEnv env
+		; wanteds' <- zonkInsts  wanteds
+	
+		; (improved, binds, irreds) <- reduceContext env' wanteds'
 
-	; (improved, binds, irreds) <- reduceContext env wanteds'
+		; if null irreds || not improved then
+	 	    return (irreds, binds)
+		  else do
+	
+		-- If improvement did some unification, we go round again.
+		-- We start again with irreds, not wanteds
+		-- Using an instance decl might have introduced a fresh type
+		-- variable which might have been unified, so we'd get an 
+                -- infinite loop if we started again with wanteds!  
+                -- See Note [LOOP]
+		{ (irreds1, binds1) <- go env' irreds
+		; return (irreds1, binds `unionBags` binds1) } }
+\end{code}
 
-	; if not improved then
- 	     return (irreds, binds)
-	  else do
+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables.  An example from tc237 in the
+testsuite is
+
+  class Modular s a | s -> a
+
+  wim ::  forall a w. Integral a 
+                        => a -> (forall s. Modular s a => M s w) -> w
+  wim i k = error "urk"
+
+  test5  ::  (Modular s a, Integral a) => M s a
+  test5  =   error "urk"
+
+  test4   =   wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside.  When type checking test4, we have to check
+whether the signature of test5 is an instance of 
+
+  (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens. 
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature).  If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+Unify.tcUnifyTys, which doesn't know about mutable type variables.
 
-	-- If improvement did some unification, we go round again.
-	-- We start again with irreds, not wanteds
-	-- Using an instance decl might have introduced a fresh type variable
-	-- which might have been unified, so we'd get an infinite loop
-	-- if we started again with wanteds!  See Note [LOOP]
-	{ (irreds1, binds1) <- checkLoop env irreds
-	; return (irreds1, binds `unionBags` binds1) } }
-\end{code}
 
 Note [LOOP]
 ~~~~~~~~~~~
@@ -1126,29 +1211,87 @@ Alas!  Alack! We can do the same for (instance D Int):
 	ds2 = $p1 dc
 
 And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
 Two more nasty cases are in
 	tcrun021
 	tcrun033
 
+Solution: 
+  - Satisfy the superclass context *all by itself* 
+    (tcSimplifySuperClasses)
+  - And do so completely; i.e. no left-over constraints
+    to mix with the constraints arising from method declarations
+
+
+Note [Recursive instances and superclases]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this code, which arises in the context of "Scrap Your 
+Boilerplate with Class".  
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)
+
+    instance Data Maybe a => Foo a
+    instance Foo a        => Foo [a]
+    instance                 Foo [Char]
+
+In the instance for Foo [a], when generating evidence for the superclasses
+(ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
+Using the instance for Data, we therefore need
+        (Sat (Maybe [a], Data Maybe a)
+But we are given (Foo a), and hence its superclass (Data Maybe a).
+So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
+we need (Foo [a]).  And that is the very dictionary we are bulding
+an instance for!  So we must put that in the "givens".  So in this
+case we have
+	Given:  Foo a, Foo [a]
+	Watend: Data Maybe [a]
+
+BUT we must *not not not* put the *superclasses* of (Foo [a]) in
+the givens, which is what 'addGiven' would normally do. Why? Because
+(Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted 
+by selecting a superclass from Foo [a], which simply makes a loop.
+
+On the other hand we *must* put the superclasses of (Foo a) in
+the givens, as you can see from the derivation described above.
+
+Conclusion: in the very special case of tcSimplifySuperClasses
+we have one 'given' (namely the "this" dictionary) whose superclasses
+must not be added to 'givens' by addGiven.  That is the *whole* reason
+for the red_given_scs field in RedEnv, and the function argument to
+addGiven.
+
 \begin{code}
-tcSimplifySuperClasses 
+tcSimplifySuperClasses
 	:: InstLoc 
+	-> Inst		-- The dict whose superclasses 
+			-- are being figured out
 	-> [Inst]	-- Given 
 	-> [Inst]	-- Wanted
 	-> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
-  = do	{ (irreds, binds1) <- checkLoop env sc_wanteds
+tcSimplifySuperClasses loc this givens sc_wanteds
+  = do	{ traceTc (text "tcSimplifySuperClasses")
+	; (irreds,binds1) <- checkLoop env sc_wanteds
 	; let (tidy_env, tidy_irreds) = tidyInsts irreds
 	; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
 	; return binds1 }
   where
-    env = mkRedEnv (pprInstLoc loc) try_me givens
-    try_me inst = ReduceMe NoSCs
-	-- Like tryHardCheckLoop, but with NoSCs
+    env =  RedEnv { red_doc = pprInstLoc loc, 
+		    red_try_me = try_me,
+	     	    red_givens = this:givens, 
+	     	    red_given_scs = add_scs,
+	     	    red_stack = (0,[]),
+	     	    red_improve = False }  -- No unification vars
+    add_scs g | g==this   = NoSCs
+	      | otherwise = AddSCs
+
+    try_me _ = ReduceMe  -- Try hard, so we completely solve the superclass 
+    	       		 -- constraints right here. See Note [SUPERCLASS-LOOP 1]
 \end{code}
 
 
@@ -1268,7 +1411,8 @@ tcSimplifyRestricted 	-- Used for restricted binding groups
 
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
 	-- Zonk everything in sight
-  = do	{ wanteds' <- mappM zonkInst wanteds
+  = do	{ traceTc (text "tcSimplifyRestricted")
+	; wanteds' <- zonkInsts wanteds
 
    	-- 'ReduceMe': Reduce as far as we can.  Don't stop at
 	-- dicts; the idea is to get rid of as many type
@@ -1279,13 +1423,13 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
 	-- BUT do no improvement!  See Plan D above
 	-- HOWEVER, some unification may take place, if we instantiate
 	-- 	    a method Inst with an equality constraint
-	; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
+	; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe)
 	; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
 
 	-- Next, figure out the tyvars we will quantify over
 	; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 	; gbl_tvs' <- tcGetGlobalTyVars
-	; constrained_dicts' <- mappM zonkInst constrained_dicts
+	; constrained_dicts' <- zonkInsts constrained_dicts
 
 	; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
 				-- As in tcSimplifyInfer
@@ -1299,9 +1443,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
 	-- Warn in the mono
 	; warn_mono <- doptM Opt_WarnMonomorphism
 	; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
-		 (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
-				<> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
-			ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
+		 (vcat[ ptext (sLit "the Monomorphism Restriction applies to the binding")
+				<> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs,
+			ptext (sLit "Consider giving a type signature for") <+> pp_bndrs])
 
 	; traceTc (text "tcSimplifyRestricted" <+> vcat [
 		pprInsts wanteds, pprInsts constrained_dicts',
@@ -1327,7 +1471,7 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
 	; let is_nested_group = isNotTopLevel top_lvl
 	      try_me inst | isFreeWrtTyVars qtvs inst,
 			   (is_nested_group || isDict inst) = Stop
-		          | otherwise  	         = ReduceMe AddSCs
+		          | otherwise  	                    = ReduceMe 
 	      env = mkNoImproveRedEnv doc try_me
 	; (_imp, binds, irreds) <- reduceContext env wanteds'
 
@@ -1402,26 +1546,55 @@ Instead we want to quantify over the dictionaries separately.
 
 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
 all dicts unchanged, with absolutely no sharing.  It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
+from scratch, rather than further parameterise simpleReduceLoop etc.
+Simpler, maybe, but alas not simple (see Trac #2494)
+
+* Type errors may give rise to an (unsatisfiable) equality constraint
+
+* Applications of a higher-rank function on the LHS may give
+  rise to an implication constraint, esp if there are unsatisfiable
+  equality constraints inside.
 
 \begin{code}
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds
-  = go [] emptyBag wanteds
+  = do	{ wanteds' <- zonkInsts wanteds
+	; (irreds, binds) <- go [] emptyBag wanteds'
+	; let (dicts, bad_irreds) = partition isDict irreds
+	; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
+	; addNoInstanceErrs (nub bad_irreds)
+		-- The nub removes duplicates, which has
+		-- not happened otherwise (see notes above)
+	; return (dicts, binds) }
   where
-    go dicts binds []
-	= return (dicts, binds)
-    go dicts binds (w:ws)
+    go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
+    go irreds binds []
+	= return (irreds, binds)
+    go irreds binds (w:ws)
 	| isDict w
-	= go (w:dicts) binds ws
+	= go (w:irreds) binds ws
+	| isImplicInst w	-- Have a go at reducing the implication
+	= do { (binds1, irreds1) <- reduceImplication red_env w
+	     ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
+	     ; go (bad_irreds ++ irreds) 
+		  (binds `unionBags` binds1) 
+		  (ok_irreds ++ ws)}
 	| otherwise
 	= do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
 				 -- to fromInteger; this looks fragile to me
 	     ; lookup_result <- lookupSimpleInst w'
 	     ; case lookup_result of
-		 GenInst ws' rhs -> go dicts (addBind binds (instToId w) rhs) (ws' ++ ws)
-		 NoInstance	 -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+		 NoInstance      -> go (w:irreds) binds ws
+		 GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
+			where
+			  binds' = addInstToDictBind binds w rhs
 	  }
+
+	-- Sigh: we need to reduce inside implications
+    red_env = mkInferRedEnv doc try_me
+    doc = ptext (sLit "Implication constraint in RULE lhs")
+    try_me inst | isMethodOrLit inst = ReduceMe
+		| otherwise	     = Stop	-- Be gentle
 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
@@ -1472,19 +1645,27 @@ tcSimplifyIPs :: [Inst]		-- The implicit parameters bound here
 	-- makes them the same.
 
 tcSimplifyIPs given_ips wanteds
-  = do	{ wanteds'   <- mappM zonkInst wanteds
-	; given_ips' <- mappM zonkInst given_ips
+  = do	{ wanteds'   <- zonkInsts wanteds
+	; given_ips' <- zonkInsts given_ips
 		-- Unusually for checking, we *must* zonk the given_ips
 
 	; let env = mkRedEnv doc try_me given_ips'
 	; (improved, binds, irreds) <- reduceContext env wanteds'
 
-	; if not improved then 
+	; if null irreds || not improved then 
 		ASSERT( all is_free irreds )
 		do { extendLIEs irreds
 		   ; return binds }
-	  else
-		tcSimplifyIPs given_ips wanteds }
+	  else do
+        -- If improvement did some unification, we go round again.
+        -- We start again with irreds, not wanteds
+        -- Using an instance decl might have introduced a fresh type
+        -- variable which might have been unified, so we'd get an 
+        -- infinite loop if we started again with wanteds!  
+        -- See Note [LOOP]
+        { binds1 <- tcSimplifyIPs given_ips' irreds
+        ; return $ binds `unionBags` binds1
+        } }
   where
     doc	   = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)
@@ -1492,7 +1673,7 @@ tcSimplifyIPs given_ips wanteds
 
 	-- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop
-		| otherwise    = ReduceMe NoSCs
+		| otherwise    = ReduceMe
 \end{code}
 
 
@@ -1531,18 +1712,17 @@ bindInstsOfLocalFuns ::	[Inst] -> [TcId] -> TcM TcDictBinds
 -- arguably a bug in Match.tidyEqnInfo (see notes there)
 
 bindInstsOfLocalFuns wanteds local_ids
-  | null overloaded_ids
+  | null overloaded_ids = do
 	-- Common case
-  = extendLIEs wanteds		`thenM_`
-    returnM emptyLHsBinds
+    extendLIEs wanteds
+    return emptyLHsBinds
 
   | otherwise
-  = do	{ (irreds, binds) <- checkLoop env for_me
+  = do	{ (irreds, binds) <- gentleInferLoop doc for_me
 	; extendLIEs not_for_me	
 	; extendLIEs irreds
 	; return binds }
   where
-    env = mkRedEnv doc try_me []
     doc		     = text "bindInsts" <+> ppr local_ids
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
@@ -1551,8 +1731,6 @@ bindInstsOfLocalFuns wanteds local_ids
     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 | isMethod inst = ReduceMe NoSCs
-		| otherwise	= Stop
 \end{code}
 
 
@@ -1570,8 +1748,11 @@ data RedEnv
 	   , red_try_me :: Inst -> WhatToDo
 	   , red_improve :: Bool		-- True <=> do improvement
 	   , red_givens :: [Inst]		-- All guaranteed rigid
-						-- Always dicts
+						-- Always dicts & equalities
 						-- but see Note [Rigidity]
+ 
+ 	   , red_given_scs :: Inst -> WantSCs	-- See Note [Recursive instances and superclases]
+ 
 	   , red_stack  :: (Int, [Inst])	-- Recursion stack (for err msg)
 						-- See Note [RedStack]
   }
@@ -1593,22 +1774,35 @@ data RedEnv
 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
-	     red_givens = givens, red_stack = (0,[]),
+	     red_givens = givens, 
+	     red_given_scs = const AddSCs,
+	     red_stack = (0,[]),
+	     red_improve = True }	
+
+mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
+-- No givens at all
+mkInferRedEnv doc try_me
+  = RedEnv { red_doc = doc, red_try_me = try_me,
+	     red_givens = [], 
+	     red_given_scs = const AddSCs,
+	     red_stack = (0,[]),
 	     red_improve = True }	
 
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
-	     red_givens = [], red_stack = (0,[]),
+	     red_givens = [], 
+	     red_given_scs = const AddSCs,
+	     red_stack = (0,[]),
 	     red_improve = True }	
 
 data WhatToDo
- = ReduceMe WantSCs	-- Try to reduce this
-			-- If there's no instance, add the inst to the 
-			-- irreductible ones, but don't produce an error 
-			-- message of any kind.
-			-- It might be quite legitimate such as (Eq a)!
+ = ReduceMe 	-- Try to reduce this
+		-- If there's no instance, add the inst to the 
+		-- irreductible ones, but don't produce an error 
+		-- message of any kind.
+		-- It might be quite legitimate such as (Eq a)!
 
  | Stop		-- Return as irreducible unless it can
 			-- be reduced to a constant in one step
@@ -1618,14 +1812,33 @@ data WantSCs = NoSCs | AddSCs	-- Tells whether we should add the superclasses
 				-- of a predicate when adding it to the avails
 	-- The reason for this flag is entirely the super-class loop problem
 	-- Note [SUPER-CLASS LOOP 1]
+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env
+  = do { givens' <- mapM zonkInst (red_givens env)
+       ; return $ env {red_givens = givens'}
+       }
 \end{code}
 
+
 %************************************************************************
 %*									*
 \subsection[reduce]{@reduce@}
 %*									*
 %************************************************************************
 
+Note [Ancestor Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+During context reduction, we add to the wanted equalities also those
+equalities that (transitively) occur in superclass contexts of wanted
+class constraints.  Consider the following code
+
+  class a ~ Int => C a
+  instance C Int
+
+If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
+substituting Int for a.  Hence, we ultimately want (C Int), which we
+discharge with the explicit instance.
 
 \begin{code}
 reduceContext :: RedEnv
@@ -1634,41 +1847,108 @@ reduceContext :: RedEnv
 		      TcDictBinds,	-- Dictionary bindings
 		      [Inst])		-- Irreducible
 
-reduceContext env wanteds
+reduceContext env wanteds0
   = do	{ traceTc (text "reduceContext" <+> (vcat [
 	     text "----------------------",
 	     red_doc env,
 	     text "given" <+> ppr (red_givens env),
-	     text "wanted" <+> ppr wanteds,
+	     text "wanted" <+> ppr wanteds0,
 	     text "----------------------"
 	     ]))
 
-        -- Build the Avail mapping from "givens"
-	; init_state <- foldlM addGiven emptyAvails (red_givens env)
-
-        -- Do the real work
-	-- Process non-implication constraints first, so that they are
-	-- available to help solving the implication constraints
-	-- 	ToDo: seems a bit inefficient and ad-hoc
-	; let (implics, rest) = partition isImplicInst wanteds
-	; avails <- reduceList env (rest ++ implics) init_state
-
-	; let improved = availsImproved avails
-	; (binds, irreds) <- extractResults avails wanteds
+          -- We want to add as wanted equalities those that (transitively) 
+          -- occur in superclass contexts of wanted class constraints.
+          -- See Note [Ancestor Equalities]
+	; ancestor_eqs <- ancestorEqualities wanteds0
+	; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
+
+          -- Normalise and solve all equality constraints as far as possible
+          -- and normalise all dictionary constraints wrt to the reduced
+          -- equalities.  The returned wanted constraints include the
+          -- irreducible wanted equalities.
+        ; let wanteds = wanteds0 ++ ancestor_eqs
+              givens  = red_givens env
+        ; (givens', 
+           wanteds', 
+           normalise_binds,
+           eq_improved)     <- tcReduceEqs givens wanteds
+	; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+		      [ppr givens', ppr wanteds', ppr normalise_binds]
+
+          -- Build the Avail mapping from "given_dicts"
+	; (init_state, _) <- getLIE $ do 
+		{ init_state <- foldlM (addGiven (red_given_scs env)) 
+		  	     	       emptyAvails givens'
+		; return init_state
+                }
+
+          -- Solve the *wanted* *dictionary* constraints (not implications)
+	  -- This may expose some further equational constraints...
+	; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
+	; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+	  	   -- The getLIE is reqd because reduceList does improvement
+		   -- (via extendAvails) which may in turn do unification
+	; (dict_binds, 
+           bound_dicts, 
+           dict_irreds)       <- extractResults avails wanted_dicts
+	; traceTc $ text "reduceContext: extractResults" <+> vcat
+		      [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+	  -- Solve the wanted *implications*.  In doing so, we can provide
+	  -- as "given"   all the dicts that were originally given, 
+	  --		  *or* for which we now have bindings, 
+	  --		  *or* which are now irreds
+          -- NB: Equality irreds need to be converted, as the recursive 
+          --     invocation of the solver will still treat them as wanteds
+          --     otherwise.
+	; let implic_env = env { red_givens 
+                                   = givens ++ bound_dicts ++
+                                     map wantedToLocalEqInst dict_irreds }
+	; (implic_binds_s, implic_irreds_s) 
+            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
+	; let implic_binds  = unionManyBags implic_binds_s
+	      implic_irreds = concat implic_irreds_s
+
+          -- Collect all irreducible instances, and determine whether we should
+          -- go round again.  We do so in either of two cases:
+          -- (1) If dictionary reduction or equality solving led to
+          --     improvement (i.e., instantiated type variables).
+          -- (2) If we uncovered extra equalities.  We will try to solve them
+          --     in the next iteration.
+          -- (3) If we reduced dictionaries (i.e., got dictionary bindings),
+          --     they may have exposed further opportunities to normalise
+          --     family applications.  See Note [Dictionary Improvement]
+
+	; let all_irreds       = dict_irreds ++ implic_irreds ++ extra_eqs
+      	      avails_improved  = availsImproved avails
+              improvedFlexible = avails_improved || eq_improved
+              extraEqs         = (not . null) extra_eqs
+              reduced_dicts    = not (isEmptyBag dict_binds)
+              improved         = improvedFlexible || extraEqs || reduced_dicts
+              --
+              improvedHint  = (if avails_improved then " [AVAILS]" else "") ++
+                              (if eq_improved then " [EQ]" else "") ++
+                              (if extraEqs then " [EXTRA EQS]" else "")
 
 	; traceTc (text "reduceContext end" <+> (vcat [
 	     text "----------------------",
 	     red_doc env,
-	     text "given" <+> ppr (red_givens env),
-	     text "wanted" <+> ppr wanteds,
+	     text "given" <+> ppr givens,
+	     text "wanted" <+> ppr wanteds0,
 	     text "----",
 	     text "avails" <+> pprAvails avails,
-	     text "improved =" <+> ppr improved,
-	     text "irreds = " <+> ppr irreds,
+	     text "improved =" <+> ppr improved <+> text improvedHint,
+	     text "(all) irreds = " <+> ppr all_irreds,
+	     text "dict-binds = " <+> ppr dict_binds,
+	     text "implic-binds = " <+> ppr implic_binds,
 	     text "----------------------"
 	     ]))
 
-	; return (improved, binds, irreds) }
+	; return (improved, 
+                  normalise_binds `unionBags` dict_binds 
+                                  `unionBags` implic_binds, 
+                  all_irreds) 
+        }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
@@ -1682,48 +1962,98 @@ tcImproveOne avails 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
+		-- NB that (?x::t1) and (?x::t2) will be held separately in 
+                --    avails so that improve will see them separate
 	; traceTc (text "improveOne" <+> ppr inst)
 	; unifyEqns eqns }
 
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] 
+unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))] 
 	  -> TcM ImprovementDone
 unifyEqns [] = return False
 unifyEqns eqns
-  = do	{ traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
-        ; mappM_ unify eqns
-	; return True }
+  = do	{ traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
+        ; improved <- mapM unify eqns
+	; return $ or improved
+        }
   where
     unify ((qtvs, pairs), what1, what2)
-	 = addErrCtxtM (mkEqnMsg what1 what2)	$
-	   tcInstTyVars (varSetElems qtvs)	`thenM` \ (_, _, tenv) ->
-	   mapM_ (unif_pr tenv) pairs
-    unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
+         = addErrCtxtM (mkEqnMsg what1 what2) $ 
+             do { let freeTyVars = unionVarSets (map tvs_pr pairs) 
+                                   `minusVarSet` qtvs
+                ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+                ; mapM_ (unif_pr tenv) pairs
+                ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
+                }
 
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+    unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
 
+    tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
+
+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _)) 
+  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)
 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
-  = do	{ pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
-	; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
-	; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
+  = do	{ pred1' <- zonkTcPredType pred1
+        ; pred2' <- zonkTcPredType pred2
+	; let { pred1'' = tidyPred tidy_env pred1'
+              ; pred2'' = tidyPred tidy_env pred2' }
+	; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
 			  nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
 			  nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
 	; return (tidy_env, msg) }
 \end{code}
 
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former.  Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings.  The following example demonstrated the point:
+
+  data EX _x _y (p :: * -> *)
+  data ANY
+
+  class Base p
+
+  class Base (Def p) => Prop p where
+   type Def p
+
+  instance Base ()
+  instance Prop () where
+   type Def () = ()
+
+  instance (Base (Def (p ANY))) => Base (EX _x _y p)
+  instance (Prop (p ANY)) => Prop (EX _x _y p) where
+   type Def (EX _x _y p) = EX _x _y p
+
+  data FOO x
+  instance Prop (FOO x) where
+   type Def (FOO x) = ()
+
+  data BAR
+  instance Prop BAR where
+   type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to 
+Base (EX () () FOO).  Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
 The main context-reduction function is @reduce@.  Here's its game plan.
 
 \begin{code}
 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
-  = do 	{ dopts <- getDOpts
-#ifdef DEBUG
-	; if n > 8 then
-		dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 
+  = do	{ traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+	; dopts <- getDOpts
+	; when (debugIsOn && (n > 8)) $ do
+		debugDumpTcRn (hang (ptext (sLit "Interesting! Context reduction stack depth") <+> int n) 
 			     2 (ifPprDebug (nest 2 (pprStack stk))))
-	  else return ()
-#endif
 	; if n >= ctxtStkDepth dopts then
 	    failWithTc (reduceDepthErr n stk)
 	  else
@@ -1734,37 +2064,47 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
 			 ; go ws state' }
 
     -- Base case: we're done!
+reduce :: RedEnv -> Inst -> Avails -> TcM Avails
 reduce env wanted avails
+
+    -- We don't reduce equalities here (and they must not end up as irreds
+    -- in the Avails!)
+  | isEqInst wanted
+  = return avails
+
     -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- findAvail avails wanted
-  = returnM avails	
+  | Just _ <- findAvail avails wanted
+  = do { traceTc (text "reduce: found " <+> ppr wanted)
+       ; return avails
+       }
 
   | otherwise
-  = case red_try_me env wanted of {
-    ; Stop -> try_simple (addIrred NoSCs)	-- See Note [No superclasses for Stop]
-
-    ; ReduceMe want_scs ->	-- It should be reduced
-	reduceInst env avails wanted      `thenM` \ (avails, lookup_result) ->
-	case lookup_result of
-	    NoInstance ->    -- No such instance!
+  = do	{ traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
+	; case red_try_me env wanted of {
+	    Stop -> try_simple (addIrred NoSCs);
+			-- See Note [No superclasses for Stop]
+
+	    ReduceMe -> do	-- It should be reduced
+		{ (avails, lookup_result) <- reduceInst env avails wanted
+		; case lookup_result of
+		    NoInstance -> addIrred AddSCs avails wanted
 			     -- Add it and its superclasses
-		    	     addIrred want_scs avails wanted
+		    	     
+		    GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
 
-	    GenInst [] rhs -> addWanted want_scs avails wanted rhs []
-
-	    GenInst wanteds' rhs -> do	{ avails1 <- addIrred NoSCs avails wanted
-					; avails2 <- reduceList env wanteds' avails1
-					; addWanted want_scs avails2 wanted rhs wanteds' }
+		    GenInst wanteds' rhs
+			  -> do	{ avails1 <- addIrred NoSCs avails wanted
+				; avails2 <- reduceList env wanteds' avails1
+				; addWanted AddSCs avails2 wanted rhs wanteds' } }
 		-- Temporarily do 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
+		--     superclasses too, and that 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
-
-    }
+    } }
   where
   	-- First, see if the inst can be reduced to a constant in one step
 	-- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
@@ -1773,14 +2113,50 @@ reduce env wanted avails
       = do { res <- lookupSimpleInst wanted
 	   ; case res of
 	        GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
-	        other	       -> do_this_otherwise avails wanted }
+	        _              -> do_this_otherwise avails wanted }
 \end{code}
 
 
+Note [RECURSIVE DICTIONARIES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider 
+    data D r = ZeroD | SuccD (r (D r));
+    
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+    
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])).  Here's how we go:
+
+	d1 : Eq (D [])
+
+by instance decl, holds if
+	d2 : Eq [D []]
+	where 	d1 = dfEqD d2
+
+by instance decl of Eq, holds if
+	d3 : D []
+	where	d2 = dfEqList d3
+		d1 = dfEqD d2
+
+But now we can "tie the knot" to give
+
+	d3 = d1
+	d2 = dfEqList d3
+	d1 = dfEqD d2
+
+and it'll even run!  The trick is to put the thing we are trying to prove
+(in this case Eq (D []) into the database before trying to prove its
+contributing clauses.
+	
 Note [SUPERCLASS-LOOP 2]
 ~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough.  Suppose we are *given* d1:Ord a,
-and want to deduce (d2:C [a]) where
+We need to be careful when adding "the constaint we are trying to prove".
+Suppose 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 ...
@@ -1818,42 +2194,6 @@ Now we implement the Right Solution, which is to check for loops directly
 when adding superclasses.  It's a bit like the occurs check in unification.
 
 
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider 
-    data D r = ZeroD | SuccD (r (D r));
-    
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-    
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])).  Here's how we go:
-
-	d1 : Eq (D [])
-
-by instance decl, holds if
-	d2 : Eq [D []]
-	where 	d1 = dfEqD d2
-
-by instance decl of Eq, holds if
-	d3 : D []
-	where	d2 = dfEqList d3
-		d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
-	d3 = d1
-	d2 = dfEqList d3
-	d1 = dfEqD d2
-
-and it'll even run!  The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-	
 
 %************************************************************************
 %*									*
@@ -1864,36 +2204,49 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
-				    tci_given = extra_givens, tci_wanted = wanteds })
-  = reduceImplication env avails reft tvs extra_givens wanteds loc
-
-reduceInst env avails other_inst
+reduceInst _ avails other_inst
   = do	{ result <- lookupSimpleInst other_inst
 	; return (avails, result) }
 \end{code}
 
+Note [Equational Constraints in Implication Constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+An implication constraint is of the form 
+	Given => Wanted 
+where Given and Wanted may contain both equational and dictionary
+constraints. The delay and reduction of these two kinds of constraints
+is distinct:
+
+-) In the generated code, wanted Dictionary constraints are wrapped up in an
+   implication constraint that is created at the code site where the wanted
+   dictionaries can be reduced via a let-binding. This let-bound implication
+   constraint is deconstructed at the use-site of the wanted dictionaries.
+
+-) While the reduction of equational constraints is also delayed, the delay
+   is not manifest in the generated code. The required evidence is generated
+   in the code directly at the use-site. There is no let-binding and deconstruction
+   necessary. The main disadvantage is that we cannot exploit sharing as the
+   same evidence may be generated at multiple use-sites. However, this disadvantage
+   is limited because it only concerns coercions which are erased.
+
+The different treatment is motivated by the different in representation. Dictionary
+constraints require manifest runtime dictionaries, while equations require coercions
+which are types.
+
 \begin{code}
 ---------------------------------------------
 reduceImplication :: RedEnv
-		 -> Avails
-		 -> Refinement	-- May refine the givens; often empty
-		 -> [TcTyVar]	-- Quantified type variables; all skolems
-		 -> [Inst]	-- Extra givens; all rigid
-		 -> [Inst]	-- Wanted
-		 -> InstLoc
-		 -> TcM (Avails, LookupInstResult)
+		  -> Inst
+		  -> TcM (TcDictBinds, [Inst])
 \end{code}
 
 Suppose we are simplifying the constraint
 	forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
+in the context of an overall simplification problem with givens 'givens'.
 
 Note that
-  * The refinement is often empty
-
-  * The 'extra givens' need not mention any of the quantified type variables
+  * The 'givens' need not mention any of the quantified type variables
 	e.g. 	forall {}. Eq a => Eq [a]
 		forall {}. C Int => D (Tree Int)
 
@@ -1907,56 +2260,123 @@ Note that
 \begin{code}
 	-- ToDo: should we instantiate tvs?  I think it's not necessary
 	--
-	-- ToDo: what about improvement?  There may be some improvement
-	--	 exposed as a result of the simplifications done by reduceList
-	--	 which are discarded if we back off.  
-	--	 This is almost certainly Wrong, but we'll fix it when dealing
-	--	 better with equality constraints
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
-  = do	{ 	-- Add refined givens, and the extra givens
-	  (refined_red_givens, avails) 
-		<- if isEmptyRefinement reft then return (red_givens env, orig_avails)
-		   else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
-	; avails <- foldlM addGiven avails extra_givens
-
-		-- Solve the sub-problem
-	; let try_me inst = ReduceMe AddSCs	-- Note [Freeness and implications]
-	      env' = env { red_givens = refined_red_givens ++ extra_givens
+	-- Note on coercion variables:
+	--
+	--	The extra given coercion variables are bound at two different 
+        --      sites:
+        --
+	--	-) in the creation context of the implication constraint	
+	--		the solved equational constraints use these binders
+	--
+	--	-) at the solving site of the implication constraint
+	--		the solved dictionaries use these binders;
+	--		these binders are generated by reduceImplication
+	--
+        -- Note [Binders for equalities]
+        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+        -- To reuse the binders of local/given equalities in the binders of 
+        -- implication constraints, it is crucial that these given equalities
+        -- always have the form
+        --   cotv :: t1 ~ t2
+        -- where cotv is a simple coercion type variable (and not a more
+        -- complex coercion term).  We require that the extra_givens always
+        -- have this form and exploit the special form when generating binders.
+reduceImplication env
+	orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+		      	   	  tci_tyvars = tvs,
+		      	   	  tci_given = extra_givens, tci_wanted = wanteds
+                                 })
+  = do	{ 	-- Solve the sub-problem
+	; let try_me _ = ReduceMe  -- Note [Freeness and implications]
+	      env' = env { red_givens = extra_givens ++ red_givens env
+			 , red_doc = sep [ptext (sLit "reduceImplication for") 
+                                            <+> ppr name,
+					  nest 2 (parens $ ptext (sLit "within")
+                                                           <+> red_doc env)]
 			 , red_try_me = try_me }
 
 	; traceTc (text "reduceImplication" <+> vcat
-			[ ppr orig_avails,
-			  ppr (red_givens env), ppr extra_givens, 
-			  ppr reft, ppr wanteds, ppr avails ])
-	; avails <- reduceList env' wanteds avails
+			[ ppr (red_givens env), ppr extra_givens, 
+			  ppr wanteds])
+	; (irreds, binds) <- checkLoop env' wanteds
 
-		-- Extract the binding
-	; (binds, irreds) <- extractResults avails wanteds
- 
 	; traceTc (text "reduceImplication result" <+> vcat
-			[ ppr irreds, ppr binds])
+			[ppr irreds, ppr binds])
+
+	; -- extract superclass binds
+	  --  (sc_binds,_) <- extractResults avails []
+-- 	; traceTc (text "reduceImplication sc_binds" <+> vcat
+--			[ppr sc_binds, ppr avails])
+--  
 
-		-- We always discard the extra avails we've generated;
-		-- but we remember if we have done any (global) improvement
-	; let ret_avails = updateImprovement orig_avails avails
+	-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+	-- Then we must iterate the outer loop too!
 
-	; if isEmptyLHsBinds binds then 	-- No progress
-		return (ret_avails, NoInstance)
+        ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+                                   -- we solve wanted eqs by side effect!
+
+            -- Progress is no longer measered by the number of bindings
+            -- If there are any irreds, but no bindings and no solved
+            -- equalities, we back off and do nothing
+        ; let backOff = isEmptyLHsBinds binds &&   -- no new bindings
+                        (not $ null irreds)   &&   -- but still some irreds
+                        didntSolveWantedEqs        -- no instantiated cotv
+
+	; if backOff then 	-- No progress
+		return (emptyBag, [orig_implic])
 	  else do
-	{ (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
-
-	; let	dict_ids = map instToId extra_givens
-		co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
-		rhs = mkHsWrap co payload
-	        loc = instLocSpan inst_loc
-		payload | [wanted] <- wanteds = HsVar (instToId wanted)
-			| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
-
-		-- If there are any irreds, we back off and return NoInstance
-	; return (ret_avails, GenInst implic_insts (L loc rhs))
-  } }
+	{ (simpler_implic_insts, bind) 
+            <- makeImplicationBind inst_loc tvs extra_givens irreds
+		-- This binding is useless if the recursive simplification
+		-- made no progress; but currently we don't try to optimise that
+		-- case.  After all, we only try hard to reduce at top level, or
+		-- when inferring types.
+
+	; let   -- extract Id binders for dicts and CoTyVar binders for eqs;
+                -- see Note [Binders for equalities]
+	      (extra_eq_givens, extra_dict_givens) = partition isEqInst 
+                                                               extra_givens
+              eq_cotvs = map instToVar extra_eq_givens
+	      dict_ids = map instToId  extra_dict_givens 
+
+                        -- Note [Always inline implication constraints]
+              wrap_inline | null dict_ids = idHsWrapper
+                          | otherwise	  = WpInline
+              co         = wrap_inline
+                           <.> mkWpTyLams tvs
+                           <.> mkWpTyLams eq_cotvs
+                           <.> mkWpLams dict_ids
+                           <.> WpLet (binds `unionBags` bind)
+              rhs        = mkLHsWrap co payload
+              loc        = instLocSpan inst_loc
+		             -- wanted equalities are solved by updating their
+                             -- cotv; we don't generate bindings for them
+              dict_bndrs =   map (L loc . HsVar . instToId) 
+                           . filter (not . isEqInst) 
+                           $ wanteds
+              payload    = mkBigLHsTup dict_bndrs
+
+	
+	; traceTc (vcat [text "reduceImplication" <+> ppr name,
+			 ppr simpler_implic_insts,
+			 text "->" <+> ppr rhs])
+	; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
+		  simpler_implic_insts)
+  	} 
+    }
+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
 \end{code}
 
+Note [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be 
+inlined.  And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code.  To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
+
 Note [Freeness and implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's hard to say when an implication constraint can be floated out.  Consider
@@ -1982,12 +2402,29 @@ We can satisfy the (C Int) from the superclass of D, so we don't want
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 
+One more example: the constraint
+	class C a => D a b
+	instance (C a, E c) => E (a,c)
+
+	constraint: forall b. D Int b => E (Int,c)
+
+You might think that the (D Int b) can't possibly contribute
+to solving (E (Int,c)), since the latter mentions 'c'.  But 
+in fact it can, because solving the (E (Int,c)) constraint needs 
+dictionaries
+	C Int, E c
+and the (C Int) can be satisfied from the superclass of (D Int b).
+So we must still not float (E (Int,c)) out.
+
+To think about: special cases for unary type classes?
+
 Note [Pruning the givens in an implication constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are about to form the implication constraint
 	forall tvs.  Eq a => Ord b
 The (Eq a) cannot contribute to the (Ord b), because it has no access to
 the type variable 'b'.  So we could filter out the (Eq a) from the givens.
+But BE CAREFUL of the examples above in [Freeness and implications].
 
 Doing so would be a bit tidier, but all the implication constraints get
 simplified away by the optimiser, so it's no great win.   So I don't take
@@ -2012,10 +2449,10 @@ type ImprovementDone = Bool	-- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsIrred TcId	-- Used for irreducible dictionaries,
+  = IsIrred 		-- Used for irreducible dictionaries,
 			-- which are going to be lambda bound
 
-  | Given TcId 		-- Used for dictionaries for which we have a binding
+  | Given Inst 		-- Used for dictionaries for which we have a binding
 			-- e.g. those "given" in a signature
 
   | Rhs 		-- Used when there is a RHS
@@ -2025,19 +2462,22 @@ data AvailHow
 instance Outputable Avails where
   ppr = pprAvails
 
+pprAvails :: Avails -> SDoc
 pprAvails (Avails imp avails)
-  = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
-	 , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
-			| (inst,avail) <- fmToList avails ])]
+  = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
+	 , nest 2 $ braces $ 
+	   vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
+		| (inst,avail) <- fmToList avails ]]
 
 instance Outputable AvailHow where
     ppr = pprAvail
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
-pprAvail (IsIrred x)	= text "Irred" <+> ppr x
+pprAvail IsIrred	= text "Irred"
 pprAvail (Given x)   	= text "Given" <+> ppr x
-pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs)   = sep [text "Rhs" <+> ppr bs,
+			       nest 2 (ppr rhs)]
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
@@ -2060,18 +2500,15 @@ elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
 
 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
 -- Does improvement
-extendAvails avails@(Avails imp env) inst avail 
+extendAvails avails@(Avails imp env) inst avail
   = do	{ imp1 <- tcImproveOne avails inst	-- Do any improvement
 	; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
 
 availsInsts :: Avails -> [Inst]
 availsInsts (Avails _ avails) = keysFM avails
 
+availsImproved :: Avails -> ImprovementDone
 availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
 \end{code}
 
 Extracting the bindings from a bunch of Avails.
@@ -2080,48 +2517,57 @@ We assume that they'll be wrapped in a big Rec, so that the
 dependency analyser can sort them out later
 
 \begin{code}
+type DoneEnv = FiniteMap Inst [Id]
+-- Tracks which things we have evidence for
+
 extractResults :: Avails
 	       -> [Inst]		-- Wanted
-	       -> TcM (	TcDictBinds, 	-- Bindings
-			[Inst])		-- Irreducible ones
+	       -> TcM (TcDictBinds, 	-- Bindings
+		       [Inst],		-- The insts bound by the bindings
+		       [Inst])		-- Irreducible ones
+			-- Note [Reducing implication constraints]
 
 extractResults (Avails _ avails) wanteds
-  = go avails emptyBag [] wanteds
+  = go emptyBag [] [] emptyFM wanteds
   where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
-	-> TcM (TcDictBinds, [Inst])
-    go avails binds irreds [] 
-      = returnM (binds, irreds)
-
-    go avails binds irreds (w:ws)
+    go	:: TcDictBinds 	-- Bindings for dicts
+	-> [Inst]	-- Bound by the bindings
+	-> [Inst]	-- Irreds
+	-> DoneEnv	-- Has an entry for each inst in the above three sets
+	-> [Inst]	-- Wanted
+	-> TcM (TcDictBinds, [Inst], [Inst])
+    go binds bound_dicts irreds _ [] 
+      = return (binds, bound_dicts, irreds)
+
+    go binds bound_dicts irreds done (w:ws)
+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
+
+      | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+      = if w_id `elem` done_ids then
+	   go binds bound_dicts irreds done ws
+	else
+	   go (add_bind (nlHsVar done_id)) bound_dicts irreds
+	      (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+      | otherwise	-- Not yet done
       = case findAvailEnv avails w of
-	  Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
-			go avails binds irreds ws
-
-	  Just (Given id) 
-		| id == w_id -> go avails binds irreds ws 
-		| otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
-		-- The sought Id can be one of the givens, via a superclass chain
-		-- and then we definitely don't want to generate an x=x binding!
-
-	  Just (IsIrred id) 
-		| id == w_id -> go (add_given avails w) binds 	        (w:irreds) ws
-		| otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
-		-- The add_given handles the case where we want (Ord a, Eq a), and we
-		-- don't want to emit *two* Irreds for Ord a, one via the superclass chain
-		-- This showed up in a dupliated Ord constraint in the error message for 
-		--	test tcfail043
-
-	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
-			     where	
-				new_binds = addBind binds w_id rhs
-      where
-	w_id = instToId w	
+	  Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+		     go binds bound_dicts irreds done ws
 
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
-	-- Don't add the same binding twice
+	  Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
 
-addBind binds id rhs = binds `unionBags` unitBag (L (getSrcSpan id) (VarBind id rhs))
+	  Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
+
+	  Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws 
+		where
+		  g_id = instToId g
+		  binds' | w_id == g_id = binds
+			 | otherwise    = add_bind (nlHsVar g_id)
+      where
+	w_id  = instToId w	
+	done' = addToFM done w [w_id]
+	add_bind rhs = addInstToDictBind binds w rhs
 \end{code}
 
 
@@ -2142,58 +2588,20 @@ addWanted want_scs avails wanted rhs_expr wanteds
   where
     avail = Rhs rhs_expr wanteds
 
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
-	-- Always add superclasses for 'givens'
+addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails
+addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given)
+	-- Conditionally add superclasses for 'givens'
+	-- See Note [Recursive instances and superclases]
 	--
 	-- No ASSERT( not (given `elemAvails` 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
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
-  | isDict given	-- We sometimes have 'given' methods, but they
-			-- are always optional, so we can drop them
-  , let pred = dictPred given
-  , isRefineablePred pred	-- See Note [ImplicInst rigidity]
-  , Just (co, pred) <- refinePred reft pred
-  = do 	{ new_given <- newDictBndr (instLoc given) pred
-	; let rhs = L (instSpan given) $
-		    HsWrap (WpCo co) (HsVar (instToId given))
-	; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
-	; return (new_given:refined_givens, avails) }
-	    -- ToDo: the superclasses of the original given all exist in Avails 
-	    -- so we could really just cast them, but it's more awkward to do,
-	    -- and hopefully the optimiser will spot the duplicated work
-  | otherwise
-  = return (refined_givens, avails)
 \end{code}
 
-Note [ImplicInst rigidity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-	C :: forall ab. (Eq a, Ord b) => b -> T a
-	
-	...(case x of C v -> <body>)...
-
-From the case (where x::T ty) we'll get an implication constraint
-	forall b. (Eq ty, Ord b) => <body-constraints>
-Now suppose <body-constraints> itself has an implication constraint 
-of form
-	forall c. <reft> => <payload>
-Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
-existential, but we probably should not apply it to the (Eq ty) because it may
-be wobbly. Hence the isRigidInst
-
-@Insts@ are ordered by their class/type info, rather than by their
-unique.  This allows the context-reduction mechanism to use standard finite
-maps to do their stuff.  It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
-
 \begin{code}
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
-    	      		         addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
+    	      		         addAvailAndSCs want_scs avails irred IsIrred
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail
@@ -2205,7 +2613,7 @@ addAvailAndSCs want_scs avails inst avail
   where
     is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
 			-- Note: this compares by *type*, not by Unique
-    deps         = findAllDeps (unitVarSet (instToId inst)) avail
+    deps         = findAllDeps (unitVarSet (instToVar inst)) avail
     dep_tys	 = map idType (varSetElems deps)
 
     findAllDeps :: IdSet -> AvailHow -> IdSet
@@ -2214,10 +2622,11 @@ addAvailAndSCs want_scs avails inst avail
     -- 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 find_all so_far kids
-    findAllDeps so_far other	    = so_far
+    findAllDeps so_far _            = so_far
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
+      | isEqInst kid                       = so_far
       | kid_id `elemVarSet` so_far	   = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise			   = so_far'
@@ -2227,7 +2636,7 @@ addAvailAndSCs want_scs avails inst avail
 
 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
 	-- Add all the superclasses of the Inst to Avails
-	-- The first param says "dont do this because the original thing
+	-- The first param says "don't do this because the original thing
 	--	depends on this one, so you'd build a loop"
 	-- Invariant: the Inst is already in Avails.
 
@@ -2238,7 +2647,8 @@ addSCs is_loop avails dict
   where
     (clas, tys) = getDictClassTys dict
     (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = substTheta (zipTopTvSubst tyvars tys) sc_theta
+    sc_theta' = filter (not . isEqPred) $
+                  substTheta (zipTopTvSubst tyvars tys) sc_theta
 
     add_sc avails (sc_dict, sc_sel)
       | is_loop (dictPred sc_dict) = return avails 	-- See Note [SUPERCLASS-LOOP 2]
@@ -2247,14 +2657,41 @@ addSCs is_loop avails dict
 					; addSCs is_loop avails' sc_dict }
       where
 	sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
-	co_fn	   = WpApp (instToId dict) <.> mkWpTyApps tys
+	co_fn	   = WpApp (instToVar dict) <.> mkWpTyApps tys
 
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
 			  Just (Given _) -> True	-- Given is cheaper than superclass selection
-			  other		 -> False	
+			  _              -> False
+
+-- From the a set of insts obtain all equalities that (transitively) occur in
+-- superclass contexts of class constraints (aka the ancestor equalities). 
+--
+ancestorEqualities :: [Inst] -> TcM [Inst]
+ancestorEqualities
+  =   mapM mkWantedEqInst               -- turn only equality predicates..
+    . filter isEqPred                   -- ..into wanted equality insts
+    . bagToList 
+    . addAEsToBag emptyBag              -- collect the superclass constraints..
+    . map dictPred                      -- ..of all predicates in a bag
+    . filter isClassDict
+  where
+    addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
+    addAEsToBag bag []           = bag
+    addAEsToBag bag (pred:preds)
+      | pred `elemBag` bag = addAEsToBag bag         preds
+      | isEqPred pred      = addAEsToBag bagWithPred preds
+      | isClassPred pred   = addAEsToBag bagWithPred predsWithSCs
+      | otherwise          = addAEsToBag bag         preds
+      where
+        bagWithPred  = bag `snocBag` pred
+        predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
+        --
+        (tyvars, sc_theta, _, _) = classBigSig clas
+        (clas, tys) 		 = getClassPredTys pred 
 \end{code}
 
+
 %************************************************************************
 %*									*
 \section{tcSimplifyTop: defaulting}
@@ -2289,13 +2726,18 @@ tcSimplifyInteractive wanteds
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
+tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
 tc_simplify_top doc interactive wanteds
   = do	{ dflags <- getDOpts
-	; wanteds <- mapM zonkInst wanteds
+	; wanteds <- zonkInsts wanteds
 	; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
+	; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
 	; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
-	; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+--	; (irreds1, binds1) <- gentleInferLoop doc1 wanteds
+	; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
+	; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
+	; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
 		-- Use the defaulting rules to do extra unification
 		-- NB: irreds2 are already zonked
@@ -2312,9 +2754,9 @@ tc_simplify_top doc interactive wanteds
 
 	; return (binds1 `unionBags` binds2 `unionBags` binds3) }
   where
-    doc1 = doc <+> ptext SLIT("(first round)")
-    doc2 = doc <+> ptext SLIT("(approximate)")
-    doc3 = doc <+> ptext SLIT("(disambiguate)")
+    doc1 = doc <+> ptext (sLit "(first round)")
+    doc2 = doc <+> ptext (sLit "(approximate)")
+    doc3 = doc <+> ptext (sLit "(disambiguate)")
 \end{code}
 
 If a dictionary constrains a type variable which is
@@ -2358,14 +2800,14 @@ disambiguate doc interactive dflags insts
   = return (insts, emptyBag)
 
   | null defaultable_groups
-  = do	{ traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+  = do	{ traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
 	; return (insts, emptyBag) }
 
   | otherwise
   = do 	{  	-- Figure out what default types to use
 	  default_tys <- getDefaultTys extended_defaulting ovl_strings
 
-	; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+	; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
 	; mapM_ (disambigGroup default_tys) defaultable_groups
 
 	-- disambigGroup does unification, hence try again
@@ -2401,7 +2843,7 @@ disambiguate doc interactive dflags insts
 	| extended_defaulting = any isInteractiveClass clss
 	| otherwise 	      = all is_std_class clss && (any is_num_class clss)
 
- 	-- In interactive mode, or with -fextended-default-rules,
+ 	-- In interactive mode, or with -XExtendedDefaultRules,
 	-- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
 	= is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
@@ -2421,7 +2863,7 @@ disambigGroup :: [Type]			-- The default types
 disambigGroup default_tys dicts
   = try_default default_tys
   where
-    (_,_,tyvar) = head dicts	-- Should be non-empty
+    (_,_,tyvar) = ASSERT(not (null dicts)) head dicts	-- Should be non-empty
     classes = [c | (_,c,_) <- dicts]
 
     try_default [] = return ()
@@ -2436,7 +2878,9 @@ disambigGroup default_tys dicts
 
 		-- After this we can't fail
 	   ; warnDefault dicts default_ty
-	   ; unifyType default_ty (mkTyVarTy tyvar) }
+	   ; unifyType default_ty (mkTyVarTy tyvar) 
+	   ; return () -- TOMDO: do something with the coercion
+	   }
 
 
 -----------------------
@@ -2460,12 +2904,12 @@ getDefaultTys extended_deflts ovl_strings
 		  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]
-    opt_deflt False ty = []
+    opt_deflt False _  = []
 \end{code}
 
 Note [Default unitTy]
 ~~~~~~~~~~~~~~~~~~~~~
-In interative mode (or with -fextended-default-rules) we add () as the first type we
+In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
 try when defaulting.  This has very little real impact, except in the following case.
 Consider: 
 	Text.Printf.printf "hello"
@@ -2512,7 +2956,6 @@ tcSimplifyDeriv :: InstOrigin
 	        -> TcM ThetaType	-- Needed
 -- Given  instance (wanted) => C inst_ty 
 -- Simplify 'wanted' as much as possible
--- The inst_ty is needed only for the termination check
 
 tcSimplifyDeriv orig tyvars theta
   = do	{ (tvs, _, tenv) <- tcInstTyVars tyvars
@@ -2522,19 +2965,22 @@ tcSimplifyDeriv orig tyvars theta
 	; wanteds <- newDictBndrsO orig (substTheta tenv theta)
 	; (irreds, _) <- tryHardCheckLoop doc wanteds
 
+	; let (tv_dicts, others) = partition ok irreds
+	; addNoInstanceErrs others
+	-- See Note [Exotic derived instance contexts] in TcMType
+
 	; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
-	      simpl_theta = substTheta rev_env (map dictPred irreds)
+	      simpl_theta = substTheta rev_env (map dictPred tv_dicts)
 		-- This reverse-mapping is a pain, but the result
 		-- should mention the original TyVars not TcTyVars
 
-	-- NB: the caller will further check the tv_dicts for
-	--     legal instance-declaration form
-
 	; return simpl_theta }
   where
-    doc = ptext SLIT("deriving classes for a data type")
-\end{code}
+    doc = ptext (sLit "deriving classes for a data type")
 
+    ok dict | isDict dict = validDerivPred (dictPred dict)
+	    | otherwise	  = False
+\end{code}
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
@@ -2545,16 +2991,16 @@ whether it worked or not.
 tcSimplifyDefault :: ThetaType	-- Wanted; has no type variables in it
 		  -> TcM ()
 
-tcSimplifyDefault theta
-  = newDictBndrsO DefaultOrigin theta	`thenM` \ wanteds ->
-    tryHardCheckLoop doc wanteds	`thenM` \ (irreds, _) ->
-    addNoInstanceErrs  irreds	 	`thenM_`
+tcSimplifyDefault theta = do
+    wanteds <- newDictBndrsO DefaultOrigin theta
+    (irreds, _) <- tryHardCheckLoop doc wanteds
+    addNoInstanceErrs  irreds
     if null irreds then
-	returnM ()
-    else
-	failM
+	return ()
+     else
+	traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
   where
-    doc = ptext SLIT("default declaration")
+    doc = ptext (sLit "default declaration")
 \end{code}
 
 
@@ -2575,12 +3021,11 @@ groupErrs :: ([Inst] -> TcM ())	-- Deal with one group
 -- Group together insts with the same origin
 -- We want to report them together in error messages
 
-groupErrs report_err [] 
-  = returnM ()
-groupErrs report_err (inst:insts) 
-  = do_one (inst:friends)		`thenM_`
-    groupErrs report_err others
-
+groupErrs _ [] 
+  = return ()
+groupErrs report_err (inst:insts)
+  = do	{ do_one (inst:friends)
+	; groupErrs report_err others }
   where
 	-- (It may seem a bit crude to compare the error messages,
 	--  but it makes sure that we combine just what the user sees,
@@ -2596,7 +3041,7 @@ addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs [] 
+addTopIPErrs _ [] 
   = return ()
 addTopIPErrs bndrs ips
   = do	{ dflags <- getDOpts
@@ -2604,9 +3049,9 @@ addTopIPErrs bndrs ips
   where
     (tidy_env, tidy_ips) = tidyInsts ips
     mk_msg dflags ips 
-	= vcat [sep [ptext SLIT("Implicit parameters escape from"),
-	        nest 2 (ptext SLIT("the monomorphic top-level binding") 
-					    <> plural bndrs <+> ptext SLIT("of")
+	= vcat [sep [ptext (sLit "Implicit parameters escape from"),
+	        nest 2 (ptext (sLit "the monomorphic top-level binding") 
+					    <> plural bndrs <+> ptext (sLit "of")
 					    <+> pprBinders bndrs <> colon)],
 		nest 2 (vcat (map ppr_ip ips)),
 		monomorphism_fix dflags]
@@ -2618,7 +3063,7 @@ topIPErrs dicts
   where
     (tidy_env, tidy_dicts) = tidyInsts dicts
     report dicts = addErrTcM (tidy_env, mk_msg dicts)
-    mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> 
+    mk_msg dicts = addInstLoc dicts (ptext (sLit "Unbound implicit parameter") <> 
 				     plural tidy_dicts <+> pprDictsTheta tidy_dicts)
 
 addNoInstanceErrs :: [Inst]	-- Wanted (can include implications)
@@ -2639,15 +3084,19 @@ reportNoInstances
 reportNoInstances tidy_env mb_what insts 
   = groupErrs (report_no_instances tidy_env mb_what) insts
 
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
 report_no_instances tidy_env mb_what insts
-  = do	{ inst_envs <- tcGetInstEnvs
-	; let (implics, insts1)  = partition isImplicInst insts
-	      (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
-	; traceTc (text "reportNoInstnces" <+> vcat 
-			[ppr implics, ppr insts1, ppr insts2])
-	; mapM_ complain_implic implics
-	; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
-	; groupErrs complain_no_inst insts2 }
+  = do { inst_envs <- tcGetInstEnvs
+       ; let (implics, insts1)  = partition isImplicInst insts
+	     (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
+             (eqInsts, insts3)  = partition isEqInst insts2
+       ; traceTc (text "reportNoInstances" <+> vcat 
+                       [ppr insts, ppr implics, ppr insts1, ppr insts2])
+       ; mapM_ complain_implic implics
+       ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
+       ; groupErrs complain_no_inst insts3 
+       ; mapM_ (addErrTcM . mk_eq_err) eqInsts
+       }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
 
@@ -2663,59 +3112,62 @@ report_no_instances tidy_env mb_what insts
 	| not (isClassDict wanted) = Left wanted
 	| otherwise
 	= case lookupInstEnv inst_envs clas tys of
-		-- 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 "reportNoInstance" (ppr wanted)
-#endif
-		([], _)  -> Left wanted		-- No match
-		res	 -> Right (mk_overlap_msg wanted res)
+		([], _) -> Left wanted		-- No match
+		-- The case of exactly one match and no unifiers means a
+		-- successful lookup.  That can't happen here, because dicts
+		-- only end up here if they didn't match in Inst.lookupInst
+		([_],[])
+		 | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
+		res -> Right (mk_overlap_msg wanted res)
 	  where
 	    (clas,tys) = getDictClassTys wanted
 
     mk_overlap_msg dict (matches, unifiers)
-      = vcat [	addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
+      = ASSERT( not (null matches) )
+        vcat [	addInstLoc [dict] ((ptext (sLit "Overlapping instances for") 
 					<+> pprPred (dictPred dict))),
-    		sep [ptext SLIT("Matching instances") <> colon,
+    		sep [ptext (sLit "Matching instances") <> colon,
     		     nest 2 (vcat [pprInstances ispecs, pprInstances 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") <+>
+		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")])]
+			      ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
+			      ptext (sLit "when compiling the other instance declarations")])]
       where
     	ispecs = [ispec | (ispec, _) <- matches]
 
+    mk_eq_err :: Inst -> (TidyEnv, SDoc)
+    mk_eq_err inst = misMatchMsg tidy_env (eqInstTys inst)
+
     mk_no_inst_err insts
       | null insts = empty
 
       | Just (loc, givens) <- mb_what,   -- Nested (type signatures, instance decls)
 	not (isEmptyVarSet (tyVarsOfInsts insts))
       = vcat [ addInstLoc insts $
-	       sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
-	           , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
+	       sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
+	           , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
 	     , show_fixes (fix1 loc : fixes2) ]
 
       | otherwise	-- Top level 
       = vcat [ addInstLoc insts $
-	       ptext SLIT("No instance") <> plural insts
-		    <+> ptext SLIT("for") <+> pprDictsTheta insts
+	       ptext (sLit "No instance") <> plural insts
+		    <+> ptext (sLit "for") <+> pprDictsTheta insts
 	     , show_fixes fixes2 ]
 
       where
-    	fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts
-				 <+> ptext SLIT("to the context of"),
+    	fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
+				 <+> ptext (sLit "to the context of"),
 			 nest 2 (ppr (instLocOrigin loc)) ]
 			 -- I'm not sure it helps to add the location
-			 -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ]
+			 -- nest 2 (ptext (sLit "at") <+> ppr (instLocSpan loc)) ]
 
     	fixes2 | null instance_dicts = []
-	       | otherwise	     = [sep [ptext SLIT("add an instance declaration for"),
+	       | otherwise	     = [sep [ptext (sLit "add an instance declaration for"),
 				        pprDictsTheta instance_dicts]]
 	instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
 		-- Insts for which it is worth suggesting an adding an instance declaration
@@ -2723,9 +3175,10 @@ report_no_instances tidy_env mb_what insts
 
 	show_fixes :: [SDoc] -> SDoc
 	show_fixes []     = empty
-	show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"), 
-				 nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))]
+	show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
+				 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 
+addTopAmbigErrs :: [Inst] -> TcRn ()
 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
   = ifErrsM (return ()) $	-- Only report ambiguity if no other errors happened
@@ -2739,11 +3192,11 @@ addTopAmbigErrs dicts
     cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
     
     report :: [(Inst,[TcTyVar])] -> TcM ()
-    report pairs@((inst,tvs) : _)	-- The pairs share a common set of ambiguous tyvars
-	= mkMonomorphismMsg tidy_env tvs	`thenM` \ (tidy_env, mono_msg) ->
+    report pairs@((inst,tvs) : _) = do	-- The pairs share a common set of ambiguous tyvars
+	  (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
 	  setSrcSpan (instSpan inst) $
 		-- the location of the first one will do for the err message
-	  addErrTcM (tidy_env, msg $$ mono_msg)
+	   addErrTcM (tidy_env, msg $$ mono_msg)
 	where
 	  dicts = map fst pairs
 	  msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
@@ -2764,47 +3217,46 @@ mkMonomorphismMsg tidy_env inst_tvs
 	; return (tidy_env, mk_msg dflags docs) }
   where
     mk_msg _ _ | any isRuntimeUnk inst_tvs
-        =  vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+        =  vcat [ptext (sLit "Cannot resolve unknown runtime types:") <+>
                    (pprWithCommas ppr inst_tvs),
-                ptext SLIT("Use :print or :force to determine these types")]
-    mk_msg _ []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
+                ptext (sLit "Use :print or :force to determine these types")]
+    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")
 			-- where monomorphism doesn't play any role
     mk_msg dflags docs 
-	= vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
+	= vcat [ptext (sLit "Possible cause: the monomorphism restriction applied to the following:"),
 		nest 2 (vcat docs),
 		monomorphism_fix dflags]
 
-isRuntimeUnk :: TcTyVar -> Bool
-isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
-  = ptext SLIT("Probable fix:") <+> vcat
-	[ptext SLIT("give these definition(s) an explicit type signature"),
+  = ptext (sLit "Probable fix:") <+> vcat
+	[ptext (sLit "give these definition(s) an explicit type signature"),
 	 if dopt Opt_MonomorphismRestriction dflags
-           then ptext SLIT("or use -fno-monomorphism-restriction")
-           else empty]	-- Only suggest adding "-fno-monomorphism-restriction"
+           then ptext (sLit "or use -XNoMonomorphismRestriction")
+           else empty]	-- Only suggest adding "-XNoMonomorphismRestriction"
 			-- if it is not already set!
     
-warnDefault ups default_ty
-  = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
+warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
+warnDefault ups default_ty = do
+    warn_flag <- doptM Opt_WarnTypeDefaults
     addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
   where
     dicts = [d | (d,_,_) <- ups]
 
 	-- Tidy them first
     (_, tidy_dicts) = tidyInsts dicts
-    warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
+    warn_msg  = vcat [ptext (sLit "Defaulting the following constraint(s) to type") <+>
 				quotes (ppr default_ty),
 		      pprDictsInFull tidy_dicts]
 
+reduceDepthErr :: Int -> [Inst] -> SDoc
 reduceDepthErr n stack
-  = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
-	  ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
+  = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
+	  ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
 	  nest 4 (pprStack stack)]
 
+pprStack :: [Inst] -> SDoc
 pprStack stack = vcat (map pprInstInFull stack)
 \end{code}