Remove GADT refinements, part 1
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index 3be5415..324bda9 100644 (file)
@@ -22,7 +22,7 @@ module TcSimplify (
        tcSimplifyBracket, tcSimplifyCheckPat,
 
        tcSimplifyDeriv, tcSimplifyDefault,
-       bindInstsOfLocalFuns, bindIrreds,
+       bindInstsOfLocalFuns, 
 
         misMatchMsg
     ) where
@@ -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) }
 
@@ -950,8 +950,10 @@ bindIrredsR loc qtvs co_vars reft givens irreds
   | null irreds
   = return emptyBag
   | otherwise
-  = do { let givens' = filter isDict givens
-               -- The givens can include methods
+  = do { let givens' = filter isAbstractableInst givens
+               -- The givens can (redundantly) include methods
+               -- We want to retain both EqInsts and Dicts
+               -- There should be no implicadtion constraints
                -- See Note [Pruning the givens in an implication constraint]
 
           -- If there are no 'givens' *and* the refinement is empty
@@ -987,7 +989,8 @@ makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
 --
 -- 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)
@@ -995,7 +998,10 @@ makeImplicationBind loc all_tvs reft
  = 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, 
@@ -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)))
-             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 }
-       ; -- 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
@@ -1023,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
@@ -1037,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
@@ -1051,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 []
@@ -1087,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]
@@ -1221,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 }
@@ -1361,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)
@@ -1410,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
@@ -1559,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 )
@@ -1613,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
@@ -1704,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}
@@ -1736,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 [
@@ -1748,14 +1761,15 @@ reduceContext env wanteds
             ]))
 
 
-       ; 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_dicts0) = partition isImplicInst wanted_non_eqs
 
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]
-       ; ancestor_eqs <- ancestorEqualities wanted_dicts
+       ; ancestor_eqs <- ancestorEqualities wanted_dicts0
         ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
@@ -1764,70 +1778,106 @@ reduceContext env wanteds
 
          -- 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
 
-         -- 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"
          --    Add dicts refined by the current type refinement
-       ; init_state <- foldlM addGiven emptyAvails given_dicts
-       ; let reft = red_reft env
-       ; init_state <- if isEmptyRefinement reft then return init_state
-                       else foldlM (addRefinedGiven reft)
-                                   init_state given_dicts
+       ; (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 }
 
-          -- 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
-       ; let (binds, irreds0, needed_givens) = extractResults avails wanted_dicts'
-       ; traceTc $ text "reduceContext extractresults" <+> vcat
-                     [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
+       -- *** ToDo: what to do with the "extra_givens"?  For the
+       -- moment I'm simply discarding them, which is probably wrong
 
          -- 7. Normalise the *wanted* *dictionary* constraints
          --    wrt. the toplevel and given equations
-       ; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
+         -- 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 (not implications)
+         --    This may expose some further equational constraints...
+       ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+       ; (dict_binds, bound_dicts, dict_irreds) <- extractResults avails wanted_dicts
+       ; traceTc $ text "reduceContext extractresults" <+> vcat
+                     [ppr avails,ppr wanted_dicts,ppr dict_binds]
+
+       -- *** 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
+
+         -- 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
+       ; 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     
-
-         -- 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)
+--     ; eliminate_skolems     
+
+         -- 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 = norm_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,
-            text "given" <+> ppr (red_givens env),
+            text "given" <+> ppr givens,
+            text "given_eqs" <+> ppr given_eqs,
             text "wanted" <+> ppr wanteds,
+            text "wanted_dicts" <+> ppr wanted_dicts,
             text "----",
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved,
-            text "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, 
-                  irreds ++ eq_irreds, 
-                  needed_givens) 
+                              `unionBags` dict_binds 
+                              `unionBags` implic_binds, 
+                  all_irreds,
+                  eliminate_skolems) 
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
@@ -1852,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)]
@@ -1877,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
@@ -1899,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
@@ -1916,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' } }
@@ -2028,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) }
@@ -2066,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
@@ -2108,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)
@@ -2119,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 []
@@ -2154,24 +2188,17 @@ 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!
 
        ; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
 
 --     Progress is no longer measered by the number of bindings
---     ; if isEmptyLHsBinds binds then         -- No progress
-       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then 
-               return (ret_avails, NoInstance)
+       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then        -- No progress
+               -- If there are any irreds, we back off and do nothing
+               return (emptyBag, [orig_implic])
          else do
-       { 
-       ; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+       { (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
@@ -2183,12 +2210,17 @@ reduceImplication env orig_avails name reft tvs extra_givens wanteds inst_loc
                --  equations depending on whether we solve
                --  dictionary constraints or equational constraints
 
-               eq_tyvars = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
+               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
-               -- dict_ids = map instToId extra_givens
-               co  = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
+               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 = mkHsWrap co payload
                loc = instLocSpan inst_loc
                payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
@@ -2196,50 +2228,23 @@ 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]])
-               -- If there are any irreds, we back off and return NoInstance
-       ; 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}
 
-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 [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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2346,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)) }
 
@@ -2371,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
@@ -2613,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)
@@ -2875,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")
@@ -2906,11 +2909,10 @@ groupErrs :: ([Inst] -> TcM ()) -- Deal with one group
 -- 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
-
+  = 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,
@@ -2975,11 +2977,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 
-                       [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_ eqInstMisMatch eqInsts
+       ; mapM_ (addErrTcM . mk_eq_err) eqInsts
        }
   where
     complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
@@ -3025,6 +3027,9 @@ report_no_instances tidy_env mb_what insts
       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
 
@@ -3073,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 <+> 
@@ -3110,11 +3115,6 @@ mkMonomorphismMsg tidy_env inst_tvs
                nest 2 (vcat docs),
                monomorphism_fix dflags]
 
-isRuntimeUnk :: TyVar -> Bool
-isRuntimeUnk x | isTcTyVar x
-               , SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
 monomorphism_fix :: DynFlags -> SDoc
 monomorphism_fix dflags
   = ptext SLIT("Probable fix:") <+> vcat
@@ -3124,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]