Three improvements to Template Haskell (fixes #3467)
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index a274cab..2ad5b2f 100644 (file)
@@ -16,7 +16,7 @@ module TcSimplify (
 
        tcSimplifyDeriv, tcSimplifyDefault,
        bindInstsOfLocalFuns, 
-
+       
         misMatchMsg
     ) where
 
@@ -43,7 +43,6 @@ import Class
 import FunDeps
 import PrelInfo
 import PrelNames
-import Type
 import TysWiredIn
 import ErrUtils
 import BasicTypes
@@ -52,12 +51,12 @@ import VarEnv
 import FiniteMap
 import Bag
 import Outputable
-import Maybes
 import ListSetOps
 import Util
 import SrcLoc
 import DynFlags
 import FastString
+
 import Control.Monad
 import Data.List
 \end{code}
@@ -656,7 +655,7 @@ tcSimplifyInfer doc tau_tvs wanted
        ; gbl_tvs  <- tcGetGlobalTyVars
        ; let preds1   = fdPredsOfInsts wanted'
              gbl_tvs1 = oclose preds1 gbl_tvs
-             qtvs     = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
+             qtvs     = growInstsTyVars wanted' tau_tvs1 `minusVarSet` gbl_tvs1
                        -- See Note [Choosing which variables to quantify]
 
                -- To maximise sharing, remove from consideration any 
@@ -665,7 +664,7 @@ tcSimplifyInfer doc tau_tvs wanted
        ; extendLIEs free
 
                -- To make types simple, reduce as much as possible
-       ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ 
+       ; traceTc (text "infer" <+> (ppr preds1 $$ ppr (growInstsTyVars wanted' tau_tvs1) $$ ppr gbl_tvs $$ 
                   ppr gbl_tvs1 $$ ppr free $$ ppr bound))
        ; (irreds1, binds1) <- tryHardCheckLoop doc bound
 
@@ -706,7 +705,13 @@ tcSimplifyInfer doc tau_tvs wanted
                -- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
                -- irreds2 will be empty.  But we don't want to generalise over b!
        ; let preds2 = fdPredsOfInsts irreds2   -- irreds2 is zonked
-             qtvs   = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+             qtvs   = growInstsTyVars irreds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
+               ---------------------------------------------------
+               -- BUG WARNING: there's a nasty bug lurking here
+               -- fdPredsOfInsts may return preds that mention variables quantified in
+               -- one of the implication constraints in irreds2; and that is clearly wrong:
+               -- we might quantify over too many variables through accidental capture
+               ---------------------------------------------------
        ; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
        ; extendLIEs free
 
@@ -861,7 +866,7 @@ Note [NO TYVARS]
 
 The excitement comes when simplifying the bindings for h.  Initially
 try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
-From this we get t1:=:t2, but also various bindings.  We can't forget
+From this we get t1~t2, but also various bindings.  We can't forget
 the bindings (because of [LOOP]), but in fact t1 is what g is
 polymorphic in.  
 
@@ -971,17 +976,17 @@ makeImplicationBind :: InstLoc -> [TcTyVar]
                    -> [Inst] -> [Inst]
                    -> TcM ([Inst], TcDictBinds)
 -- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
+-- constraint for them.
+--
 -- The binding looks like
 --     (ir1, .., irn) = f qtvs givens
 -- where f is (evidence for) the new implication constraint
---     f :: forall qtvs. {reft} givens => (ir1, .., irn)
+--     f :: forall qtvs. givens => (ir1, .., irn)
 -- qtvs includes coercion variables
 --
 -- This binding must line up the 'rhs' in reduceImplication
 makeImplicationBind loc all_tvs
-                   givens      -- Guaranteed all Dicts
-                               -- or EqInsts
+                   givens      -- Guaranteed all Dicts or EqInsts
                    irreds
  | null irreds                 -- If there are no irreds, we are done
  = return ([], emptyBag)
@@ -989,28 +994,38 @@ makeImplicationBind loc all_tvs
  = do  { uniq <- newUnique 
        ; span <- getSrcSpanM
        ; let (eq_givens, dict_givens) = partition isEqInst 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
+                -- extract equality binders
+              eq_cotvs = map eqInstType eq_givens
+
+                -- make the implication constraint instance
+             name = mkInternalName uniq (mkVarOcc "ic") span
              implic_inst = ImplicInst { tci_name = name,
                                         tci_tyvars = all_tvs, 
-                                        tci_given = (eq_givens ++ dict_givens),
-                                        tci_wanted = irreds, tci_loc = loc }
-       ; let   -- only create binder for dict_irreds
-             (_, dict_irreds) = partition isEqInst irreds
+                                        tci_given = eq_givens ++ dict_givens,
+                                                       -- same order as binders
+                                        tci_wanted = irreds, 
+                                         tci_loc = loc }
+
+               -- create binders for the irreducible dictionaries
+             dict_irreds    = filter (not . 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)))
-             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 = lpat, 
-                                                 pat_rhs = unguardedGRHSs rhs, 
-                                                 pat_rhs_ty = hsLPatType lpat,
-                                                 bind_fvs = placeHolderNames }
+
+                -- create the binding
+             rhs  = L span (mkHsWrap co (HsVar (instToId implic_inst)))
+             co   =     mkWpApps (map instToId dict_givens)
+                    <.> mkWpTyApps eq_cotvs
+                    <.> mkWpTyApps (mkTyVarTys all_tvs)
+             bind | [dict_irred_id] <- dict_irred_ids  
+                   = VarBind dict_irred_id rhs
+                  | otherwise        
+                   = PatBind { pat_lhs = lpat
+                            , pat_rhs = unguardedGRHSs rhs 
+                            , pat_rhs_ty = hsLPatType lpat
+                            , bind_fvs = placeHolderNames 
+                             }
+
        ; traceTc $ text "makeImplicationBind" <+> ppr implic_inst
        ; return ([implic_inst], unitBag (L span bind)) 
         }
@@ -1096,7 +1111,9 @@ checkLoop env wanteds
                 ; env'     <- zonkRedEnv env
                ; wanteds' <- zonkInsts  wanteds
        
-               ; (improved, binds, irreds) <- reduceContext env' wanteds'
+               ; (improved, tybinds, binds, irreds) 
+                    <- reduceContext env' wanteds'
+                ; execTcTyVarBinds tybinds
 
                ; if null irreds || not improved then
                    return (irreds, binds)
@@ -1252,9 +1269,23 @@ the givens, as you can see from the derivation described above.
 
 Conclusion: in the very special case of tcSimplifySuperClasses
 we have one 'given' (namely the "this" dictionary) whose superclasses
-must not be added to 'givens' by addGiven.  That is the *whole* reason
-for the red_given_scs field in RedEnv, and the function argument to
-addGiven.
+must not be added to 'givens' by addGiven.  
+
+There is a complication though.  Suppose there are equalities
+      instance (Eq a, a~b) => Num (a,b)
+Then we normalise the 'givens' wrt the equalities, so the original
+given "this" dictionary is cast to one of a different type.  So it's a
+bit trickier than before to identify the "special" dictionary whose
+superclasses must not be added. See test
+   indexed-types/should_run/EqInInstance
+
+We need a persistent property of the dictionary to record this
+special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
+but cool), which is maintained by dictionary normalisation.
+Specifically, the InstLocOrigin is
+            NoScOrigin
+then the no-superclass thing kicks in.  WATCH OUT if you fiddle
+with InstLocOrigin!
 
 \begin{code}
 tcSimplifySuperClasses
@@ -1266,20 +1297,23 @@ tcSimplifySuperClasses
        -> TcM TcDictBinds
 tcSimplifySuperClasses loc this givens sc_wanteds
   = do { traceTc (text "tcSimplifySuperClasses")
+
+             -- Note [Recursive instances and superclases]
+        ; no_sc_loc <- getInstLoc NoScOrigin
+       ; let no_sc_this = setInstLoc this no_sc_loc
+
+       ; let env =  RedEnv { red_doc = pprInstLoc loc, 
+                             red_try_me = try_me,
+                             red_givens = no_sc_this : givens, 
+                             red_stack = (0,[]),
+                             red_improve = False }  -- No unification vars
+
+
        ; (irreds,binds1) <- checkLoop env sc_wanteds
        ; let (tidy_env, tidy_irreds) = tidyInsts irreds
-       ; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
+       ; reportNoInstances tidy_env (Just (loc, givens)) [] tidy_irreds
        ; return binds1 }
   where
-    env =  RedEnv { red_doc = pprInstLoc loc, 
-                   red_try_me = try_me,
-                   red_givens = this:givens, 
-                   red_given_scs = add_scs,
-                   red_stack = (0,[]),
-                   red_improve = False }  -- No unification vars
-    add_scs g | g==this   = NoSCs
-             | otherwise = AddSCs
-
     try_me _ = ReduceMe  -- Try hard, so we completely solve the superclass 
                         -- constraints right here. See Note [SUPERCLASS-LOOP 1]
 \end{code}
@@ -1402,7 +1436,7 @@ tcSimplifyRestricted      -- Used for restricted binding groups
 tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
        -- Zonk everything in sight
   = do { traceTc (text "tcSimplifyRestricted")
-       ; wanteds' <- zonkInsts wanteds
+       ; wanteds_z <- zonkInsts wanteds
 
        -- 'ReduceMe': Reduce as far as we can.  Don't stop at
        -- dicts; the idea is to get rid of as many type
@@ -1414,7 +1448,8 @@ 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 (\_ -> ReduceMe)
-       ; (_imp, _binds, constrained_dicts) <- reduceContext env wanteds'
+       ; (_imp, _tybinds, _binds, constrained_dicts) 
+            <- reduceContext env wanteds_z
 
        -- Next, figure out the tyvars we will quantify over
        ; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
@@ -1463,7 +1498,8 @@ tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
                           (is_nested_group || isDict inst) = Stop
                          | otherwise                       = ReduceMe 
              env = mkNoImproveRedEnv doc try_me
-       ; (_imp, binds, irreds) <- reduceContext env wanteds'
+       ; (_imp, tybinds, binds, irreds) <- reduceContext env wanteds_z
+        ; execTcTyVarBinds tybinds
 
        -- See "Notes on implicit parameters, Question 4: top level"
        ; ASSERT( all (isFreeWrtTyVars qtvs) irreds )   -- None should be captured
@@ -1549,13 +1585,23 @@ Simpler, maybe, but alas not simple (see Trac #2494)
 tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
 tcSimplifyRuleLhs wanteds
   = do { wanteds' <- zonkInsts wanteds
-       ; (irreds, binds) <- go [] emptyBag wanteds'
+       
+               -- Simplify equalities  
+               -- It's important to do this: Trac #3346 for example
+        ; (_, wanteds'', tybinds, binds1) <- tcReduceEqs [] wanteds'
+        ; execTcTyVarBinds tybinds
+
+               -- Simplify other constraints
+       ; (irreds, binds2) <- go [] emptyBag wanteds''
+
+               -- Report anything that is left
        ; 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) }
+
+       ; return (dicts, binds1 `unionBags` binds2) }
   where
     go :: [Inst] -> TcDictBinds -> [Inst] -> TcM ([Inst], TcDictBinds)
     go irreds binds []
@@ -1597,7 +1643,7 @@ this bracket again at its usage site.
 \begin{code}
 tcSimplifyBracket :: [Inst] -> TcM ()
 tcSimplifyBracket wanteds
-  = do { tryHardCheckLoop doc wanteds
+  = do { _ <- tryHardCheckLoop doc wanteds
        ; return () }
   where
     doc = text "tcSimplifyBracket"
@@ -1640,14 +1686,23 @@ 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, tybinds, binds, irreds) <- reduceContext env wanteds'
+        ; execTcTyVarBinds tybinds
 
-       ; if not improved then 
+       ; if null irreds || not improved then 
                ASSERT( all is_free irreds )
                do { extendLIEs irreds
                   ; return binds }
-         else
-               tcSimplifyIPs given_ips wanteds }
+         else do
+        -- If improvement did some unification, we go round again.
+        -- We start again with irreds, not wanteds
+        -- Using an instance decl might have introduced a fresh type
+        -- variable which might have been unified, so we'd get an 
+        -- infinite loop if we started again with wanteds!  
+        -- See Note [LOOP]
+        { binds1 <- tcSimplifyIPs given_ips' irreds
+        ; return $ binds `unionBags` binds1
+        } }
   where
     doc           = text "tcSimplifyIPs" <+> ppr given_ips
     ip_set = mkNameSet (ipNamesOfInsts given_ips)
@@ -1733,8 +1788,6 @@ data RedEnv
                                                -- Always dicts & equalities
                                                -- but see Note [Rigidity]
  
-          , red_given_scs :: Inst -> WantSCs   -- See Note [Recursive instances and superclases]
           , red_stack  :: (Int, [Inst])        -- Recursion stack (for err msg)
                                                -- See Note [RedStack]
   }
@@ -1757,7 +1810,6 @@ mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
 mkRedEnv doc try_me givens
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_givens = givens, 
-            red_given_scs = const AddSCs,
             red_stack = (0,[]),
             red_improve = True }       
 
@@ -1766,7 +1818,6 @@ mkInferRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 mkInferRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_givens = [], 
-            red_given_scs = const AddSCs,
             red_stack = (0,[]),
             red_improve = True }       
 
@@ -1775,7 +1826,6 @@ mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
 mkNoImproveRedEnv doc try_me
   = RedEnv { red_doc = doc, red_try_me = try_me,
             red_givens = [], 
-            red_given_scs = const AddSCs,
             red_stack = (0,[]),
             red_improve = True }       
 
@@ -1826,6 +1876,7 @@ discharge with the explicit instance.
 reduceContext :: RedEnv
              -> [Inst]                 -- Wanted
              -> TcM (ImprovementDone,
+                      TcTyVarBinds,     -- Type variable bindings
                      TcDictBinds,      -- Dictionary bindings
                      [Inst])           -- Irreducible
 
@@ -1852,22 +1903,26 @@ reduceContext env wanteds0
               givens  = red_givens env
         ; (givens', 
            wanteds', 
-           normalise_binds,
-           eq_improved)     <- tcReduceEqs givens wanteds
+           tybinds,
+           normalise_binds) <- tcReduceEqs givens wanteds
        ; traceTc $ text "reduceContext: tcReduceEqs result" <+> vcat
-                     [ppr givens', ppr wanteds', ppr normalise_binds]
+                     [ppr givens', ppr wanteds', ppr tybinds, 
+                       ppr normalise_binds]
 
           -- Build the Avail mapping from "given_dicts"
        ; (init_state, _) <- getLIE $ do 
-               { init_state <- foldlM (addGiven (red_given_scs env)) 
-                                      emptyAvails givens'
+               { init_state <- foldlM addGiven emptyAvails givens'
                ; return init_state
                 }
 
           -- Solve the *wanted* *dictionary* constraints (not implications)
-         -- This may expose some further equational constraints...
+         -- This may expose some further equational constraints in the course
+          -- of improvement due to functional dependencies if any of the
+          -- involved unifications gets deferred.
        ; let (wanted_implics, wanted_dicts) = partition isImplicInst wanteds'
        ; (avails, extra_eqs) <- getLIE (reduceList env wanted_dicts init_state)
+                  -- The getLIE is reqd because reduceList does improvement
+                  -- (via extendAvails) which may in turn do unification
        ; (dict_binds, 
            bound_dicts, 
            dict_irreds)       <- extractResults avails wanted_dicts
@@ -1892,19 +1947,26 @@ reduceContext env wanteds0
           -- 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.
+          --     improvement (i.e., bindings for type variables).
+          -- (2) If we reduced dictionaries (i.e., got dictionary bindings),
+          --     they may have exposed further opportunities to normalise
+          --     family applications.  See Note [Dictionary Improvement]
+          --
+          -- NB: We do *not* go around for new extra_eqs.  Morally, we should,
+          --     but we can't without risking non-termination (see #2688).  By
+          --     not going around, we miss some legal programs mixing FDs and
+          --     TFs, but we never claimed to support such programs in the
+          --     current implementation anyway.
 
        ; let all_irreds       = dict_irreds ++ implic_irreds ++ extra_eqs
              avails_improved  = availsImproved avails
+              eq_improved      = anyBag (not . isCoVarBind) tybinds
               improvedFlexible = avails_improved || eq_improved
-              extraEqs         = (not . null) extra_eqs
-              improved         = improvedFlexible || extraEqs
+              reduced_dicts    = not (isEmptyBag dict_binds)
+              improved         = improvedFlexible || reduced_dicts
               --
               improvedHint  = (if avails_improved then " [AVAILS]" else "") ++
-                              (if eq_improved then " [EQ]" else "") ++
-                              (if extraEqs then " [EXTRA EQS]" else "")
+                              (if eq_improved then " [EQ]" else "")
 
        ; traceTc (text "reduceContext end" <+> (vcat [
             text "----------------------",
@@ -1912,6 +1974,7 @@ reduceContext env wanteds0
             text "given" <+> ppr givens,
             text "wanted" <+> ppr wanteds0,
             text "----",
+            text "tybinds" <+> ppr tybinds,
             text "avails" <+> pprAvails avails,
             text "improved =" <+> ppr improved <+> text improvedHint,
             text "(all) irreds = " <+> ppr all_irreds,
@@ -1921,10 +1984,13 @@ reduceContext env wanteds0
             ]))
 
        ; return (improved, 
+                  tybinds,
                   normalise_binds `unionBags` dict_binds 
                                   `unionBags` implic_binds, 
                   all_irreds) 
         }
+  where
+    isCoVarBind (TcTyVarBind tv _) = isCoVar tv
 
 tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
 tcImproveOne avails inst
@@ -1982,6 +2048,44 @@ mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
        ; return (tidy_env, msg) }
 \end{code}
 
+Note [Dictionary Improvement]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In reduceContext, we first reduce equalities and then class constraints.
+However, the letter may expose further opportunities for the former.  Hence,
+we need to go around again if dictionary reduction produced any dictionary
+bindings.  The following example demonstrated the point:
+
+  data EX _x _y (p :: * -> *)
+  data ANY
+
+  class Base p
+
+  class Base (Def p) => Prop p where
+   type Def p
+
+  instance Base ()
+  instance Prop () where
+   type Def () = ()
+
+  instance (Base (Def (p ANY))) => Base (EX _x _y p)
+  instance (Prop (p ANY)) => Prop (EX _x _y p) where
+   type Def (EX _x _y p) = EX _x _y p
+
+  data FOO x
+  instance Prop (FOO x) where
+   type Def (FOO x) = ()
+
+  data BAR
+  instance Prop BAR where
+   type Def BAR = EX () () FOO
+
+During checking the last instance declaration, we need to check the superclass
+cosntraint Base (Def BAR), which family normalisation reduced to 
+Base (EX () () FOO).  Chasing the instance for Base (EX _x _y p), gives us
+Base (Def (FOO ANY)), which again requires family normalisation of Def to
+Base () before we can finish.
+
+
 The main context-reduction function is @reduce@.  Here's its game plan.
 
 \begin{code}
@@ -2200,18 +2304,30 @@ Note that
        --
        -- Note on coercion variables:
        --
-       --      The extra given coercion variables are bound at two different sites:
+       --      The extra given coercion variables are bound at two different 
+        --      sites:
+        --
        --      -) in the creation context of the implication constraint        
        --              the solved equational constraints use these binders
        --
        --      -) at the solving site of the implication constraint
-       --              the solved dictionaries use these binders               
+       --              the solved dictionaries use these binders;
        --              these binders are generated by reduceImplication
        --
+        -- Note [Binders for equalities]
+        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+        -- To reuse the binders of local/given equalities in the binders of 
+        -- implication constraints, it is crucial that these given equalities
+        -- always have the form
+        --   cotv :: t1 ~ t2
+        -- where cotv is a simple coercion type variable (and not a more
+        -- complex coercion term).  We require that the extra_givens always
+        -- have this form and exploit the special form when generating binders.
 reduceImplication env
        orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
                                  tci_tyvars = tvs,
-                                 tci_given = extra_givens, tci_wanted = wanteds })
+                                 tci_given = extra_givens, tci_wanted = wanteds
+                                 })
   = do {       -- Solve the sub-problem
        ; let try_me _ = ReduceMe  -- Note [Freeness and implications]
              env' = env { red_givens = extra_givens ++ red_givens env
@@ -2225,13 +2341,6 @@ reduceImplication env
                        [ ppr (red_givens env), ppr extra_givens, 
                          ppr wanteds])
        ; (irreds, binds) <- checkLoop env' wanteds
-       ; let   (extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-                       -- SLPJ Sept 07: I think this is bogus; currently
-                       -- there are no Eqinsts in extra_givens
-               dict_ids = map instToId extra_dict_givens 
-
-               -- Note [Reducing implication constraints]
-               -- Tom -- update note, put somewhere!
 
        ; traceTc (text "reduceImplication result" <+> vcat
                        [ppr irreds, ppr binds])
@@ -2245,17 +2354,17 @@ reduceImplication env
        -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
        -- Then we must iterate the outer loop too!
 
+        ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+                                   -- we solve wanted eqs by side effect!
+
+            -- Progress is no longer measered by the number of bindings
+            -- If there are any irreds, but no bindings and no solved
+            -- equalities, we back off and do nothing
         ; 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
+                        didntSolveWantedEqs        -- no instantiated cotv
 
-          -- 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
        { (simpler_implic_insts, bind) 
@@ -2265,26 +2374,29 @@ reduceImplication env
                -- case.  After all, we only try hard to reduce at top level, or
                -- when inferring types.
 
-       ; let   dict_wanteds = filter (not . isEqInst) wanteds
-               -- TOMDO: given equational constraints bug!
-               --  we need a different evidence for given
-               --  equations depending on whether we solve
-               --  dictionary constraints or equational constraints
-
-               eq_tyvars = varSetElems $ tyVarsOfTypes $ map eqInstType extra_eq_givens
-                       -- SLPJ Sept07: this looks Utterly Wrong to me, but I think
-                       --              that current extra_givens has no EqInsts, so
-                       --              it makes no difference
-               co  = wrap_inline       -- Note [Always inline implication constraints]
-                     <.> mkWpTyLams tvs
-                     <.> mkWpLams eq_tyvars
-                     <.> mkWpLams dict_ids
-                     <.> WpLet (binds `unionBags` bind)
-               wrap_inline | null dict_ids = idHsWrapper
-                           | otherwise     = WpInline
-               rhs = mkLHsWrap co payload
-               loc = instLocSpan inst_loc
-               payload = mkBigLHsTup (map (L loc . HsVar . instToId) dict_wanteds)
+       ; let   -- extract Id binders for dicts and CoTyVar binders for eqs;
+                -- see Note [Binders for equalities]
+             (extra_eq_givens, extra_dict_givens) = partition isEqInst 
+                                                               extra_givens
+              eq_cotvs = map instToVar extra_eq_givens
+             dict_ids = map instToId  extra_dict_givens 
+
+                        -- Note [Always inline implication constraints]
+              wrap_inline | null dict_ids = idHsWrapper
+                          | otherwise    = WpInline
+              co         = wrap_inline
+                           <.> mkWpTyLams tvs
+                           <.> mkWpTyLams eq_cotvs
+                           <.> mkWpLams dict_ids
+                           <.> WpLet (binds `unionBags` bind)
+              rhs        = mkLHsWrap co payload
+              loc        = instLocSpan inst_loc
+                            -- wanted equalities are solved by updating their
+                             -- cotv; we don't generate bindings for them
+              dict_bndrs =   map (L loc . HsVar . instToId) 
+                           . filter (not . isEqInst) 
+                           $ wanteds
+              payload    = mkBigLHsTup dict_bndrs
 
        
        ; traceTc (vcat [text "reduceImplication" <+> ppr name,
@@ -2518,14 +2630,19 @@ addWanted want_scs avails wanted rhs_expr wanteds
   where
     avail = Rhs rhs_expr wanteds
 
-addGiven :: (Inst -> WantSCs) -> Avails -> Inst -> TcM Avails
-addGiven want_scs avails given = addAvailAndSCs (want_scs given) avails given (Given given)
-       -- Conditionally add superclasses for 'givens'
+addGiven :: Avails -> Inst -> TcM Avails
+addGiven avails given 
+  = addAvailAndSCs want_scs avails given (Given given)
+  where
+    want_scs = case instLocOrigin (instLoc given) of
+                NoScOrigin -> NoSCs
+                _other     -> AddSCs
+       -- Conditionally add superclasses for 'given'
        -- See Note [Recursive instances and superclases]
-       --
-       -- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-       -- decl for Ord t we can add both Ord t and Eq t as 'givens', 
-       -- so the assert isn't true
+
+  -- No ASSERT( not (given `elemAvails` avails) ) because in an
+  -- instance decl for Ord t we can add both Ord t and Eq t as
+  -- 'givens', so the assert isn't true
 \end{code}
 
 \begin{code}
@@ -2745,6 +2862,7 @@ disambiguate doc interactive dflags insts
 
   where
    extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
+                      -- See also Trac #1974
    ovl_strings = dopt Opt_OverloadedStrings dflags
 
    unaries :: [(Inst, Class, TcTyVar)]  -- (C tv) constraints
@@ -2791,12 +2909,16 @@ disambigGroup :: [Type]                 -- The default types
              -> TcM () -- Just does unification, to fix the default types
 
 disambigGroup default_tys dicts
-  = try_default default_tys
+  = do { mb_chosen_ty <- try_default default_tys
+       ; case mb_chosen_ty of
+            Nothing        -> return ()
+            Just chosen_ty -> do { _ <- unifyType chosen_ty (mkTyVarTy tyvar) 
+                                ; warnDefault dicts chosen_ty } }
   where
     (_,_,tyvar) = ASSERT(not (null dicts)) head dicts  -- Should be non-empty
     classes = [c | (_,c,_) <- dicts]
 
-    try_default [] = return ()
+    try_default [] = return Nothing
     try_default (default_ty : default_tys)
       = tryTcLIE_ (try_default default_tys) $
        do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
@@ -2806,10 +2928,7 @@ disambigGroup default_tys dicts
                -- For example, if Real a is reqd, but the only type in the
                -- default list is Int.
 
-               -- After this we can't fail
-          ; warnDefault dicts default_ty
-          ; unifyType default_ty (mkTyVarTy tyvar) 
-          ; return () -- TOMDO: do something with the coercion
+          ; return (Just default_ty) -- TOMDO: do something with the coercion
           }
 
 
@@ -2896,7 +3015,8 @@ tcSimplifyDeriv orig tyvars theta
        ; (irreds, _) <- tryHardCheckLoop doc wanteds
 
        ; let (tv_dicts, others) = partition ok irreds
-       ; addNoInstanceErrs others
+             (tidy_env, tidy_insts) = tidyInsts others
+        ; reportNoInstances tidy_env Nothing [alt_fix] tidy_insts
        -- See Note [Exotic derived instance contexts] in TcMType
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
@@ -2910,6 +3030,8 @@ tcSimplifyDeriv orig tyvars theta
 
     ok dict | isDict dict = validDerivPred (dictPred dict)
            | otherwise   = False
+    alt_fix = vcat [ptext (sLit "use a standalone 'deriving instance' declaration instead,"),
+                    ptext (sLit "so you can specify the instance context yourself")]
 \end{code}
 
 
@@ -2924,7 +3046,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
 tcSimplifyDefault theta = do
     wanteds <- newDictBndrsO DefaultOrigin theta
     (irreds, _) <- tryHardCheckLoop doc wanteds
-    addNoInstanceErrs  irreds
+    addNoInstanceErrs irreds
     if null irreds then
        return ()
      else
@@ -2934,6 +3056,7 @@ tcSimplifyDefault theta = do
 \end{code}
 
 
+
 %************************************************************************
 %*                                                                     *
 \section{Errors and contexts}
@@ -2963,7 +3086,7 @@ groupErrs report_err (inst:insts)
    (friends, others) = partition is_friend insts
    loc_msg          = showSDoc (pprInstLoc (instLoc inst))
    is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
-   do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
+   do_one insts = setInstCtxt (instLoc (head insts)) (report_err insts)
                -- Add location and context information derived from the Insts
 
 -- Add the "arising from..." part to a message about bunch of dicts
@@ -3000,7 +3123,7 @@ addNoInstanceErrs :: [Inst]       -- Wanted (can include implications)
                  -> TcM ()     
 addNoInstanceErrs insts
   = do { let (tidy_env, tidy_insts) = tidyInsts insts
-       ; reportNoInstances tidy_env Nothing tidy_insts }
+       ; reportNoInstances tidy_env Nothing [] tidy_insts }
 
 reportNoInstances 
        :: TidyEnv
@@ -3008,14 +3131,15 @@ reportNoInstances
                        -- Nothing => top level
                        -- Just (d,g) => d describes the construct
                        --               with givens g
+        -> [SDoc]      -- Alternative fix for no-such-instance
        -> [Inst]       -- What is wanted (can include implications)
        -> TcM ()       
 
-reportNoInstances tidy_env mb_what insts 
-  = groupErrs (report_no_instances tidy_env mb_what) insts
+reportNoInstances tidy_env mb_what alt_fix insts 
+  = groupErrs (report_no_instances tidy_env mb_what alt_fix) insts
 
-report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [Inst] -> TcM ()
-report_no_instances tidy_env mb_what insts
+report_no_instances :: TidyEnv -> Maybe (InstLoc, [Inst]) -> [SDoc] -> [Inst] -> TcM ()
+report_no_instances tidy_env mb_what alt_fixes insts
   = do { inst_envs <- tcGetInstEnvs
        ; let (implics, insts1)  = partition isImplicInst insts
             (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
@@ -3033,7 +3157,7 @@ report_no_instances tidy_env mb_what insts
     complain_implic inst       -- Recurse!
       = reportNoInstances tidy_env 
                          (Just (tci_loc inst, tci_given inst)) 
-                         (tci_wanted inst)
+                         alt_fixes (tci_wanted inst)
 
     check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
        -- Right msg  => overlap message
@@ -3081,13 +3205,13 @@ report_no_instances tidy_env mb_what insts
       = vcat [ addInstLoc insts $
               sep [ ptext (sLit "Could not deduce") <+> pprDictsTheta insts
                   , nest 2 $ ptext (sLit "from the context") <+> pprDictsTheta givens]
-            , show_fixes (fix1 loc : fixes2) ]
+            , show_fixes (fix1 loc : fixes2 ++ alt_fixes) ]
 
       | otherwise      -- Top level 
       = vcat [ addInstLoc insts $
               ptext (sLit "No instance") <> plural insts
                    <+> ptext (sLit "for") <+> pprDictsTheta insts
-            , show_fixes fixes2 ]
+            , show_fixes (fixes2 ++ alt_fixes) ]
 
       where
        fix1 loc = sep [ ptext (sLit "add") <+> pprDictsTheta insts
@@ -3171,7 +3295,7 @@ monomorphism_fix dflags
 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)
+    setInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
   where
     dicts = [d | (d,_,_) <- ups]