Fix Haddock errors.

[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 292c231..9ebae01 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -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,15 +26,15 @@ 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 Name
 import NameSet
 import Var
 import Name
 import NameSet

@@ -55,17 +48,17 @@ 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:
 

@@ -657,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

@@ -726,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

@@ -781,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

@@ -806,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,

@@ -888,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}
 

@@ -921,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) }
 
 -----------------------------------------------------------

@@ -939,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

@@ -966,15 +960,14 @@ 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

@@ -986,8 +979,9 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 -- qtvs includes coercion variables
 --
 -- This binding must line up the 'rhs' in reduceImplication
 -- qtvs includes coercion variables
 --
 -- 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)

@@ -995,27 +989,31 @@ 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
+             eq_tyvar_cos = mkTyVarTys (varSetElems $ tyVarsOfTypes $ map eqInstType eq_givens)
+               -- Urgh! See line 2187 or thereabouts.  I believe that all these
+               -- 'givens' must be a simple CoVar.  This MUST be cleaned up.
+

        ; let name = mkInternalName uniq (mkVarOcc "ic") span
        ; let name = mkInternalName uniq (mkVarOcc "ic") span

-             implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
+             implic_inst = ImplicInst { tci_name = name,

                                         tci_tyvars = all_tvs, 
                                         tci_given = (eq_givens ++ dict_givens),
                                         tci_wanted = irreds, tci_loc = loc }
        ; let   -- only create binder for dict_irreds
                                         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
+             (_, dict_irreds) = partition 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
+             lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)

              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))

-             co  = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
+             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
              bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs

-                  | otherwise        = PatBind { pat_lhs = L span pat, 
+                  | otherwise        = PatBind { pat_lhs = lpat, 

                                                  pat_rhs = unguardedGRHSs rhs, 
                                                  pat_rhs = unguardedGRHSs rhs, 

-                                                 pat_rhs_ty = tup_ty,
+                                                 pat_rhs_ty = hsLPatType lpat,

                                                  bind_fvs = placeHolderNames }
                                                  bind_fvs = placeHolderNames }

-       ; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
-         return ([implic_inst], unitBag (L span bind)) }
+       ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
+       ; return ([implic_inst], unitBag (L span bind)) 
+        }

 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc
 
 -----------------------------------------------------------
 tryHardCheckLoop :: SDoc

@@ -1023,11 +1021,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 (mkRedEnv doc try_me []) wanteds

        ; return (irreds,binds)
        }
   where
        ; return (irreds,binds)
        }
   where

-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe AddSCs

        -- Here's the try-hard bit
 
 -----------------------------------------------------------
        -- Here's the try-hard bit
 
 -----------------------------------------------------------

@@ -1037,7 +1035,7 @@ 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
        ; return (irreds,binds)
        }
   where

@@ -1047,6 +1045,16 @@ gentleCheckLoop inst_loc givens wanteds
                | 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 = mkRedEnv doc try_me []
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+               | otherwise          = Stop

 \end{code}
 
 Note [Check gently]
 \end{code}
 
 Note [Check gently]

@@ -1064,7 +1072,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

@@ -1077,33 +1085,33 @@ 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 {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+  = go env wanteds (return ())
+  where go env wanteds elim_skolems
+         = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]

                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        
                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        

-               ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
+               ; (improved, binds, irreds, elim_more_skolems)
+                    <- reduceContext env' wanteds'
+                ; let elim_skolems' = elim_skolems >> elim_more_skolems

 
 

-               ; let all_needed_givens = needed_givens ++ more_needed_givens
-       

                ; if not improved then
                ; if not improved then

-                    return (irreds, binds, all_needed_givens)
+                   elim_skolems' >> 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 elim_skolems'
+               ; return (irreds1, binds `unionBags` binds1) } }

 \end{code}
 
 Note [Zonking RedEnv]
 \end{code}
 
 Note [Zonking RedEnv]

@@ -1137,7 +1145,7 @@ 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
 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

-TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+Unify.tcUnifyTys, which doesn't know about mutable type variables.

 
 
 Note [LOOP]
 
 
 Note [LOOP]

@@ -1211,13 +1219,13 @@ tcSimplifySuperClasses
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
   = do { traceTc (text "tcSimplifySuperClasses")
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc givens sc_wanteds
   = 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
     env = mkRedEnv (pprInstLoc loc) try_me givens
        ; 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
+    try_me _ = ReduceMe NoSCs

        -- Like tryHardCheckLoop, but with NoSCs
 \end{code}
 
        -- Like tryHardCheckLoop, but with NoSCs
 \end{code}
 

@@ -1350,8 +1358,10 @@ 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 AddSCs)
+       ; (_imp, _binds, constrained_dicts, elim_skolems) 
+            <- reduceContext env wanteds'
+        ; elim_skolems

 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)

@@ -1370,9 +1380,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Warn in the mono
        ; warn_mono <- doptM Opt_WarnMonomorphism
        ; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
        -- 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',

@@ -1400,7 +1410,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
                           (is_nested_group || isDict inst) = Stop
                          | otherwise            = ReduceMe AddSCs
              env = mkNoImproveRedEnv doc try_me
                           (is_nested_group || isDict inst) = Stop
                          | otherwise            = ReduceMe AddSCs
              env = mkNoImproveRedEnv doc try_me

-       ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
+       ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+        ; elim_skolems

 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured

@@ -1549,7 +1560,8 @@ 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, elim_skolems) <- reduceContext env wanteds'
+        ; elim_skolems

 
        ; if not improved then 
                ASSERT( all is_free irreds )
 
        ; if not improved then 
                ASSERT( all is_free irreds )

@@ -1603,18 +1615,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)

@@ -1623,8 +1634,6 @@ bindInstsOfLocalFuns wanteds local_ids
     overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
                                                -- so it's worth building a set, so that
                                                -- lookup (in isMethodFor) is faster
     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}
 
 

@@ -1665,14 +1674,16 @@ data RedEnv
 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
 mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,

-            red_givens = givens, red_stack = (0,[]),
+            red_givens = givens, 
+            red_stack = (0,[]),

             red_improve = True }       
 
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_improve = True }       
 
 mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 -- Do not do improvement; no givens
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,

-            red_givens = [], red_stack = (0,[]),
+            red_givens = [], 
+            red_stack = (0,[]),

             red_improve = True }       
 
 data WhatToDo
             red_improve = True }       
 
 data WhatToDo

@@ -1692,8 +1703,8 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
        -- Note [SUPER-CLASS LOOP 1]
 
 zonkRedEnv :: RedEnv -> TcM RedEnv
        -- Note [SUPER-CLASS LOOP 1]
 
 zonkRedEnv :: RedEnv -> TcM RedEnv

-zonkRedEnv env 
-  = do { givens' <- mappM zonkInst (red_givens env)
+zonkRedEnv env
+  = do { givens' <- mapM zonkInst (red_givens env)

        ; return $ env {red_givens = givens'}
        }
 \end{code}
        ; return $ env {red_givens = givens'}
        }
 \end{code}

@@ -1724,7 +1735,7 @@ reduceContext :: RedEnv
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
                      [Inst],           -- Irreducible
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
                      [Inst],           -- Irreducible

-                     [Inst])           -- Needed givens
+                      TcM ())           -- Undo skolems from SkolemOccurs

 
 reduceContext env wanteds
   = do { traceTc (text "reduceContext" <+> (vcat [
 
 reduceContext env wanteds
   = do { traceTc (text "reduceContext" <+> (vcat [

@@ -1735,9 +1746,11 @@ reduceContext env wanteds
             text "----------------------"
             ]))
 
             text "----------------------"
             ]))
 

-       ; let givens                      = red_givens env
-             (given_eqs0, given_dicts0)  = partition isEqInst givens
-             (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
+
+       ; let givens                       = red_givens env
+             (given_eqs0, given_dicts0)   = partition isEqInst givens
+             (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
+             (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs

 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.

@@ -1751,65 +1764,92 @@ reduceContext env wanteds
 
          -- 2. Normalise the *given* *dictionary* constraints
          --    wrt. the toplevel and given equations
 
          -- 2. Normalise the *given* *dictionary* constraints
          --    wrt. the toplevel and given equations

-       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs 
+       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs

                                                             given_dicts0
 
                                                             given_dicts0
 

-         -- 3. Solve the *wanted* *equation* constraints
-       ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs 
-
-         -- 4. Normalise the *wanted* equality constraints with respect to
-         --    each other 
-       ; eq_irreds <- normaliseWantedEqs eq_irreds0
-

           -- 5. Build the Avail mapping from "given_dicts"
           -- 5. Build the Avail mapping from "given_dicts"

-       ; init_state <- foldlM addGiven emptyAvails given_dicts
+       ; (init_state, _) <- getLIE $ do 
+               { init_state <- foldlM addGiven emptyAvails given_dicts
+               ; return init_state
+                }
+
+       -- !!! ToDo: what to do with the "extra_givens"?  For the
+       -- moment I'm simply discarding them, which is probably wrong

 
 

-          -- 6. Solve the *wanted* *dictionary* constraints
+          -- 6. Solve the *wanted* *dictionary* constraints (not implications)

          --    This may expose some further equational 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'
+       ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+       ; (dict_binds, bound_dicts, dict_irreds) 
+            <- extractResults avails wanted_dicts

        ; traceTc $ text "reduceContext extractresults" <+> vcat
        ; 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
+                     [ppr avails, ppr wanted_dicts, ppr dict_binds]
+
+         -- Solve the wanted *implications*.  In doing so, we can provide
+         -- as "given"   all the dicts that were originally given, 
+         --              *or* for which we now have bindings, 
+         --              *or* which are now irreds
+       ; let implic_env = env { red_givens = givens ++ bound_dicts 
+                                              ++ dict_irreds }
+       ; (implic_binds_s, implic_irreds_s) 
+            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+       ; let implic_binds  = unionManyBags implic_binds_s
+             implic_irreds = concat implic_irreds_s
+
+         -- Normalise the wanted equality constraints
+       ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
+
+         -- Normalise the wanted dictionaries
+       ; let irreds = dict_irreds ++ implic_irreds
+              eqs    = eq_irreds ++ given_eqs
+       ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds

                
                

-         -- 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)
+         -- Figure out whether we should go round again.  We do so in either
+          -- two cases:
+          -- (1) If any of the mutable tyvars in givens or irreds has been
+          --     filled in by improvement, there is merit in going around 
+          --     again, because we may make further progress.
+          -- (2) If we managed to normalise any dicts, there is merit in going
+          --     around gain, because reduceList may be able to get further.
+         -- 
+         -- ToDo: We may have exposed new
+         --       equality constraints and should probably go round again
+         --       then as well.  But currently we are dropping them on the
+         --       floor anyway.
+
+       ; let all_irreds = norm_irreds ++ eq_irreds
+       ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
+                           tyVarsOfInsts (givens ++ all_irreds)
+        ; let improvedDicts = not $ isEmptyBag normalise_binds
+              improved      = improvedMetaTy || improvedDicts
+
+       -- The old plan (fragile)
+       -- improveed   = availsImproved avails 
+       --               || (not $ isEmptyBag normalise_binds1)
+       --               || (not $ isEmptyBag normalise_binds2)
+       --               || (any isEqInst irreds)

 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,

-            text "given" <+> ppr (red_givens env),
+            text "given" <+> ppr givens,
+            text "given_eqs" <+> ppr given_eqs,

             text "wanted" <+> ppr wanteds,
             text "wanted" <+> ppr wanteds,

+            text "wanted_dicts" <+> ppr wanted_dicts,

             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,

-            text "irreds = " <+> ppr irreds,
-            text "binds = " <+> ppr binds,
-            text "needed givens = " <+> ppr needed_givens,
+            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) 
+                  given_binds `unionBags` normalise_binds
+                              `unionBags` dict_binds 
+                              `unionBags` implic_binds, 
+                  all_irreds,
+                  eliminate_skolems) 

         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone

@@ -1833,22 +1873,25 @@ 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
+  = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
+        ; mapM_ unify eqns

        ; return True }
   where
     unify ((qtvs, pairs), what1, what2)
        ; return True }
   where
     unify ((qtvs, pairs), what1, what2)

-        = addErrCtxtM (mkEqnMsg what1 what2)   $
-          tcInstTyVars (varSetElems qtvs)      `thenM` \ (_, _, tenv) ->
-          mapM_ (unif_pr tenv) pairs
+         = addErrCtxtM (mkEqnMsg what1 what2) $ do
+           (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+           mapM_ (unif_pr tenv) pairs

     unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
 
     unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
 

-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]

 
 

+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)

 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
   = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
        ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
   = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
        ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }

-       ; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
+       ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),

                          nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
                          nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
        ; return (tidy_env, msg) }
                          nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
                          nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
        ; return (tidy_env, msg) }

@@ -1859,33 +1902,31 @@ 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
 \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
     -- It's the same as an existing inst, or a superclass thereof
 reduce env wanted avails
     -- 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]

@@ -1898,7 +1939,7 @@ reduce env wanted avails
                             
                    GenInst [] rhs -> addWanted want_scs avails wanted rhs []
 
                             
                    GenInst [] rhs -> addWanted want_scs avails wanted rhs []
 

-                   GenInst wanteds' rhs 
+                   GenInst wanteds' rhs

                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
                                ; addWanted want_scs avails2 wanted rhs wanteds' } }
                          -> do { avails1 <- addIrred NoSCs avails wanted
                                ; avails2 <- reduceList env wanteds' avails1
                                ; addWanted want_scs avails2 wanted rhs wanteds' } }

@@ -1919,7 +1960,7 @@ 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}
 
 

@@ -2010,11 +2051,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}

@@ -2022,7 +2059,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

@@ -2047,24 +2084,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)
 

@@ -2088,37 +2117,33 @@ Note that
        --              the solved dictionaries use these binders               
        --              these binders are generated by reduceImplication
        --
        --              the solved dictionaries use these binders               
        --              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
+reduceImplication env
+       orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+                                 tci_tyvars = tvs,
+                                 tci_given = extra_givens, tci_wanted = wanteds })
+  = do {       -- Solve the sub-problem
+       ; let try_me _ = ReduceMe AddSCs  -- Note [Freeness and implications]
+             env' = env { red_givens = extra_givens ++ red_givens env
+                        , red_doc = sep [ptext (sLit "reduceImplication for") 
+                                            <+> ppr name,
+                                         nest 2 (parens $ ptext (sLit "within")
+                                                           <+> red_doc env)]

                         , red_try_me = try_me }
 
        ; traceTc (text "reduceImplication" <+> vcat
                         , 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]
+                       [ ppr (red_givens env), ppr extra_givens, 
+                         ppr wanteds])
+       ; (irreds, binds) <- checkLoop env' wanteds
+       ; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
+                       -- SLPJ Sept 07: I think this is bogus; currently
+                       -- there are no Eqinsts in extra_givens
+               dict_ids = map instToId extra_dict_givens 

 
                -- Note [Reducing implication constraints]
                -- Tom -- update note, put somewhere!
 
        ; traceTc (text "reduceImplication result" <+> vcat
 
                -- Note [Reducing implication constraints]
                -- Tom -- update note, put somewhere!
 
        ; 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 []

@@ -2126,76 +2151,64 @@ 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!

 
        ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
 
 
        ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
 

---     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)
+--     Progress is no longer measered by the number of bindings
+       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then        -- No progress
+               -- If there are any irreds, we back off and do nothing
+               return (emptyBag, [orig_implic])

          else do
          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.
+       { (simpler_implic_insts, bind) 
+            <- makeImplicationBind inst_loc tvs extra_givens irreds
+               -- This binding is useless if the recursive simplification
+               -- made no progress; but currently we don't try to optimise that
+               -- case.  After all, we only try hard to reduce at top level, or
+               -- when inferring types.

 
        ; let   dict_wanteds = filter (not . isEqInst) wanteds
 
        ; 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
                -- 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
+
+               eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+                       -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
+                       --              that current extra_givens has no EqInsts, so
+                       --              it makes no difference
+               co  = wrap_inline       -- Note [Always inline implication constraints]
+                     <.> mkWpTyLams tvs
+                     <.> mkWpLams eq_tyvars
+                     <.> mkWpLams dict_ids
+                     <.> WpLet (binds `unionBags` bind)
+               wrap_inline | null dict_ids = idHsWrapper
+                           | otherwise     = WpInline
+               rhs = mkLHsWrap co payload

                loc = instLocSpan inst_loc
                loc = instLocSpan inst_loc

-               payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
-                       | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
+               payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)

 
        
 
        

-       ; 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

@@ -2222,12 +2235,29 @@ We can satisfy the (C Int) from the superclass of D, so we don't want
 to float the (C Int) out, even though it mentions no type variable in
 the constraints!
 
 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

@@ -2255,7 +2285,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

@@ -2265,10 +2295,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

@@ -2277,7 +2309,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

@@ -2300,18 +2333,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 imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
+_availsImproved :: Avails -> ImprovementDone
+_availsImproved (Avails imp _) = imp

 \end{code}
 
 Extracting the bindings from a bunch of Avails.
 \end{code}
 
 Extracting the bindings from a bunch of Avails.

@@ -2320,83 +2350,54 @@ We assume that they'll be wrapped in a big Rec, so that the
 dependency analyser can sort them out later
 
 \begin{code}
 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)
+    go binds bound_dicts irreds _ [] 
+      = return (binds, bound_dicts, irreds)
+
+    go binds bound_dicts irreds done (w:ws)
+      | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+      = if w_id `elem` done_ids then
+          go binds bound_dicts irreds done ws
+       else
+          go (add_bind (nlHsVar done_id)) bound_dicts irreds
+             (addToFM done w (done_id : w_id : rest_done_ids)) ws
+
+      | otherwise      -- Not yet done

       = case findAvailEnv avails w of
          Nothing -> pprTrace "Urk: extractResults" (ppr w) $
       = 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 (addInstToDictBind 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 = addInstToDictBind 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))
-
-extractLocalResults :: Avails
-              -> [Inst]                -- Wanted
-              -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst])         -- Needed givens, i.e. ones used in the bindings
+                    go binds bound_dicts 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)
-
-    go avails binds givens (w:ws)
-      = case findAvailEnv avails w of
-         Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
-                    go avails binds givens 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 = addInstToDictBind 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}
 
 

@@ -2418,53 +2419,14 @@ addWanted want_scs avails wanted rhs_expr wanteds
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails
     avail = Rhs rhs_expr wanteds
 
 addGiven :: Avails -> Inst -> TcM Avails

-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
+addGiven avails given = addAvailAndSCs AddSCs avails given (Given given)

        -- Always add superclasses for 'givens'
        --
        -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
        -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
        -- so the assert isn't true
        -- Always add superclasses for 'givens'
        --
        -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
        -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
        -- so the assert isn't true

-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
-  | isDict given       -- We sometimes have 'given' methods, but they
-                       -- are always optional, so we can drop them
-  , let pred = dictPred given
-  , isRefineablePred pred      -- See Note [ImplicInst rigidity]
-  , Just (co, pred) <- refinePred reft pred
-  = do         { new_given <- newDictBndr (instLoc given) pred
-       ; let rhs = L (instSpan given) $
-                   HsWrap (WpCo co) (HsVar (instToId given))
-       ; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
-       ; return (new_given:refined_givens, avails) }
-           -- ToDo: the superclasses of the original given all exist in Avails 
-           -- so we could really just cast them, but it's more awkward to do,
-           -- and hopefully the optimiser will spot the duplicated work
-  | otherwise
-  = return (refined_givens, avails)

 \end{code}
 
 \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 )

@@ -2489,7 +2451,7 @@ 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

@@ -2503,7 +2465,7 @@ addAvailAndSCs want_scs avails inst avail
 
 addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
        -- Add all the superclasses of the Inst to Avails
 
 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.
 

@@ -2529,7 +2491,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). 

@@ -2593,15 +2555,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

@@ -2619,9 +2583,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

@@ -2708,7 +2672,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])

@@ -2769,12 +2733,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"

@@ -2841,7 +2805,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

@@ -2856,16 +2820,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}
 
 

@@ -2886,12 +2850,11 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
 -- Group together insts with the same origin
 -- We want to report them together in error messages
 
 -- 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,

@@ -2907,7 +2870,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

@@ -2915,9 +2878,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]

@@ -2929,7 +2892,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)

@@ -2950,17 +2913,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_ eqInstMisMatch 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)

@@ -2977,60 +2941,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

@@ -3038,9 +3004,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

@@ -3054,11 +3021,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 <+> 

@@ -3079,47 +3046,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)
 \end{code}
 pprStack stack = vcat (map pprInstInFull stack)
 \end{code}