Type families: fixes in the new solver
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index d2f8242..c285c5e 100644 (file)
@@ -6,13 +6,6 @@
 TcSimplify
 
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
 module TcSimplify (
        tcSimplifyInfer, tcSimplifyInferCheck,
        tcSimplifyCheck, tcSimplifyRestricted,
@@ -42,8 +35,8 @@ import TcMType
 import TcIface
 import TcTyFuns
 import DsUtils -- Big-tuple functions
-import TypeRep
 import Var
+import Id
 import Name
 import NameSet
 import Class
@@ -56,18 +49,15 @@ import ErrUtils
 import BasicTypes
 import VarSet
 import VarEnv
-import Module
 import FiniteMap
 import Bag
 import Outputable
 import Maybes
 import ListSetOps
 import Util
-import UniqSet
 import SrcLoc
 import DynFlags
 import FastString
-
 import Control.Monad
 import Data.List
 \end{code}
@@ -101,34 +91,36 @@ we reduce the (C a b1) constraint from the call of f to (D a b1).
 
 Here is a more complicated example:
 
-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-| 
-| *Test> runFoo foo
-| 
-| <interactive>:1:
-|     Could not deduce (Bar a b) from the context (Foo a b)
-|       arising from use of `foo' at <interactive>:1
-|     Probable fix:
-|         Add (Bar a b) to the expected type of an expression
-|     In the first argument of `runFoo', namely `foo'
-|     In the definition of `it': it = runFoo foo
-| 
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that... 
+@
+  > class Foo a b | a->b
+  >
+  > class Bar a b | a->b
+  >
+  > data Obj = Obj
+  >
+  > instance Bar Obj Obj
+  >
+  > instance (Bar a b) => Foo a b
+  >
+  > foo:: (Foo a b) => a -> String
+  > foo _ = "works"
+  >
+  > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
+  > runFoo f = f Obj
+
+  *Test> runFoo foo
+
+  <interactive>:1:
+      Could not deduce (Bar a b) from the context (Foo a b)
+        arising from use of `foo' at <interactive>:1
+      Probable fix:
+          Add (Bar a b) to the expected type of an expression
+      In the first argument of `runFoo', namely `foo'
+      In the definition of `it': it = runFoo foo
+
+  Why all of the sudden does GHC need the constraint Bar a b? The
+  function foo didn't ask for that...
+@
 
 The trouble is that to type (runFoo foo), GHC has to solve the problem:
 
@@ -891,7 +883,9 @@ isFreeWhenChecking qtvs ips inst
   && isFreeWrtIPs    ips inst
 -}
 
+isFreeWrtTyVars :: VarSet -> Inst -> Bool
 isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
+isFreeWrtIPs :: NameSet -> Inst -> Bool
 isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
 \end{code}
 
@@ -1005,8 +999,7 @@ makeImplicationBind loc all_tvs
                                         tci_given = (eq_givens ++ dict_givens),
                                         tci_wanted = irreds, tci_loc = loc }
        ; let   -- only create binder for dict_irreds
-             (eq_irreds, dict_irreds) = partition isEqInst irreds
-              n_dict_irreds = length dict_irreds
+             (_, dict_irreds) = partition isEqInst irreds
              dict_irred_ids = map instToId dict_irreds
              lpat = mkBigLHsPatTup (map (L span . VarPat) dict_irred_ids)
              rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
@@ -1032,7 +1025,7 @@ tryHardCheckLoop doc wanteds
        ; return (irreds,binds)
        }
   where
-    try_me inst = ReduceMe AddSCs
+    try_me _ = ReduceMe AddSCs
        -- Here's the try-hard bit
 
 -----------------------------------------------------------
@@ -1097,18 +1090,16 @@ checkLoop :: RedEnv
 -- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
-  = go env wanteds (return ())
-  where go env wanteds elim_skolems
+  = go env wanteds
+  where go env wanteds
          = do  {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        
-               ; (improved, binds, irreds, elim_more_skolems)
-                    <- reduceContext env' wanteds'
-                ; let elim_skolems' = elim_skolems >> elim_more_skolems
+               ; (improved, binds, irreds) <- reduceContext env' wanteds'
 
-               ; if not improved then
-                   elim_skolems' >> return (irreds, binds)
+               ; if null irreds || not improved then
+                   return (irreds, binds)
                  else do
        
                -- If improvement did some unification, we go round again.
@@ -1117,7 +1108,7 @@ checkLoop env wanteds
                -- 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'
+               { (irreds1, binds1) <- go env' irreds
                ; return (irreds1, binds `unionBags` binds1) } }
 \end{code}
 
@@ -1232,7 +1223,7 @@ tcSimplifySuperClasses loc givens sc_wanteds
        ; return binds1 }
   where
     env = mkRedEnv (pprInstLoc loc) try_me givens
-    try_me inst = ReduceMe NoSCs
+    try_me _ = ReduceMe NoSCs
        -- Like tryHardCheckLoop, but with NoSCs
 \end{code}
 
@@ -1365,10 +1356,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- BUT do no improvement!  See Plan D above
        -- HOWEVER, some unification may take place, if we instantiate
        --          a method Inst with an equality constraint
-       ; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
-       ; (_imp, _binds, constrained_dicts, elim_skolems) 
-            <- reduceContext env wanteds'
-        ; elim_skolems
+       ; let env = mkNoImproveRedEnv doc (\_ -> ReduceMe AddSCs)
+       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
@@ -1417,8 +1406,7 @@ 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, elim_skolems) <- reduceContext env wanteds'
-        ; elim_skolems
+       ; (_imp, binds, irreds) <- reduceContext env wanteds'
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
@@ -1491,27 +1479,55 @@ Instead we want to quantify over the dictionaries separately.
 
 In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
 all dicts unchanged, with absolutely no sharing.  It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
+from scratch, rather than further parameterise simpleReduceLoop etc.
+Simpler, maybe, but alas not simple (see Trac #2494)
+
+* Type errors may give rise to an (unsatisfiable) equality constraint
+
+* Applications of a higher-rank function on the LHS may give
+  rise to an implication constraint, esp if there are unsatisfiable
+  equality constraints inside.
 
 \begin{code}
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds
-  = go [] emptyBag wanteds
+  = do { wanteds' <- zonkInsts wanteds
+       ; (irreds, binds) <- go [] emptyBag wanteds'
+       ; let (dicts, bad_irreds) = partition isDict irreds
+       ; traceTc (text "tcSimplifyrulelhs" <+> pprInsts bad_irreds)
+       ; addNoInstanceErrs (nub bad_irreds)
+               -- The nub removes duplicates, which has
+               -- not happened otherwise (see notes above)
+       ; return (dicts, binds) }
   where
-    go dicts binds []
-       = return (dicts, binds)
-    go dicts binds (w:ws)
+    go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
+    go irreds binds []
+       = return (irreds, binds)
+    go irreds binds (w:ws)
        | isDict w
-       = go (w:dicts) binds ws
+       = go (w:irreds) binds ws
+       | isImplicInst w        -- Have a go at reducing the implication
+       = do { (binds1, irreds1) <- reduceImplication red_env w
+            ; let (bad_irreds, ok_irreds) = partition isImplicInst irreds1
+            ; go (bad_irreds ++ irreds) 
+                 (binds `unionBags` binds1) 
+                 (ok_irreds ++ ws)}
        | otherwise
        = do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
                                 -- to fromInteger; this looks fragile to me
             ; lookup_result <- lookupSimpleInst w'
             ; case lookup_result of
-                GenInst ws' rhs -> 
-                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
-                NoInstance      -> pprPanic "tcSimplifyRuleLhs" (ppr w)
+                NoInstance      -> go (w:irreds) binds ws
+                GenInst ws' rhs -> go irreds binds' (ws' ++ ws)
+                       where
+                         binds' = addInstToDictBind binds w rhs
          }
+
+       -- Sigh: we need to reduce inside implications
+    red_env = mkRedEnv doc try_me []
+    doc = ptext (sLit "Implication constraint in RULE lhs")
+    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
+               | otherwise          = Stop     -- Be gentle
 \end{code}
 
 tcSimplifyBracket is used when simplifying the constraints arising from
@@ -1567,8 +1583,7 @@ tcSimplifyIPs given_ips wanteds
                -- Unusually for checking, we *must* zonk the given_ips
 
        ; let env = mkRedEnv doc try_me given_ips'
-       ; (improved, binds, irreds, elim_skolems) <- reduceContext env wanteds'
-        ; elim_skolems
+       ; (improved, binds, irreds) <- reduceContext env wanteds'
 
        ; if not improved then 
                ASSERT( all is_free irreds )
@@ -1658,7 +1673,7 @@ data RedEnv
           , red_try_me :: Inst -> WhatToDo
           , red_improve :: Bool                -- True <=> do improvement
           , red_givens :: [Inst]               -- All guaranteed rigid
-                                               -- Always dicts
+                                               -- Always dicts & equalities
                                                -- but see Note [Rigidity]
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
@@ -1741,110 +1756,92 @@ reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
                      TcDictBinds,      -- Dictionary bindings
-                     [Inst],           -- Irreducible
-                      TcM ())           -- Undo skolems from SkolemOccurs
+                     [Inst])           -- Irreducible
 
-reduceContext env wanteds
+reduceContext env wanteds0
   = do { traceTc (text "reduceContext" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr (red_givens env),
-            text "wanted" <+> ppr wanteds,
+            text "wanted" <+> ppr wanteds0,
             text "----------------------"
             ]))
 
-
-       ; let givens                       = red_givens env
-             (given_eqs0, given_dicts0)   = partition isEqInst givens
-             (wanted_eqs0, wanted_non_eqs) = partition isEqInst wanteds
-             (wanted_implics0, wanted_dicts) = partition isImplicInst wanted_non_eqs
-
           -- We want to add as wanted equalities those that (transitively) 
           -- occur in superclass contexts of wanted class constraints.
           -- See Note [Ancestor Equalities]
-       ; ancestor_eqs <- ancestorEqualities wanted_dicts
-        ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
+       ; ancestor_eqs <- ancestorEqualities wanteds0
        ; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
 
-         -- 1. Normalise the *given* *equality* constraints
-       ; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
-
-         -- 2. Normalise the *given* *dictionary* constraints
-         --    wrt. the toplevel and given equations
-       ; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs
-                                                            given_dicts0
-
-          -- 5. Build the Avail mapping from "given_dicts"
-       ; (init_state, extra_givens) <- getLIE $ do 
-               { init_state <- foldlM addGiven emptyAvails given_dicts
+          -- Normalise and solve all equality constraints as far as possible
+          -- and normalise all dictionary constraints wrt to the reduced
+          -- equalities.  The returned wanted constraints include the
+          -- irreducible wanted equalities.
+        ; let wanteds = wanteds0 ++ ancestor_eqs
+              givens  = red_givens env
+        ; (givens', 
+           wanteds', 
+           normalise_binds,
+           eq_improved)     <- tcReduceEqs givens wanteds
+       ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
+                     [ppr givens', ppr wanteds', ppr normalise_binds]
+
+          -- Build the Avail mapping from "given_dicts"
+       ; (init_state, _) <- getLIE $ do 
+               { init_state <- foldlM addGiven emptyAvails givens'
                ; return init_state
                 }
 
-       -- *** ToDo: what to do with the "extra_givens"?  For the
-       -- moment I'm simply discarding them, which is probably wrong
-
-          -- 6. Solve the *wanted* *dictionary* constraints (not implications)
-         --    This may expose some further equational constraints...
+          -- Solve the *wanted* *dictionary* constraints (not implications)
+         -- This may expose some further equational constraints...
+       ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
-       ; (dict_binds, bound_dicts, dict_irreds) 
-            <- extractResults avails wanted_dicts
-       ; traceTc $ text "reduceContext extractresults" <+> vcat
+       ; (dict_binds, 
+           bound_dicts, 
+           dict_irreds)       <- extractResults avails wanted_dicts
+       ; traceTc $ text "reduceContext: extractResults" <+> vcat
                      [ppr avails, ppr wanted_dicts, ppr dict_binds]
 
          -- Solve the wanted *implications*.  In doing so, we can provide
          -- as "given"   all the dicts that were originally given, 
          --              *or* for which we now have bindings, 
          --              *or* which are now irreds
-       ; let implic_env = env { red_givens = givens ++ bound_dicts 
-                                              ++ dict_irreds }
+          -- NB: Equality irreds need to be converted, as the recursive 
+          --     invocation of the solver will still treat them as wanteds
+          --     otherwise.
+       ; let implic_env = env { red_givens 
+                                   = givens ++ bound_dicts ++
+                                     map wantedToLocalEqInst dict_irreds }
        ; (implic_binds_s, implic_irreds_s) 
-            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics0
+            <- mapAndUnzipM (reduceImplication implic_env) wanted_implics
        ; let implic_binds  = unionManyBags implic_binds_s
              implic_irreds = concat implic_irreds_s
 
-         -- Normalise the wanted equality constraints
-       ; eq_irreds <- normaliseWantedEqs given_eqs (wanted_eqs ++ extra_eqs)
-
-         -- Normalise the wanted dictionaries
-       ; let irreds = dict_irreds ++ implic_irreds
-              eqs    = eq_irreds ++ given_eqs
-       ; (norm_irreds, normalise_binds) <- normaliseWantedDicts eqs irreds
-               
-         -- Figure out whether we should go round again.  We do so in either
-          -- two cases:
-          -- (1) If any of the mutable tyvars in givens or irreds has been
-          --     filled in by improvement, there is merit in going around 
-          --     again, because we may make further progress.
-          -- (2) If we managed to normalise any dicts, there is merit in going
-          --     around gain, because reduceList may be able to get further.
-         -- 
-         -- ToDo: We may have exposed new
-         --       equality constraints and should probably go round again
-         --       then as well.  But currently we are dropping them on the
-         --       floor anyway.
-
-       ; let all_irreds = norm_irreds ++ eq_irreds
-       ; improvedMetaTy <- anyM isFilledMetaTyVar $ varSetElems $
-                           tyVarsOfInsts (givens ++ all_irreds)
-        ; let improvedDicts = not $ isEmptyBag normalise_binds
-              improved      = improvedMetaTy || improvedDicts
-
-       -- The old plan (fragile)
-       -- improveed   = availsImproved avails 
-       --               || (not $ isEmptyBag normalise_binds1)
-       --               || (not $ isEmptyBag normalise_binds2)
-       --               || (any isEqInst irreds)
+          -- Collect all irreducible instances, and determine whether we should
+          -- go round again.  We do so in either of two cases:
+          -- (1) If dictionary reduction or equality solving led to
+          --     improvement (i.e., instantiated type variables).
+          -- (2) If we uncovered extra equalities.  We will try to solve them
+          --     in the next iteration.
+
+       ; let all_irreds       = dict_irreds ++ implic_irreds ++ extra_eqs
+             avails_improved  = availsImproved avails
+              improvedFlexible = avails_improved || eq_improved
+              extraEqs         = (not . null) extra_eqs
+              improved         = improvedFlexible || extraEqs
+              --
+              improvedHint  = (if avails_improved then " [AVAILS]" else "") ++
+                              (if eq_improved then " [EQ]" else "") ++
+                              (if extraEqs then " [EXTRA EQS]" else "")
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
             red_doc env,
             text "given" <+> ppr givens,
-            text "given_eqs" <+> ppr given_eqs,
-            text "wanted" <+> ppr wanteds,
-            text "wanted_dicts" <+> ppr wanted_dicts,
+            text "wanted" <+> ppr wanteds0,
             text "----",
             text "avails" <+> pprAvails avails,
-            text "improved =" <+> ppr improved,
+            text "improved =" <+> ppr improved <+> text improvedHint,
             text "(all) irreds = " <+> ppr all_irreds,
             text "dict-binds = " <+> ppr dict_binds,
             text "implic-binds = " <+> ppr implic_binds,
@@ -1852,11 +1849,9 @@ reduceContext env wanteds
             ]))
 
        ; return (improved, 
-                  given_binds `unionBags` normalise_binds
-                              `unionBags` dict_binds 
-                              `unionBags` implic_binds, 
-                  all_irreds,
-                  eliminate_skolems) 
+                  normalise_binds `unionBags` dict_binds 
+                                  `unionBags` implic_binds, 
+                  all_irreds) 
         }
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
@@ -1871,30 +1866,44 @@ tcImproveOne avails inst
                -- Avails has all the superclasses etc (good)
                -- It also has all the intermediates of the deduction (good)
                -- It does not have duplicates (good)
-               -- NB that (?x::t1) and (?x::t2) will be held separately in avails
-               --    so that improve will see them separate
+               -- NB that (?x::t1) and (?x::t2) will be held separately in 
+                --    avails so that improve will see them separate
        ; traceTc (text "improveOne" <+> ppr inst)
        ; unifyEqns eqns }
 
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] 
+unifyEqns :: [(Equation, (PredType, SDoc), (PredType, SDoc))] 
          -> TcM ImprovementDone
 unifyEqns [] = return False
 unifyEqns eqns
   = do { traceTc (ptext (sLit "Improve:") <+> vcat (map pprEquationDoc eqns))
-        ; mapM_ unify eqns
-       ; return True }
+        ; improved <- mapM unify eqns
+       ; return $ or improved
+        }
   where
     unify ((qtvs, pairs), what1, what2)
-         = 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)
+         = addErrCtxtM (mkEqnMsg what1 what2) $ 
+             do { let freeTyVars = unionVarSets (map tvs_pr pairs) 
+                                   `minusVarSet` qtvs
+                ; (_, _, tenv) <- tcInstTyVars (varSetElems qtvs)
+                ; mapM_ (unif_pr tenv) pairs
+                ; anyM isFilledMetaTyVar $ varSetElems freeTyVars
+                }
+
+    unif_pr tenv (ty1, ty2) = unifyType (substTy tenv ty1) (substTy tenv ty2)
+
+    tvs_pr (ty1, ty2) = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2
 
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
+pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
+pprEquationDoc (eqn, (p1, _), (p2, _)) 
+  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
 
+mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
+         -> TcM (TidyEnv, SDoc)
 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
-  = do { pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
-       ; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
+  = do { pred1' <- zonkTcPredType pred1
+        ; pred2' <- zonkTcPredType pred2
+       ; let { pred1'' = tidyPred tidy_env pred1'
+              ; pred2'' = tidyPred tidy_env pred2' }
        ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
                          nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
                          nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
@@ -1921,9 +1930,16 @@ reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
                         ; go ws state' }
 
     -- Base case: we're done!
+reduce :: RedEnv -> Inst -> Avails -> TcM Avails
 reduce env wanted avails
+
+    -- We don't reduce equalities here (and they must not end up as irreds
+    -- in the Avails!)
+  | isEqInst wanted
+  = return avails
+
     -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- findAvail avails wanted
+  | Just _ <- findAvail avails wanted
   = do { traceTc (text "reduce: found " <+> ppr wanted)
        ; return avails
        }
@@ -1963,7 +1979,7 @@ reduce env wanted avails
       = do { res <- lookupSimpleInst wanted
           ; case res of
                GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
-               other          -> do_this_otherwise avails wanted }
+               _              -> do_this_otherwise avails wanted }
 \end{code}
 
 
@@ -2054,7 +2070,7 @@ contributing clauses.
 \begin{code}
 ---------------------------------------------
 reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails other_inst
+reduceInst _ avails other_inst
   = do { result <- lookupSimpleInst other_inst
        ; return (avails, result) }
 \end{code}
@@ -2125,7 +2141,7 @@ reduceImplication env
                                  tci_tyvars = tvs,
                                  tci_given = extra_givens, tci_wanted = wanteds })
   = do {       -- Solve the sub-problem
-       ; let try_me inst = ReduceMe AddSCs  -- Note [Freeness and implications]
+       ; let try_me _ = ReduceMe AddSCs  -- Note [Freeness and implications]
              env' = env { red_givens = extra_givens ++ red_givens env
                         , red_doc = sep [ptext (sLit "reduceImplication for") 
                                             <+> ppr name,
@@ -2157,10 +2173,16 @@ reduceImplication env
        -- 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)))
+        ; let backOff = isEmptyLHsBinds binds &&   -- no new bindings
+                        (not $ null irreds)   &&   -- but still some irreds
+                        all (not . isEqInst) wanteds  
+                          -- we may have instantiated a cotv 
+                          -- => must make a new implication constraint!
+
+       ; traceTc $ text "reduceImplication condition" <+> ppr backOff
 
---     Progress is no longer measered by the number of bindings
-       ; if (isEmptyLHsBinds binds) && (not $ null irreds) then        -- No progress
+          -- Progress is no longer measered by the number of bindings
+       ; if backOff then       -- No progress
                -- If there are any irreds, we back off and do nothing
                return (emptyBag, [orig_implic])
          else do
@@ -2200,6 +2222,7 @@ reduceImplication env
                  simpler_implic_insts)
        } 
     }
+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
 \end{code}
 
 Note [Always inline implication constraints]
@@ -2297,6 +2320,7 @@ data AvailHow
 instance Outputable Avails where
   ppr = pprAvails
 
+pprAvails :: Avails -> SDoc
 pprAvails (Avails imp avails)
   = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
         , nest 2 $ braces $ 
@@ -2341,11 +2365,8 @@ extendAvails avails@(Avails imp env) inst avail
 availsInsts :: Avails -> [Inst]
 availsInsts (Avails _ avails) = keysFM avails
 
+availsImproved :: Avails -> ImprovementDone
 availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
 \end{code}
 
 Extracting the bindings from a bunch of Avails.
@@ -2373,10 +2394,13 @@ extractResults (Avails _ avails) wanteds
        -> DoneEnv      -- Has an entry for each inst in the above three sets
        -> [Inst]       -- Wanted
        -> TcM (TcDictBinds, [Inst], [Inst])
-    go binds bound_dicts irreds done [] 
+    go binds bound_dicts irreds _ [] 
       = return (binds, bound_dicts, irreds)
 
     go binds bound_dicts irreds done (w:ws)
+      | isEqInst w
+      = go binds bound_dicts (w:irreds) done' ws
+
       | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
       = if w_id `elem` done_ids then
           go binds bound_dicts irreds done ws
@@ -2455,7 +2479,7 @@ addAvailAndSCs want_scs avails inst avail
     -- Watch out, though.  Since the avails may contain loops 
     -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
     findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
-    findAllDeps so_far other       = so_far
+    findAllDeps so_far _            = so_far
 
     find_all :: IdSet -> Inst -> IdSet
     find_all so_far kid
@@ -2495,7 +2519,7 @@ addSCs is_loop avails dict
     is_given :: Inst -> Bool
     is_given sc_dict = case findAvail avails sc_dict of
                          Just (Given _) -> True        -- Given is cheaper than superclass selection
-                         other          -> False       
+                         _              -> False
 
 -- From the a set of insts obtain all equalities that (transitively) occur in
 -- superclass contexts of class constraints (aka the ancestor equalities). 
@@ -2559,6 +2583,7 @@ tcSimplifyInteractive wanteds
 
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
+tc_simplify_top :: SDoc -> Bool -> [Inst] -> TcM (Bag (LHsBind TcId))
 tc_simplify_top doc interactive wanteds
   = do { dflags <- getDOpts
        ; wanteds <- zonkInsts wanteds
@@ -2568,7 +2593,7 @@ tc_simplify_top doc interactive 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
+       ; (irreds2, binds2) <- approximateImplications doc2 (\_ -> True) irreds1
        ; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
 
                -- Use the defaulting rules to do extra unification
@@ -2675,7 +2700,7 @@ disambiguate doc interactive dflags insts
        | extended_defaulting = any isInteractiveClass clss
        | otherwise           = all is_std_class clss && (any is_num_class clss)
 
-       -- In interactive mode, or with -fextended-default-rules,
+       -- In interactive mode, or with -XExtendedDefaultRules,
        -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
@@ -2736,12 +2761,12 @@ getDefaultTys extended_deflts ovl_strings
                  opt_deflt ovl_strings string_ty) } } }
   where
     opt_deflt True  ty = [ty]
-    opt_deflt False ty = []
+    opt_deflt False _  = []
 \end{code}
 
 Note [Default unitTy]
 ~~~~~~~~~~~~~~~~~~~~~
-In interative mode (or with -fextended-default-rules) we add () as the first type we
+In interative mode (or with -XExtendedDefaultRules) we add () as the first type we
 try when defaulting.  This has very little real impact, except in the following case.
 Consider: 
        Text.Printf.printf "hello"
@@ -2853,7 +2878,7 @@ groupErrs :: ([Inst] -> TcM ())   -- Deal with one group
 -- Group together insts with the same origin
 -- We want to report them together in error messages
 
-groupErrs report_err [] 
+groupErrs _ [] 
   = return ()
 groupErrs report_err (inst:insts)
   = do { do_one (inst:friends)
@@ -2873,7 +2898,7 @@ addInstLoc :: [Inst] -> Message -> Message
 addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
 
 addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs [] 
+addTopIPErrs _ [] 
   = return ()
 addTopIPErrs bndrs ips
   = do { dflags <- getDOpts
@@ -2916,6 +2941,7 @@ reportNoInstances
 reportNoInstances tidy_env mb_what insts 
   = groupErrs (report_no_instances tidy_env mb_what) insts
 
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
 report_no_instances tidy_env mb_what insts
   = do { inst_envs <- tcGetInstEnvs
        ; let (implics, insts1)  = partition isImplicInst insts
@@ -2947,7 +2973,7 @@ report_no_instances tidy_env mb_what insts
                -- The case of exactly one match and no unifiers means a
                -- successful lookup.  That can't happen here, because dicts
                -- only end up here if they didn't match in Inst.lookupInst
-               ([m],[])
+               ([_],[])
                 | debugIsOn -> pprPanic "reportNoInstance" (ppr wanted)
                res -> Right (mk_overlap_msg wanted res)
          where
@@ -2966,7 +2992,7 @@ report_no_instances tidy_env mb_what insts
                ASSERT( not (null unifiers) )
                parens (vcat [ptext (sLit "The choice depends on the instantiation of") <+>
                                 quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
-                             ptext (sLit "To pick the first instance above, use -fallow-incoherent-instances"),
+                             ptext (sLit "To pick the first instance above, use -XIncoherentInstances"),
                              ptext (sLit "when compiling the other instance declarations")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]
@@ -3009,6 +3035,7 @@ report_no_instances tidy_env mb_what insts
        show_fixes (f:fs) = sep [ptext (sLit "Possible fix:"), 
                                 nest 2 (vcat (f : map (ptext (sLit "or") <+>) fs))]
 
+addTopAmbigErrs :: [Inst] -> TcRn ()
 addTopAmbigErrs dicts
 -- Divide into groups that share a common set of ambiguous tyvars
   = ifErrsM (return ()) $      -- Only report ambiguity if no other errors happened
@@ -3064,10 +3091,11 @@ monomorphism_fix dflags
   = ptext (sLit "Probable fix:") <+> vcat
        [ptext (sLit "give these definition(s) an explicit type signature"),
         if dopt Opt_MonomorphismRestriction dflags
-           then ptext (sLit "or use -fno-monomorphism-restriction")
-           else empty] -- Only suggest adding "-fno-monomorphism-restriction"
+           then ptext (sLit "or use -XNoMonomorphismRestriction")
+           else empty] -- Only suggest adding "-XNoMonomorphismRestriction"
                        -- if it is not already set!
     
+warnDefault :: [(Inst, Class, Var)] -> Type -> TcM ()
 warnDefault ups default_ty = do
     warn_flag <- doptM Opt_WarnTypeDefaults
     addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
@@ -3080,10 +3108,12 @@ warnDefault ups default_ty = do
                                quotes (ppr default_ty),
                      pprDictsInFull tidy_dicts]
 
+reduceDepthErr :: Int -> [Inst] -> SDoc
 reduceDepthErr n stack
   = vcat [ptext (sLit "Context reduction stack overflow; size =") <+> int n,
          ptext (sLit "Use -fcontext-stack=N to increase stack size to N"),
          nest 4 (pprStack stack)]
 
+pprStack :: [Inst] -> SDoc
 pprStack stack = vcat (map pprInstInFull stack)
 \end{code}