Remove GADT refinements, part 1
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 769068b..324bda9 100644 (file)
@@ -657,7 +657,7 @@ tcSimplifyInfer
 \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
@@ -726,7 +726,7 @@ tcSimplifyInfer doc tau_tvs wanted
 
                -- 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
@@ -806,7 +806,7 @@ tcSimplifyInferCheck
 
 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,
@@ -921,16 +921,16 @@ tcSimplifyCheck loc qtvs givens wanteds
 -----------------------------------------------------------
 -- tcSimplifyCheckPat is used for existential pattern match
 tcSimplifyCheckPat :: InstLoc
-                  -> [CoVar] -> Refinement
+                  -> [CoVar]
                   -> [TcTyVar]         -- Quantify over these
                   -> [Inst]            -- Given
                   -> [Inst]            -- Wanted
                   -> TcM TcDictBinds   -- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
+tcSimplifyCheckPat loc co_vars qtvs 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 
+       ; implic_bind <- bindIrredsR loc qtvs co_vars emptyRefinement 
                                    givens irreds
        ; return (binds `unionBags` implic_bind) }
 
@@ -1022,8 +1022,9 @@ makeImplicationBind loc all_tvs reft
                                                  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
@@ -1031,7 +1032,7 @@ tryHardCheckLoop :: SDoc
             -> 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
@@ -1045,7 +1046,7 @@ gentleCheckLoop :: InstLoc
               -> TcM ([Inst], TcDictBinds)
 
 gentleCheckLoop inst_loc givens wanteds
-  = do { (irreds,binds,_) <- checkLoop env wanteds
+  = do { (irreds,binds) <- checkLoop env wanteds
        ; return (irreds,binds)
        }
   where
@@ -1059,7 +1060,7 @@ gentleCheckLoop inst_loc givens wanteds
 gentleInferLoop :: SDoc -> [Inst]
                -> TcM ([Inst], TcDictBinds)
 gentleInferLoop doc wanteds
-  = do         { (irreds, binds, _) <- checkLoop env wanteds
+  = do         { (irreds, binds) <- checkLoop env wanteds
        ; return (irreds, binds) }
   where
     env = mkRedEnv doc try_me []
@@ -1095,33 +1096,33 @@ with tryHardCheckLooop.
 -----------------------------------------------------------
 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
-  = 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
        
-               ; (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
-                    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
-               -- 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]
@@ -1229,7 +1230,7 @@ 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 }
@@ -1369,7 +1370,9 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- 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'
+       ; (_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)
@@ -1418,7 +1421,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
                           (is_nested_group || isDict inst) = Stop
                          | otherwise            = ReduceMe AddSCs
              env = mkNoImproveRedEnv doc try_me
-       ; (_imp, binds, irreds, _) <- reduceContext env wanteds'
+       ; (_imp, binds, irreds, elim_skolems) <- reduceContext env wanteds'
+        ; elim_skolems
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
@@ -1567,7 +1571,8 @@ tcSimplifyIPs given_ips wanteds
                -- 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 )
@@ -1621,10 +1626,10 @@ bindInstsOfLocalFuns :: [Inst] -> [TcId] -> TcM TcDictBinds
 -- arguably a bug in Match.tidyEqnInfo (see notes there)
 
 bindInstsOfLocalFuns wanteds local_ids
-  | null overloaded_ids
+  | null overloaded_ids = do
        -- Common case
-  = extendLIEs wanteds         `thenM_`
-    returnM emptyLHsBinds
+    extendLIEs wanteds
+    return emptyLHsBinds
 
   | otherwise
   = do { (irreds, binds) <- gentleInferLoop doc for_me
@@ -1712,8 +1717,8 @@ data WantSCs = NoSCs | AddSCs     -- Tells whether we should add the superclasses
        -- 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}
@@ -1744,7 +1749,7 @@ reduceContext :: RedEnv
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
                      [Inst],           -- Irreducible
-                     [Inst])           -- Needed givens
+                      TcM ())           -- Undo skolems from SkolemOccurs
 
 reduceContext env wanteds
   = do { traceTc (text "reduceContext" <+> (vcat [
@@ -1758,7 +1763,8 @@ reduceContext env wanteds
 
        ; let givens                       = red_givens env
              (given_eqs0, given_dicts0)   = partition isEqInst givens
-             (wanted_eqs0, wanted_dicts0) = partition isEqInst wanteds
+             (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
+             (wanted_implics0, wanted_dicts0) = partition isImplicInst wanted_non_eqs
 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
@@ -1794,16 +1800,25 @@ reduceContext env wanteds
          --     that happened as a result of the addGivens
        ; (wanted_dicts,normalise_binds1) <- normaliseWantedDicts given_eqs wanted_dicts0
 
-          -- 6. Solve the *wanted* *dictionary* constraints
+          -- 6. Solve the *wanted* *dictionary* constraints (not implications)
          --    This may expose some further equational constraints...
        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
-       ; let (binds, irreds1, needed_givens) = extractResults avails wanted_dicts
+       ; (dict_binds, bound_dicts, dict_irreds) <- extractResults avails wanted_dicts
        ; traceTc $ text "reduceContext extractresults" <+> vcat
-                     [ppr avails,ppr wanted_dicts,ppr binds,ppr needed_givens]
+                     [ppr avails,ppr wanted_dicts,ppr dict_binds]
 
        -- *** ToDo: what to do with the "extra_eqs"?  For the
        -- moment I'm simply discarding them, which is probably wrong
 
+         -- 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
+
          -- 3. Solve the *wanted* *equation* constraints
        ; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs
 
@@ -1812,10 +1827,12 @@ reduceContext env wanteds
        ; eq_irreds <- normaliseWantedEqs eq_irreds0
 
          -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
-       ; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
+       ; let irreds = dict_irreds ++ implic_irreds
+       ; (norm_irreds, normalise_binds2) <- substEqInDictInsts True {-wanted-}
+                                                                eq_irreds irreds
                
          -- 9. eliminate the artificial skolem constants introduced in 1.
-       ; eliminate_skolems     
+--     ; eliminate_skolems     
 
          -- Figure out whether we should go round again
          -- My current plan is to see if any of the mutable tyvars in
@@ -1828,7 +1845,7 @@ reduceContext env wanteds
          --       then as well.  But currently we are dropping them on the
          --       floor anyway.
 
-       ; let all_irreds = irreds ++ eq_irreds
+       ; let all_irreds = norm_irreds ++ eq_irreds
        ; improved <- anyM isFilledMetaTyVar $ varSetElems $
                      tyVarsOfInsts (givens ++ all_irreds)
 
@@ -1848,18 +1865,19 @@ reduceContext env wanteds
             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, 
                   given_binds `unionBags` normalise_binds1 
                               `unionBags` normalise_binds2 
-                              `unionBags` binds, 
+                              `unionBags` dict_binds 
+                              `unionBags` implic_binds, 
                   all_irreds,
-                  needed_givens) 
+                  eliminate_skolems) 
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
@@ -1884,13 +1902,13 @@ unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))]
 unifyEqns [] = return False
 unifyEqns eqns
   = do { traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
-        ; mappM_ unify eqns
+        ; mapM_ unify eqns
        ; return True }
   where
     unify ((qtvs, pairs), what1, what2)
-        = addErrCtxtM (mkEqnMsg what1 what2)   $
-          tcInstTyVars (varSetElems qtvs)      `thenM` \ (_, _, tenv) ->
-          mapM_ (unif_pr tenv) pairs
+         = addErrCtxtM (mkEqnMsg what1 what2) $ do
+           (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+           mapM_ (unif_pr tenv) pairs
     unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
 
 pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
@@ -1909,7 +1927,7 @@ The main context-reduction function is @reduce@.  Here's its game plan.
 \begin{code}
 reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
 reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
-  = do         { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
+  = do { traceTc (text "reduceList " <+> (ppr wanteds $$ ppr state))
        ; dopts <- getDOpts
 #ifdef DEBUG
        ; if n > 8 then
@@ -1931,7 +1949,7 @@ reduce env wanted avails
     -- It's the same as an existing inst, or a superclass thereof
   | Just avail <- findAvail avails wanted
   = do { traceTc (text "reduce: found " <+> ppr wanted)
-       ; returnM avails        
+       ; return avails
        }
 
   | otherwise
@@ -1948,7 +1966,7 @@ reduce env wanted avails
                             
                    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' } }
@@ -2060,11 +2078,6 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_name = name,
-                                   tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
-                                   tci_given = extra_givens, tci_wanted = wanteds })
-  = reduceImplication env avails name reft tvs extra_givens wanteds loc
-
 reduceInst env avails other_inst
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
@@ -2098,14 +2111,8 @@ which are types.
 \begin{code}
 ---------------------------------------------
 reduceImplication :: RedEnv
-                -> Avails
-                -> Name
-                -> 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
@@ -2140,7 +2147,10 @@ Note that
        --              the solved dictionaries use these binders               
        --              these binders are generated by reduceImplication
        --
-reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
+reduceImplication env
+       orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+                                 tci_tyvars = tvs, tci_reft = reft,
+                                 tci_given = extra_givens, tci_wanted = wanteds })
   = do {       -- Add refined givens, and the extra givens
                -- Todo fix this 
 --       (refined_red_givens,refined_avails)
@@ -2151,34 +2161,26 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
 
                -- Solve the sub-problem
        ; let try_me inst = ReduceMe AddSCs     -- Note [Freeness and implications]
-             env' = env { red_givens = extra_givens ++ availsInsts orig_avails
+             env' = env { red_givens = extra_givens ++ red_givens env
                         , 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
-                       [ ppr orig_avails,
-                         ppr (red_givens env), ppr extra_givens, 
+                       [ ppr (red_givens env), ppr extra_givens, 
                          ppr reft, ppr wanteds])
-       ; (irreds,binds,needed_givens0) <- checkLoop env' 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 
 
-               -- 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
-                       [ppr irreds, ppr binds, ppr needed_givens])
+                       [ppr irreds, ppr binds])
 
        ; -- extract superclass binds
          --  (sc_binds,_) <- extractResults avails []
@@ -2186,12 +2188,6 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
 --                     [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!
 
@@ -2199,10 +2195,10 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
 
 --     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)
+               -- If there are any irreds, we back off and do nothing
+               return (emptyBag, [orig_implic])
          else do
-       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+       { (simpler_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
@@ -2220,7 +2216,7 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
                        --              it makes no difference
                co  = wrap_inline       -- Note [Always inline implication constraints]
                      <.> mkWpTyLams tvs
-                     <.> mkWpTyLams eq_tyvars
+                     <.> mkWpLams eq_tyvars
                      <.> mkWpLams dict_ids
                      <.> WpLet (binds `unionBags` bind)
                wrap_inline | null dict_ids = idHsWrapper
@@ -2232,9 +2228,10 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
 
        
        ; 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))
+                        ppr simpler_implic_insts,
+                        text "->" <+> ppr rhs])
+       ; return (unitBag (L loc (VarBind (instToId orig_implic) (L loc rhs))),
+                 simpler_implic_insts)
        } 
     }
 \end{code}
@@ -2249,43 +2246,6 @@ 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
-       ( 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
-       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 GenInst
-like this
-
-   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.
-
-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
-
-
 Note [Freeness and implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's hard to say when an implication constraint can be floated out.  Consider
@@ -2391,7 +2351,7 @@ elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
 
 extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
 -- Does improvement
-extendAvails avails@(Avails imp env) inst avail 
+extendAvails avails@(Avails imp env) inst avail
   = do { imp1 <- tcImproveOne avails inst      -- Do any improvement
        ; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
 
@@ -2416,43 +2376,41 @@ type DoneEnv = FiniteMap Inst [Id]
 
 extractResults :: Avails
               -> [Inst]                -- Wanted
-              -> (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
+              -> TcM (TcDictBinds,     -- Bindings
+                      [Inst],          -- The insts bound by the bindings
+                      [Inst])          -- Irreducible ones
                        -- Note [Reducing implication constraints]
 
 extractResults (Avails _ avails) wanteds
   = go emptyBag [] [] emptyFM wanteds
   where
     go :: TcDictBinds  -- Bindings for dicts
+       -> [Inst]       -- Bound by the bindings
        -> [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)
+       -> TcM (TcDictBinds, [Inst], [Inst])
+    go binds bound_dicts irreds done [] 
+      = return (binds, bound_dicts, irreds)
 
-    go binds irreds givens done (w:ws)
+    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 irreds givens done ws
+          go binds bound_dicts irreds done ws
        else
-          go (add_bind (nlHsVar done_id)) irreds givens 
+          go (add_bind (nlHsVar done_id)) bound_dicts irreds
              (addToFM done w (done_id : w_id : rest_done_ids)) ws
 
       | otherwise      -- Not yet done
       = case findAvailEnv avails w of
          Nothing -> pprTrace "Urk: extractResults" (ppr w) $
-                    go binds irreds givens done ws
+                    go binds bound_dicts irreds done ws
 
-         Just IsIrred -> go binds (w:irreds) givens done' ws
+         Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
 
-         Just (Rhs rhs ws') -> go (add_bind rhs) irreds givens done' (ws' ++ ws)
+         Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
 
-         Just (Given g) -> go binds' irreds (g:givens) (addToFM done w [g_id]) ws 
+         Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws 
                where
                  g_id = instToId g
                  binds' | w_id == g_id = binds
@@ -2658,7 +2616,7 @@ tcSimplifyInteractive wanteds
 -- error message generation for the monomorphism restriction
 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)
@@ -2920,13 +2878,13 @@ whether it worked or not.
 tcSimplifyDefault :: ThetaType -- Wanted; has no type variables in it
                  -> TcM ()
 
-tcSimplifyDefault theta
-  = newDictBndrsO DefaultOrigin theta  `thenM` \ wanteds ->
-    tryHardCheckLoop doc wanteds       `thenM` \ (irreds, _) ->
-    addNoInstanceErrs  irreds          `thenM_`
+tcSimplifyDefault theta = do
+    wanteds <- newDictBndrsO DefaultOrigin theta
+    (irreds, _) <- tryHardCheckLoop doc wanteds
+    addNoInstanceErrs  irreds
     if null irreds then
-       returnM ()
-    else
+       return ()
+     else
        traceTc (ptext SLIT("tcSimplifyDefault failing")) >> failM
   where
     doc = ptext SLIT("default declaration")
@@ -2952,7 +2910,7 @@ groupErrs :: ([Inst] -> TcM ())   -- Deal with one group
 
 groupErrs report_err [] 
   = return ()
-groupErrs report_err (inst:insts) 
+groupErrs report_err (inst:insts)
   = do { do_one (inst:friends)
        ; groupErrs report_err others }
   where
@@ -3120,11 +3078,11 @@ addTopAmbigErrs dicts
     cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
     
     report :: [(Inst,[TcTyVar])] -> TcM ()
-    report pairs@((inst,tvs) : _)      -- The pairs share a common set of ambiguous tyvars
-       = mkMonomorphismMsg tidy_env tvs        `thenM` \ (tidy_env, mono_msg) ->
+    report pairs@((inst,tvs) : _) = do -- The pairs share a common set of ambiguous tyvars
+         (tidy_env, mono_msg) <- mkMonomorphismMsg tidy_env tvs
          setSrcSpan (instSpan inst) $
                -- the location of the first one will do for the err message
-         addErrTcM (tidy_env, msg $$ mono_msg)
+          addErrTcM (tidy_env, msg $$ mono_msg)
        where
          dicts = map fst pairs
          msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
@@ -3166,8 +3124,8 @@ monomorphism_fix dflags
            else empty] -- Only suggest adding "-fno-monomorphism-restriction"
                        -- if it is not already set!
     
-warnDefault ups default_ty
-  = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
+warnDefault ups default_ty = do
+    warn_flag <- doptM Opt_WarnTypeDefaults
     addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
   where
     dicts = [d | (d,_,_) <- ups]