Adding pushing of hpc translation status through hi files.
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index adf0f78..c229733 100644 (file)
@@ -47,6 +47,7 @@ import VarEnv
 import FiniteMap
 import Bag
 import Outputable
+import Maybes
 import ListSetOps
 import Util
 import SrcLoc
@@ -132,14 +133,9 @@ from.
 The Right Thing is to improve whenever the constraint set changes at
 all.  Not hard in principle, but it'll take a bit of fiddling to do.  
 
-
-
-       --------------------------------------
-               Notes on quantification
-       --------------------------------------
-
-Suppose we are about to do a generalisation step.
-We have in our hand
+Note [Choosing which variables to quantify]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are about to do a generalisation step.  We have in our hand
 
        G       the environment
        T       the type of the RHS
@@ -162,11 +158,12 @@ Here are the things that *must* be true:
  (A)   Q intersect fv(G) = EMPTY                       limits how big Q can be
  (B)   Q superset fv(Cq union T) \ oclose(fv(G),C)     limits how small Q can be
 
-(A) says we can't quantify over a variable that's free in the
-environment.  (B) says we must quantify over all the truly free
-variables in T, else we won't get a sufficiently general type.  We do
-not *need* to quantify over any variable that is fixed by the free
-vars of the environment G.
+ (A) says we can't quantify over a variable that's free in the environment. 
+ (B) says we must quantify over all the truly free variables in T, else 
+     we won't get a sufficiently general type.  
+
+We do not *need* to quantify over any variable that is fixed by the
+free vars of the environment G.
 
        BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
 
@@ -180,38 +177,15 @@ Example:  class H x y | x->y where ...
 
        So Q can be {c,d}, {b,c,d}
 
+In particular, it's perfectly OK to quantify over more type variables
+than strictly necessary; there is no need to quantify over 'b', since
+it is determined by 'a' which is free in the envt, but it's perfectly
+OK to do so.  However we must not quantify over 'a' itself.
+
 Other things being equal, however, we'd like to quantify over as few
 variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq.
-
-
------------------------------------------
-We will make use of
-
-  fv(T)                the free type vars of T
-
-  oclose(vs,C) The result of extending the set of tyvars vs
-               using the functional dependencies from C
-
-  grow(vs,C)   The result of extend the set of tyvars vs
-               using all conceivable links from C.
-
-               E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
-               Then grow(vs,C) = {a,b,c}
-
-               Note that grow(vs,C) `superset` grow(vs,simplify(C))
-               That is, simplfication can only shrink the result of grow.
-
-Notice that
-   oclose is conservative one way:      v `elem` oclose(vs,C) => v is definitely fixed by vs
-   grow is conservative the other way:  if v might be fixed by vs => v `elem` grow(vs,C)
-
-
------------------------------------------
-
-Note [Choosing which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here's a good way to choose Q:
+constraints can get into Ct instead of Cq.  Here's a good way to
+choose Q:
 
        Q = grow( fv(T), C ) \ oclose( fv(G), C )
 
@@ -245,9 +219,8 @@ all the functional dependencies yet:
        T = c->c
        C = (Eq (T c d))
 
-  Now oclose(fv(T),C) = {c}, because the functional dependency isn't
-  apparent yet, and that's wrong.  We must really quantify over d too.
-
+Now oclose(fv(T),C) = {c}, because the functional dependency isn't
+apparent yet, and that's wrong.  We must really quantify over d too.
 
 There really isn't any point in quantifying over any more than
 grow( fv(T), C ), because the call sites can't possibly influence
@@ -680,18 +653,11 @@ tcSimplifyInfer doc tau_tvs wanted
                -- To make types simple, reduce as much as possible
        ; traceTc (text "infer" <+> (ppr preds $$ ppr (grow preds tau_tvs') $$ ppr gbl_tvs $$ 
                   ppr (oclose preds gbl_tvs) $$ ppr free1 $$ ppr bound))
-       ; let try_me inst = ReduceMe AddSCs
-             red_env     = mkRedEnv doc try_me []
-       ; (irreds1, binds1) <- checkLoop red_env bound
+       ; (irreds1, binds1) <- tryHardCheckLoop doc bound
 
                -- Note [Inference and implication constraints]
-               -- By putting extra_dicts first, we make them available
-               -- to solve the implication constraints
-       ; let extra_dicts = getImplicWanteds qtvs irreds1
-       ; (irreds2, binds2) <- if null extra_dicts 
-                              then return (irreds1, emptyBag)
-                              else do { extra_dicts' <- mapM cloneDict extra_dicts
-                                      ; checkLoop red_env (extra_dicts' ++ irreds1) }
+       ; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
+       ; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
 
                -- By now improvment may have taken place, and we must *not*
                -- quantify over any variable free in the environment
@@ -723,32 +689,60 @@ tcSimplifyInfer doc tau_tvs wanted
        -- NB: when we are done, we might have some bindings, but
        -- the final qtvs might be empty.  See Note [NO TYVARS] below.
 
-getImplicWanteds :: TcTyVarSet -> [Inst] -> [Inst]
--- See Note [Inference and implication constraints]
--- Find the wanted constraints in implication constraints that mention the 
--- quantified type variables, and are not bound by forall's in the constraint itself
--- Returns only Dicts
-getImplicWanteds qtvs implics
-  = concatMap get implics
-  where
-    get d@(Dict {}) | tyVarsOfInst d `intersectsVarSet` qtvs = [d]
-                   | otherwise                              = []
-    get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
+approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
+-- Note [Inference and implication constraints]
+-- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
+--     - fetching any dicts inside them that are free
+--     - using those dicts as cruder constraints, to solve the implications
+--     - returning the extra ones too
+
+approximateImplications doc want_dict irreds
+  | null extra_dicts 
+  = return (irreds, emptyBag)
+  | otherwise
+  = do { extra_dicts' <- mapM cloneDict extra_dicts
+       ; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
+               -- By adding extra_dicts', we make them 
+               -- available to solve the implication constraints
+  where 
+    extra_dicts = get_dicts (filter isImplicInst irreds)
+
+    get_dicts :: [Inst] -> [Inst]      -- Returns only Dicts
+       -- Find the wanted constraints in implication constraints that satisfy
+       -- want_dict, and are not bound by forall's in the constraint itself
+    get_dicts ds = concatMap get_dict ds
+
+    get_dict d@(Dict {}) | want_dict d = [d]
+                        | otherwise   = []
+    get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
        = [ d | let tv_set = mkVarSet tvs
-             , d <- getImplicWanteds qtvs wanteds 
+             , d <- get_dicts wanteds 
              , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
+    get_dict other = pprPanic "approximateImplications" (ppr other)
 \end{code}
 
 Note [Inference and implication constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
-We can't (or at least don't) abstract over implications.  But we might
-have an implication constraint (perhaps arising from a nested pattern
-match) like
-       C a => D a
-when we are now trying to quantify over 'a'.  Our best approximation
-is to make (D a) part of the inferred context, so we can use that to
-discharge the implication. Hence getImplicWanteds.
-
+Suppose we have a wanted implication constraint (perhaps arising from
+a nested pattern match) like
+       C a => D [a]
+and we are now trying to quantify over 'a' when inferring the type for
+a function.  In principle it's possible that there might be an instance
+       instance (C a, E a) => D [a]
+so the context (E a) would suffice.  The Right Thing is to abstract over
+the implication constraint, but we don't do that (a) because it'll be
+surprising to programmers and (b) because we don't have the machinery to deal
+with 'given' implications.
+
+So our best approximation is to make (D [a]) part of the inferred
+context, so we can use that to discharge the implication. Hence
+the strange function get_dictsin approximateImplications.
+
+The common cases are more clear-cut, when we have things like
+       forall a. C a => C b
+Here, abstracting over (C b) is not an approximation at all -- but see
+Note [Freeness and implications].
 See Trac #1430 and test tc228.
 
 
@@ -766,7 +760,7 @@ tcSimplifyInferCheck
                 TcDictBinds)   -- Bindings
 
 tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+  = do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
 
        -- Figure out which type variables to quantify over
        -- You might think it should just be the signature tyvars,
@@ -872,7 +866,7 @@ tcSimplifyCheck     :: InstLoc
                -> TcM TcDictBinds      -- Bindings
 tcSimplifyCheck loc qtvs givens wanteds 
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+    do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
        ; implic_bind <- bindIrreds loc qtvs givens irreds
        ; return (binds `unionBags` implic_bind) }
 
@@ -886,7 +880,7 @@ tcSimplifyCheckPat :: InstLoc
                   -> TcM TcDictBinds   -- Bindings
 tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
   = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do { (irreds, binds) <- innerCheckLoop loc givens wanteds
+    do { (irreds, binds) <- gentleCheckLoop loc givens wanteds
        ; implic_bind <- bindIrredsR loc qtvs co_vars reft 
                                    givens irreds
        ; return (binds `unionBags` implic_bind) }
@@ -972,22 +966,23 @@ makeImplicationBind loc all_tvs reft
          return ([implic_inst], unitBag (L span bind)) }
 
 -----------------------------------------------------------
-topCheckLoop :: SDoc
+tryHardCheckLoop :: SDoc
             -> [Inst]                  -- Wanted
             -> TcM ([Inst], TcDictBinds)
 
-topCheckLoop doc wanteds
+tryHardCheckLoop doc wanteds
   = checkLoop (mkRedEnv doc try_me []) wanteds
   where
     try_me inst = ReduceMe AddSCs
+       -- Here's the try-hard bit
 
 -----------------------------------------------------------
-innerCheckLoop :: InstLoc
+gentleCheckLoop :: InstLoc
               -> [Inst]                -- Given
               -> [Inst]                -- Wanted
               -> TcM ([Inst], TcDictBinds)
 
-innerCheckLoop inst_loc givens wanteds
+gentleCheckLoop inst_loc givens wanteds
   = checkLoop env wanteds
   where
     env = mkRedEnv (pprInstLoc inst_loc) try_me givens
@@ -1019,7 +1014,7 @@ But we MUST NOT reduce (Show [a]) to (Show a), else the whole
 thing becomes insoluble.  So we simplify gently (get rid of literals
 and methods only, plus common up equal things), deferring the real
 work until top level, when we solve the implication constraint
-with topCheckLooop.
+with tryHardCheckLooop.
 
 
 \begin{code}
@@ -1028,6 +1023,7 @@ checkLoop :: RedEnv
          -> [Inst]                     -- Wanted
          -> TcM ([Inst], TcDictBinds)
 -- Precondition: givens are completely rigid
+-- Postcondition: returned Insts are zonked
 
 checkLoop env wanteds
   = do { -- Givens are skolems, so no need to zonk them
@@ -1125,7 +1121,7 @@ tcSimplifySuperClasses loc givens sc_wanteds
   where
     env = mkRedEnv (pprInstLoc loc) try_me givens
     try_me inst = ReduceMe NoSCs
-       -- Like topCheckLoop, but with NoSCs
+       -- Like tryHardCheckLoop, but with NoSCs
 \end{code}
 
 
@@ -1411,7 +1407,7 @@ this bracket again at its usage site.
 \begin{code}
 tcSimplifyBracket :: [Inst] -> TcM ()
 tcSimplifyBracket wanteds
-  = do { topCheckLoop doc wanteds
+  = do { tryHardCheckLoop doc wanteds
        ; return () }
   where
     doc = text "tcSimplifyBracket"
@@ -1624,7 +1620,11 @@ reduceContext env wanteds
        ; init_state <- foldlM addGiven emptyAvails (red_givens env)
 
         -- Do the real work
-       ; avails <- reduceList env wanteds init_state
+       -- Process non-implication constraints first, so that they are
+       -- available to help solving the implication constraints
+       --      ToDo: seems a bit inefficient and ad-hoc
+       ; let (implics, rest) = partition isImplicInst wanteds
+       ; avails <- reduceList env (rest ++ implics) init_state
 
        ; let improved = availsImproved avails
        ; (binds, irreds) <- extractResults avails wanteds
@@ -1903,20 +1903,22 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                          ppr reft, ppr wanteds, ppr avails ])
        ; avails <- reduceList env' wanteds avails
 
-               -- Extract the binding
+               -- Extract the results 
+               -- Note [Reducing implication constraints]
        ; (binds, irreds) <- extractResults avails wanteds
+       ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+
        ; traceTc (text "reduceImplication result" <+> vcat
-                       [ ppr irreds, ppr binds])
+                       [ ppr outer, ppr inner, ppr binds])
 
                -- We always discard the extra avails we've generated;
                -- but we remember if we have done any (global) improvement
        ; let ret_avails = updateImprovement orig_avails avails
 
-       ; if isEmptyLHsBinds binds then         -- No progress
+       ; if isEmptyLHsBinds binds && null outer then   -- No progress
                return (ret_avails, NoInstance)
          else do
-       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+       { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
 
        ; let   dict_ids = map instToId extra_givens
                co  = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
@@ -1925,11 +1927,36 @@ reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
                payload | [wanted] <- wanteds = HsVar (instToId wanted)
                        | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
 
-               -- If there are any irreds, we back off and return NoInstance
-       ; return (ret_avails, GenInst implic_insts (L loc rhs))
+       ; return (ret_avails, GenInst (implic_insts ++ outer) (L loc rhs))
   } }
 \end{code}
 
+Note [Reducing implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are trying to simplify
+       (Ord a, 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 Rhs binding
+like this
+
+       ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
+          depending on
+               do :: Ord a
+               ic' :: forall b. C a b => D c b
+
+The 'depending on' part of the Rhs is important, because it drives
+the extractResults code.
+
+The "inside" and "outside" distinction is what's going on with 'inner' and
+'outer' in reduceImplication
+
+
 Note [Freeness and implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's hard to say when an implication constraint can be floated out.  Consider
@@ -1985,7 +2012,7 @@ type ImprovementDone = Bool       -- True <=> some unification has happened
 
 type AvailEnv = FiniteMap Inst AvailHow
 data AvailHow
-  = IsIrred TcId       -- Used for irreducible dictionaries,
+  = IsIrred            -- Used for irreducible dictionaries,
                        -- which are going to be lambda bound
 
   | Given TcId                 -- Used for dictionaries for which we have a binding
@@ -2008,9 +2035,9 @@ instance Outputable AvailHow where
 
 -------------------------
 pprAvail :: AvailHow -> SDoc
-pprAvail (IsIrred x)   = text "Irred" <+> ppr x
+pprAvail IsIrred       = text "Irred"
 pprAvail (Given x)     = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs)   = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs)   = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
 
 -------------------------
 extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
@@ -2068,8 +2095,8 @@ extractResults (Avails _ avails) wanteds
 
     go avails binds irreds (w:ws)
       = case findAvailEnv avails w of
-         Nothing    -> pprTrace "Urk: extractResults" (ppr w) $
-                       go avails binds irreds ws
+         Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+                    go avails binds irreds ws
 
          Just (Given id) 
                | id == w_id -> go avails binds irreds ws 
@@ -2077,9 +2104,7 @@ extractResults (Avails _ avails) wanteds
                -- The sought Id can be one of the givens, via a superclass chain
                -- and then we definitely don't want to generate an x=x binding!
 
-         Just (IsIrred id) 
-               | id == w_id -> go (add_given avails w) binds           (w:irreds) ws
-               | otherwise  -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+         Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
                -- The add_given handles the case where we want (Ord a, Eq a), and we
                -- don't want to emit *two* Irreds for Ord a, one via the superclass chain
                -- This showed up in a dupliated Ord constraint in the error message for 
@@ -2166,7 +2191,7 @@ than with the Avails handling stuff in TcSimplify
 \begin{code}
 addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
 addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
-                                addAvailAndSCs want_scs avails irred (IsIrred (instToId irred))
+                                addAvailAndSCs want_scs avails irred IsIrred
 
 addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
 addAvailAndSCs want_scs avails inst avail
@@ -2263,24 +2288,19 @@ tcSimplifyInteractive wanteds
 -- The TcLclEnv should be valid here, solely to improve
 -- error message generation for the monomorphism restriction
 tc_simplify_top doc interactive wanteds
-  = do { wanteds <- mapM zonkInst wanteds
+  = do { dflags <- getDOpts
+       ; wanteds <- mapM zonkInst wanteds
        ; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
 
-       ; (irreds1, binds1) <- topCheckLoop doc wanteds
+       ; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
+       ; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
 
-       ; if null irreds1 then 
-               return binds1
-         else do
-       -- OK, so there are some errors
-       {       -- Use the defaulting rules to do extra unification
-               -- NB: irreds are already zonked
-       ; dflags <- getDOpts
-       ; disambiguate interactive dflags irreds1       -- Does unification
-                                                       -- hence try again
+               -- Use the defaulting rules to do extra unification
+               -- NB: irreds2 are already zonked
+       ; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
 
                -- Deal with implicit parameters
-       ; (irreds2, binds2) <- topCheckLoop doc irreds1
-       ; let (bad_ips, non_ips) = partition isIPDict irreds2
+       ; let (bad_ips, non_ips) = partition isIPDict irreds3
              (ambigs, others)   = partition isTyVarDict non_ips
 
        ; topIPErrs bad_ips     -- Can arise from   f :: Int -> Int
@@ -2288,7 +2308,11 @@ tc_simplify_top doc interactive wanteds
        ; addNoInstanceErrs others
        ; addTopAmbigErrs ambigs        
 
-       ; return (binds1 `unionBags` binds2) }}
+       ; return (binds1 `unionBags` binds2 `unionBags` binds3) }
+  where
+    doc1 = doc <+> ptext SLIT("(first round)")
+    doc2 = doc <+> ptext SLIT("(approximate)")
+    doc3 = doc <+> ptext SLIT("(disambiguate)")
 \end{code}
 
 If a dictionary constrains a type variable which is
@@ -2324,26 +2348,40 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambiguate :: Bool -> DynFlags -> [Inst] -> TcM ()
+disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
        -- Just does unification to fix the default types
        -- The Insts are assumed to be pre-zonked
-disambiguate interactive dflags insts
+disambiguate doc interactive dflags insts
+  | null insts
+  = return (insts, emptyBag)
+
   | null defaultable_groups
-  = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
-       ;     return () }
+  = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+       ; return (insts, emptyBag) }
+
   | otherwise
   = do         {       -- Figure out what default types to use
-       ; default_tys <- getDefaultTys extended_defaulting ovl_strings
+         default_tys <- getDefaultTys extended_defaulting ovl_strings
+
+       ; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+       ; mapM_ (disambigGroup default_tys) defaultable_groups
+
+       -- disambigGroup does unification, hence try again
+       ; tryHardCheckLoop doc insts }
 
-       ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
-       ; mapM_ (disambigGroup default_tys) defaultable_groups  }
   where
    extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
    ovl_strings = dopt Opt_OverloadedStrings dflags
 
-   unaries :: [(Inst,Class, TcTyVar)]  -- (C tv) constraints
-   bad_tvs :: TcTyVarSet         -- Tyvars mentioned by *other* constraints
-   (unaries, bad_tvs) = getDefaultableDicts insts
+   unaries :: [(Inst, Class, TcTyVar)]  -- (C tv) constraints
+   bad_tvs :: TcTyVarSet  -- Tyvars mentioned by *other* constraints
+   (unaries, bad_tvs_s) = partitionWith find_unary insts 
+   bad_tvs             = unionVarSets bad_tvs_s
+
+       -- Finds unary type-class constraints
+   find_unary d@(Dict {tci_pred = ClassP cls [ty]})
+       | Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
+   find_unary inst                      = Right (tyVarsOfInst inst)
 
                -- Group by type variable
    defaultable_groups :: [[(Inst,Class,TcTyVar)]]
@@ -2421,26 +2459,6 @@ getDefaultTys extended_deflts ovl_strings
   where
     opt_deflt True  ty = [ty]
     opt_deflt False ty = []
-
------------------------
-getDefaultableDicts :: [Inst] -> ([(Inst, Class, TcTyVar)], TcTyVarSet)
--- Look for free dicts of the form (C tv), even inside implications
--- *and* the set of tyvars mentioned by all *other* constaints
--- This disgustingly ad-hoc function is solely to support defaulting
-getDefaultableDicts insts
-  = (concat ps, unionVarSets tvs)
-  where
-    (ps, tvs) = mapAndUnzip get insts
-    get d@(Dict {tci_pred = ClassP cls [ty]})
-       | Just tv <- tcGetTyVar_maybe ty = ([(d,cls,tv)], emptyVarSet)
-       | otherwise                      = ([], tyVarsOfType ty)
-    get (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
-       = ([ up | up@(_,_,tv) <- ups, not (tv `elemVarSet` tv_set)],
-          ftvs `minusVarSet` tv_set)
-       where
-          tv_set = mkVarSet tvs
-          (ups, ftvs) = getDefaultableDicts wanteds
-    get inst = ([], tyVarsOfInst inst)
 \end{code}
 
 Note [Default unitTy]
@@ -2500,21 +2518,62 @@ tcSimplifyDeriv orig tyvars theta
        -- it doesn't see a TcTyVar, so we have to instantiate. Sigh
        -- ToDo: what if two of them do get unified?
        ; wanteds <- newDictBndrsO orig (substTheta tenv theta)
-       ; (irreds, _) <- topCheckLoop doc wanteds
+       ; (irreds, _) <- tryHardCheckLoop doc wanteds
+
+       ; let (tv_dicts, others) = partition isTyVarDict irreds
+       ; addNoInstanceErrs others
 
        ; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
-             simpl_theta = substTheta rev_env (map dictPred irreds)
+             simpl_theta = substTheta rev_env (map dictPred tv_dicts)
                -- This reverse-mapping is a pain, but the result
                -- should mention the original TyVars not TcTyVars
 
-       -- NB: the caller will further check the tv_dicts for
-       --     legal instance-declaration form
-
        ; return simpl_theta }
   where
     doc = ptext SLIT("deriving classes for a data type")
 \end{code}
 
+Note [Exotic derived instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+       data T a b c = MkT (Foo a b c) deriving( Eq )
+       instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
+
+Notice that this instance (just) satisfies the Paterson termination 
+conditions.  Then we *could* derive an instance decl like this:
+
+       instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
+
+even though there is no instance for (C Int a), because there just
+*might* be an instance for, say, (C Int Bool) at a site where we
+need the equality instance for T's.  
+
+However, this seems pretty exotic, and it's quite tricky to allow
+this, and yet give sensible error messages in the (much more common)
+case where we really want that instance decl for C.
+
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
+
+Here is another example:
+       data Fix f = In (f (Fix f)) deriving( Eq )
+Here, if we are prepared to allow -fallow-undecidable-instances we
+could derive the instance
+       instance Eq (f (Fix f)) => Eq (Fix f)
+but this is so delicate that I don't think it should happen inside
+'deriving'. If you want this, write it yourself!
+
+NB: if you want to lift this condition, make sure you still meet the
+termination conditions!  If not, the deriving mechanism generates
+larger and larger constraints.  Example:
+  data Succ a = S a
+  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ.  First we'll generate
+  instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on.  Instead we want to complain of no instance for (Show (Succ a)).
 
 
 @tcSimplifyDefault@ just checks class-type constraints, essentially;
@@ -2527,7 +2586,7 @@ tcSimplifyDefault :: ThetaType    -- Wanted; has no type variables in it
 
 tcSimplifyDefault theta
   = newDictBndrsO DefaultOrigin theta  `thenM` \ wanteds ->
-    topCheckLoop doc wanteds           `thenM` \ (irreds, _) ->
+    tryHardCheckLoop doc wanteds       `thenM` \ (irreds, _) ->
     addNoInstanceErrs  irreds          `thenM_`
     if null irreds then
        returnM ()
@@ -2655,11 +2714,11 @@ report_no_instances tidy_env mb_what insts
            (clas,tys) = getDictClassTys wanted
 
     mk_overlap_msg dict (matches, unifiers)
-      = vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
+      = ASSERT( not (null matches) )
+        vcat [ addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
                                        <+> pprPred (dictPred dict))),
                sep [ptext SLIT("Matching instances") <> colon,
                     nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
-               ASSERT( not (null matches) )
                if not (isSingleton matches)
                then    -- Two or more matches
                     empty
@@ -2667,7 +2726,8 @@ 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("Use -fallow-incoherent-instances to use the first choice above")])]
+                             ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
+                             ptext SLIT("when compiling the other instances")])]
       where
        ispecs = [ispec | (ispec, _) <- matches]