[project @ 2001-01-29 08:42:54 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index e6fc689..d4617b2 100644 (file)
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
 \section[TcSimplify]{TcSimplify}
 
-\begin{code}
-#include "HsVersions.h"
 
+
+\begin{code}
 module TcSimplify (
-       tcSimplify, tcSimplifyAndCheck,
-       tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas, tcSimplifyRank2,
+       tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyCheck, 
+       tcSimplifyToDicts, tcSimplifyIPs, tcSimplifyTop, 
+       tcSimplifyThetas, tcSimplifyCheckThetas,
        bindInstsOfLocalFuns
     ) where
 
-IMP_Ubiq()
-
-import HsSyn           ( MonoBinds(..), HsExpr(..), InPat, OutPat, HsLit, 
-                         Match, HsBinds, Qualifier, PolyType, ArithSeqInfo,
-                         GRHSsAndBinds, Stmt, Fake )
-import TcHsSyn         ( TcIdOcc(..), SYN_IE(TcIdBndr), SYN_IE(TcExpr), SYN_IE(TcMonoBinds) )
-
-import TcMonad         hiding ( rnMtoTcM )
-import Inst            ( lookupInst, lookupSimpleInst,
-                         tyVarsOfInst, isTyVarDict, isDict,
-                         matchesInst, instToId, instBindingRequired,
-                         instCanBeGeneralised, newDictsAtLoc,
-                         pprInst,
-                         Inst(..), SYN_IE(LIE), zonkLIE, emptyLIE,
-                         plusLIE, unitLIE, consLIE, InstOrigin(..),
-                         OverloadedLit )
-import TcEnv           ( tcGetGlobalTyVars )
-import TcType          ( SYN_IE(TcType), SYN_IE(TcTyVar), SYN_IE(TcTyVarSet), TcMaybe, tcInstType )
-import Unify           ( unifyTauTy )
-
-import Bag             ( Bag, unitBag, listToBag, foldBag, filterBag, emptyBag, bagToList, 
-                         snocBag, consBag, unionBags, isEmptyBag )
-import Class           ( GenClass, SYN_IE(Class), SYN_IE(ClassInstEnv),
-                         isNumericClass, isStandardClass, isCcallishClass,
-                         isSuperClassOf, classSuperDictSelId, classInstEnv
+#include "HsVersions.h"
+
+import HsSyn           ( MonoBinds(..), HsExpr(..), andMonoBinds, andMonoBindList )
+import TcHsSyn         ( TcExpr, TcId, 
+                         TcMonoBinds, TcDictBinds
                        )
-import Id              ( GenId )
-import Maybes          ( expectJust, firstJust, catMaybes, seqMaybe, maybeToBool )
-import Outputable      ( Outputable(..){-instance * []-} )
-import PprStyle--ToDo:rm
-import PprType         ( GenType, GenTyVar, GenClass{-instance Outputable;ToDo:rm-} )
-import Pretty
-import SrcLoc          ( mkUnknownSrcLoc )
-import Util
-import Type            ( GenType, SYN_IE(Type), SYN_IE(TauType), mkTyVarTy, getTyVar, eqSimpleTy,
-                         getTyVar_maybe )
-import TysWiredIn      ( intTy )
-import TyVar           ( GenTyVar, SYN_IE(GenTyVarSet), 
-                         elementOfTyVarSet, emptyTyVarSet, unionTyVarSets,
-                         isEmptyTyVarSet, tyVarSetToList )
-import Unique          ( Unique )
+
+import TcMonad
+import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
+                         tyVarsOfInst, predsOfInsts, 
+                         isDict, isClassDict, 
+                         isStdClassTyVarDict, isMethodFor,
+                         instToId, tyVarsOfInsts,
+                         instBindingRequired, instCanBeGeneralised,
+                         newDictsFromOld, instMentionsIPs,
+                         getDictClassTys, getIPs, isTyVarDict,
+                         instLoc, pprInst, zonkInst, tidyInst, tidyInsts,
+                         Inst, LIE, pprInsts, pprInstsInFull,
+                         mkLIE, 
+                         lieToList 
+                       )
+import TcEnv           ( tcGetGlobalTyVars, tcGetInstEnv )
+import InstEnv         ( lookupInstEnv, classInstEnv, InstLookupResult(..) )
+
+import TcType          ( zonkTcTyVarsAndFV )
+import TcUnify         ( unifyTauTy )
+import Id              ( idType )
+import Name            ( Name )
+import NameSet         ( mkNameSet )
+import Class           ( Class, classBigSig )
+import FunDeps         ( oclose, grow, improve )
+import PrelInfo                ( isNumericClass, isCreturnableClass, isCcallishClass )
+
+import Type            ( Type, ClassContext,
+                         mkTyVarTy, getTyVar, 
+                         isTyVarTy, splitSigmaTy, tyVarsOfTypes
+                       )
+import Subst           ( mkTopTyVarSubst, substClasses )
+import PprType         ( pprClassPred )
+import TysWiredIn      ( unitTy )
+import VarSet
+import FiniteMap
+import Outputable
+import ListSetOps      ( equivClasses )
+import Util            ( zipEqual, mapAccumL )
+import List            ( partition )
+import CmdLineOpts
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[tcSimplify-main]{Main entry function}
+\subsection{NOTES}
 %*                                                                     *
 %************************************************************************
 
-* May modify the substitution to bind ambiguous type variables.
+       --------------------------------------  
+               Notes on quantification
+       --------------------------------------  
 
-Specification
-~~~~~~~~~~~~~
-(1) If an inst constrains only ``global'' type variables, (or none),
-    return it as a ``global'' inst.
+Suppose we are about to do a generalisation step.
+We have in our hand
 
-OTHERWISE
+       G       the environment
+       T       the type of the RHS
+       C       the constraints from that RHS
 
-(2) Simplify it repeatedly (checking for (1) of course) until it is a dict
-    constraining only a type variable.
+The game is to figure out
 
-(3) If it constrains a ``local'' type variable, return it as a ``local'' inst.
-    Otherwise it must be ambiguous, so try to resolve the ambiguity.
+       Q       the set of type variables over which to quantify
+       Ct      the constraints we will *not* quantify over
+       Cq      the constraints we will quantify over
 
+So we're going to infer the type
 
-\begin{code}
-tcSimpl :: Bool                                -- True <=> simplify const insts
-       -> TcTyVarSet s                 -- ``Global'' type variables
-       -> TcTyVarSet s                 -- ``Local''  type variables
-                                       -- ASSERT: both these tyvar sets are already zonked
-       -> LIE s                        -- Given; these constrain only local tyvars
-       -> LIE s                        -- Wanted
-       -> TcM s (LIE s,                        -- Free
-                 [(TcIdOcc s,TcExpr s)],       -- Bindings
-                 LIE s)                        -- Remaining wanteds; no dups
-
-tcSimpl squash_consts global_tvs local_tvs givens wanteds
-  =    -- ASSSERT: global_tvs and local_tvs are already zonked
-       -- Make sure the insts fixed points of the substitution
-    zonkLIE givens                     `thenNF_Tc` \ givens ->
-    zonkLIE wanteds                    `thenNF_Tc` \ wanteds ->
-
-       -- Deal with duplicates and type constructors
-    elimTyCons
-        squash_consts (\tv -> tv `elementOfTyVarSet` global_tvs)
-        givens wanteds         `thenTc` \ (globals, tycon_binds, locals_and_ambigs) ->
-
-       -- Now disambiguate if necessary
-    let
-       ambigs = filterBag is_ambiguous locals_and_ambigs
-    in
-    if not (isEmptyBag ambigs) then
-       -- Some ambiguous dictionaries.  We now disambiguate them,
-       -- which binds the offending type variables to suitable types in the
-       -- substitution, and then we retry the whole process.  This
-       -- time there won't be any ambiguous ones.
-       -- There's no need to back-substitute on global and local tvs,
-       -- because the ambiguous type variables can't be in either.
+       forall Q. Cq => T
 
-       -- Why do we retry the whole process?  Because binding a type variable
-       -- to a particular type might enable a short-cut simplification which
-       -- elimTyCons will have missed the first time.
+and float the constraints Ct further outwards.  
 
-       disambiguateDicts ambigs                `thenTc_`
-       tcSimpl squash_consts global_tvs local_tvs givens wanteds
+Here are the things that *must* be true:
 
-    else
-       -- No ambiguous dictionaries.  Just bash on with the results
-       -- of the elimTyCons
+ (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
 
-       -- Check for non-generalisable insts
-    let
-       locals          = locals_and_ambigs     -- ambigs is empty
-       cant_generalise = filterBag (not . instCanBeGeneralised) locals
-    in
-    checkTc (isEmptyBag cant_generalise)
-           (genCantGenErr cant_generalise)     `thenTc_`
+(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!
 
-       -- Deal with superclass relationships
-    elimSCs givens locals              `thenNF_Tc` \ (sc_binds, locals2) ->
+Example:       class H x y | x->y where ...
 
-        -- Finished
-    returnTc (globals, bagToList (sc_binds `unionBags` tycon_binds), locals2)
-  where
-    is_ambiguous (Dict _ _ ty _ _)
-       = not (getTyVar "is_ambiguous" ty `elementOfTyVarSet` local_tvs)
-\end{code}
+       fv(G) = {a}     C = {H a b, H c d}
+                       T = c -> b
 
-The main wrapper is @tcSimplify@.  It just calls @tcSimpl@, but with
-the ``don't-squash-consts'' flag set depending on top-level ness.  For
-top level defns we *do* squash constants, so that they stay local to a
-single defn.  This makes things which are inlined more likely to be
-exportable, because their constants are "inside".  Later passes will
-float them out if poss, after inlinings are sorted out.
+       (A)  Q intersect {a} is empty
+       (B)  Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
 
-\begin{code}
-tcSimplify
-       :: TcTyVarSet s                 -- ``Local''  type variables
-       -> LIE s                        -- Wanted
-       -> TcM s (LIE s,                        -- Free
-                 [(TcIdOcc s,TcExpr s)],       -- Bindings
-                 LIE s)                        -- Remaining wanteds; no dups
-
-tcSimplify local_tvs wanteds
-  = tcGetGlobalTyVars                  `thenNF_Tc` \ global_tvs ->
-    tcSimpl False global_tvs local_tvs emptyBag wanteds
-\end{code}
+       So Q can be {c,d}, {b,c,d}
 
-@tcSimplifyAndCheck@ is similar to the above, except that it checks
-that there is an empty wanted-set at the end.  It may still return
-some of constant insts, which have to be resolved finally at the end.
+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.
 
-\begin{code}
-tcSimplifyAndCheck
-        :: TcTyVarSet s                -- ``Local''  type variables; ASSERT is fixpoint
-        -> LIE s                       -- Given
-        -> LIE s                       -- Wanted
-        -> TcM s (LIE s,                       -- Free
-                  [(TcIdOcc s,TcExpr s)])      -- Bindings
-
-tcSimplifyAndCheck local_tvs givens wanteds
-  = tcGetGlobalTyVars                  `thenNF_Tc` \ global_tvs ->
-    tcSimpl False global_tvs local_tvs
-           givens wanteds              `thenTc` \ (free_insts, binds, wanteds') ->
-    checkTc (isEmptyBag wanteds')
-           (reduceErr wanteds')        `thenTc_`
-    returnTc (free_insts, binds)
-\end{code}
 
-@tcSimplifyRank2@ checks that the argument of a rank-2 polymorphic function
-is not overloaded.
+-----------------------------------------
+We will make use of
 
-\begin{code}
-tcSimplifyRank2 :: TcTyVarSet s                -- ``Local'' type variables; ASSERT is fixpoint
-               -> LIE s                -- Given
-               -> TcM s (LIE s,                        -- Free
-                         [(TcIdOcc s,TcExpr s)])       -- Bindings
+  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
 
-tcSimplifyRank2 local_tvs givens
-  = zonkLIE givens                     `thenNF_Tc` \ givens' ->
-    elimTyCons True
-              (\tv -> not (tv `elementOfTyVarSet` local_tvs))
-               -- This predicate claims that all
-               -- any non-local tyvars are global,
-               -- thereby postponing dealing with
-               -- ambiguity until the enclosing Gen
-              emptyLIE givens' `thenTc` \ (free, dict_binds, wanteds) ->
+  grow(vs,C)   The result of extend the set of tyvars vs
+               using all conceivable links from C.  
 
-    checkTc (isEmptyBag wanteds) (reduceErr wanteds)   `thenTc_`
+               E.g. vs = {a}, C = {H [a] b, K (b,Int) c, Eq e}
+               Then grow(vs,C) = {a,b,c}
 
-    returnTc (free, bagToList dict_binds)
-\end{code}
+               Note that grow(vs,C) `superset` grow(vs,simplify(C))
+               That is, simplfication can only shrink the result of grow.
 
-@tcSimplifyTop@ deals with constant @Insts@, using the standard simplification
-mechansim with the extra flag to say ``beat out constant insts''.
+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)
 
-\begin{code}
-tcSimplifyTop :: LIE s -> TcM s [(TcIdOcc s, TcExpr s)]
-tcSimplifyTop dicts
-  = tcSimpl True emptyTyVarSet emptyTyVarSet emptyBag dicts    `thenTc` \ (_, binds, _) ->
-    returnTc binds
-\end{code}
 
+-----------------------------------------
+
+Choosing Q
+~~~~~~~~~~
+Here's a good way to choose Q:
+
+       Q = grow( fv(T), C ) \ oclose( fv(G), C )
+
+That is, quantify over all variable that that MIGHT be fixed by the
+call site (which influences T), but which aren't DEFINITELY fixed by
+G.  This choice definitely quantifies over enough type variables,
+albeit perhaps too many.
+
+Why grow( fv(T), C ) rather than fv(T)?  Consider
+
+       class H x y | x->y where ...
+       
+       T = c->c
+       C = (H c d)
+
+  If we used fv(T) = {c} we'd get the type
+
+       forall c. H c d => c -> b
+
+  And then if the fn was called at several different c's, each of 
+  which fixed d differently, we'd get a unification error, because
+  d isn't quantified.  Solution: quantify d.  So we must quantify
+  everything that might be influenced by c.
+
+Why not oclose( fv(T), C )?  Because we might not be able to see
+all the functional dependencies yet:
+
+       class H x y | x->y where ...
+       instance H x y => Eq (T x y) where ...
+
+       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.
+
+
+There really isn't any point in quantifying over any more than
+grow( fv(T), C ), because the call sites can't possibly influence
+any other type variables.
+
+
+
+       --------------------------------------  
+               Notes on ambiguity  
+       --------------------------------------  
+
+It's very hard to be certain when a type is ambiguous.  Consider
+
+       class K x
+       class H x y | x -> y
+       instance H x y => K (x,y)
+
+Is this type ambiguous?
+       forall a b. (K (a,b), Eq b) => a -> a
+
+Looks like it!  But if we simplify (K (a,b)) we get (H a b) and
+now we see that a fixes b.  So we can't tell about ambiguity for sure
+without doing a full simplification.  And even that isn't possible if
+the context has some free vars that may get unified.  Urgle!
+
+Here's another example: is this ambiguous?
+       forall a b. Eq (T b) => a -> a
+Not if there's an insance decl (with no context)
+       instance Eq (T b) where ...
+
+You may say of this example that we should use the instance decl right
+away, but you can't always do that:
+
+       class J a b where ...
+       instance J Int b where ...
+
+       f :: forall a b. J a b => a -> a
+
+(Notice: no functional dependency in J's class decl.)
+Here f's type is perfectly fine, provided f is only called at Int.
+It's premature to complain when meeting f's signature, or even
+when inferring a type for f.
+
+
+
+However, we don't *need* to report ambiguity right away.  It'll always
+show up at the call site.... and eventually at main, which needs special
+treatment.  Nevertheless, reporting ambiguity promptly is an excellent thing.
+
+So heres the plan.  We WARN about probable ambiguity if
+
+       fv(Cq) is not a subset of  oclose(fv(T) union fv(G), C)
+
+(all tested before quantification).
+That is, all the type variables in Cq must be fixed by the the variables
+in the environment, or by the variables in the type.  
+
+Notice that we union before calling oclose.  Here's an example:
+
+       class J a b c | a b -> c
+       fv(G) = {a}
+
+Is this ambiguous?
+       forall b c. (J a b c) => b -> b
+
+Only if we union {a} from G with {b} from T before using oclose,
+do we see that c is fixed.  
+
+It's a bit vague exactly which C we should use for this oclose call.  If we 
+don't fix enough variables we might complain when we shouldn't (see
+the above nasty example).  Nothing will be perfect.  That's why we can
+only issue a warning.
+
+
+Can we ever be *certain* about ambiguity?  Yes: if there's a constraint
+
+       c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
+
+then c is a "bubble"; there's no way it can ever improve, and it's 
+certainly ambiguous.  UNLESS it is a constant (sigh).  And what about
+the nasty example?
+
+       class K x
+       class H x y | x -> y
+       instance H x y => K (x,y)
+
+Is this type ambiguous?
+       forall a b. (K (a,b), Eq b) => a -> a
+
+Urk.  The (Eq b) looks "definitely ambiguous" but it isn't.  What we are after
+is a "bubble" that's a set of constraints
+
+       Cq = Ca union Cq'  st  fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
+
+Hence another idea.  To decide Q start with fv(T) and grow it
+by transitive closure in Cq (no functional dependencies involved).
+Now partition Cq using Q, leaving the definitely-ambiguous and probably-ok.
+The definitely-ambigous can then float out, and get smashed at top level
+(which squashes out the constants, like Eq (T a) above)
+
+
+       --------------------------------------  
+               Notes on implicit parameters
+       --------------------------------------  
+
+Consider
+
+       f x = ...?y...
+
+Then we get an LIE like (?y::Int).  Doesn't constrain a type variable,
+but we must nevertheless infer a type like
+
+       f :: (?y::Int) => Int -> Int
+
+so that f is passed the value of y at the call site.  Is this legal?
+       
+       f :: Int -> Int
+       f x = x + ?y
+
+Should f be overloaded on "?y" ?  Or does the type signature say that it
+shouldn't be?  Our position is that it should be illegal.  Otherwise
+you can change the *dynamic* semantics by adding a type signature:
+
+       (let f x = x + ?y       -- f :: (?y::Int) => Int -> Int
+        in (f 3, f 3 with ?y=5))  with ?y = 6
+
+               returns (3+6, 3+5)
+vs
+       (let f :: Int -> Int 
+           f x = x + ?y
+        in (f 3, f 3 with ?y=5))  with ?y = 6
+
+               returns (3+6, 3+6)
+
+URK!  Let's not do this. So this is illegal:
+
+       f :: Int -> Int
+       f x = x + ?y
+
+BOTTOM LINE: you *must* quantify over implicit parameters.
+
+
+       --------------------------------------  
+               Notes on principal types
+       --------------------------------------  
+
+    class C a where
+      op :: a -> a
+    
+    f x = let g y = op (y::Int) in True
+
+Here the principal type of f is (forall a. a->a)
+but we'll produce the non-principal type
+    f :: forall a. C Int => a -> a
+
+       
 %************************************************************************
 %*                                                                     *
-\subsection[elimTyCons]{@elimTyCons@}
+\subsection{tcSimplifyInfer}
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-elimTyCons :: Bool                             -- True <=> Simplify const insts
-          -> (TcTyVar s -> Bool)               -- Free tyvar predicate
-          -> LIE s                             -- Given
-          -> LIE s                             -- Wanted
-          -> TcM s (LIE s,                     -- Free
-                    Bag (TcIdOcc s, TcExpr s), -- Bindings
-                    LIE s                      -- Remaining wanteds; no dups;
-                                               -- dicts only (no Methods)
-              )
-\end{code}
+tcSimplify is called when we *inferring* a type.  Here's the overall game plan:
 
-The bindings returned may mention any or all of ``givens'', so the
-order in which the generated binds are put together is {\em tricky}.
-Case~4 of @try@ is the general case to see.
+    1. Compute Q = grow( fvs(T), C )
+    
+    2. Partition C based on Q into Ct and Cq.  Notice that ambiguous 
+       predicates will end up in Ct; we deal with them at the top level
+    
+    3. Try improvement, using functional dependencies
+    
+    4. If Step 3 did any unification, repeat from step 1
+       (Unification can change the result of 'grow'.)
 
-When we do @eTC givens (wanted:wanteds)@ [some details omitted], we...
+Note: we don't reduce dictionaries in step 2.  For example, if we have
+Eq (a,b), we don't simplify to (Eq a, Eq b).  So Q won't be different 
+after step 2.  However note that we may therefore quantify over more
+type variables than we absolutely have to.
 
-    (1) first look up @wanted@; this gives us one binding to heave in:
-           wanted = rhs
+For the guts, we need a loop, that alternates context reduction and
+improvement with unification.  E.g. Suppose we have
 
-    (2) step (1) also gave us some @simpler_wanteds@; we simplify
-       these and get some (simpler-wanted-)bindings {\em that must be
-       in scope} for the @wanted=rhs@ binding above!
+       class C x y | x->y where ...
+    
+and tcSimplify is called with:
+       (C Int a, C Int b)
+Then improvement unifies a with b, giving
+       (C Int a, C Int a)
 
-    (3) we simplify the remaining @wanteds@ (recursive call), giving
-       us yet more bindings.
+If we need to unify anything, we rattle round the whole thing all over
+again. 
 
-The final arrangement of the {\em non-recursive} bindings is
 
-    let <simpler-wanted-binds> in
-    let wanted = rhs          in
-    let <yet-more-bindings> ...
+\begin{code}
+tcSimplifyInfer
+       :: SDoc 
+       -> [TcTyVar]            -- fv(T); type vars 
+       -> LIE                  -- Wanted
+       -> TcM ([TcTyVar],      -- Tyvars to quantify (zonked)
+               LIE,            -- Free
+               TcDictBinds,    -- Bindings
+               [TcId])         -- Dict Ids that must be bound here (zonked)
+\end{code}
+
 
 \begin{code}
-elimTyCons squash_consts is_free_tv givens wanteds
-  = eTC givens (bagToList wanteds)     `thenTc` \ (_, free, binds, irreds) ->
-    returnTc (free,binds,irreds)
-  where
---    eTC :: LIE s -> [Inst s]
---       -> TcM s (LIE s, LIE s, Bag (TcIdOcc s, TcExpr s), LIE s)
-
-    eTC givens [] = returnTc (givens, emptyBag, emptyBag, emptyBag)
-
-    eTC givens (wanted:wanteds)
-    -- Case 0: same as an existing inst
-      | maybeToBool maybe_equiv
-      = eTC givens wanteds     `thenTc` \ (givens1, frees, binds, irreds) ->
-       let
-         -- Create a new binding iff it's needed
-         this = expectJust "eTC" maybe_equiv
-         new_binds | instBindingRequired wanted = (instToId wanted, HsVar (instToId this))
-                                                  `consBag` binds
-                   | otherwise                  = binds
-       in
-       returnTc (givens1, frees, new_binds, irreds)
-
-    -- Case 1: constrains no type variables at all
-    -- In this case we have a quick go to see if it has an
-    -- instance which requires no inputs (ie a constant); if so we use
-    -- it; if not, we give up on the instance and just heave it out the
-    -- top in the free result
-      | isEmptyTyVarSet tvs_of_wanted
-      = simplify_it squash_consts      {- If squash_consts is false,
-                                          simplify only if trival -}
-                   givens wanted wanteds
-
-    -- Case 2: constrains free vars only, so fling it out the top in free_ids
-      | all is_free_tv (tyVarSetToList tvs_of_wanted)
-      = eTC (wanted `consBag` givens) wanteds  `thenTc` \ (givens1, frees, binds, irreds) ->
-       returnTc (givens1, wanted `consBag` frees, binds, irreds)
-
-    -- Case 3: is a dict constraining only a tyvar,
-    -- so return it as part of the "wanteds" result
-      | isTyVarDict wanted
-      = eTC (wanted `consBag` givens) wanteds  `thenTc` \ (givens1, frees, binds, irreds) ->
-       returnTc (givens1, frees, binds, wanted `consBag` irreds)
-
-    -- Case 4: is not a simple dict, so look up in instance environment
-      | otherwise
-      = simplify_it True {- Simplify even if not trivial -}
-                   givens wanted wanteds
-      where
-       tvs_of_wanted  = tyVarsOfInst wanted
-
-       -- Look for something in "givens" that matches "wanted"
-       Just the_equiv = maybe_equiv
-       maybe_equiv    = foldBag seqMaybe try Nothing givens
-       try given | wanted `matchesInst` given = Just given
-                 | otherwise                  = Nothing
-
-
-    simplify_it simplify_always givens wanted wanteds
-       -- Recover immediately on no-such-instance errors
-      = recoverTc (returnTc (wanted `consBag` givens, emptyLIE, emptyBag, emptyLIE)) 
-                 (simplify_one simplify_always givens wanted)
-                               `thenTc` \ (givens1, frees1, binds1, irreds1) ->
-       eTC givens1 wanteds     `thenTc` \ (givens2, frees2, binds2, irreds2) ->
-       returnTc (givens2, frees1 `plusLIE` frees2,
-                          binds1 `unionBags` binds2,
-                          irreds1 `plusLIE` irreds2)
-
-
-    simplify_one simplify_always givens wanted
-     | not (instBindingRequired wanted)
-     =                 -- No binding required for this chap, so squash right away
-          lookupInst wanted            `thenTc` \ (simpler_wanteds, _) ->
-          eTC givens simpler_wanteds   `thenTc` \ (givens1, frees1, binds1, irreds1) ->
-          returnTc (wanted `consBag` givens1, frees1, binds1, irreds1)
-
-     | otherwise
-     =                 -- An binding is required for this inst
-       lookupInst wanted               `thenTc` \ (simpler_wanteds, bind@(_,rhs)) ->
-
-       if (not_var rhs && not simplify_always) then
-          -- Ho ho!  It isn't trivial to simplify "wanted",
-          -- because the rhs isn't a simple variable.  Unless the flag
-          -- simplify_always is set, just give up now and
-          -- just fling it out the top.
-          returnTc (wanted `consLIE` givens, unitLIE wanted, emptyBag, emptyLIE)
-       else
-          -- Aha! Either it's easy, or simplify_always is True
-          -- so we must do it right here.
-          eTC givens simpler_wanteds   `thenTc` \ (givens1, frees1, binds1, irreds1) ->
-          returnTc (wanted `consLIE` givens1, frees1,
-                    binds1 `snocBag` bind,
-                    irreds1)
-
-    not_var :: TcExpr s -> Bool
-    not_var (HsVar _) = False
-    not_var other     = True
+tcSimplifyInfer doc tau_tvs wanted_lie
+  = inferLoop doc tau_tvs (lieToList wanted_lie)       `thenTc` \ (qtvs, frees, binds, irreds) ->
+
+       -- Check for non-generalisable insts
+    mapTc_ addCantGenErr (filter (not . instCanBeGeneralised) irreds)  `thenTc_`
+
+    returnTc (qtvs, mkLIE frees, binds, map instToId irreds)
+
+inferLoop doc tau_tvs wanteds
+  =    -- Step 1
+    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
+    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
+    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
+    let
+       preds = predsOfInsts wanteds'
+       qtvs  = grow preds tau_tvs' `minusVarSet` oclose preds gbl_tvs
+       
+       try_me inst     
+         | isFree qtvs inst  = Free
+         | isClassDict inst  = DontReduceUnlessConstant        -- Dicts
+         | otherwise         = ReduceMe AddToIrreds            -- Lits and Methods
+    in
+               -- Step 2
+    reduceContext doc try_me [] wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+       
+               -- Step 3
+    if no_improvement then
+           returnTc (varSetElems qtvs, frees, binds, irreds)
+    else
+           inferLoop doc tau_tvs wanteds
+\end{code}     
+
+\begin{code}
+isFree qtvs inst
+  =  not (tyVarsOfInst inst `intersectsVarSet` qtvs)   -- Constrains no quantified vars
+  && null (getIPs inst)                                        -- And no implicit parameter involved
+                                                       -- (see "Notes on implicit parameters")
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[elimSCs]{@elimSCs@}
+\subsection{tcSimplifyCheck}
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-elimSCs :: LIE s                               -- Given; no dups
-       -> LIE s                                -- Wanted; no dups; all dictionaries, all
-                                               -- constraining just a type variable
-       -> NF_TcM s (Bag (TcIdOcc s,TcExpr s),  -- Bindings
-                    LIE s)                     -- Minimal wanted set
-
-elimSCs givens wanteds
-  = -- Sort the wanteds so that subclasses occur before superclasses
-    elimSCs_help
-       (filterBag isDict givens)       -- Filter out non-dictionaries
-       (sortSC wanteds)
-
-elimSCs_help :: LIE s                                  -- Given; no dups
-            -> [Inst s]                                -- Wanted; no dups;
-            -> NF_TcM s (Bag (TcIdOcc s, TcExpr s),    -- Bindings
-                         LIE s)                        -- Minimal wanted set
-
-elimSCs_help given [] = returnNF_Tc (emptyBag, emptyLIE)
-
-elimSCs_help givens (wanted:wanteds)
-  = trySC givens wanted                `thenNF_Tc` \ (givens1, binds1, irreds1) ->
-    elimSCs_help givens1 wanteds       `thenNF_Tc` \ (binds2, irreds2) ->
-    returnNF_Tc (binds1 `unionBags` binds2, irreds1 `plusLIE` irreds2)
-
-
-trySC :: LIE s                         -- Givens
-      -> Inst s                                -- Wanted
-      -> NF_TcM s (LIE s,                      -- New givens,
-                  Bag (TcIdOcc s,TcExpr s),    -- Bindings
-                  LIE s)                       -- Irreducible wanted set
-
-trySC givens wanted@(Dict _ wanted_class wanted_ty wanted_orig loc)
-  | not (maybeToBool maybe_best_subclass_chain)
-  =    -- No superclass relationship
-    returnNF_Tc (givens, emptyBag, unitLIE wanted)
-
-  | otherwise
-  =    -- There's a subclass relationship with a "given"
-       -- Build intermediate dictionaries
-    let
-       theta = [ (clas, wanted_ty) | clas <- reverse classes ]
-       -- The reverse is because the list comes back in the "wrong" order I think
-    in
-    newDictsAtLoc wanted_orig loc theta                `thenNF_Tc` \ (intermediates, _) ->
+@tcSimplifyCheck@ is used when we know exactly the set of variables
+we are going to quantify over.
 
-       -- Create bindings for the wanted dictionary and the intermediates.
-       -- Later binds may depend on earlier ones, so each new binding is pushed
-       -- on the front of the accumulating parameter list of bindings
+\begin{code}
+tcSimplifyCheck
+        :: SDoc 
+        -> [TcTyVar]           -- Quantify over these
+        -> [Inst]              -- Given
+        -> LIE                 -- Wanted
+        -> TcM (LIE,           -- Free
+                TcDictBinds)   -- Bindings
+
+tcSimplifyCheck doc qtvs givens wanted_lie
+  = checkLoop doc qtvs givens (lieToList wanted_lie)   `thenTc` \ (frees, binds, irreds) ->
+
+       -- Complain about any irreducible ones
+    complainCheck doc givens irreds            `thenNF_Tc_`
+
+       -- Done
+    returnTc (mkLIE frees, binds)
+
+checkLoop doc qtvs givens wanteds
+  =    -- Step 1
+    zonkTcTyVarsAndFV qtvs             `thenNF_Tc` \ qtvs' ->
+    mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
+    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
     let
-       mk_bind (dict,clas) dict_sub@(Dict _ dict_sub_class ty _ _)
-         = ((dict_sub, dict_sub_class),
-            (instToId dict, DictApp (TyApp (HsVar (RealId (classSuperDictSelId dict_sub_class 
-                                                                             clas)))
-                                           [ty])
-                                    [instToId dict_sub]))
-       (_, new_binds) = mapAccumR mk_bind (wanted,wanted_class) (given : intermediates)
+             -- When checking against a given signature we always reduce
+             -- until we find a match against something given, or can't reduce
+       try_me inst | isFree qtvs' inst  = Free
+                   | otherwise          = ReduceMe AddToIrreds
     in
-    returnNF_Tc (wanted `consLIE` givens `plusLIE` listToBag intermediates,
-                listToBag new_binds,
-                emptyLIE)
+               -- Step 2
+    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+       
+               -- Step 3
+    if no_improvement then
+           returnTc (frees, binds, irreds)
+    else
+           checkLoop doc qtvs givens wanteds
 
+complainCheck doc givens irreds
+  = mapNF_Tc zonkInst given_dicts                      `thenNF_Tc` \ givens' ->
+    mapNF_Tc (addNoInstanceErr doc given_dicts) irreds `thenNF_Tc_`
+    returnTc ()
   where
-    maybe_best_subclass_chain = foldBag choose_best find_subclass_chain Nothing givens
-    Just (given, classes, _) = maybe_best_subclass_chain
-
-    choose_best c1@(Just (_,_,n1)) c2@(Just (_,_,n2)) | n1 <= n2  = c1
-                                                     | otherwise = c2
-    choose_best Nothing                   c2                             = c2
-    choose_best c1                Nothing                        = c1
-
-    find_subclass_chain given@(Dict _ given_class given_ty _ _)
-        | wanted_ty `eqSimpleTy` given_ty
-        = case (wanted_class `isSuperClassOf` given_class) of
+    given_dicts = filter isDict givens
+       -- Filter out methods, which are only added to 
+       -- the given set as an optimisation
+\end{code}
 
-                Just classes -> Just (given,
-                                      classes,
-                                      length classes)
 
-                Nothing      -> Nothing
 
-        | otherwise = Nothing
+%************************************************************************
+%*                                                                     *
+\subsection{tcSimplifyAndCheck}
+%*                                                                     *
+%************************************************************************
 
+@tcSimplifyInferCheck@ is used when we know the consraints we are to simplify
+against, but we don't know the type variables over which we are going to quantify.
 
-sortSC :: LIE s     -- Expected to be all dicts (no MethodIds), all of
-                   -- which constrain type variables
-       -> [Inst s]  -- Sorted with subclasses before superclasses
+\begin{code}
+tcSimplifyInferCheck
+        :: SDoc 
+        -> [TcTyVar]           -- fv(T)
+        -> [Inst]              -- Given
+        -> LIE                 -- Wanted
+        -> TcM ([TcTyVar],     -- Variables over which to quantify
+                LIE,           -- Free
+                TcDictBinds)   -- Bindings
+
+tcSimplifyInferCheck doc tau_tvs givens wanted
+  = inferCheckLoop doc tau_tvs givens (lieToList wanted)       `thenTc` \ (qtvs, frees, binds, irreds) ->
+
+       -- Complain about any irreducible ones
+    complainCheck doc givens irreds            `thenNF_Tc_`
+
+       -- Done
+    returnTc (qtvs, mkLIE frees, binds)
+
+inferCheckLoop doc tau_tvs givens wanteds
+  =    -- Step 1
+    zonkTcTyVarsAndFV tau_tvs          `thenNF_Tc` \ tau_tvs' ->
+    mapNF_Tc zonkInst givens           `thenNF_Tc` \ givens' ->
+    mapNF_Tc zonkInst wanteds          `thenNF_Tc` \ wanteds' ->
+    tcGetGlobalTyVars                  `thenNF_Tc` \ gbl_tvs ->
 
-sortSC dicts = sortLt lt (bagToList dicts)
-  where
-    (Dict _ c1 ty1 _ _) `lt` (Dict _ c2 ty2 _ _)
-       = if ty1 `eqSimpleTy` ty2 then
-               maybeToBool (c2 `isSuperClassOf` c1)
-        else
-               -- Order is immaterial, I think...
-               False
+    let
+       -- Figure out what we are going to generalise over
+       -- You might think it should just be the signature tyvars,
+       -- but in bizarre cases you can get extra ones
+       --      f :: forall a. Num a => a -> a
+       --      f x = fst (g (x, head [])) + 1
+       --      g a b = (b,a)
+       -- Here we infer g :: forall a b. a -> b -> (b,a)
+       -- We don't want g to be monomorphic in b just because
+       -- f isn't quantified over b.
+       qtvs    = (tau_tvs' `unionVarSet` tyVarsOfInsts givens') `minusVarSet` gbl_tvs
+                       -- We could close gbl_tvs, but its not necessary for
+                       -- soundness, and it'll only affect which tyvars, not which 
+                       -- dictionaries, we quantify over
+
+             -- When checking against a given signature we always reduce
+             -- until we find a match against something given, or can't reduce
+       try_me inst | isFree qtvs inst  = Free
+                   | otherwise         = ReduceMe AddToIrreds
+    in
+               -- Step 2
+    reduceContext doc try_me givens' wanteds'    `thenTc` \ (no_improvement, frees, binds, irreds) ->
+       
+               -- Step 3
+    if no_improvement then
+           returnTc (varSetElems qtvs, frees, binds, irreds)
+    else
+           inferCheckLoop doc tau_tvs givens wanteds
 \end{code}
 
 
+
 %************************************************************************
 %*                                                                     *
-\subsection[simple]{@Simple@ versions}
+\subsection{tcSimplifyToDicts}
 %*                                                                     *
 %************************************************************************
 
-Much simpler versions when there are no bindings to make!
+On the LHS of transformation rules we only simplify methods and constants,
+getting dictionaries.  We want to keep all of them unsimplified, to serve
+as the available stuff for the RHS of the rule.
 
-@tcSimplifyThetas@ simplifies class-type constraints formed by
-@deriving@ declarations and when specialising instances.  We are
-only interested in the simplified bunch of class/type constraints.
+The same thing is used for specialise pragmas. Consider
+       
+       f :: Num a => a -> a
+       {-# SPECIALISE f :: Int -> Int #-}
+       f = ...
 
-\begin{code}
-tcSimplifyThetas :: (Class -> ClassInstEnv)            -- How to find the ClassInstEnv
-                -> [(Class, TauType)]                  -- Given
-                -> [(Class, TauType)]                  -- Wanted
-                -> TcM s [(Class, TauType)]
+The type checker generates a binding like:
 
+       f_spec = (f :: Int -> Int)
 
-tcSimplifyThetas inst_mapper given wanted
-  = elimTyConsSimple inst_mapper wanted        `thenTc`    \ wanted1 ->
-    returnTc (elimSCsSimple given wanted1)
-\end{code}
+and we want to end up with
 
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
-used with \tr{default} declarations.  We are only interested in
-whether it worked or not.
+       f_spec = _inline_me_ (f Int dNumInt)
+
+But that means that we must simplify the Method for f to (f Int dNumInt)! 
+So tcSimplifyToDicts squeezes out all Methods.
 
 \begin{code}
-tcSimplifyCheckThetas :: [(Class, TauType)]    -- Simplify this to nothing at all
-                     -> TcM s ()
+tcSimplifyToDicts :: LIE -> TcM ([Inst], TcDictBinds)
+tcSimplifyToDicts wanted_lie
+  = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) ->
+       -- Since try_me doesn't look at types, we don't need to 
+       -- do any zonking, so it's safe to call reduceContext directly
+    ASSERT( null frees )
+    returnTc (irreds, binds)
 
-tcSimplifyCheckThetas theta
-  = elimTyConsSimple classInstEnv theta    `thenTc`    \ theta1 ->
-    ASSERT( null theta1 )
-    returnTc ()
+  where
+    doc = text "tcSimplifyToDicts"
+    wanteds = lieToList wanted_lie
+
+       -- Reduce methods and lits only; stop as soon as we get a dictionary
+    try_me inst        | isDict inst = DontReduce
+               | otherwise   = ReduceMe AddToIrreds
 \end{code}
 
 
+%************************************************************************
+%*                                                                     *
+\subsection{Filtering at a dynamic binding}
+%*                                                                     *
+%************************************************************************
+
+When we have
+       let ?x = R in B
+
+we must discharge all the ?x constraints from B.  We also do an improvement
+step; if we have ?x::t1 and ?x::t2 we must unify t1, t2.  No need to iterate, though.
+
 \begin{code}
-elimTyConsSimple :: (Class -> ClassInstEnv) 
-                -> [(Class,Type)]
-                -> TcM s [(Class,Type)]
-elimTyConsSimple inst_mapper theta
-  = elim theta
-  where
-    elim []              = returnTc []
-    elim ((clas,ty):rest) = elim_one clas ty   `thenTc` \ r1 ->
-                           elim rest           `thenTc` \ r2 ->
-                           returnTc (r1++r2)
-
-    elim_one clas ty
-       = case getTyVar_maybe ty of
-
-           Just tv   -> returnTc [(clas,ty)]
-
-           otherwise -> recoverTc (returnTc []) $
-                        lookupSimpleInst (inst_mapper clas) clas ty    `thenTc` \ theta ->
-                        elim theta
-
-elimSCsSimple :: [(Class,Type)]        -- Given
-             -> [(Class,Type)]         -- Wanted
-             -> [(Class,Type)]         -- Subset of wanted; no dups, no subclass relnships
-
-elimSCsSimple givens [] = []
-elimSCsSimple givens (c_t@(clas,ty) : rest)
-  | any (`subsumes` c_t) givens ||
-    any (`subsumes` c_t) rest                          -- (clas,ty) is old hat
-  = elimSCsSimple givens rest
-  | otherwise                                          -- (clas,ty) is new
-  = c_t : elimSCsSimple (c_t : givens) rest
+tcSimplifyIPs :: [Name]                -- The implicit parameters bound here
+             -> LIE
+             -> TcM (LIE, TcDictBinds)
+tcSimplifyIPs ip_names wanted_lie
+  = simpleReduceLoop doc try_me wanteds        `thenTc` \ (frees, binds, irreds) ->
+       -- The irreducible ones should be a subset of the implicit
+       -- parameters we provided
+    ASSERT( all here_ip irreds )
+    returnTc (mkLIE frees, binds)
+    
   where
-    rest' = elimSCsSimple rest
-    (c1,t1) `subsumes` (c2,t2) = t1 `eqSimpleTy` t2 && 
-                                (c1 == c2 || maybeToBool (c2 `isSuperClassOf` c1))
--- We deal with duplicates here   ^^^^^^^^
--- It's a simple place to do it, although it's done in elimTyCons in the
--- full-blown version of the simpifier.
+    doc            = text "tcSimplifyIPs" <+> ppr ip_names
+    wanteds = lieToList wanted_lie
+    ip_set  = mkNameSet ip_names
+    here_ip ip = isDict ip && ip `instMentionsIPs` ip_set
+
+       -- Simplify any methods that mention the implicit parameter
+    try_me inst | inst `instMentionsIPs` ip_set = ReduceMe AddToIrreds
+               | otherwise                     = Free
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
@@ -569,53 +662,452 @@ For each method @Inst@ in the @init_lie@ that mentions one of the
 @LIE@), as well as the @HsBinds@ generated.
 
 \begin{code}
-bindInstsOfLocalFuns ::        LIE s -> [TcIdBndr s] -> TcM s (LIE s, TcMonoBinds s)
+bindInstsOfLocalFuns ::        LIE -> [TcId] -> TcM (LIE, TcMonoBinds)
 
 bindInstsOfLocalFuns init_lie local_ids
-  = foldrTc bind_inst (emptyBag, EmptyMonoBinds) (bagToList init_lie)
+  | null overloaded_ids 
+       -- Common case
+  = returnTc (init_lie, EmptyMonoBinds)
+
+  | otherwise
+  = simpleReduceLoop doc try_me wanteds                `thenTc` \ (frees, binds, irreds) -> 
+    ASSERT( null irreds )
+    returnTc (mkLIE frees, binds)
+  where
+    doc                     = text "bindInsts" <+> ppr local_ids
+    wanteds         = lieToList init_lie
+    overloaded_ids   = filter is_overloaded local_ids
+    is_overloaded id = case splitSigmaTy (idType id) of
+                         (_, theta, _) -> not (null theta)
+
+    overloaded_set = mkVarSet overloaded_ids   -- There can occasionally be a lot of them
+                                               -- so it's worth building a set, so that 
+                                               -- lookup (in isMethodFor) is faster
+
+    try_me inst | isMethodFor overloaded_set inst = ReduceMe AddToIrreds
+               | otherwise                       = Free
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection{Data types for the reduction mechanism}
+%*                                                                     *
+%************************************************************************
+
+The main control over context reduction is here
+
+\begin{code}
+data WhatToDo 
+ = ReduceMe              -- Try to reduce this
+       NoInstanceAction  -- What to do if there's no such instance
+
+ | DontReduce                  -- Return as irreducible 
+
+ | DontReduceUnlessConstant    -- Return as irreducible unless it can
+                               -- be reduced to a constant in one step
+
+ | Free                          -- Return as free
+
+data NoInstanceAction
+  = Stop               -- Fail; no error message
+                       -- (Only used when tautology checking.)
+
+  | AddToIrreds                -- Just add the inst to the irreductible ones; don't 
+                       -- produce an error message of any kind.
+                       -- It might be quite legitimate such as (Eq a)!
+\end{code}
+
+
+
+\begin{code}
+type RedState = (Avails,       -- What's available
+                [Inst])        -- Insts for which try_me returned Free
+
+type Avails = FiniteMap Inst Avail
+
+data Avail
+  = Irred              -- Used for irreducible dictionaries,
+                       -- which are going to be lambda bound
+
+  | BoundTo TcId       -- Used for dictionaries for which we have a binding
+                       -- e.g. those "given" in a signature
+
+  | NoRhs              -- Used for Insts like (CCallable f)
+                       -- where no witness is required.
+
+  | Rhs                -- Used when there is a RHS 
+       TcExpr          -- The RHS
+       [Inst]          -- Insts free in the RHS; we need these too
+
+pprAvails avails = vcat (map pprAvail (eltsFM avails))
+
+instance Outputable Avail where
+    ppr = pprAvail
+
+pprAvail NoRhs       = text "<no rhs>"
+pprAvail Irred       = text "Irred"
+pprAvail (BoundTo x)  = text "Bound to" <+> ppr x
+pprAvail (Rhs rhs bs) = ppr rhs <+> braces (ppr bs)
+\end{code}
+
+Extracting the bindings from a bunch of Avails.
+The bindings do *not* come back sorted in dependency order.
+We assume that they'll be wrapped in a big Rec, so that the
+dependency analyser can sort them out later
+
+The loop startes
+\begin{code}
+bindsAndIrreds :: Avails
+              -> [Inst]                -- Wanted
+              -> (TcDictBinds,         -- Bindings
+                  [Inst])              -- Irreducible ones
+
+bindsAndIrreds avails wanteds
+  = go avails EmptyMonoBinds [] wanteds
   where
-    bind_inst inst@(Method uniq (TcId id) tys rho orig loc) (insts, binds)
-      | id `is_elem` local_ids
-      = lookupInst inst                `thenTc` \ (dict_insts, (id,rhs)) ->
-       returnTc (listToBag dict_insts `plusLIE` insts, 
-                 VarMonoBind id rhs `AndMonoBinds` binds)
+    go avails binds irreds [] = (binds, irreds)
+
+    go avails binds irreds (w:ws)
+      = case lookupFM avails w of
+         Nothing    -> -- Free guys come out here
+                       -- (If we didn't do addFree we could use this as the
+                       --  criterion for free-ness, and pick up the free ones here too)
+                       go avails binds irreds ws
+
+         Just NoRhs -> go avails binds irreds ws
+
+         Just Irred -> go (addToFM avails w (BoundTo (instToId w))) binds (w:irreds) ws
+
+         Just (BoundTo id) -> go avails new_binds irreds ws
+                           where
+                               -- For implicit parameters, all occurrences share the same
+                               -- Id, so there is no need for synonym bindings
+                              new_binds | new_id == id = binds
+                                        | otherwise    = binds `AndMonoBinds` new_bind
+                              new_bind = VarMonoBind new_id (HsVar id)
+                              new_id   = instToId w
+
+         Just (Rhs rhs ws') -> go avails' (binds `AndMonoBinds` new_bind) irreds (ws' ++ ws)
+                            where
+                               id       = instToId w
+                               avails'  = addToFM avails w (BoundTo id)
+                               new_bind = VarMonoBind id rhs
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\subsection[reduce]{@reduce@}
+%*                                                                     *
+%************************************************************************
+
+When the "what to do" predicate doesn't depend on the quantified type variables,
+matters are easier.  We don't need to do any zonking, unless the improvement step
+does something, in which case we zonk before iterating.
+
+The "given" set is always empty.
+
+\begin{code}
+simpleReduceLoop :: SDoc
+                -> (Inst -> WhatToDo)          -- What to do, *not* based on the quantified type variables
+                -> [Inst]                      -- Wanted
+                -> TcM ([Inst],                -- Free
+                        TcDictBinds,
+                        [Inst])                -- Irreducible
+
+simpleReduceLoop doc try_me wanteds
+  = mapNF_Tc zonkInst wanteds                  `thenNF_Tc` \ wanteds' ->
+    reduceContext doc try_me [] wanteds'       `thenTc` \ (no_improvement, frees, binds, irreds) ->
+    if no_improvement then
+       returnTc (frees, binds, irreds)
+    else
+       simpleReduceLoop doc try_me wanteds
+\end{code}     
 
-    bind_inst some_other_inst (insts, binds)
-       -- Either not a method, or a method instance for an id not in local_ids
-      = returnTc (some_other_inst `consBag` insts, binds)
 
-    is_elem = isIn "bindInstsOfLocalFuns"
+
+\begin{code}
+reduceContext :: SDoc
+             -> (Inst -> WhatToDo)
+             -> [Inst]                 -- Given
+             -> [Inst]                 -- Wanted
+             -> NF_TcM (Bool,          -- True <=> improve step did no unification
+                        [Inst],        -- Free
+                        TcDictBinds,   -- Dictionary bindings
+                        [Inst])        -- Irreducible
+
+reduceContext doc try_me givens wanteds
+  =
+{-    traceTc (text "reduceContext" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "given" <+> ppr givens,
+            text "wanted" <+> ppr wanteds,
+            text "----------------------"
+            ]))                                        `thenNF_Tc_`
+
+-}
+        -- Build the Avail mapping from "givens"
+    foldlNF_Tc addGiven (emptyFM, []) givens           `thenNF_Tc` \ init_state ->
+
+        -- Do the real work
+    reduceList (0,[]) try_me wanteds init_state                `thenNF_Tc` \ state@(avails, frees) ->
+
+       -- Do improvement, using everything in avails
+       -- In particular, avails includes all superclasses of everything
+    tcImprove avails                                   `thenTc` \ no_improvement ->
+
+{-
+    traceTc (text "reduceContext end" <+> (vcat [
+            text "----------------------",
+            doc,
+            text "given" <+> ppr givens,
+            text "wanted" <+> ppr wanteds,
+            text "----", 
+            text "avails" <+> pprAvails avails,
+            text "frees" <+> ppr frees,
+            text "no_improvement =" <+> ppr no_improvement,
+            text "----------------------"
+            ]))                                        `thenNF_Tc_`
+-}
+     let
+       (binds, irreds) = bindsAndIrreds avails wanteds
+     in
+     returnTc (no_improvement, frees, binds, irreds)
+
+tcImprove avails
+ =  tcGetInstEnv                               `thenTc` \ inst_env ->
+    let
+       preds = predsOfInsts (keysFM avails)
+               -- 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
+       eqns  = improve (classInstEnv inst_env) preds
+     in
+     if null eqns then
+       returnTc True
+     else
+        mapTc_ (\ (t1,t2) -> unifyTauTy t1 t2) eqns    `thenTc_`
+       returnTc False
+\end{code}
+
+The main context-reduction function is @reduce@.  Here's its game plan.
+
+\begin{code}
+reduceList :: (Int,[Inst])             -- Stack (for err msgs)
+                                       -- along with its depth
+                  -> (Inst -> WhatToDo)
+                  -> [Inst]
+                  -> RedState
+                  -> TcM RedState
+\end{code}
+
+@reduce@ is passed
+     try_me:   given an inst, this function returns
+                 Reduce       reduce this
+                 DontReduce   return this in "irreds"
+                 Free         return this in "frees"
+
+     wanteds:  The list of insts to reduce
+     state:    An accumulating parameter of type RedState 
+               that contains the state of the algorithm
+  It returns a RedState.
+
+The (n,stack) pair is just used for error reporting.  
+n is always the depth of the stack.
+The stack is the stack of Insts being reduced: to produce X
+I had to produce Y, to produce Y I had to produce Z, and so on.
+
+\begin{code}
+reduceList (n,stack) try_me wanteds state
+  | n > opt_MaxContextReductionDepth
+  = failWithTc (reduceDepthErr n stack)
+
+  | otherwise
+  =
+#ifdef DEBUG
+   (if n > 8 then
+       pprTrace "Jeepers! ReduceContext:" (reduceDepthMsg n stack)
+    else (\x->x))
+#endif
+    go wanteds state
+  where
+    go []     state = returnTc state
+    go (w:ws) state = reduce (n+1, w:stack) try_me w state     `thenTc` \ state' ->
+                     go ws state'
+
+    -- Base case: we're done!
+reduce stack try_me wanted state
+    -- It's the same as an existing inst, or a superclass thereof
+  | isAvailable state wanted
+  = returnTc state
+
+  | otherwise
+  = case try_me wanted of {
+
+      DontReduce -> addIrred state wanted
+
+    ; DontReduceUnlessConstant ->    -- It's irreducible (or at least should not be reduced)
+                                    -- First, see if the inst can be reduced to a constant in one step
+       try_simple addIrred
+
+    ; Free ->  -- It's free so just chuck it upstairs
+               -- First, see if the inst can be reduced to a constant in one step
+       try_simple addFree
+
+    ; ReduceMe no_instance_action ->   -- It should be reduced
+       lookupInst wanted             `thenNF_Tc` \ lookup_result ->
+       case lookup_result of
+           GenInst wanteds' rhs -> reduceList stack try_me wanteds' state      `thenTc` \ state' -> 
+                                   addWanted state' wanted rhs wanteds'
+           SimpleInst rhs       -> addWanted state wanted rhs []
+
+           NoInstance ->    -- No such instance! 
+                   case no_instance_action of
+                       Stop        -> failTc           
+                       AddToIrreds -> addIrred state wanted
+
+    }
+  where
+    try_simple do_this_otherwise
+      = lookupInst wanted        `thenNF_Tc` \ lookup_result ->
+       case lookup_result of
+           SimpleInst rhs -> addWanted state wanted rhs []
+           other          -> do_this_otherwise state wanted
+\end{code}
+
+
+\begin{code}
+isAvailable :: RedState -> Inst -> Bool
+isAvailable (avails, _) wanted = wanted `elemFM` avails
+       -- NB: the Ord instance of Inst compares by the class/type info
+       -- *not* by unique.  So 
+       --      d1::C Int ==  d2::C Int
+
+-------------------------
+addFree :: RedState -> Inst -> NF_TcM RedState
+       -- When an Inst is tossed upstairs as 'free' we nevertheless add it
+       -- to avails, so that any other equal Insts will be commoned up right
+       -- here rather than also being tossed upstairs.  This is really just
+       -- an optimisation, and perhaps it is more trouble that it is worth,
+       -- as the following comments show!
+       --
+       -- NB1: do *not* add superclasses.  If we have
+       --      df::Floating a
+       --      dn::Num a
+       -- but a is not bound here, then we *don't* want to derive 
+       -- dn from df here lest we lose sharing.
+       --
+       -- NB2: do *not* add the Inst to avails at all if it's a method.
+       -- The following situation shows why this is bad:
+       --      truncate :: forall a. RealFrac a => forall b. Integral b => a -> b
+       -- From an application (truncate f i) we get
+       --      t1 = truncate at f 
+       --      t2 = t1 at i
+       -- If we have also have a second occurrence of truncate, we get
+       --      t3 = truncate at f
+       --      t4 = t3 at i
+       -- When simplifying with i,f free, we might still notice that
+       --   t1=t3; but alas, the binding for t2 (which mentions t1)
+       --   will continue to float out!
+       -- Solution: never put methods in avail till they are captured
+       -- in which case addFree isn't used
+       --
+       -- NB3: make sure that CCallable/CReturnable use NoRhs rather
+       --      than BoundTo, else we end up with bogus bindings.
+       --      c.f. instBindingRequired in addWanted
+addFree (avails, frees) free
+  | isDict free = returnNF_Tc (addToFM avails free avail, free:frees)
+  | otherwise   = returnNF_Tc (avails,                   free:frees)
+  where
+    avail | instBindingRequired free = BoundTo (instToId free)
+         | otherwise                = NoRhs
+
+addGiven :: RedState -> Inst -> NF_TcM RedState
+addGiven state given = add_avail state given (BoundTo (instToId given))
+
+addIrred :: RedState -> Inst -> NF_TcM RedState
+addIrred state irred = add_avail state irred Irred
+
+addWanted :: RedState -> Inst -> TcExpr -> [Inst] -> NF_TcM RedState
+addWanted state wanted rhs_expr wanteds
+  = ASSERT( not (isAvailable state wanted) )
+    add_avail state wanted avail
+  where 
+    avail | instBindingRequired wanted = Rhs rhs_expr wanteds
+         | otherwise                  = ASSERT( null wanteds ) NoRhs
+
+add_avail :: RedState -> Inst -> Avail -> NF_TcM RedState
+add_avail (avails, frees) wanted avail
+  = addAvail avails wanted avail       `thenNF_Tc` \ avails' ->
+    returnNF_Tc (avails', frees)
+
+---------------------
+addAvail :: Avails -> Inst -> Avail -> NF_TcM Avails
+addAvail avails wanted avail
+  = addSuperClasses (addToFM avails wanted avail) wanted
+
+addSuperClasses :: Avails -> Inst -> NF_TcM Avails
+       -- Add all the superclasses of the Inst to Avails
+       -- Invariant: the Inst is already in Avails.
+
+addSuperClasses avails dict
+  | not (isClassDict dict)
+  = returnNF_Tc avails
+
+  | otherwise  -- It is a dictionary
+  = newDictsFromOld dict sc_theta'     `thenNF_Tc` \ sc_dicts ->
+    foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_dicts sc_sels)
+  where
+    (clas, tys) = getDictClassTys dict
+    (tyvars, sc_theta, sc_sels, _) = classBigSig clas
+    sc_theta' = substClasses (mkTopTyVarSubst tyvars tys) sc_theta
+
+    add_sc avails (sc_dict, sc_sel)    -- Add it, and its superclasses
+      = case lookupFM avails sc_dict of
+         Just (BoundTo _) -> returnNF_Tc avails        -- See Note [SUPER] below
+         other            -> addAvail avails sc_dict avail
+      where
+       sc_sel_rhs = DictApp (TyApp (HsVar sc_sel) tys) [instToId dict]
+       avail      = Rhs sc_sel_rhs [dict]
 \end{code}
 
+Note [SUPER].  We have to be careful here.  If we are *given* d1:Ord a,
+and want to deduce (d2:C [a]) where
+
+       class Ord a => C a where
+       instance Ord a => C [a] where ...
+
+Then we'll use the instance decl to deduce C [a] and then add the 
+superclasses of C [a] to avails.  But we must not overwrite the binding
+for d1:Ord a (which is given) with a superclass selection or we'll just
+build a loop!  Hence looking for BoundTo.  Crudely, BoundTo is cheaper
+than a selection.
+
 
 %************************************************************************
 %*                                                                     *
-\section[Disambig]{Disambiguation of overloading}
+\section{tcSimplifyTop: defaulting}
 %*                                                                     *
 %************************************************************************
 
 
 If a dictionary constrains a type variable which is
-\begin{itemize}
-\item
-not mentioned in the environment
-\item
-and not mentioned in the type of the expression
-\end{itemize}
+       * not mentioned in the environment
+       * and not mentioned in the type of the expression
 then it is ambiguous. No further information will arise to instantiate
 the type variable; nor will it be generalised and turned into an extra
 parameter to a function.
 
 It is an error for this to occur, except that Haskell provided for
 certain rules to be applied in the special case of numeric types.
-
 Specifically, if
-\begin{itemize}
-\item
-at least one of its classes is a numeric class, and
-\item
-all of its classes are numeric or standard
-\end{itemize}
+       * at least one of its classes is a numeric class, and
+       * all of its classes are numeric or standard
 then the type variable can be defaulted to the first type in the
 default-type list which is an instance of all the offending classes.
 
@@ -624,23 +1116,61 @@ dictionaries and either resolves them (producing bindings) or
 complains.  It works by splitting the dictionary list by type
 variable, and using @disambigOne@ to do the real business.
 
-IMPORTANT: @disambiguate@ assumes that its argument dictionaries
-constrain only a simple type variable.
+@tcSimplifyTop@ is called once per module to simplify all the constant
+and ambiguous Insts.
+
+We need to be careful of one case.  Suppose we have
+
+       instance Num a => Num (Foo a b) where ...
+
+and @tcSimplifyTop@ is given a constraint (Num (Foo x y)).  Then it'll simplify
+to (Num x), and default x to Int.  But what about y??  
+
+It's OK: the final zonking stage should zap y to (), which is fine.
+
 
 \begin{code}
-type SimpleDictInfo s = (Inst s, Class, TcTyVar s)
+tcSimplifyTop :: LIE -> TcM TcDictBinds
+tcSimplifyTop wanted_lie
+  = simpleReduceLoop (text "tcSimplTop") try_me wanteds        `thenTc` \ (frees, binds, irreds) ->
+    ASSERT( null frees )
 
-disambiguateDicts :: LIE s -> TcM s ()
+    let
+               -- All the non-std ones are definite errors
+       (stds, non_stds) = partition isStdClassTyVarDict irreds
+       
+               -- Group by type variable
+       std_groups = equivClasses cmp_by_tyvar stds
+
+               -- Pick the ones which its worth trying to disambiguate
+       (std_oks, std_bads) = partition worth_a_try std_groups
+
+               -- Have a try at disambiguation 
+               -- if the type variable isn't bound
+               -- up with one of the non-standard classes
+       worth_a_try group@(d:_) = not (non_std_tyvars `intersectsVarSet` tyVarsOfInst d)
+       non_std_tyvars          = unionVarSets (map tyVarsOfInst non_stds)
+
+               -- Collect together all the bad guys
+       bad_guys = non_stds ++ concat std_bads
+    in
+       -- Disambiguate the ones that look feasible
+    mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
 
-disambiguateDicts insts
-  = mapTc disambigOne inst_infos    `thenTc` \ binds_lists ->
-    returnTc ()
+       -- And complain about the ones that don't
+    addTopAmbigErrs bad_guys           `thenNF_Tc_`
+
+    returnTc (binds `andMonoBinds` andMonoBindList binds_ambig)
   where
-    inst_infos = equivClasses cmp_tyvars (map mk_inst_info (bagToList insts))
-    (_,_,tv1) `cmp_tyvars` (_,_,tv2) = tv1 `cmp` tv2
+    wanteds    = lieToList wanted_lie
+    try_me inst        = ReduceMe AddToIrreds
+
+    d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
 
-    mk_inst_info dict@(Dict _ clas ty _ _)
-      = (dict, clas, getTyVar "disambiguateDicts" ty)
+get_tv d   = case getDictClassTys d of
+                  (clas, [ty]) -> getTyVar "tcSimplifyTop" ty
+get_clas d = case getDictClassTys d of
+                  (clas, [ty]) -> clas
 \end{code}
 
 @disambigOne@ assumes that its arguments dictionaries constrain all
@@ -656,13 +1186,15 @@ Since we're not using the result of @foo@, the result if (presumably)
 @void@.
 
 \begin{code}
-disambigOne :: [SimpleDictInfo s] -> TcM s ()
-
-disambigOne dict_infos
-  | not (isStandardNumericDefaultable classes)
-  = failTc (ambigErr dicts) -- no default
-
-  | otherwise -- isStandardNumericDefaultable dict_infos
+disambigGroup :: [Inst]        -- All standard classes of form (C a)
+             -> TcM TcDictBinds
+
+disambigGroup dicts
+  |   any isNumericClass classes       -- Guaranteed all standard classes
+         -- see comment at the end of function for reasons as to 
+         -- why the defaulting mechanism doesn't apply to groups that
+         -- include CCallable or CReturnable dicts.
+   && not (any isCcallishClass classes)
   =    -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
        -- SO, TRY DEFAULT TYPES IN ORDER
 
@@ -673,77 +1205,332 @@ disambigOne dict_infos
     tcGetDefaultTys                    `thenNF_Tc` \ default_tys ->
     let
       try_default []   -- No defaults work, so fail
-       = failTc (defaultErr dicts default_tys) 
+       = failTc
 
       try_default (default_ty : default_tys)
-       = tryTc (try_default default_tys) $     -- If default_ty fails, we try
+       = tryTc_ (try_default default_tys) $    -- If default_ty fails, we try
                                                -- default_tys instead
-         tcSimplifyCheckThetas thetas  `thenTc` \ _ ->
+         tcSimplifyCheckThetas [] thetas       `thenTc` \ _ ->
          returnTc default_ty
         where
-         thetas = classes `zip` repeat default_ty
+         thetas = classes `zip` repeat [default_ty]
     in
        -- See if any default works, and if so bind the type variable to it
-    try_default default_tys            `thenTc` \ chosen_default_ty ->
-    tcInstType [] chosen_default_ty    `thenNF_Tc` \ chosen_default_tc_ty ->   -- Tiresome!
-    unifyTauTy (mkTyVarTy tyvar) chosen_default_tc_ty
+       -- If not, add an AmbigErr
+    recoverTc (addAmbigErrs dicts `thenNF_Tc_` returnTc EmptyMonoBinds)        $
 
-  where
-    (_,_,tyvar) = head dict_infos              -- Should be non-empty
-    dicts   = [dict | (dict,_,_) <- dict_infos]
-    classes = [clas | (_,clas,_) <- dict_infos]
+    try_default default_tys                    `thenTc` \ chosen_default_ty ->
+
+       -- Bind the type variable and reduce the context, for real this time
+    unifyTauTy chosen_default_ty (mkTyVarTy tyvar)     `thenTc_`
+    simpleReduceLoop (text "disambig" <+> ppr dicts)
+                    try_me dicts                       `thenTc` \ (frees, binds, ambigs) ->
+    WARN( not (null frees && null ambigs), ppr frees $$ ppr ambigs )
+    warnDefault dicts chosen_default_ty                        `thenTc_`
+    returnTc binds
 
+  | all isCreturnableClass classes
+  =    -- Default CCall stuff to (); we don't even both to check that () is an 
+       -- instance of CReturnable, because we know it is.
+    unifyTauTy (mkTyVarTy tyvar) unitTy    `thenTc_`
+    returnTc EmptyMonoBinds
+    
+  | otherwise -- No defaults
+  = addAmbigErrs dicts `thenNF_Tc_`
+    returnTc EmptyMonoBinds
+
+  where
+    try_me inst = ReduceMe AddToIrreds         -- This reduce should not fail
+    tyvar       = get_tv (head dicts)          -- Should be non-empty
+    classes     = map get_clas dicts
 \end{code}
 
-@isStandardNumericDefaultable@ sees whether the dicts have the
-property required for defaulting; namely at least one is numeric, and
-all are standard; or all are CcallIsh.
+[Aside - why the defaulting mechanism is turned off when
+ dealing with arguments and results to ccalls.
 
-\begin{code}
-isStandardNumericDefaultable :: [Class] -> Bool
+When typechecking _ccall_s, TcExpr ensures that the external
+function is only passed arguments (and in the other direction,
+results) of a restricted set of 'native' types. This is
+implemented via the help of the pseudo-type classes,
+@CReturnable@ (CR) and @CCallable@ (CC.)
+The interaction between the defaulting mechanism for numeric
+values and CC & CR can be a bit puzzling to the user at times.
+For example,
 
-isStandardNumericDefaultable classes
-  = --pprTrace "isStdNumeric:\n" (ppAboves [ppCat (map (ppr PprDebug) classes), ppCat (map (ppr PprDebug . isNumericClass) classes), ppCat (map (ppr PprDebug . isStandardClass) classes), ppCat (map (ppr PprDebug . isCcallishClass) classes)]) $
-     (any isNumericClass classes && all isStandardClass classes)
-  || (all isCcallishClass classes)
-\end{code}
+    x <- _ccall_ f
+    if (x /= 0) then
+       _ccall_ g x
+     else
+       return ()
 
+What type has 'x' got here? That depends on the default list
+in operation, if it is equal to Haskell 98's default-default
+of (Integer, Double), 'x' has type Double, since Integer
+is not an instance of CR. If the default list is equal to
+Haskell 1.4's default-default of (Int, Double), 'x' has type
+Int. 
 
+To try to minimise the potential for surprises here, the
+defaulting mechanism is turned off in the presence of
+CCallable and CReturnable.
 
-Errors and contexts
-~~~~~~~~~~~~~~~~~~~
-ToDo: for these error messages, should we note the location as coming
-from the insts, or just whatever seems to be around in the monad just
-now?
+]
+
+
+%************************************************************************
+%*                                                                     *
+\subsection[simple]{@Simple@ versions}
+%*                                                                     *
+%************************************************************************
+
+Much simpler versions when there are no bindings to make!
+
+@tcSimplifyThetas@ simplifies class-type constraints formed by
+@deriving@ declarations and when specialising instances.  We are
+only interested in the simplified bunch of class/type constraints.
+
+It simplifies to constraints of the form (C a b c) where
+a,b,c are type variables.  This is required for the context of
+instance declarations.
 
 \begin{code}
-genCantGenErr insts sty        -- Can't generalise these Insts
-  = ppHang (ppStr "Cannot generalise these overloadings (in a _ccall_):") 
-          4  (ppAboves (map (ppr sty) (bagToList insts)))
+tcSimplifyThetas :: ClassContext               -- Wanted
+                -> TcM ClassContext            -- Needed
+
+tcSimplifyThetas wanteds
+  = doptsTc Opt_GlasgowExts            `thenNF_Tc` \ glaExts ->
+    reduceSimple [] wanteds            `thenNF_Tc` \ irreds ->
+    let
+       -- For multi-param Haskell, check that the returned dictionaries
+       -- don't have any of the form (C Int Bool) for which
+       -- we expect an instance here
+       -- For Haskell 98, check that all the constraints are of the form C a,
+       -- where a is a type variable
+       bad_guys | glaExts   = [ct | ct@(clas,tys) <- irreds, 
+                                    isEmptyVarSet (tyVarsOfTypes tys)]
+                | otherwise = [ct | ct@(clas,tys) <- irreds, 
+                                    not (all isTyVarTy tys)]
+    in
+    if null bad_guys then
+       returnTc irreds
+    else
+       mapNF_Tc addNoInstErr bad_guys          `thenNF_Tc_`
+       failTc
 \end{code}
 
+@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+used with \tr{default} declarations.  We are only interested in
+whether it worked or not.
+
 \begin{code}
-ambigErr insts sty
-  = ppAboves (map (pprInst sty "Ambiguous overloading") insts)
+tcSimplifyCheckThetas :: ClassContext  -- Given
+                     -> ClassContext   -- Wanted
+                     -> TcM ()
+
+tcSimplifyCheckThetas givens wanteds
+  = reduceSimple givens wanteds    `thenNF_Tc` \ irreds ->
+    if null irreds then
+       returnTc ()
+    else
+       mapNF_Tc addNoInstErr irreds            `thenNF_Tc_`
+       failTc
 \end{code}
 
-@reduceErr@ complains if we can't express required dictionaries in
-terms of the signature.
 
 \begin{code}
-reduceErr insts sty
-  = ppAboves (map (pprInst sty "Context required by inferred type, but missing on a type signature")
-                 (bagToList insts))
+type AvailsSimple = FiniteMap (Class,[Type]) Bool
+                   -- True  => irreducible 
+                   -- False => given, or can be derived from a given or from an irreducible
+
+reduceSimple :: ClassContext                   -- Given
+            -> ClassContext                    -- Wanted
+            -> NF_TcM ClassContext             -- Irreducible
+
+reduceSimple givens wanteds
+  = reduce_simple (0,[]) givens_fm wanteds     `thenNF_Tc` \ givens_fm' ->
+    returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
+  where
+    givens_fm     = foldl addNonIrred emptyFM givens
+
+reduce_simple :: (Int,ClassContext)            -- Stack
+             -> AvailsSimple
+             -> ClassContext
+             -> NF_TcM AvailsSimple
+
+reduce_simple (n,stack) avails wanteds
+  = go avails wanteds
+  where
+    go avails []     = returnNF_Tc avails
+    go avails (w:ws) = reduce_simple_help (n+1,w:stack) avails w       `thenNF_Tc` \ avails' ->
+                      go avails' ws
+
+reduce_simple_help stack givens wanted@(clas,tys)
+  | wanted `elemFM` givens
+  = returnNF_Tc givens
+
+  | otherwise
+  = lookupSimpleInst clas tys  `thenNF_Tc` \ maybe_theta ->
+
+    case maybe_theta of
+      Nothing ->    returnNF_Tc (addSimpleIrred givens wanted)
+      Just theta -> reduce_simple stack (addNonIrred givens wanted) theta
+
+addSimpleIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addSimpleIrred givens ct@(clas,tys)
+  = addSCs (addToFM givens ct True) ct
+
+addNonIrred :: AvailsSimple -> (Class,[Type]) -> AvailsSimple
+addNonIrred givens ct@(clas,tys)
+  = addSCs (addToFM givens ct False) ct
+
+addSCs givens ct@(clas,tys)
+ = foldl add givens sc_theta
+ where
+   (tyvars, sc_theta_tmpl, _, _) = classBigSig clas
+   sc_theta = substClasses (mkTopTyVarSubst tyvars tys) sc_theta_tmpl
+
+   add givens ct@(clas, tys)
+     = case lookupFM givens ct of
+       Nothing    -> -- Add it and its superclasses
+                    addSCs (addToFM givens ct False) ct
+
+       Just True  -> -- Set its flag to False; superclasses already done
+                    addToFM givens ct False
+
+       Just False -> -- Already done
+                    givens
+                          
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+\section{Errors and contexts}
+%*                                                                     *
+%************************************************************************
+
+ToDo: for these error messages, should we note the location as coming
+from the insts, or just whatever seems to be around in the monad just
+now?
+
 \begin{code}
-defaultErr dicts defaulting_tys sty
-  = ppHang (ppStr "Ambiguously-overloaded types could not be resolved:")
-        4 (ppAboves [
-            ppHang (ppStr "Conflicting:")
-                 4 (ppInterleave ppSemi (map (pprInst sty ""{-???-}) dicts)),
-            ppHang (ppStr "Defaulting types :")
-                 4 (ppr sty defaulting_tys),
-            ppStr "([Int, Double] is the default list of defaulting types.)" ])
-\end{code}
+addTopAmbigErrs dicts
+  = mapNF_Tc complain tidy_dicts
+  where
+    fixed_tvs = oclose (predsOfInsts tidy_dicts) emptyVarSet
+    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
+    complain d | not (null (getIPs d))               = addTopIPErr tidy_env d
+              | tyVarsOfInst d `subVarSet` fixed_tvs = addTopInstanceErr tidy_env d
+              | otherwise                            = addAmbigErr tidy_env d
+
+addTopIPErr tidy_env tidy_dict
+  = addInstErrTcM (instLoc tidy_dict) 
+       (tidy_env, 
+        ptext SLIT("Unbound implicit parameter") <+> quotes (pprInst tidy_dict))
+
+-- Used for top-level irreducibles
+addTopInstanceErr tidy_env tidy_dict
+  = addInstErrTcM (instLoc tidy_dict) 
+       (tidy_env, 
+        ptext SLIT("No instance for") <+> quotes (pprInst tidy_dict))
+
+addAmbigErrs dicts
+  = mapNF_Tc (addAmbigErr tidy_env) tidy_dicts
+  where
+    (tidy_env, tidy_dicts) = tidyInsts emptyTidyEnv dicts
+
+addAmbigErr tidy_env tidy_dict
+  = addInstErrTcM (instLoc tidy_dict)
+       (tidy_env,
+        sep [text "Ambiguous type variable(s)" <+> pprQuotedList ambig_tvs,
+             nest 4 (text "in the constraint" <+> quotes (pprInst tidy_dict))])
+  where
+    ambig_tvs = varSetElems (tyVarsOfInst tidy_dict)
+
+warnDefault dicts default_ty
+  = doptsTc Opt_WarnTypeDefaults  `thenTc` \ warn_flag ->
+    if warn_flag 
+       then mapNF_Tc warn groups  `thenNF_Tc_`  returnNF_Tc ()
+       else returnNF_Tc ()
+
+  where
+       -- Tidy them first
+    (_, tidy_dicts) = mapAccumL tidyInst emptyTidyEnv dicts
+
+       -- Group the dictionaries by source location
+    groups      = equivClasses cmp tidy_dicts
+    i1 `cmp` i2 = get_loc i1 `compare` get_loc i2
+    get_loc i   = case instLoc i of { (_,loc,_) -> loc }
+
+    warn [dict] = tcAddSrcLoc (get_loc dict) $
+                 warnTc True (ptext SLIT("Defaulting") <+> quotes (pprInst dict) <+> 
+                              ptext SLIT("to type") <+> quotes (ppr default_ty))
+
+    warn dicts  = tcAddSrcLoc (get_loc (head dicts)) $
+                 warnTc True (vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+> quotes (ppr default_ty),
+                                    pprInstsInFull dicts])
+
+-- The error message when we don't find a suitable instance
+-- is complicated by the fact that sometimes this is because
+-- there is no instance, and sometimes it's because there are
+-- too many instances (overlap).  See the comments in TcEnv.lhs
+-- with the InstEnv stuff.
+addNoInstanceErr what_doc givens dict
+  = tcGetInstEnv       `thenNF_Tc` \ inst_env ->
+    let
+       doc = vcat [sep [herald <+> quotes (pprInst tidy_dict),
+                        nest 4 $ ptext SLIT("from the context") <+> pprInsts tidy_givens],
+                   ambig_doc,
+                   ptext SLIT("Probable fix:"),
+                   nest 4 fix1,
+                   nest 4 fix2]
+    
+       herald = ptext SLIT("Could not") <+> unambig_doc <+> ptext SLIT("deduce")
+       unambig_doc | ambig_overlap = ptext SLIT("unambiguously")       
+                   | otherwise     = empty
+    
+       ambig_doc 
+           | not ambig_overlap = empty
+           | otherwise             
+           = vcat [ptext SLIT("The choice of (overlapping) instance declaration"),
+                   nest 4 (ptext SLIT("depends on the instantiation of") <+> 
+                           quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst tidy_dict))))]
+    
+       fix1 = sep [ptext SLIT("Add") <+> quotes (pprInst tidy_dict),
+                   ptext SLIT("to the") <+> what_doc]
+    
+       fix2 | isTyVarDict dict || ambig_overlap
+            = empty
+            | otherwise
+            = ptext SLIT("Or add an instance declaration for") <+> quotes (pprInst tidy_dict)
+    
+       (tidy_env, tidy_dict:tidy_givens) = tidyInsts emptyTidyEnv (dict:givens)
+    
+           -- Checks for the ambiguous case when we have overlapping instances
+       ambig_overlap | isClassDict dict
+                     = case lookupInstEnv inst_env clas tys of
+                           NoMatch ambig -> ambig
+                           other         -> False
+                     | otherwise = False
+                     where
+                       (clas,tys) = getDictClassTys dict
+    in
+    addInstErrTcM (instLoc dict) (tidy_env, doc)
+
+-- Used for the ...Thetas variants; all top level
+addNoInstErr (c,ts)
+  = addErrTc (ptext SLIT("No instance for") <+> quotes (pprClassPred c ts))
+
+reduceDepthErr n stack
+  = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
+         ptext SLIT("Use -fcontext-stack20 to increase stack size to (e.g.) 20"),
+         nest 4 (pprInstsInFull stack)]
 
+reduceDepthMsg n stack = nest 4 (pprInstsInFull stack)
+
+-----------------------------------------------
+addCantGenErr inst
+  = addErrTc (sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"), 
+                  nest 4 (ppr inst <+> pprInstLoc (instLoc inst))])
+\end{code}