X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=9ebae019e27310dd9e4074fa6e416f9784b8e22c;hp=b9ff78917e93d3a158c4a9428a0ba70969f67f5e;hb=bb7ffa1642e2110e26e1243c42a8a24adafa985d;hpb=940524aec90652b5ef81789c9a453c57c0e42cc9

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index b9ff789..9ebae01 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,13 +26,15 @@ 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 Name
 import NameSet
@@ -47,11 +51,14 @@ 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)
-
-
------------------------------------------
-
-Choosing Q
-~~~~~~~~~~
-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,31 +651,141 @@ 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
-	      (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
-	; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ ppr (oclose preds gbl_tvs) $$ ppr free $$ ppr bound))
+	; 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 (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
 	; extendLIEs free
 
 		-- To make types simple, reduce as much as possible
-	; let try_me inst = ReduceMe AddSCs
-	; (irreds, binds) <- checkLoop (mkRedEnv doc try_me []) 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
+
+		-- 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
 
-	; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
+		-- Turn the quantified meta-type variables into real type variables
+	; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
 
-	-- We can't abstract over implications
-	; let (dicts, implics) = partition isDict irreds
+		-- We can't abstract over any remaining unsolved 
+		-- implications so instead just float them outwards. Ugh.
+	; let (q_dicts0, implics) = partition isAbstractableInst irreds3
 	; loc <- getInstLoc (ImplicOrigin doc)
-	; implic_bind <- bindIrreds loc qtvs' 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 (qtvs', dicts, binds `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.
+
+approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
+-- Note [Inference and implication constraints]
+-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
+--	- fetching any dicts inside them that are free
+--	- using those dicts as cruder constraints, to solve the implications
+--	- returning the extra ones too
+
+approximateImplications doc want_dict irreds
+  | null extra_dicts 
+  = return (irreds, emptyBag)
+  | otherwise
+  = do	{ extra_dicts' <- mapM cloneDict extra_dicts
+	; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
+		-- By adding extra_dicts', we make them 
+		-- available to solve the implication constraints
+  where 
+    extra_dicts = get_dicts (filter isImplicInst irreds)
+
+    get_dicts :: [Inst] -> [Inst]	-- Returns only Dicts
+	-- Find the wanted constraints in implication constraints that satisfy
+	-- want_dict, and are not bound by forall's in the constraint itself
+    get_dicts ds = concatMap get_dict ds
+
+    get_dict d@(Dict {}) | want_dict d = [d]
+		         | otherwise   = []
+    get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+	= [ 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}
 
+Note [Inference and implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+Suppose we have a wanted implication constraint (perhaps arising from
+a nested pattern match) like
+	C a => D [a]
+and we are now trying to quantify over 'a' when inferring the type for
+a function.  In principle it's possible that there might be an instance
+	instance (C a, E a) => D [a]
+so the context (E a) would suffice.  The Right Thing is to abstract over
+the implication constraint, but we don't do that (a) because it'll be
+surprising to programmers and (b) because we don't have the machinery to deal
+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 get_dicts in approximateImplications.
+
+The common cases are more clear-cut, when we have things like
+	forall a. C a => C b
+Here, abstracting over (C b) is not an approximation at all -- but see
+Note [Freeness and implications].
+ 
+See Trac #1430 and test tc228.
+
+
 \begin{code}
 -----------------------------------------------------------
 -- tcSimplifyInferCheck is used when we know the constraints we are to simplify
@@ -704,7 +800,8 @@ tcSimplifyInferCheck
 		 TcDictBinds)	-- Bindings
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do	{ (irreds, binds) <- innerCheckLoop 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,
@@ -728,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}
 
@@ -785,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}
 
@@ -810,23 +910,23 @@ tcSimplifyCheck	:: InstLoc
 	 	-> TcM TcDictBinds	-- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do	{ (irreds, binds) <- innerCheckLoop 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) <- innerCheckLoop 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) }
 
 -----------------------------------------------------------
@@ -834,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
@@ -861,15 +960,14 @@ 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
@@ -881,52 +979,65 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 -- qtvs includes coercion variables
 --
 -- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
+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 (eq_givens, dict_givens) = partition isEqInst givens
+	      eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
+		-- Urgh! See line 2187 or thereabouts.  I believe that all these
+		-- 'givens' must be a simple CoVar.  This MUST be cleaned up.
+
 	; let name = mkInternalName uniq (mkVarOcc "ic") span
-	      implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+	      implic_inst = ImplicInst { tci_name = name,
 					 tci_tyvars = all_tvs, 
-					 tci_given = givens,
+					 tci_given = (eq_givens ++ dict_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
+	; let   -- only create binder for dict_irreds
+	      (_, dict_irreds) = partition isEqInst irreds
+	      dict_irred_ids = map instToId dict_irreds
+	      lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
 	      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)) }
+	      co  = mkWpApps (map instToId dict_givens)
+		    <.> mkWpTyApps eq_tyvar_cos
+		    <.> 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)) 
+        }
 
 -----------------------------------------------------------
-topCheckLoop :: SDoc
+tryHardCheckLoop :: SDoc
 	     -> [Inst]			-- Wanted
 	     -> TcM ([Inst], TcDictBinds)
 
-topCheckLoop doc wanteds
-  = checkLoop (mkRedEnv doc try_me []) wanteds
+tryHardCheckLoop doc wanteds
+  = do { (irreds,binds) <- checkLoop (mkRedEnv doc try_me []) wanteds
+       ; return (irreds,binds)
+       }
   where
-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe AddSCs
+	-- Here's the try-hard bit
 
 -----------------------------------------------------------
-innerCheckLoop :: InstLoc
+gentleCheckLoop :: InstLoc
 	       -> [Inst]		-- Given
 	       -> [Inst]		-- Wanted
 	       -> TcM ([Inst], TcDictBinds)
 
-innerCheckLoop inst_loc givens wanteds
-  = checkLoop env wanteds
+gentleCheckLoop inst_loc givens wanteds
+  = do { (irreds,binds) <- checkLoop env wanteds
+       ; return (irreds,binds)
+       }
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
@@ -934,6 +1045,16 @@ innerCheckLoop inst_loc givens wanteds
 		| 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 = mkRedEnv doc try_me []
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+		| otherwise	     = Stop
 \end{code}
 
 Note [Check gently]
@@ -957,34 +1078,75 @@ But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
 and methods only, plus common up equal things), deferring the real
 work until top level, when we solve the implication constraint
-with topCheckLooop.
+with tryHardCheckLooop.
 
 
 \begin{code}
 -----------------------------------------------------------
 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 (return ())
+  where go env wanteds elim_skolems
+	  = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+                ; env'     <- zonkRedEnv env
+		; wanteds' <- zonkInsts  wanteds
+	
+		; (improved, binds, irreds, elim_more_skolems)
+                    <- reduceContext env' wanteds'
+                ; let elim_skolems' = elim_skolems >> elim_more_skolems
 
-	; (improved, binds, irreds) <- reduceContext env wanteds'
+		; if not improved then
+	 	    elim_skolems' >> 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 elim_skolems'
+		; 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]
 ~~~~~~~~~~~
@@ -1056,14 +1218,15 @@ tcSimplifySuperClasses
 	-> [Inst]	-- Wanted
 	-> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
-  = do	{ (irreds, binds1) <- checkLoop env 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 topCheckLoop, but with NoSCs
+    try_me _ = ReduceMe NoSCs
+	-- Like tryHardCheckLoop, but with NoSCs
 \end{code}
 
 
@@ -1183,7 +1346,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
@@ -1194,13 +1358,15 @@ 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)
-	; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
+	; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe AddSCs)
+	; (_imp, _binds, constrained_dicts, elim_skolems) 
+            <- reduceContext env wanteds'
+        ; elim_skolems
 
 	-- 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
@@ -1214,9 +1380,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',
@@ -1244,7 +1410,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
 			   (is_nested_group || isDict inst) = Stop
 		          | otherwise  	         = ReduceMe AddSCs
 	      env = mkNoImproveRedEnv doc try_me
-	; (_imp, binds, irreds) <- reduceContext env wanteds'
+	; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+        ; elim_skolems
 
 	-- See "Notes on implicit parameters, Question 4: top level"
 	; ASSERT( all (isFreeWrtTyVars qtvs) irreds )	-- None should be captured
@@ -1334,7 +1501,8 @@ tcSimplifyRuleLhs wanteds
 				 -- to fromInteger; this looks fragile to me
 	     ; lookup_result <- lookupSimpleInst w'
 	     ; case lookup_result of
-		 GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+		 GenInst ws' rhs -> 
+                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
 		 NoInstance	 -> pprPanic "tcSimplifyRuleLhs" (ppr w)
 	  }
 \end{code}
@@ -1349,7 +1517,7 @@ this bracket again at its usage site.
 \begin{code}
 tcSimplifyBracket :: [Inst] -> TcM ()
 tcSimplifyBracket wanteds
-  = do	{ topCheckLoop doc wanteds
+  = do	{ tryHardCheckLoop doc wanteds
 	; return () }
   where
     doc = text "tcSimplifyBracket"
@@ -1387,12 +1555,13 @@ 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'
+	; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+        ; elim_skolems
 
 	; if not improved then 
 		ASSERT( all is_free irreds )
@@ -1446,18 +1615,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)
@@ -1466,8 +1634,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}
 
 
@@ -1508,14 +1674,16 @@ 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_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_stack = (0,[]),
 	     red_improve = True }	
 
 data WhatToDo
@@ -1533,21 +1701,41 @@ 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
 	      -> [Inst]			-- Wanted
 	      -> TcM (ImprovementDone,
 		      TcDictBinds,	-- Dictionary bindings
-		      [Inst])		-- Irreducible
+		      [Inst],		-- Irreducible
+                      TcM ())           -- Undo skolems from SkolemOccurs
 
 reduceContext env wanteds
   = do	{ traceTc (text "reduceContext" <+> (vcat [
@@ -1558,27 +1746,111 @@ reduceContext env wanteds
 	     text "----------------------"
 	     ]))
 
-        -- Build the Avail mapping from "givens"
-	; init_state <- foldlM addGiven emptyAvails (red_givens env)
 
-        -- Do the real work
-	; avails <- reduceList env wanteds init_state
-
-	; let improved = availsImproved avails
-	; (binds, irreds) <- extractResults avails wanteds
+	; let givens 		 	   = red_givens env
+	      (given_eqs0, given_dicts0)   = partition isEqInst givens
+	      (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
+	      (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs
+
+          -- 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 wanted_dicts
+        ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+	; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
+
+	  -- 1. Normalise the *given* *equality* constraints
+	; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
+
+	  -- 2. Normalise the *given* *dictionary* constraints
+	  --    wrt. the toplevel and given equations
+	; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
+                                                            given_dicts0
+
+          -- 5. Build the Avail mapping from "given_dicts"
+	; (init_state, _) <- getLIE $ do 
+		{ init_state <- foldlM addGiven emptyAvails given_dicts
+		; return init_state
+                }
+
+	-- !!! ToDo: what to do with the "extra_givens"?  For the
+	-- moment I'm simply discarding them, which is probably wrong
+
+          -- 6. Solve the *wanted* *dictionary* constraints (not implications)
+	  --    This may expose some further equational constraints...
+	; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+	; (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
+	; let implic_env = env { red_givens = givens ++ bound_dicts 
+                                              ++ dict_irreds }
+	; (implic_binds_s, implic_irreds_s) 
+            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+	; let implic_binds  = unionManyBags implic_binds_s
+	      implic_irreds = concat implic_irreds_s
+
+	  -- Normalise the wanted equality constraints
+	; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
+
+	  -- Normalise the wanted dictionaries
+	; let irreds = dict_irreds ++ implic_irreds
+              eqs    = eq_irreds ++ given_eqs
+	; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds
+		
+	  -- Figure out whether we should go round again.  We do so in either
+          -- two cases:
+          -- (1) If any of the mutable tyvars in givens or irreds has been
+          --     filled in by improvement, there is merit in going around 
+          --     again, because we may make further progress.
+          -- (2) If we managed to normalise any dicts, there is merit in going
+          --     around gain, because reduceList may be able to get further.
+	  -- 
+	  -- ToDo: We may have exposed new
+	  --	   equality constraints and should probably go round again
+	  --	   then as well.  But currently we are dropping them on the
+	  --	   floor anyway.
+
+	; let all_irreds = norm_irreds ++ eq_irreds
+	; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
+		            tyVarsOfInsts (givens ++ all_irreds)
+        ; let improvedDicts = not $ isEmptyBag normalise_binds
+              improved      = improvedMetaTy || improvedDicts
+
+	-- The old plan (fragile)
+	-- improveed   = availsImproved avails 
+	--		 || (not $ isEmptyBag normalise_binds1)
+	--		 || (not $ isEmptyBag normalise_binds2)
+	--		 || (any isEqInst irreds)
 
 	; traceTc (text "reduceContext end" <+> (vcat [
 	     text "----------------------",
 	     red_doc env,
-	     text "given" <+> ppr (red_givens env),
+	     text "given" <+> ppr givens,
+	     text "given_eqs" <+> ppr given_eqs,
 	     text "wanted" <+> ppr wanteds,
+	     text "wanted_dicts" <+> ppr wanted_dicts,
 	     text "----",
 	     text "avails" <+> pprAvails avails,
 	     text "improved =" <+> ppr improved,
+	     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, 
+                  given_binds `unionBags` normalise_binds
+                              `unionBags` dict_binds 
+                              `unionBags` implic_binds, 
+                  all_irreds,
+                  eliminate_skolems) 
+        }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
@@ -1601,22 +1873,25 @@ 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
+  = do	{ traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
+        ; mapM_ unify eqns
 	; return True }
   where
     unify ((qtvs, pairs), what1, what2)
-	 = addErrCtxtM (mkEqnMsg what1 what2)	$
-	   tcInstTyVars (varSetElems qtvs)	`thenM` \ (_, _, tenv) ->
-	   mapM_ (unif_pr tenv) pairs
+         = addErrCtxtM (mkEqnMsg what1 what2) $ do
+           (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+           mapM_ (unif_pr tenv) pairs
     unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
 
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+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"),
+	; 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) }
@@ -1627,13 +1902,11 @@ 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
@@ -1644,37 +1917,41 @@ 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
     -- 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 want_scs -> do	-- It should be reduced
+		{ (avails, lookup_result) <- reduceInst env avails wanted
+		; case lookup_result of
+		    NoInstance -> addIrred want_scs avails wanted
 			     -- Add it and its superclasses
-		    	     addIrred want_scs avails wanted
+		    	     
+		    GenInst [] rhs -> addWanted want_scs 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 want_scs 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)
@@ -1683,7 +1960,7 @@ 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}
 
 
@@ -1774,36 +2051,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)
 
@@ -1817,57 +2107,109 @@ 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
+	--
+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 AddSCs  -- 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
-
-		-- Extract the binding
-	; (binds, irreds) <- extractResults avails wanteds
- 
-		-- 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
-
-	; if isEmptyLHsBinds binds then 	-- No progress
-		return (ret_avails, NoInstance)
+			[ ppr (red_givens env), ppr extra_givens, 
+			  ppr wanteds])
+	; (irreds, binds) <- checkLoop env' wanteds
+	; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
+			-- SLPJ Sept 07: I think this is bogus; currently
+			-- there are no Eqinsts in extra_givens
+		dict_ids = map instToId extra_dict_givens 
+
+		-- Note [Reducing implication constraints]
+		-- Tom -- update note, put somewhere!
+
+	; traceTc (text "reduceImplication result" <+> vcat
+			[ppr irreds, ppr binds])
+
+	; -- extract superclass binds
+	  --  (sc_binds,_) <- extractResults avails []
+-- 	; traceTc (text "reduceImplication sc_binds" <+> vcat
+--			[ppr sc_binds, ppr avails])
+--  
+
+	-- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+	-- Then we must iterate the outer loop too!
+
+	; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+
+--	Progress is no longer measered by the number of bindings
+	; if (isEmptyLHsBinds binds) && (not $ null irreds) then 	-- No progress
+		-- If there are any irreds, we back off and do nothing
+		return (emptyBag, [orig_implic])
 	  else do
-	{ (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft 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	dict_ids = map instToId extra_givens
-		co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
-		rhs = mkHsWrap co payload
+	{ (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	dict_wanteds = filter (not . isEqInst) wanteds
+		-- TOMDO: given equational constraints bug!
+		--  we need a different evidence for given
+		--  equations depending on whether we solve
+		--  dictionary constraints or equational constraints
+
+		eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+			-- SLPJ Sept07: this looks Utterly Wrong to me, but I think
+			--	        that current extra_givens has no EqInsts, so
+			--		it makes no difference
+		co  = wrap_inline	-- Note [Always inline implication constraints]
+		      <.> mkWpTyLams tvs
+		      <.> mkWpLams eq_tyvars
+		      <.> mkWpLams dict_ids
+		      <.> WpLet (binds `unionBags` bind)
+		wrap_inline | null dict_ids = idHsWrapper
+			    | otherwise	    = WpInline
+		rhs = mkLHsWrap co payload
 	        loc = instLocSpan inst_loc
-		payload | isSingleton wanteds = HsVar (instToId (head wanteds))
-			| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
+		payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
 
-		-- If there are any irreds, we back off and return NoInstance
-	; return (ret_avails, GenInst implic_insts (L loc rhs))
-  } }
+	
+	; 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
@@ -1893,12 +2235,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
@@ -1923,10 +2282,10 @@ type ImprovementDone = Bool	-- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsIrred		-- 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
@@ -1936,10 +2295,12 @@ 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
@@ -1948,7 +2309,8 @@ instance Outputable AvailHow where
 pprAvail :: AvailHow -> SDoc
 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
@@ -1971,18 +2333,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 imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
+_availsImproved :: Avails -> ImprovementDone
+_availsImproved (Avails imp _) = imp
 \end{code}
 
 Extracting the bindings from a bunch of Avails.
@@ -1991,43 +2350,54 @@ 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)
+      | 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 IsIrred -> go (add_given avails w) binds (w:irreds) ws
+	  Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+		     go binds bound_dicts irreds done ws
 
-	  Just (Given id) 
-		| id == instToId w
-		-> go avails binds 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 -> go binds bound_dicts (w:irreds) done' ws
 
-		| otherwise
-		-> go avails (addBind binds w (nlHsVar id)) irreds ws
+	  Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
 
-	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
-			     where
-				new_binds = addBind binds w rhs
-
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst) 
-						      (VarBind (instToId inst) rhs))
+	  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}
 
 
@@ -2049,53 +2419,14 @@ addWanted want_scs avails wanted rhs_expr wanteds
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)
 	-- Always add superclasses for 'givens'
 	--
 	-- 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 )
@@ -2111,7 +2442,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
@@ -2120,10 +2451,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'
@@ -2133,7 +2465,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.
 
@@ -2144,7 +2476,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]
@@ -2153,14 +2486,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}
@@ -2195,24 +2555,25 @@ 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	{ wanteds <- mapM zonkInst wanteds
+  = do	{ dflags <- getDOpts
+	; wanteds <- zonkInsts wanteds
 	; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
-	; (irreds1, binds1) <- topCheckLoop doc wanteds
+	; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
+	; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+--	; (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)
 
-	; if null irreds1 then 
-		return binds1
-	  else do
-	-- OK, so there are some errors
-	{	-- Use the defaulting rules to do extra unification
-		-- NB: irreds are already zonked
-	; dflags <- getDOpts
-	; disambiguate interactive dflags irreds1	-- Does unification
-	; (irreds2, binds2) <- topCheckLoop doc irreds1
-
-		-- Deal with implicit parameter
-	; let (bad_ips, non_ips) = partition isIPDict irreds2
+		-- Use the defaulting rules to do extra unification
+		-- NB: irreds2 are already zonked
+	; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
+
+		-- Deal with implicit parameters
+	; let (bad_ips, non_ips) = partition isIPDict irreds3
 	      (ambigs, others)   = partition isTyVarDict non_ips
 
 	; topIPErrs bad_ips	-- Can arise from   f :: Int -> Int
@@ -2220,7 +2581,11 @@ tc_simplify_top doc interactive wanteds
 	; addNoInstanceErrs others
 	; addTopAmbigErrs ambigs	
 
-	; return (binds1 `unionBags` binds2) }}
+	; return (binds1 `unionBags` binds2 `unionBags` binds3) }
+  where
+    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
@@ -2256,26 +2621,40 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambiguate :: Bool -> DynFlags -> [Inst] -> TcM ()
+disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
 	-- Just does unification to fix the default types
 	-- The Insts are assumed to be pre-zonked
-disambiguate interactive dflags insts
+disambiguate doc interactive dflags insts
+  | null insts
+  = return (insts, emptyBag)
+
   | null defaultable_groups
-  = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
-	;     return () }
+  = 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
+	  default_tys <- getDefaultTys extended_defaulting ovl_strings
+
+	; 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
+	; tryHardCheckLoop doc insts }
 
-	; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
-	; mapM_ (disambigGroup default_tys) defaultable_groups  }
   where
    extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
    ovl_strings = dopt Opt_OverloadedStrings dflags
 
-   unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints
-   bad_tvs :: TcTyVarSet	  -- Tyvars mentioned by *other* constraints
-   (unaries, bad_tvs) = getDefaultableDicts insts
+   unaries :: [(Inst, Class, TcTyVar)]  -- (C tv) constraints
+   bad_tvs :: TcTyVarSet  -- Tyvars mentioned by *other* constraints
+   (unaries, bad_tvs_s) = partitionWith find_unary insts 
+   bad_tvs 		= unionVarSets bad_tvs_s
+
+	-- Finds unary type-class constraints
+   find_unary d@(Dict {tci_pred = ClassP cls [ty]})
+	| Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
+   find_unary inst			 = Right (tyVarsOfInst inst)
 
 		-- Group by type variable
    defaultable_groups :: [[(Inst,Class,TcTyVar)]]
@@ -2293,7 +2672,7 @@ disambiguate 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])
@@ -2305,6 +2684,7 @@ disambiguate interactive dflags insts
    is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
 	-- Similarly is_std_class
 
+-----------------------
 disambigGroup :: [Type]			-- The default types
 	      -> [(Inst,Class,TcTyVar)]	-- All standard classes of form (C a)
 	      -> TcM ()	-- Just does unification, to fix the default types
@@ -2312,7 +2692,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 ()
@@ -2327,9 +2707,12 @@ 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
+	   }
 
 
+-----------------------
 getDefaultTys :: Bool -> Bool -> TcM [Type]
 getDefaultTys extended_deflts ovl_strings
   = do	{ mb_defaults <- getDeclaredDefaultTys
@@ -2350,12 +2733,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"
@@ -2402,7 +2785,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
@@ -2410,21 +2792,24 @@ tcSimplifyDeriv orig tyvars theta
 	-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
 	-- ToDo: what if two of them do get unified?
 	; wanteds <- newDictBndrsO orig (substTheta tenv theta)
-	; (irreds, _) <- topCheckLoop doc wanteds
+	; (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;
@@ -2435,16 +2820,16 @@ whether it worked or not.
 tcSimplifyDefault :: ThetaType	-- Wanted; has no type variables in it
 		  -> TcM ()
 
-tcSimplifyDefault theta
-  = newDictBndrsO DefaultOrigin theta	`thenM` \ wanteds ->
-    topCheckLoop 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}
 
 
@@ -2465,12 +2850,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,
@@ -2486,18 +2870,20 @@ addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs [] 
+addTopIPErrs _ [] 
   = return ()
 addTopIPErrs bndrs ips
-  = addErrTcM (tidy_env, mk_msg tidy_ips)
+  = do	{ dflags <- getDOpts
+	; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
   where
     (tidy_env, tidy_ips) = tidyInsts ips
-    mk_msg ips = vcat [sep [ptext SLIT("Implicit parameters escape from"),
-			    nest 2 (ptext SLIT("the monomorphic top-level binding") 
-					    <> plural bndrs <+> ptext SLIT("of")
+    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")
 					    <+> pprBinders bndrs <> colon)],
-		       nest 2 (vcat (map ppr_ip ips)),
-		       monomorphism_fix]
+		nest 2 (vcat (map ppr_ip ips)),
+		monomorphism_fix dflags]
     ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
 
 topIPErrs :: [Inst] -> TcM ()
@@ -2506,7 +2892,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)
@@ -2527,15 +2913,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)
 
@@ -2551,59 +2941,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
@@ -2611,9 +3004,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
@@ -2627,11 +3021,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 <+> 
@@ -2647,47 +3041,51 @@ mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
 -- Try to identify the offending variable
 -- ASSUMPTION: the Insts are fully zonked
 mkMonomorphismMsg tidy_env inst_tvs
-  = findGlobals (mkVarSet inst_tvs) tidy_env	`thenM` \ (tidy_env, docs) ->
-    returnM (tidy_env, mk_msg docs)
+  = do	{ dflags <- getDOpts
+	; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
+	; return (tidy_env, mk_msg dflags docs) }
   where
-    mk_msg _ | any isRuntimeUnk inst_tvs
-        =  vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
+    mk_msg _ _ | any isRuntimeUnk inst_tvs
+        =  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 docs = vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
-			nest 2 (vcat docs),
-			monomorphism_fix
-		       ]
-
-isRuntimeUnk :: TcTyVar -> Bool
-isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
-monomorphism_fix :: SDoc
-monomorphism_fix = ptext SLIT("Probable fix:") <+> 
-		   (ptext SLIT("give these definition(s) an explicit type signature")
-		    $$ ptext SLIT("or use -fno-monomorphism-restriction"))
+    mk_msg dflags docs 
+	= vcat [ptext (sLit "Possible cause: the monomorphism restriction applied to the following:"),
+		nest 2 (vcat docs),
+		monomorphism_fix dflags]
+
+monomorphism_fix :: DynFlags -> SDoc
+monomorphism_fix dflags
+  = 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 -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}