Properly ppr InstEqs in wanteds of implication constraints

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

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index be27405..aff019e 100644 (file)
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -22,7 +22,7 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,

-       bindInstsOfLocalFuns, bindIrreds,
+       bindInstsOfLocalFuns, 

 
         misMatchMsg
     ) where
 
         misMatchMsg
     ) where

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

@@ -950,8 +950,10 @@ bindIrredsR loc qtvs co_vars reft 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]
 
           -- If there are no 'givens' *and* the refinement is empty
                -- See Note [Pruning the givens in an implication constraint]
 
           -- If there are no 'givens' *and* the refinement is empty

@@ -987,7 +989,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs reft
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs reft

-                   givens      -- Guaranteed all Dicts (TOMDO: true?)
+                   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,7 +998,10 @@ 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
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 
        ; let name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
                                         tci_tyvars = all_tvs, 

@@ -1008,14 +1014,17 @@ makeImplicationBind loc all_tvs reft
              tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
              pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
              tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
              pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))

-             co  = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
+             co  = mkWpApps (map instToId dict_givens)
+                   <.> mkWpTyApps eq_tyvar_cos
+                   <.> mkWpTyApps (mkTyVarTys all_tvs)

              bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs
                   | otherwise        = PatBind { pat_lhs = L span pat, 
                                                  pat_rhs = unguardedGRHSs rhs, 
                                                  pat_rhs_ty = tup_ty,
                                                  bind_fvs = placeHolderNames }
              bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs
                   | otherwise        = PatBind { pat_lhs = L span pat, 
                                                  pat_rhs = unguardedGRHSs rhs, 
                                                  pat_rhs_ty = tup_ty,
                                                  bind_fvs = placeHolderNames }

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

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

@@ -1047,6 +1056,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 +1083,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

@@ -1085,10 +1104,11 @@ checkLoop :: RedEnv
 checkLoop env wanteds
   = go env wanteds []
   where go env wanteds needed_givens
 checkLoop env wanteds
   = go env wanteds []
   where go env wanteds needed_givens

-         = do { -- Givens are skolems, so no need to zonk them
-                wanteds' <- zonkInsts wanteds
+         = do {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
+                ; env'     <- zonkRedEnv env
+               ; wanteds' <- zonkInsts  wanteds

        
        

-               ; (improved, binds, irreds, more_needed_givens) <- reduceContext env wanteds'
+               ; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'

 
                ; let all_needed_givens = needed_givens ++ more_needed_givens
        
 
                ; let all_needed_givens = needed_givens ++ more_needed_givens
        

@@ -1101,10 +1121,44 @@ checkLoop env 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]
                -- 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
+               { (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens

                ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
 \end{code}
 
                ; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
 \end{code}
 

+Note [Zonking RedEnv]
+~~~~~~~~~~~~~~~~~~~~~
+It might appear as if the givens in RedEnv are always rigid, but that is not
+necessarily the case for programs involving higher-rank types that have class
+contexts constraining the higher-rank variables.  An example from tc237 in the
+testsuite is
+
+  class Modular s a | s -> a
+
+  wim ::  forall a w. Integral a 
+                        => a -> (forall s. Modular s a => M s w) -> w
+  wim i k = error "urk"
+
+  test5  ::  (Modular s a, Integral a) => M s a
+  test5  =   error "urk"
+
+  test4   =   wim 4 test4'
+
+Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
+quantified further outside.  When type checking test4, we have to check
+whether the signature of test5 is an instance of 
+
+  (forall s. Modular s a => M s w)
+
+Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
+givens. 
+
+Given the FD of Modular in this example, class improvement will instantiate
+t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
+Modular s a predicate in that signature).  If we don't zonk (Modular s t_a) in
+the givens, we will get into a loop as improveOne uses the unification engine
+TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
+
+

 Note [LOOP]
 ~~~~~~~~~~~
        class If b t e r | b t e -> r
 Note [LOOP]
 ~~~~~~~~~~~
        class If b t e r | b t e -> r

@@ -1455,7 +1509,8 @@ tcSimplifyRuleLhs wanteds
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of

-                GenInst ws' rhs -> go dicts (addBind binds w rhs) (ws' ++ ws)
+                GenInst ws' rhs -> 
+                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)

                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}
                 NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
          }
 \end{code}

@@ -1573,12 +1628,11 @@ bindInstsOfLocalFuns wanteds local_ids
     returnM emptyLHsBinds
 
   | otherwise
     returnM emptyLHsBinds
 
   | otherwise

-  = do { (irreds, binds,_) <- checkLoop env for_me
+  = do { (irreds, binds) <- gentleInferLoop doc for_me

        ; extendLIEs not_for_me 
        ; extendLIEs irreds
        ; return binds }
   where
        ; 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)

@@ -1587,8 +1641,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}
 
 

@@ -1608,6 +1660,8 @@ data RedEnv
           , red_givens :: [Inst]               -- All guaranteed rigid
                                                -- Always dicts
                                                -- but see Note [Rigidity]
           , red_givens :: [Inst]               -- All guaranteed rigid
                                                -- Always dicts
                                                -- but see Note [Rigidity]

+          , red_reft :: Refinement             -- The refinement to apply to the 'givens'
+                                               -- You should think of it as 'given equalities'

           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }

@@ -1629,14 +1683,17 @@ 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_reft = emptyRefinement,
+            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_reft = emptyRefinement,
+            red_stack = (0,[]),

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

@@ -1654,6 +1711,12 @@ data WantSCs = NoSCs | AddSCs    -- Tells whether we should add the superclasses
                                -- of a predicate when adding it to the avails
        -- The reason for this flag is entirely the super-class loop problem
        -- Note [SUPER-CLASS LOOP 1]
                                -- of a predicate when adding it to the avails
        -- The reason for this flag is entirely the super-class loop problem
        -- Note [SUPER-CLASS LOOP 1]

+
+zonkRedEnv :: RedEnv -> TcM RedEnv
+zonkRedEnv env 
+  = do { givens' <- mappM zonkInst (red_givens env)
+       ; return $ env {red_givens = givens'}
+       }

 \end{code}
 
 
 \end{code}
 
 

@@ -1693,46 +1756,61 @@ 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_dicts0) = partition isEqInst wanteds

 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]
 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]

-       ; ancestor_eqs <- ancestorEqualities wanted_dicts
+       ; ancestor_eqs <- ancestorEqualities wanted_dicts0

         ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
          -- 1. Normalise the *given* *equality* constraints
         ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
          -- 1. Normalise the *given* *equality* constraints

-       ; (given_eqs, eliminate_skolems) <- normaliseGivens given_eqs0
+       ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0

 
          -- 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 <- solveWanteds given_eqs wanted_eqs 
+          -- 5. Build the Avail mapping from "given_dicts"
+         --    Add dicts refined by the current type refinement
+       ; (init_state, extra_givens) <- getLIE $ do 
+               { init_state <- foldlM addGiven emptyAvails given_dicts
+               ; let reft = red_reft env
+               ; if isEmptyRefinement reft then return init_state
+                 else foldlM (addRefinedGiven reft)
+                                   init_state given_dicts }

 
 

-         -- 4. Normalise the *wanted* equality constraints with respect to
-         --    each other 
-       ; eq_irreds <- normaliseWanteds eq_irreds0
+       -- *** ToDo: what to do with the "extra_givens"?  For the
+       -- moment I'm simply discarding them, which is probably wrong

 
 

-          -- 5. Build the Avail mapping from "given_dicts"
-       ; init_state <- foldlM addGiven emptyAvails given_dicts
+         -- 7. Normalise the *wanted* *dictionary* constraints
+         --    wrt. the toplevel and given equations
+         -- NB: normalisation includes zonking as part of what it does
+         --     so it's important to do it after any unifications
+         --     that happened as a result of the addGivens
+       ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0

 
           -- 6. Solve the *wanted* *dictionary* constraints
          --    This may expose some further equational constraints...
 
           -- 6. Solve the *wanted* *dictionary* constraints
          --    This may expose some further equational constraints...

-       ; wanted_dicts' <- zonkInsts wanted_dicts
-       ; avails <- reduceList env wanted_dicts' init_state
-       ; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
+       ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+       ; let (binds, irreds1, needed_givens) = extractResults avails wanted_dicts

        ; traceTc $ text "reduceContext extractresults" <+> vcat
        ; traceTc $ text "reduceContext extractresults" <+> vcat

-                     [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
+                     [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
+       -- *** ToDo: what to do with the "extra_eqs"?  For the
+       -- moment I'm simply discarding them, which is probably wrong
+
+         -- 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

 
          -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
        ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
 
          -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
        ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1

@@ -1740,23 +1818,38 @@ reduceContext env wanteds
          -- 9. eliminate the artificial skolem constants introduced in 1.
        ; eliminate_skolems     
 
          -- 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
+         -- My current plan is to see if any of the mutable tyvars in
+         -- givens or irreds has been filled in by improvement.  
+         -- If so, there is merit in going around again, because
+         -- we may make further progress
+         -- 
+         -- ToDo: is it only mutable stuff?  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 = irreds ++ eq_irreds
+       ; improved <- anyM isFilledMetaTyVar $ varSetElems $
+                     tyVarsOfInsts (givens ++ all_irreds)
+
+       -- 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 "(all) irreds = " <+> ppr all_irreds,

             text "binds = " <+> ppr binds,
             text "needed givens = " <+> ppr needed_givens,
             text "----------------------"
             text "binds = " <+> ppr binds,
             text "needed givens = " <+> ppr needed_givens,
             text "----------------------"

@@ -1766,7 +1859,7 @@ reduceContext env wanteds
                   given_binds `unionBags` normalise_binds1 
                               `unionBags` normalise_binds2 
                               `unionBags` binds, 
                   given_binds `unionBags` normalise_binds1 
                               `unionBags` normalise_binds2 
                               `unionBags` binds, 

-                  irreds ++ eq_irreds, 
+                  all_irreds,

                   needed_givens) 
         }
 
                   needed_givens) 
         }
 

@@ -1817,7 +1910,8 @@ 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
+  = do         { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+       ; dopts <- getDOpts

 #ifdef DEBUG
        ; if n > 8 then
                dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 
 #ifdef DEBUG
        ; if n > 8 then
                dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 

@@ -1830,8 +1924,7 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
            go wanteds state }
   where
     go []     state = return state
            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!

@@ -1843,7 +1936,7 @@ reduce env wanted 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]

@@ -1968,9 +2061,10 @@ 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,
+reduceInst env avails (ImplicInst { tci_name = name,
+                                   tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,

                                    tci_given = extra_givens, tci_wanted = wanteds })
                                    tci_given = extra_givens, tci_wanted = wanteds })

-  = reduceImplication env avails reft tvs extra_givens wanteds loc
+  = reduceImplication env avails name reft tvs extra_givens wanteds loc

 
 reduceInst env avails other_inst
   = do { result <- lookupSimpleInst other_inst
 
 reduceInst env avails other_inst
   = do { result <- lookupSimpleInst other_inst

@@ -1980,7 +2074,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

@@ -2006,6 +2100,7 @@ which are types.
 ---------------------------------------------
 reduceImplication :: RedEnv
                 -> Avails
 ---------------------------------------------
 reduceImplication :: RedEnv
                 -> Avails

+                -> Name

                 -> Refinement  -- May refine the givens; often empty
                 -> [TcTyVar]   -- Quantified type variables; all skolems
                 -> [Inst]      -- Extra givens; all rigid
                 -> Refinement  -- May refine the givens; often empty
                 -> [TcTyVar]   -- Quantified type variables; all skolems
                 -> [Inst]      -- Extra givens; all rigid

@@ -2046,16 +2141,21 @@ 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
+reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc

   = do {       -- Add refined givens, and the extra givens
                -- Todo fix this 
   = 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)
+--       (refined_red_givens,refined_avails)
+--             <- if isEmptyRefinement reft then return (red_givens env,orig_avails)
+--                else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
+--     Commented out SLPJ Sept 07; see comment with extractLocalResults below
+         let refined_red_givens = []

 
                -- Solve the sub-problem
        ; let try_me inst = ReduceMe AddSCs     -- Note [Freeness and implications]
 
                -- 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
+             env' = env { red_givens = extra_givens ++ availsInsts orig_avails
+                        , red_reft = reft
+                        , 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

@@ -2063,20 +2163,23 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                          ppr (red_givens env), ppr extra_givens, 
                          ppr reft, ppr wanteds])
        ; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
                          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]
+       ; 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 
+
+               -- needed_givens0 is the free vars of the bindings
+               -- Remove the ones we are going to lambda-bind
+               -- Use the actual dictionary identity *not* equality on Insts
+               -- (Mind you, it should make no difference here.)
+        ; let needed_givens = [ng | ng <- needed_givens0
+                                  , instToVar ng `notElem` dict_ids]

 
                -- 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, ppr needed_givens])

 
        ; -- extract superclass binds
          --  (sc_binds,_) <- extractResults avails []
 
        ; -- extract superclass binds
          --  (sc_binds,_) <- extractResults avails []

@@ -2090,49 +2193,68 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
        ; let ret_avails = orig_avails
 --     ; let ret_avails = updateImprovement orig_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 
+--     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 return NoInstance

                return (ret_avails, NoInstance)
          else do
                return (ret_avails, NoInstance)
          else do

-       { 
-       ; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds

                        -- This binding is useless if the recursive simplification
                        -- made no progress; but currently we don't try to optimise that
                        -- case.  After all, we only try hard to reduce at top level, or
                        -- when inferring types.
 
        ; let   dict_wanteds = filter (not . isEqInst) wanteds
                        -- This binding is useless if the recursive simplification
                        -- made no progress; but currently we don't try to optimise that
                        -- case.  After all, we only try hard to reduce at top level, or
                        -- when inferring types.
 
        ; let   dict_wanteds = filter (not . isEqInst) wanteds

-               (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-               dict_ids = map instToId extra_dict_givens 

                -- TOMDO: given equational constraints bug!
                --  we need a different evidence for given
                --  equations depending on whether we solve
                --  dictionary constraints or equational constraints
                -- 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)
+
+               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
+                     <.> mkWpTyLams eq_tyvars
+                     <.> mkWpLams dict_ids
+                     <.> WpLet (binds `unionBags` bind)
+               wrap_inline | null dict_ids = idHsWrapper
+                           | otherwise     = WpInline

                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
                payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
 
        
                rhs = mkHsWrap co payload
                loc = instLocSpan inst_loc
                payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
 
        

-       ; traceTc (text "reduceImplication ->"  <+> vcat
-                       [ ppr ret_avails,
-                         ppr implic_insts])
-               -- If there are any irreds, we back off and return NoInstance
+       ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+                        ppr implic_insts,
+                        text "->" <+> sep [ppr needed_givens, ppr rhs]])

        ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
        } 
     }
 \end{code}
 
        ; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
        } 
     }
 \end{code}
 

+Note [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be 
+inlined.  And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code.  To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
+

 Note [Reducing implication constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are trying to simplify
 Note [Reducing implication constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we are trying to simplify

-       (Ord a, forall b. C a b => (W [a] b, D c b))
+       ( do: Ord a, 
+         ic: (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
 where
        instance (C a b, Ord a) => W [a] b
 When solving the implication constraint, we'll start with

@@ -2140,16 +2262,26 @@ When solving the implication constraint, we'll start with
 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,
 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
+but the (D d b) is from "inside".  So we want to generate a GenInst

 like this
 
 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
+   ic = GenInst 
+          [ do  :: Ord a,
+            ic' :: forall b. C a b => D c b]
+          (/\b \(dc:C a b). (df a b dc do, ic' b dc))
+
+The first arg of GenInst gives the free dictionary variables of the
+second argument -- the "needed givens".  And that list in turn is
+vital because it's used to determine what other dicts must be solved.
+This very list ends up in the second field of the Rhs, and drives
+extractResults.
+
+The need for this field is why we have to return "needed givens"
+from extractResults, reduceContext, checkLoop, and so on.

 
 

-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
+NB: the "needed givens" in a GenInst or Rhs, may contain two dicts
+with the same type but different Ids, e.g. [d12 :: Eq a, d81 :: Eq a]
+That says we must generate a binding for both d12 and d81.

 
 The "inside" and "outside" distinction is what's going on with 'inner' and
 'outer' in reduceImplication
 
 The "inside" and "outside" distinction is what's going on with 'inner' and
 'outer' in reduceImplication

@@ -2213,7 +2345,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

@@ -2225,8 +2357,9 @@ instance Outputable Avails where
 
 pprAvails (Avails imp avails)
   = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
 
 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 ])]
+        , 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

@@ -2235,7 +2368,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

@@ -2278,81 +2412,56 @@ 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
+              -> (TcDictBinds,         -- Bindings
+                  [Inst],              -- Irreducible ones
+                  [Inst])              -- Needed givens, i.e. ones used in the bindings
+                       -- Postcondition: needed-givens = free vars( binds ) \ irreds
+                       --                needed-gives is subset of Givens in incoming Avails
+                       -- 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]
-       -> TcM (TcDictBinds, [Inst], [Inst])
-    go avails binds irreds givens [] 
-      = returnM (binds, irreds, givens)
-
-    go avails binds irreds givens (w:ws)
+    go :: TcDictBinds  -- Bindings for dicts
+       -> [Inst]       -- Irreds
+       -> [Inst]       -- Needed givens
+       -> DoneEnv      -- Has an entry for each inst in the above three sets
+       -> [Inst]       -- Wanted
+       -> (TcDictBinds, [Inst], [Inst])
+    go binds irreds givens done [] 
+      = (binds, irreds, givens)
+
+    go binds irreds givens done (w:ws)
+      | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
+      = if w_id `elem` done_ids then
+          go binds irreds givens done ws
+       else
+          go (add_bind (nlHsVar done_id)) irreds givens 
+             (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 (addBind binds w (nlHsVar id)) irreds (update_id w  id:givens) ws
-               -- The sought Id can be one of the givens, via a superclass chain
-               -- and then we definitely don't want to generate an x=x binding!
-
-         Just IsIrred -> go (add_given avails w) binds (w:irreds) givens ws
-               -- The add_given handles the case where we want (Ord a, Eq a), and we
-               -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
-               -- This showed up in a dupliated Ord constraint in the error message for 
-               --      test tcfail043
-
-         Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
-                            where      
-                               new_binds = addBind binds w rhs
-      where
-       w_id = instToId w       
-       update_id m@(Method{}) id = m {tci_id = id}
-        update_id w            id = w {tci_name = idName id} 
+                    go binds irreds givens done ws

 
 

-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
+         Just IsIrred -> go binds (w:irreds) givens done' ws

 
 

-extractLocalResults :: Avails
-              -> [Inst]                -- Wanted
-              -> TcM ( TcDictBinds,    -- Bindings
-                       [Inst])         -- Needed givens, i.e. ones used in the bindings
-
-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 (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws)

 
 

-         Just IsIrred ->
-                    go avails binds givens 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_given avails w) new_binds givens (ws' ++ ws)
-                            where      
-                               new_binds = addBind binds w rhs
+         Just (Given g) -> go binds' irreds (g:givens) (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}
 
 

@@ -2374,15 +2483,15 @@ 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
+addRefinedGiven :: Refinement -> Avails -> Inst -> TcM Avails
+addRefinedGiven reft avails given

   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them
   , let pred = dictPred given
   | isDict given       -- We sometimes have 'given' methods, but they
                        -- are always optional, so we can drop them
   , let pred = dictPred given

@@ -2391,13 +2500,12 @@ addRefinedGiven reft (refined_givens, avails) given
   = do         { new_given <- newDictBndr (instLoc given) pred
        ; let rhs = L (instSpan given) $
                    HsWrap (WpCo co) (HsVar (instToId given))
   = 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) }
+       ; addAvailAndSCs AddSCs avails new_given (Rhs rhs [given]) }

            -- 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
            -- 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)
+  = return avails

 \end{code}
 
 Note [ImplicInst rigidity]
 \end{code}
 
 Note [ImplicInst rigidity]

@@ -2449,6 +2557,7 @@ addAvailAndSCs want_scs avails inst avail
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid

+      | isEqInst kid                       = so_far

       | kid_id `elemVarSet` so_far        = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise                         = so_far'
       | kid_id `elemVarSet` so_far        = so_far
       | Just avail <- findAvail avails kid = findAllDeps so_far' avail
       | otherwise                         = so_far'

@@ -2458,7 +2567,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.
 

@@ -2555,6 +2664,7 @@ tc_simplify_top doc interactive wanteds
 
        ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
 
        ; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
        ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds

+--     ; (irreds1, binds1) <- gentleInferLoop doc1 wanteds

        ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
        ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
        ; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
        ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)

@@ -2818,7 +2928,7 @@ tcSimplifyDefault theta
     if null irreds then
        returnM ()
     else
     if null irreds then
        returnM ()
     else

-       failM
+       traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM

   where
     doc = ptext SLIT("default declaration")
 \end{code}
   where
     doc = ptext SLIT("default declaration")
 \end{code}

@@ -2842,11 +2952,10 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
 -- We want to report them together in error messages
 
 groupErrs report_err [] 
 -- We want to report them together in error messages
 
 groupErrs report_err [] 

-  = returnM ()
+  = return ()

 groupErrs report_err (inst:insts) 
 groupErrs report_err (inst:insts) 

-  = do_one (inst:friends)              `thenM_`
-    groupErrs report_err others
-
+  = 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,

@@ -2911,11 +3020,11 @@ report_no_instances tidy_env mb_what insts
             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
              (eqInsts, insts3)  = partition isEqInst insts2
        ; traceTc (text "reportNoInstances" <+> vcat 
             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
              (eqInsts, insts3)  = partition isEqInst insts2
        ; traceTc (text "reportNoInstances" <+> vcat 

-                       [ppr implics, ppr insts1, ppr insts2])
+                       [ppr insts, ppr implics, ppr insts1, ppr insts2])

        ; mapM_ complain_implic implics
        ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
        ; groupErrs complain_no_inst insts3 
        ; mapM_ complain_implic implics
        ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
        ; groupErrs complain_no_inst insts3 

-       ; mapM_ complain_eq eqInsts
+       ; mapM_ (addErrTcM . mk_eq_err) eqInsts

        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)

@@ -2925,13 +3034,6 @@ report_no_instances tidy_env mb_what insts
                          (Just (tci_loc inst, tci_given inst)) 
                          (tci_wanted inst)
 
                          (Just (tci_loc inst, tci_given inst)) 
                          (tci_wanted inst)
 

-    complain_eq EqInst {tci_left = lty, tci_right = rty, 
-                        tci_loc = InstLoc _ _ ctxt}
-      = do { (env, msg) <- misMatchMsg lty rty
-           ; setErrCtxt ctxt $
-               failWithTcM (env, msg)
-           }
-

     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
        -- Left  inst => no instance
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
        -- Left  inst => no instance

@@ -2968,6 +3070,9 @@ report_no_instances tidy_env mb_what insts
       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
 
     mk_no_inst_err insts
       | null insts = empty
 

@@ -3053,10 +3158,6 @@ mkMonomorphismMsg tidy_env inst_tvs
                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
   = ptext SLIT("Probable fix:") <+> vcat
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
   = ptext SLIT("Probable fix:") <+> vcat

@@ -3084,36 +3185,4 @@ reduceDepthErr n stack
          nest 4 (pprStack stack)]
 
 pprStack stack = vcat (map pprInstInFull stack)
          nest 4 (pprStack stack)]
 
 pprStack stack = vcat (map pprInstInFull stack)

-
------------------------
-misMatchMsg :: TcType -> TcType -> TcM (TidyEnv, SDoc)
--- Generate the message when two types fail to match,
--- going to some trouble to make it helpful.
--- The argument order is: actual type, expected type
-misMatchMsg ty_act ty_exp
-  = do { env0 <- tcInitTidyEnv
-        ; ty_exp <- zonkTcType ty_exp
-        ; ty_act <- zonkTcType ty_act
-       ; (env1, pp_exp, extra_exp) <- ppr_ty env0 ty_exp
-       ; (env2, pp_act, extra_act) <- ppr_ty env1 ty_act
-       ; return (env2, 
-                  sep [sep [ptext SLIT("Couldn't match expected type") <+> pp_exp, 
-                           nest 7 $
-                              ptext SLIT("against inferred type") <+> pp_act],
-                      nest 2 (extra_exp $$ extra_act)]) }
-
-ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
-ppr_ty env ty
-  = do { let (env1, tidy_ty) = tidyOpenType env ty
-       ; (env2, extra) <- ppr_extra env1 tidy_ty
-       ; return (env2, quotes (ppr tidy_ty), extra) }
-
--- (ppr_extra env ty) shows extra info about 'ty'
-ppr_extra env (TyVarTy tv)
-  | isSkolemTyVar tv || isSigTyVar tv
-  = return (env1, pprSkolTvBinding tv1)
-  where
-    (env1, tv1) = tidySkolemTyVar env tv
-
-ppr_extra env ty = return (env, empty)         -- Normal case

 \end{code}
 \end{code}