Comments only
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index f2ad101..534c5d0 100644 (file)
@@ -6,13 +6,6 @@
 TcSimplify
 
 \begin{code}
 TcSimplify
 
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
@@ -22,7 +15,7 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
-       bindInstsOfLocalFuns, bindIrreds,
+       bindInstsOfLocalFuns, 
 
         misMatchMsg
     ) where
 
         misMatchMsg
     ) where
@@ -33,16 +26,17 @@ import {-# SOURCE #-} TcUnify( unifyType )
 import HsSyn
 
 import TcRnMonad
 import HsSyn
 
 import TcRnMonad
+import TcHsSyn ( hsLPatType )
 import Inst
 import TcEnv
 import InstEnv
 import Inst
 import TcEnv
 import InstEnv
-import TcGadt
 import TcType
 import TcMType
 import TcIface
 import TcTyFuns
 import TcType
 import TcMType
 import TcIface
 import TcTyFuns
-import TypeRep
+import DsUtils -- Big-tuple functions
 import Var
 import Var
+import Id
 import Name
 import NameSet
 import Class
 import Name
 import NameSet
 import Class
@@ -55,17 +49,16 @@ import ErrUtils
 import BasicTypes
 import VarSet
 import VarEnv
 import BasicTypes
 import VarSet
 import VarEnv
-import Module
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
-import UniqSet
 import SrcLoc
 import DynFlags
 import SrcLoc
 import DynFlags
-
+import FastString
+import Control.Monad
 import Data.List
 \end{code}
 
 import Data.List
 \end{code}
 
@@ -98,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:
 
 
 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:
 
 
 The trouble is that to type (runFoo foo), GHC has to solve the problem:
 
@@ -411,14 +406,19 @@ over implicit parameters. See the predicate isFreeWhenInferring.
 
 Note [Implicit parameters and ambiguity] 
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 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'.
 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'.
@@ -652,7 +652,7 @@ tcSimplifyInfer
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted
   = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 \begin{code}
 tcSimplifyInfer doc tau_tvs wanted
   = do { tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
-       ; wanted'  <- mappM zonkInst wanted     -- Zonk before deciding quantified tyvars
+       ; wanted'  <- mapM zonkInst wanted      -- Zonk before deciding quantified tyvars
        ; gbl_tvs  <- tcGetGlobalTyVars
        ; let preds1   = fdPredsOfInsts wanted'
              gbl_tvs1 = oclose preds1 gbl_tvs
        ; gbl_tvs  <- tcGetGlobalTyVars
        ; let preds1   = fdPredsOfInsts wanted'
              gbl_tvs1 = oclose preds1 gbl_tvs
@@ -721,7 +721,7 @@ tcSimplifyInfer doc tau_tvs wanted
 
                -- Prepare equality instances for quantification
        ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
 
                -- Prepare equality instances for quantification
        ; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
-       ; q_eqs <- mappM finalizeEqInst q_eqs0
+       ; q_eqs <- mapM finalizeEqInst q_eqs0
 
        ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
        -- NB: when we are done, we might have some bindings, but
 
        ; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
        -- NB: when we are done, we might have some bindings, but
@@ -776,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
 
 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_dictsin approximateImplications.
+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
 
 The common cases are more clear-cut, when we have things like
        forall a. C a => C b
@@ -801,7 +801,7 @@ tcSimplifyInferCheck
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
   = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
   = do { traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
-       ; (irreds, binds) <- gentleCheckLoop loc givens 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,
 
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
@@ -883,7 +883,9 @@ isFreeWhenChecking qtvs ips inst
   && isFreeWrtIPs    ips inst
 -}
 
   && isFreeWrtIPs    ips inst
 -}
 
+isFreeWrtTyVars :: VarSet -> Inst -> Bool
 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
+isFreeWrtIPs :: NameSet -> Inst -> Bool
 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 
 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 
@@ -916,17 +918,15 @@ tcSimplifyCheck loc qtvs givens wanteds
 -----------------------------------------------------------
 -- tcSimplifyCheckPat is used for existential pattern match
 tcSimplifyCheckPat :: InstLoc
 -----------------------------------------------------------
 -- tcSimplifyCheckPat is used for existential pattern match
 tcSimplifyCheckPat :: InstLoc
-                  -> [CoVar] -> Refinement
                   -> [TcTyVar]         -- Quantify over these
                   -> [Inst]            -- Given
                   -> [Inst]            -- Wanted
                   -> TcM TcDictBinds   -- Bindings
                   -> [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 { traceTc (text "tcSimplifyCheckPat")
        ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
     do { traceTc (text "tcSimplifyCheckPat")
        ; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-       ; implic_bind <- bindIrredsR loc qtvs co_vars reft 
-                                   givens irreds
+       ; implic_bind <- bindIrredsR loc qtvs givens irreds
        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
        ; return (binds `unionBags` implic_bind) }
 
 -----------------------------------------------------------
@@ -934,26 +934,25 @@ bindIrreds :: InstLoc -> [TcTyVar]
           -> [Inst] -> [Inst]
           -> TcM TcDictBinds
 bindIrreds loc qtvs givens irreds 
           -> [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
 -- 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
   | 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]
 
                -- 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]
           -- 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
                     then do
                        { let qtv_set = mkVarSet qtvs
                              (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
@@ -961,28 +960,28 @@ bindIrredsR loc qtvs co_vars reft givens irreds
                        ; return real_irreds }
                     else return 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 } 
 
 
                        -- 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
                    -> [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
 -- 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
 --
 -- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
-                   givens      -- Guaranteed all Dicts (TOMDO: true?)
+makeImplicationBind loc all_tvs
+                   givens      -- Guaranteed all Dicts or EqInsts
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
@@ -990,27 +989,41 @@ makeImplicationBind loc all_tvs reft
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
        ; let (eq_givens, dict_givens) = partition isEqInst givens
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
        ; let (eq_givens, dict_givens) = partition isEqInst givens
-             eq_tyvar_cos =  map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
-       ; let name = mkInternalName uniq (mkVarOcc "ic") span
-             implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+
+                -- 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 = (eq_givens ++ dict_givens),
                                         tci_tyvars = all_tvs, 
                                         tci_given = (eq_givens ++ dict_givens),
-                                        tci_wanted = irreds, tci_loc = loc }
-       ; let   -- only create binder for dict_irreds
-             (eq_irreds, dict_irreds) = partition isEqInst irreds
-              n_dict_irreds = length dict_irreds
+                                                       -- 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
              dict_irred_ids = map instToId dict_irreds
-             tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
-             pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
-             rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-             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 = L span pat, 
-                                                 pat_rhs = unguardedGRHSs rhs, 
-                                                 pat_rhs_ty = tup_ty,
-                                                 bind_fvs = placeHolderNames }
-       ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
-         return ([implic_inst], unitBag (L span bind)) }
+             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
 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc
@@ -1018,11 +1031,11 @@ tryHardCheckLoop :: SDoc
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
             -> TcM ([Inst], TcDictBinds)
 
 tryHardCheckLoop doc wanteds
-  = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
+  = do { (irreds,binds) <- checkLoop (mkInferRedEnv doc try_me) wanteds
        ; return (irreds,binds)
        }
   where
        ; return (irreds,binds)
        }
   where
-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe
        -- Here's the try-hard bit
 
 -----------------------------------------------------------
        -- Here's the try-hard bit
 
 -----------------------------------------------------------
@@ -1032,16 +1045,26 @@ gentleCheckLoop :: InstLoc
               -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
               -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
-  = do { (irreds,binds,_) <- checkLoop env wanteds
+  = do { (irreds,binds) <- checkLoop env wanteds
        ; return (irreds,binds)
        }
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
 
        ; 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]
                | 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]
 \end{code}
 
 Note [Check gently]
@@ -1059,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]
 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
        
 But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
@@ -1072,34 +1095,67 @@ with tryHardCheckLooop.
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
 -----------------------------------------------------------
 checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
-         -> TcM ([Inst], TcDictBinds,
-                 [Inst])               -- needed givens
+         -> TcM ([Inst], TcDictBinds) 
 -- Precondition: givens are completely rigid
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
 -- Precondition: givens are completely rigid
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
-  = go env wanteds []
-  where go env wanteds needed_givens
-         = do { -- Givens are skolems, so no need to zonk them
-                wanteds' <- zonkInsts 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, more_needed_givens) <- reduceContext env wanteds'
+               ; (improved, binds, irreds) <- reduceContext env' wanteds'
 
 
-               ; let all_needed_givens = needed_givens ++ more_needed_givens
-       
-               ; if not improved then
-                    return (irreds, binds, all_needed_givens)
+               ; 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
                  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, all_needed_givens1) <- go env irreds all_needed_givens
-               ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
+               -- 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}
 
 \end{code}
 
+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.
+
+
 Note [LOOP]
 ~~~~~~~~~~~
        class If b t e r | b t e -> r
 Note [LOOP]
 ~~~~~~~~~~~
        class If b t e r | b t e -> r
@@ -1155,30 +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.
        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
 
 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}
 \begin{code}
-tcSimplifySuperClasses 
+tcSimplifySuperClasses
        :: InstLoc 
        :: InstLoc 
+       -> Inst         -- The dict whose superclasses 
+                       -- are being figured out
        -> [Inst]       -- Given 
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
        -> [Inst]       -- Given 
        -> [Inst]       -- Wanted
        -> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
+tcSimplifySuperClasses loc this givens sc_wanteds
   = do { traceTc (text "tcSimplifySuperClasses")
   = do { traceTc (text "tcSimplifySuperClasses")
-       ; (irreds,binds1,_) <- checkLoop env sc_wanteds
+       ; (irreds,binds1) <- checkLoop env sc_wanteds
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
        ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
        ; return binds1 }
   where
        ; 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}
 
 
 \end{code}
 
 
@@ -1310,8 +1423,8 @@ 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
        -- 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)
+       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
@@ -1330,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))
        -- 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',
 
        ; traceTc (text "tcSimplifyRestricted" <+> vcat [
                pprInsts wanteds, pprInsts constrained_dicts',
@@ -1358,9 +1471,9 @@ 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
        ; 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
              env = mkNoImproveRedEnv doc try_me
-       ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
+       ; (_imp, binds, irreds) <- reduceContext env wanteds'
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
@@ -1433,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
 
 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
 
 \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
   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
        | 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
        | 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 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
 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
@@ -1508,14 +1650,22 @@ tcSimplifyIPs given_ips wanteds
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me 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) <- reduceContext env wanteds'
 
 
-       ; if not improved then 
+       ; if null irreds || not improved then 
                ASSERT( all is_free irreds )
                do { extendLIEs irreds
                   ; return binds }
                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)
   where
     doc           = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)
@@ -1523,7 +1673,7 @@ tcSimplifyIPs given_ips wanteds
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop
 
        -- Simplify any methods that mention the implicit parameter
     try_me inst | is_free inst = Stop
-               | otherwise    = ReduceMe NoSCs
+               | otherwise    = ReduceMe
 \end{code}
 
 
 \end{code}
 
 
@@ -1562,18 +1712,17 @@ bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
 -- arguably a bug in Match.tidyEqnInfo (see notes there)
 
 bindInstsOfLocalFuns wanteds local_ids
 -- arguably a bug in Match.tidyEqnInfo (see notes there)
 
 bindInstsOfLocalFuns wanteds local_ids
-  | null overloaded_ids
+  | null overloaded_ids = do
        -- Common case
        -- Common case
-  = extendLIEs wanteds         `thenM_`
-    returnM emptyLHsBinds
+    extendLIEs wanteds
+    return emptyLHsBinds
 
   | otherwise
 
   | otherwise
-  = do { (irreds, binds,_) <- checkLoop env for_me
+  = do { (irreds, binds) <- gentleInferLoop doc for_me
        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }
   where
        ; 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)
     doc                     = text "bindInsts" <+> ppr local_ids
     overloaded_ids   = filter is_overloaded local_ids
     is_overloaded id = isOverloadedTy (idType id)
@@ -1582,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
     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}
 
 
 \end{code}
 
 
@@ -1601,8 +1748,11 @@ data RedEnv
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid
           , 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]
                                                -- 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]
   }
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
@@ -1624,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,
 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_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
             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
 
  | Stop                -- Return as irreducible unless it can
                        -- be reduced to a constant in one step
@@ -1649,6 +1812,12 @@ 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]
                                -- 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}
 
 
 \end{code}
 
 
@@ -1676,93 +1845,109 @@ reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
-                     [Inst],           -- Irreducible
-                     [Inst])           -- Needed givens
+                     [Inst])           -- Irreducible
 
 
-reduceContext env wanteds
+reduceContext env wanteds0
   = do { traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr (red_givens env),
   = do { traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr (red_givens env),
-            text "wanted" <+> ppr wanteds,
+            text "wanted" <+> ppr wanteds0,
             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 
-       ; let givens                      = red_givens env
-             (given_eqs0, given_dicts0)  = partition isEqInst givens
-             (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
-
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]
           -- 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
+       ; ancestor_eqs <- ancestorEqualities wanteds0
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
-         -- 1. Normalise the *given* *equality* constraints
-       ; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
-
-         -- 2. Normalise the *given* *dictionary* constraints
-         --    wrt. the toplevel and given equations
-       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs 
-                                                            given_dicts0
-
-         -- 3. Solve the *wanted* *equation* constraints
-       ; eq_irreds0 <- solveWanteds given_eqs wanted_eqs 
-
-         -- 4. Normalise the *wanted* equality constraints with respect to
-         --    each other 
-       ; eq_irreds <- normaliseWanteds eq_irreds0
-
-          -- 5. Build the Avail mapping from "given_dicts"
-       ; init_state <- foldlM addGiven emptyAvails given_dicts
-
-          -- 6. Solve the *wanted* *dictionary* constraints
-         --    This may expose some further equational constraints...
-       ; wanted_dicts' <- zonkInsts wanted_dicts
-       ; avails <- reduceList env wanted_dicts' init_state
-       ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
-       ; traceTc $ text "reduceContext extractresults" <+> vcat
-                     [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
-
-         -- 7. Normalise the *wanted* *dictionary* constraints
-         --    wrt. the toplevel and given equations
-       ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
-
-         -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
-       ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
-               
-         -- 9. eliminate the artificial skolem constants introduced in 1.
-       ; eliminate_skolems     
-
-         -- If there was some FD improvement,
-         -- or new wanted equations have been exposed,
-         -- we should have another go at solving.
-       ; let improved = availsImproved avails 
-                        || (not $ isEmptyBag normalise_binds1)
-                        || (not $ isEmptyBag normalise_binds2)
-                        || (any isEqInst irreds)
+          -- 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,
 
        ; 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 "----",
             text "avails" <+> pprAvails avails,
-            text "improved =" <+> ppr improved,
-            text "irreds = " <+> ppr irreds,
-            text "binds = " <+> ppr binds,
-            text "needed givens = " <+> ppr needed_givens,
+            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, 
             text "----------------------"
             ]))
 
        ; return (improved, 
-                  given_binds `unionBags` normalise_binds1 
-                              `unionBags` normalise_binds2 
-                              `unionBags` binds, 
-                  irreds ++ eq_irreds, 
-                  needed_givens) 
+                  normalise_binds `unionBags` dict_binds 
+                                  `unionBags` implic_binds, 
+                  all_irreds) 
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
@@ -1777,84 +1962,140 @@ 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)
                -- 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 }
 
        ; 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
          -> 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)
   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
+                }
+
+    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)]
+    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
 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}
 
                          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
 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))))
                             2 (ifPprDebug (nest 2 (pprStack stk))))
-         else return ()
-#endif
        ; if n >= ctxtStkDepth dopts then
            failWithTc (reduceDepthErr n stk)
          else
            go wanteds state }
   where
     go []     state = return state
        ; if n >= ctxtStkDepth dopts then
            failWithTc (reduceDepthErr n stk)
          else
            go wanteds state }
   where
     go []     state = return state
-    go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
-                        ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
+    go (w:ws) state = do { state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
                         ; go ws state' }
 
     -- Base case: we're done!
                         ; go ws state' }
 
     -- Base case: we're done!
+reduce :: RedEnv -> Inst -> Avails -> TcM Avails
 reduce env wanted 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
     -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- findAvail avails wanted
+  | Just _ <- findAvail avails wanted
   = do { traceTc (text "reduce: found " <+> ppr wanted)
   = do { traceTc (text "reduce: found " <+> ppr wanted)
-       ; returnM avails        
+       ; return avails
        }
 
   | otherwise
        }
 
   | otherwise
-  = do { traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
+  = 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]
 
        ; 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
+           ReduceMe -> do      -- It should be reduced
                { (avails, lookup_result) <- reduceInst env avails wanted
                ; case lookup_result of
                { (avails, lookup_result) <- reduceInst env avails wanted
                ; case lookup_result of
-                   NoInstance -> addIrred want_scs avails wanted
+                   NoInstance -> addIrred AddSCs avails wanted
                             -- Add it and its superclasses
                             
                             -- Add it and its superclasses
                             
-                   GenInst [] rhs -> addWanted want_scs avails wanted rhs []
+                   GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
 
 
-                   GenInst wanteds' rhs 
+                   GenInst wanteds' rhs
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
-                               ; addWanted want_scs avails2 wanted rhs wanteds' } }
+                               ; 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
                -- 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
@@ -1872,14 +2113,50 @@ reduce env wanted avails
       = do { res <- lookupSimpleInst wanted
           ; case res of
                GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
       = 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}
 
 
 \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]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 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 ...
 
        class Ord a => C a where
        instance Ord [a] => C [a] where ...
@@ -1917,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.
 
 
 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.
-       
 
 %************************************************************************
 %*                                                                     *
 
 %************************************************************************
 %*                                                                     *
@@ -1963,11 +2204,7 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
 \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}
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}
@@ -1975,7 +2212,7 @@ reduceInst env avails other_inst
 Note [Equational Constraints in Implication Constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Equational Constraints in Implication Constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-An equational constraint is of the form 
+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
        Given => Wanted 
 where Given and Wanted may contain both equational and dictionary
 constraints. The delay and reduction of these two kinds of constraints
@@ -2000,24 +2237,16 @@ which are types.
 \begin{code}
 ---------------------------------------------
 reduceImplication :: RedEnv
 \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
 \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
 
 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)
 
        e.g.    forall {}. Eq a => Eq [a]
                forall {}. C Int => D (Tree Int)
 
@@ -2033,45 +2262,46 @@ Note that
        --
        -- Note on coercion variables:
        --
        --
        -- Note on coercion variables:
        --
-       --      The extra given coercion variables are bound at two different sites:
+       --      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
        --      -) 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               
+       --              the solved dictionaries use these binders;
        --              these binders are generated by reduceImplication
        --
        --              these binders are generated by reduceImplication
        --
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
-  = do {       -- Add refined givens, and the extra givens
-               -- Todo fix this 
-         (refined_red_givens,refined_avails)
-               <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
-                  else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
-
-               -- Solve the sub-problem
-       ; let try_me inst = ReduceMe AddSCs     -- Note [Freeness and implications]
-             env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
+        -- 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
                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat
-                       [ ppr orig_avails,
-                         ppr (red_givens env), ppr extra_givens, 
-                         ppr reft, ppr wanteds])
-       ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
-        ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens]
-
-               -- Note [Reducing implication constraints]
-               -- Tom -- update note, put somewhere!
+                       [ ppr (red_givens env), ppr extra_givens, 
+                         ppr wanteds])
+       ; (irreds, binds) <- checkLoop env' wanteds
 
        ; traceTc (text "reduceImplication result" <+> vcat
 
        ; traceTc (text "reduceImplication result" <+> vcat
-                       [ppr irreds, ppr binds, ppr needed_givens1])
---     ; avails <- reduceList env' wanteds avails
--- 
---             -- Extract the binding
---     ; (binds, irreds) <- extractResults avails wanteds
-       ; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1
-       ; traceTc (text "reduceImplication local results" <+> vcat
-                       [ppr refinement_binds, ppr needed_givens])
+                       [ppr irreds, ppr binds])
 
        ; -- extract superclass binds
          --  (sc_binds,_) <- extractResults avails []
 
        ; -- extract superclass binds
          --  (sc_binds,_) <- extractResults avails []
@@ -2079,76 +2309,73 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
 --                     [ppr sc_binds, ppr avails])
 --  
 
 --                     [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 = avails
-       ; let ret_avails = orig_avails
---     ; 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!
+
+        ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+                                   -- we solve wanted eqs by side effect!
 
 
-       ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
+            -- 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
 
 
---     Porgress is no longer measered by the number of bindings
---     ; if isEmptyLHsBinds binds then         -- No progress
-       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then 
-               return (ret_avails, NoInstance)
+       ; if backOff then       -- No progress
+               return (emptyBag, [orig_implic])
          else do
          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_wanteds = filter (not . isEqInst) wanteds
-               (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-               dict_ids = map instToId extra_dict_givens 
-               -- 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 = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
-               -- dict_ids = map instToId extra_givens
-               co  = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_binds `unionBags` bind)
-               rhs = mkHsWrap co payload
-               loc = instLocSpan inst_loc
-               payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
-                       | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
+       { (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 (text "reduceImplication ->"  <+> vcat
-                       [ ppr ret_avails,
-                         ppr implic_insts])
-               -- If there are any irreds, we back off and return NoInstance
-       ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (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}
 
 \end{code}
 
-Note [Reducing implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are trying to simplify
-       (Ord a, forall b. C a b => (W [a] b, D c b))
-where
-       instance (C a b, Ord a) => W [a] b
-When solving the implication constraint, we'll start with
-       Ord a -> Irred
-in the Avails.  Then we add (C a b -> Given) and solve. Extracting
-the results gives us a binding for the (W [a] b), with an Irred of 
-(Ord a, D c b).  Now, the (Ord a) comes from "outside" the implication,
-but the (D d b) is from "inside".  So we want to generate a Rhs binding
-like this
-
-       ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
-          depending on
-               do :: Ord a
-               ic' :: forall b. C a b => D c b
-
-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
-
-The "inside" and "outside" distinction is what's going on with 'inner' and
-'outer' in reduceImplication
-
+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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 Note [Freeness and implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2175,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!
 
 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.
 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
 
 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
@@ -2208,7 +2452,7 @@ data AvailHow
   = IsIrred            -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
   = 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
                        -- e.g. those "given" in a signature
 
   | Rhs                -- Used when there is a RHS
@@ -2218,10 +2462,12 @@ data AvailHow
 instance Outputable Avails where
   ppr = pprAvails
 
 instance Outputable Avails where
   ppr = pprAvails
 
+pprAvails :: Avails -> SDoc
 pprAvails (Avails imp avails)
 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
 
 instance Outputable AvailHow where
     ppr = pprAvail
@@ -2230,7 +2476,8 @@ instance Outputable AvailHow where
 pprAvail :: AvailHow -> SDoc
 pprAvail IsIrred       = text "Irred"
 pprAvail (Given x)     = text "Given" <+> ppr x
 pprAvail :: AvailHow -> SDoc
 pprAvail IsIrred       = text "Irred"
 pprAvail (Given x)     = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs)   = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
+pprAvail (Rhs rhs bs)   = sep [text "Rhs" <+> ppr bs,
+                              nest 2 (ppr rhs)]
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
@@ -2253,18 +2500,15 @@ elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
 
 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
 -- Does improvement
 
 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
 
   = 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
 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.
 \end{code}
 
 Extracting the bindings from a bunch of Avails.
@@ -2273,81 +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}
 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
 extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst],         -- Irreducible ones
-                       [Inst])         -- Needed givens, i.e. ones used in the bindings
+              -> TcM (TcDictBinds,     -- Bindings
+                      [Inst],          -- The insts bound by the bindings
+                      [Inst])          -- Irreducible ones
+                       -- Note [Reducing implication constraints]
 
 extractResults (Avails _ avails) wanteds
 
 extractResults (Avails _ avails) wanteds
-  = go avails emptyBag [] [] wanteds
+  = go emptyBag [] [] emptyFM wanteds
   where
   where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
+    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])
        -> TcM (TcDictBinds, [Inst], [Inst])
-    go avails binds irreds givens [] 
-      = returnM (binds, irreds, givens)
-
-    go avails binds irreds givens (w:ws)
-      = case findAvailEnv avails w of
-         Nothing -> pprTrace "Urk: extractResults" (ppr w) $
-                    go avails binds irreds givens ws
-
-         Just (Given id) 
-               | id == w_id -> go avails binds irreds (w:givens) ws 
-               | otherwise  -> go avails (addBind binds w (nlHsVar id)) irreds (update_id w  id:givens) 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 (add_given avails w) binds (w:irreds) givens 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 givens (ws' ++ ws)
-                            where      
-                               new_binds = addBind binds w rhs
-      where
-       w_id = instToId w       
-       update_id m@(Method{}) id = m {tci_id = id}
-        update_id w            id = w {tci_name = idName id} 
-
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
+    go binds bound_dicts irreds _ [] 
+      = return (binds, bound_dicts, irreds)
 
 
-extractLocalResults :: Avails
-              -> [Inst]                -- Wanted
-              -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst])         -- Needed givens, i.e. ones used in the bindings
+    go binds bound_dicts irreds done (w:ws)
+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
 
 
-extractLocalResults (Avails _ avails) wanteds
-  = go avails emptyBag [] wanteds
-  where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
-       -> TcM (TcDictBinds, [Inst])
-    go avails binds givens [] 
-      = returnM (binds, givens)
+      | 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
 
 
-    go avails binds givens (w:ws)
+      | otherwise      -- Not yet done
       = case findAvailEnv avails w of
       = case findAvailEnv avails w of
-         Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
-                    go avails binds givens ws
+         Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+                    go binds bound_dicts irreds done ws
 
 
-         Just IsIrred ->
-                    go avails binds givens ws
+         Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
 
 
-         Just (Given id) 
-               | id == w_id -> go avails binds (w:givens) ws 
-               | otherwise  -> go avails binds (w{tci_name=idName id}:givens) 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 (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 givens (ws' ++ ws)
-                            where      
-                               new_binds = addBind binds w 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
       where
-       w_id = instToId w       
-
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
+       w_id  = instToId w      
+       done' = addToFM done w [w_id]
+       add_bind rhs = addInstToDictBind binds w rhs
 \end{code}
 
 
 \end{code}
 
 
@@ -2368,54 +2588,16 @@ addWanted want_scs avails wanted rhs_expr wanteds
   where
     avail = Rhs 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
        --
        -- 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}
 
 \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 )
 \begin{code}
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
@@ -2440,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
     -- 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
 
     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'
       | kid_id `elemVarSet` so_far        = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise                         = so_far'
@@ -2453,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
 
 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.
 
        --      depends on this one, so you'd build a loop"
        -- Invariant: the Inst is already in Avails.
 
@@ -2479,7 +2662,7 @@ addSCs is_loop avails dict
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection
     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). 
 
 -- From the a set of insts obtain all equalities that (transitively) occur in
 -- superclass contexts of class constraints (aka the ancestor equalities). 
@@ -2543,15 +2726,17 @@ tcSimplifyInteractive wanteds
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
 
 -- 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
 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
-       ; wanteds <- zonkInsts wanteds
+       ; wanteds <- zonkInsts wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
        ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts 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)
        ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
-       ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
+       ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification
@@ -2569,9 +2754,9 @@ tc_simplify_top doc interactive wanteds
 
        ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
   where
 
        ; 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
 \end{code}
 
 If a dictionary constrains a type variable which is
@@ -2658,7 +2843,7 @@ disambiguate doc interactive dflags insts
        | extended_defaulting = any isInteractiveClass clss
        | otherwise           = all is_std_class clss && (any is_num_class clss)
 
        | 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])
        -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
@@ -2719,12 +2904,12 @@ getDefaultTys extended_deflts ovl_strings
                  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]
                  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]
-    opt_deflt False ty = []
+    opt_deflt False _  = []
 \end{code}
 
 Note [Default unitTy]
 ~~~~~~~~~~~~~~~~~~~~~
 \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"
 try when defaulting.  This has very little real impact, except in the following case.
 Consider: 
        Text.Printf.printf "hello"
@@ -2791,7 +2976,7 @@ tcSimplifyDeriv orig tyvars theta
 
        ; return simpl_theta }
   where
 
        ; return simpl_theta }
   where
-    doc = ptext SLIT("deriving classes for a data type")
+    doc = ptext (sLit "deriving classes for a data type")
 
     ok dict | isDict dict = validDerivPred (dictPred dict)
            | otherwise   = False
 
     ok dict | isDict dict = validDerivPred (dictPred dict)
            | otherwise   = False
@@ -2806,16 +2991,16 @@ whether it worked or not.
 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
                  -> TcM ()
 
 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
     if null irreds then
-       returnM ()
-    else
-       failM
+       return ()
+     else
+       traceTc (ptext (sLit "tcSimplifyDefault failing")) >> failM
   where
   where
-    doc = ptext SLIT("default declaration")
+    doc = ptext (sLit "default declaration")
 \end{code}
 
 
 \end{code}
 
 
@@ -2836,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
 
 -- 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,
   where
        -- (It may seem a bit crude to compare the error messages,
        --  but it makes sure that we combine just what the user sees,
@@ -2857,7 +3041,7 @@ addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs [] 
+addTopIPErrs _ [] 
   = return ()
 addTopIPErrs bndrs ips
   = do { dflags <- getDOpts
   = return ()
 addTopIPErrs bndrs ips
   = do { dflags <- getDOpts
@@ -2865,9 +3049,9 @@ addTopIPErrs bndrs ips
   where
     (tidy_env, tidy_ips) = tidyInsts ips
     mk_msg dflags 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]
                                            <+> pprBinders bndrs <> colon)],
                nest 2 (vcat (map ppr_ip ips)),
                monomorphism_fix dflags]
@@ -2879,7 +3063,7 @@ topIPErrs dicts
   where
     (tidy_env, tidy_dicts) = tidyInsts dicts
     report dicts = addErrTcM (tidy_env, mk_msg 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)
                                     plural tidy_dicts <+> pprDictsTheta tidy_dicts)
 
 addNoInstanceErrs :: [Inst]    -- Wanted (can include implications)
@@ -2900,17 +3084,18 @@ reportNoInstances
 reportNoInstances tidy_env mb_what insts 
   = groupErrs (report_no_instances tidy_env mb_what) insts
 
 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
              (eqInsts, insts3)  = partition isEqInst insts2
        ; traceTc (text "reportNoInstances" <+> vcat 
 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
              (eqInsts, insts3)  = partition isEqInst insts2
        ; traceTc (text "reportNoInstances" <+> vcat 
-                       [ppr implics, ppr insts1, ppr insts2])
+                       [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_ complain_implic implics
        ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
        ; groupErrs complain_no_inst insts3 
-       ; mapM_ complain_eq eqInsts
+       ; mapM_ (addErrTcM . mk_eq_err) eqInsts
        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
@@ -2920,13 +3105,6 @@ report_no_instances tidy_env mb_what insts
                          (Just (tci_loc inst, tci_given inst)) 
                          (tci_wanted inst)
 
                          (Just (tci_loc inst, tci_given inst)) 
                          (tci_wanted inst)
 
-    complain_eq EqInst {tci_left = lty, tci_right = rty, 
-                        tci_loc = InstLoc _ _ ctxt}
-      = do { (env, msg) <- misMatchMsg lty rty
-           ; setErrCtxt ctxt $
-               failWithTcM (env, msg)
-           }
-
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
        -- Left  inst => no instance
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
        -- Left  inst => no instance
@@ -2934,60 +3112,62 @@ report_no_instances tidy_env mb_what insts
        | not (isClassDict wanted) = Left wanted
        | otherwise
        = case lookupInstEnv inst_envs clas tys of
        | not (isClassDict wanted) = Left wanted
        | otherwise
        = case lookupInstEnv inst_envs clas tys of
+               ([], _) -> 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
                -- 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
-#ifdef DEBUG
-               ([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
-#endif
-               ([], _)  -> Left wanted         -- No match
-               res      -> Right (mk_overlap_msg wanted res)
+               ([_],[])
+                | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
+               res -> Right (mk_overlap_msg wanted res)
          where
            (clas,tys) = getDictClassTys wanted
 
     mk_overlap_msg dict (matches, unifiers)
       = ASSERT( not (null matches) )
          where
            (clas,tys) = getDictClassTys wanted
 
     mk_overlap_msg dict (matches, unifiers)
       = ASSERT( not (null matches) )
-        vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
+        vcat [ addInstLoc [dict] ((ptext (sLit "Overlapping instances for") 
                                        <+> pprPred (dictPred dict))),
                                        <+> pprPred (dictPred dict))),
-               sep [ptext SLIT("Matching instances") <> colon,
+               sep [ptext (sLit "Matching instances") <> colon,
                     nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
                if not (isSingleton matches)
                then    -- Two or more matches
                     empty
                else    -- One match, plus some unifiers
                ASSERT( not (null unifiers) )
                     nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
                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))),
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
-                             ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
-                             ptext SLIT("when compiling the other instance declarations")])]
+                             ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
+                             ptext (sLit "when compiling the other instance declarations")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]
 
       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 $
     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 $
             , 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
             , 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 (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 = []
 
        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
                                        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
@@ -2995,9 +3175,10 @@ report_no_instances tidy_env mb_what insts
 
        show_fixes :: [SDoc] -> SDoc
        show_fixes []     = empty
 
        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
 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
   = ifErrsM (return ()) $      -- Only report ambiguity if no other errors happened
@@ -3011,11 +3192,11 @@ addTopAmbigErrs dicts
     cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
     
     report :: [(Inst,[TcTyVar])] -> TcM ()
     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
          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 <+> 
        where
          dicts = map fst pairs
          msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
@@ -3036,79 +3217,46 @@ mkMonomorphismMsg tidy_env inst_tvs
        ; return (tidy_env, mk_msg dflags docs) }
   where
     mk_msg _ _ | any isRuntimeUnk 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),
                    (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 
                        -- 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]
 
                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
 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
         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!
     
                        -- 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
     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]
 
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 
+reduceDepthErr :: Int -> [Inst] -> SDoc
 reduceDepthErr n stack
 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)]
 
          nest 4 (pprStack stack)]
 
+pprStack :: [Inst] -> SDoc
 pprStack stack = vcat (map pprInstInFull stack)
 pprStack stack = vcat (map pprInstInFull stack)
-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
-  = do { env0 <- tcInitTidyEnv
-        ; ty_exp <- zonkTcType ty_exp
-        ; ty_act <- zonkTcType ty_act
-       ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
-       ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
-       ; return (env2, 
-                  sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
-                           nest 7 $
-                              ptext SLIT("against inferred type") <+> pp_act],
-                      nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do { let (env1, tidy_ty) = tidyOpenType env ty
-       ; (env2, extra) <- ppr_extra env1 tidy_ty
-       ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv)
-  | isSkolemTyVar tv || isSigTyVar tv
-  = return (env1, pprSkolTvBinding tv1)
-  where
-    (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env ty = return (env, empty)         -- Normal case
 \end{code}
 \end{code}