[project @ 1998-06-08 11:45:09 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcSimplify.lhs
index 126109a..e289201 100644 (file)
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
+% (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
 %
 \section[TcSimplify]{TcSimplify}
 
-\begin{code}
-#include "HsVersions.h"
+Notes:
 
-module TcSimplify (
-       tcSimplify, tcSimplifyAndCheck,
-       tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas, tcSimplifyRank2,
-       bindInstsOfLocalFuns
-    ) where
+Inference (local definitions)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the inst constrains a local type variable, then
+  [ReduceMe] if it's a literal or method inst, reduce it
 
-IMPORT_Trace           -- ToDo: rm (debugging)
-import Outputable
-import Pretty
+  [DontReduce] otherwise see whether the inst is just a constant
+    if succeed, use it
+    if not, add original to context
+  This check gets rid of constant dictionaries without
+  losing sharing.
 
-import TcMonad         -- typechecking monadic machinery
-import TcMonadFns      ( newDicts, applyTcSubstAndExpectTyVars )
-import AbsSyn          -- the stuff being typechecked
+If the inst does not constrain a local type variable then
+  [Free] then throw it out as free.
 
-import AbsUniType      ( isSuperClassOf, getTyVar, eqTyVar, ltTyVar,
-                         instantiateThetaTy, isFunType, getUniDataTyCon,
-                         getSuperDictSelId, InstTyEnv(..)
-                         IF_ATTACK_PRAGMAS(COMMA isTyVarTy COMMA pprUniType)
-                         IF_ATTACK_PRAGMAS(COMMA assocMaybe)
-                       )
-import UniType         ( UniType(..) ) -- ******* CHEATING ************
-import Disambig                ( disambiguateDicts )
-import Errors          ( reduceErr, genCantGenErr, Error(..) )
-import Id              ( mkInstId )
-import Inst            ( extractTyVarsFromInst, isTyVarDict, matchesInst,
-                         instBindingRequired, instCanBeGeneralised,
-                         Inst(..),     -- We import the CONCRETE type, because
-                                       -- TcSimplify is allowed to see the rep
-                                       -- of Insts
-                         InstOrigin, OverloadedLit, InstTemplate
-                       )
-import InstEnv
-import LIE
-import ListSetOps      ( minusList )
-import Maybes          ( catMaybes, maybeToBool, Maybe(..) )
-import Util
-\end{code}
+Inference (top level definitions)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If the inst does not constrain a local type variable, then
+  [FreeIfTautological] try for tautology; 
+      if so, throw it out as free
+        (discarding result of tautology check)
+      if not, make original inst part of the context 
+        (eliminating superclasses as usual)
 
+If the inst constrains a local type variable, then
+   as for inference (local defns)
 
-%************************************************************************
-%*                                                                     *
-\subsection[tcSimplify-main]{Main entry function}
-%*                                                                     *
-%************************************************************************
 
-* May modify the substitution to bind ambiguous type variables.
+Checking (local defns)
+~~~~~~~~
+If the inst constrains a local type variable then 
+  [ReduceMe] reduce (signal error on failure)
 
-Specification
-~~~~~~~~~~~~~
-(1) If an inst constrains only ``global'' type variables, (or none),
-    return it as a ``global'' inst.
+If the inst does not constrain a local type variable then
+  [Free] throw it out as free.
 
-OTHERWISE
+Checking (top level)
+~~~~~~~~~~~~~~~~~~~~
+If the inst constrains a local type variable then
+   as for checking (local defns)
 
-(2) Simplify it repeatedly (checking for (1) of course) until it is a dict
-    constraining only a type variable.
+If the inst does not constrain a local type variable then
+   as for checking (local defns)
 
-(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.
 
 
-\begin{code}
-tcSimpl :: Bool                                -- True <=> Don't simplify const insts
-       -> [TyVar]                      -- ``Global'' type variables
-       -> [TyVar]                      -- ``Local''  type variables
-       -> [Inst]                       -- Given; these constrain only local tyvars
-       -> [Inst]                       -- Wanted
-       -> TcM ([Inst],                 -- Free
-               [(Inst,TypecheckedExpr)],-- Bindings
-               [Inst])                 -- Remaining wanteds; no dups
-
-tcSimpl dont_squash_consts global_tvs local_tvs givens wanteds
-  =
-        -- Make sure the insts and type variables are fixed points of the substitution
-    applyTcSubstAndExpectTyVars global_tvs `thenNF_Tc` \ global_tvs ->
-    applyTcSubstAndExpectTyVars local_tvs  `thenNF_Tc` \ local_tvs ->
-    applyTcSubstToInsts givens          `thenNF_Tc` \ givens ->
-    applyTcSubstToInsts wanteds                 `thenNF_Tc` \ wanteds ->
-    let
-       is_elem1 = isIn "tcSimpl1"
-       is_elem2 = isIn "tcSimpl2"
-    in
-       -- Deal with duplicates and type constructors
-    elimTyCons
-        dont_squash_consts (\tv -> tv `is_elem1` global_tvs)
-        givens wanteds         `thenTc` \ (globals, tycon_binds, locals_and_ambigs) ->
+Checking once per module
+~~~~~~~~~~~~~~~~~~~~~~~~~
+For dicts of the form (C a), where C is a std class
+  and "a" is a type variable,
+  [DontReduce] add to context
 
-       -- Now disambiguate if necessary
-    let
-       (ambigs, unambigs) = partition (is_ambiguous local_tvs) locals_and_ambigs
-       (locals, cant_generalise) = partition instCanBeGeneralised unambigs
-    in
-    checkTc (not (null cant_generalise)) (genCantGenErr cant_generalise)       `thenTc_`
+otherwise [ReduceMe] always reduce
 
-    (if (null ambigs) then
+[NB: we may generate one Tree [Int] dict per module, so 
+     sharing is not complete.]
 
-       -- No ambiguous dictionaries.  Just bash on with the results
-       -- of the elimTyCons
-       returnTc (globals, tycon_binds, locals_and_ambigs)
+Sort out ambiguity at the end.
 
-    else
+Principal types
+~~~~~~~~~~~~~~~
+class C a where
+  op :: a -> a
 
-       -- 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.
+f x = let g y = op (y::Int) in True
 
-       -- 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.
+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
 
-       disambiguateDicts ambigs        `thenTc_`
-       applyTcSubstToInsts givens      `thenNF_Tc` \ givens ->
-       applyTcSubstToInsts wanteds     `thenNF_Tc` \ wanteds ->
-       elimTyCons
-               dont_squash_consts (\tv -> tv `is_elem2` global_tvs)
-               givens wanteds
 
-    ) {- End of the "if" -} `thenTc` \ (globals, tycon_binds, locals) ->
+Ambiguity
+~~~~~~~~~
+Consider this:
 
-       -- Deal with superclass relationships
-    elimSCs givens locals              `thenNF_Tc` \ (sc_binds, locals2) ->
+       instance C (T a) Int  where ...
+       instance C (T a) Bool where ...
 
-        -- Finished
-    returnTc (globals, sc_binds ++ tycon_binds, locals2)
-  where
-    is_ambiguous local_tvs (Dict _ _ ty _)
-      = getTyVar "is_ambiguous" ty `not_elem` local_tvs
-      where
-       not_elem = isn'tIn "is_ambiguous"
+and suppose we infer a context
+
+           C (T x) y
+
+from some expression, where x and y are type varibles,
+and x is ambiguous, and y is being quantified over.
+Should we complain, or should we generate the type
+
+       forall x y. C (T x) y => <type not involving x>
+
+The idea is that at the call of the function we might
+know that y is Int (say), so the "x" isn't really ambiguous.
+Notice that we have to add "x" to the type variables over
+which we generalise.
+
+Something similar can happen even if C constrains only ambiguous
+variables.  Suppose we infer the context 
+
+       C [x]
+
+where x is ambiguous.  Then we could infer the type
+
+       forall x. C [x] => <type not involving x>
+
+in the hope that at the call site there was an instance
+decl such as
+
+       instance Num a => C [a] where ...
+
+and hence the default mechanism would resolve the "a".
+
+
+\begin{code}
+module TcSimplify (
+       tcSimplify, tcSimplifyAndCheck,
+       tcSimplifyTop, tcSimplifyThetas, tcSimplifyCheckThetas,
+       bindInstsOfLocalFuns
+    ) where
+
+#include "HsVersions.h"
+
+import HsSyn           ( MonoBinds(..), HsExpr(..), andMonoBinds )
+import TcHsSyn         ( TcExpr, TcIdOcc(..), TcIdBndr, 
+                         TcMonoBinds, TcDictBinds
+                       )
+
+import TcMonad
+import Inst            ( lookupInst, lookupSimpleInst, LookupInstResult(..),
+                         tyVarsOfInst, 
+                         isDict, isStdClassTyVarDict, isMethodFor,
+                         instToId, instBindingRequired, instCanBeGeneralised,
+                         newDictFromOld,
+                         instLoc, getDictClassTys,
+                         pprInst, zonkInst,
+                         Inst, LIE, pprInsts, pprInstsInFull, mkLIE, 
+                         InstOrigin, pprOrigin
+                       )
+import TcEnv           ( TcIdOcc(..), tcGetGlobalTyVars )
+import TcType          ( TcType, TcTyVarSet, TcMaybe, tcInstType, tcInstTheta )
+import Unify           ( unifyTauTy )
+import Id              ( mkIdSet )
+
+import Bag             ( Bag, bagToList, snocBag )
+import Class           ( Class, ClassInstEnv, classBigSig, classInstEnv )
+import PrelInfo                ( isNumericClass, isCreturnableClass )
+
+import Maybes          ( maybeToBool )
+import Type            ( Type, ThetaType, TauType, mkTyVarTy, getTyVar,
+                         isTyVarTy, instantiateThetaTy
+                       )
+import PprType         ( pprConstraint )
+import TysWiredIn      ( unitTy )
+import TyVar           ( intersectTyVarSets, unionManyTyVarSets, minusTyVarSet,
+                         isEmptyTyVarSet, tyVarSetToList, unionTyVarSets,
+                         zipTyVarEnv, emptyTyVarEnv
+                       )
+import FiniteMap
+import BasicTypes      ( TopLevelFlag(..) )
+import Unique          ( Unique )
+import Outputable
+import Util
+import List            ( partition )
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+\subsection[tcSimplify-main]{Main entry function}
+%*                                                                     *
+%************************************************************************
+
 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
@@ -149,400 +182,587 @@ float them out if poss, after inlinings are sorted out.
 
 \begin{code}
 tcSimplify
-       :: Bool                         -- True <=> top level
-       -> [TyVar]                      -- ``Global'' type variables
-       -> [TyVar]                      -- ``Local''  type variables
-       -> [Inst]                       -- Wanted
-       -> TcM ([Inst],                 -- Free
-               [(Inst, TypecheckedExpr)],-- Bindings
-               [Inst])                 -- Remaining wanteds; no dups
-
-tcSimplify top_level global_tvs local_tvs wanteds
-  = tcSimpl (not top_level) global_tvs local_tvs [] wanteds
+       :: SDoc 
+       -> TopLevelFlag
+       -> TcTyVarSet s                 -- ``Local''  type variables
+                                       -- ASSERT: this tyvar set is already zonked
+       -> LIE s                        -- Wanted
+       -> TcM s (LIE s,                        -- Free
+                 TcDictBinds s,                -- Bindings
+                 LIE s)                        -- Remaining wanteds; no dups
+
+tcSimplify str top_lvl local_tvs wanted_lie
+  = reduceContext str try_me [] wanteds                `thenTc` \ (binds, frees, irreds) ->
+
+       -- Check for non-generalisable insts
+    let
+       cant_generalise = filter (not . instCanBeGeneralised) irreds
+    in
+    checkTc (null cant_generalise)
+           (genCantGenErr cant_generalise)     `thenTc_`
+
+       -- Check for ambiguous insts.
+       -- You might think these can't happen (I did) because an ambiguous
+       -- inst like (Eq a) will get tossed out with "frees", and eventually
+       -- dealt with by tcSimplifyTop.
+       -- But we can get stuck with 
+       --      C a b
+       -- where "a" is one of the local_tvs, but "b" is unconstrained.
+       -- Then we must yell about the ambiguous b.
+       -- But we must only do so if "b" really is unconstrained; so
+       -- we must grab the global tyvars to answer that question
+    tcGetGlobalTyVars                          `thenNF_Tc` \ global_tvs ->
+    let
+       avail_tvs           = local_tvs `unionTyVarSets` global_tvs
+       (irreds', bad_guys) = partition (isEmptyTyVarSet . ambig_tv_fn) irreds
+       ambig_tv_fn dict    = tyVarsOfInst dict `minusTyVarSet` avail_tvs
+    in
+    addAmbigErrs ambig_tv_fn bad_guys  `thenNF_Tc_`
+
+
+       -- Finished
+    returnTc (mkLIE frees, binds, mkLIE irreds')
+  where
+    wanteds = bagToList wanted_lie
+
+    try_me inst 
+      -- Does not constrain a local tyvar
+      | isEmptyTyVarSet (tyVarsOfInst inst `intersectTyVarSets` local_tvs)
+      = -- if is_top_level then
+       --   FreeIfTautological           -- Special case for inference on 
+       --                                -- top-level defns
+       -- else
+       Free
+
+      -- We're infering (not checking) the type, and 
+      -- the inst constrains a local type variable
+      | isDict inst  = DontReduce              -- Dicts
+      | otherwise    = ReduceMe AddToIrreds    -- Lits and Methods
 \end{code}
 
 @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.
+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.
 
 \begin{code}
 tcSimplifyAndCheck
-        :: Bool                                -- True <=> top level
-        -> [TyVar]                             -- ``Global''  type variables
-        -> [TyVar]                             -- ``Local''  type variables
-        -> [Inst]                              -- Given
-        -> [Inst]                              -- Wanted
-        -> UnifyErrContext                     -- Context info for error 
-        -> TcM ([Inst],                        -- Free
-                [(Inst, TypecheckedExpr)])     -- Bindings
-
-tcSimplifyAndCheck top_level global_tvs local_tvs givens wanteds err_ctxt
-  = tcSimpl (not top_level) global_tvs local_tvs givens wanteds
-                       `thenTc` \ (free_insts, binds, wanteds') ->
-    checkTc (not (null wanteds')) (reduceErr wanteds' err_ctxt)
-                       `thenTc_`
-    returnTc (free_insts, binds)
-\end{code}
+        :: SDoc 
+        -> TcTyVarSet s                -- ``Local''  type variables
+                                       -- ASSERT: this tyvar set is already zonked
+        -> LIE s                       -- Given; constrain only local tyvars
+        -> LIE s                       -- Wanted
+        -> TcM s (LIE s,               -- Free
+                  TcDictBinds s)       -- Bindings
+
+tcSimplifyAndCheck str local_tvs given_lie wanted_lie
+  = reduceContext str try_me givens wanteds    `thenTc` \ (binds, frees, irreds) ->
+
+       -- Complain about any irreducible ones
+    mapNF_Tc complain irreds   `thenNF_Tc_`
+
+       -- Done
+    returnTc (mkLIE frees, binds)
+  where
+    givens  = bagToList given_lie
+    wanteds = bagToList wanted_lie
 
-@tcSimplifyRank2@ checks that the argument of a rank-2 polymorphic function
-is not overloaded.  
+    try_me inst 
+      -- Does not constrain a local tyvar
+      | isEmptyTyVarSet (tyVarsOfInst inst `intersectTyVarSets` local_tvs)
+      = Free
 
-\begin{code}
-tcSimplifyRank2 :: [TyVar]             -- ``Local'' type variables; guaranteed fixpoint of subst
-               -> [Inst]               -- Given
-               -> UnifyErrContext
-               -> TcM ([Inst],                         -- Free
-                       [(Inst, TypecheckedExpr)])      -- Bindings
-
-tcSimplifyRank2 local_tvs givens err_ctxt
-  = applyTcSubstToInsts givens          `thenNF_Tc` \ givens' ->
-    elimTyCons False 
-              (\tv -> not (tv `is_elem` local_tvs))
-               -- This predicate claims that all
-               -- any non-local tyvars are global,
-               -- thereby postponing dealing with
-               -- ambiguity until the enclosing Gen
-              [] givens'       `thenTc` \ (free, dict_binds, wanteds) ->
-
-    checkTc (not (null wanteds)) (reduceErr wanteds err_ctxt)  `thenTc_`
-
-    returnTc (free, dict_binds)
-  where
-    is_elem = isIn "tcSimplifyRank2"
+      -- When checking against a given signature we always reduce
+      -- until we find a match against something given, or can't reduce
+      | otherwise
+      = ReduceMe AddToIrreds
+
+    complain dict = mapNF_Tc zonkInst givens   `thenNF_Tc` \ givens ->
+                   addNoInstanceErr str givens dict
 \end{code}
 
-@tcSimplifyTop@ deals with constant @Insts@, using the standard simplification
-mechansim with the extra flag to say ``beat out constant insts''.
 
-\begin{code}
-tcSimplifyTop :: [Inst] -> TcM [(Inst, TypecheckedExpr)]
-tcSimplifyTop dicts
-  = tcSimpl False [] [] [] dicts    `thenTc` \ (_, binds, _) ->
-    returnTc binds
-\end{code}
+%************************************************************************
+%*                                                                     *
+\subsection{Data types for the reduction mechanism}
+%*                                                                     *
+%************************************************************************
 
-@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 main control over context reduction is here
 
 \begin{code}
-tcSimplifyThetas :: (Class -> TauType -> InstOrigin)  -- Creates an origin for the dummy dicts
-                -> [(Class, TauType)]                -- Simplify this
-                -> TcM [(Class, TauType)]            -- Result
+data WhatToDo 
+ = ReduceMe              -- Try to reduce this
+       NoInstanceAction  -- What to do if there's no such instance
 
-tcSimplifyThetas mk_inst_origin theta
-  = let
-       dicts = map mk_dummy_dict theta
-    in
-        -- Do the business (this is just the heart of "tcSimpl")
-    elimTyCons False (\tv -> False) [] dicts    `thenTc`       \ (_, _, dicts2) ->
+ | DontReduce            -- Return as irreducible
 
-         -- Deal with superclass relationships
-    elimSCs [] dicts2              `thenNF_Tc` \ (_, dicts3) ->
+ | Free                          -- Return as free
 
-    returnTc (map unmk_dummy_dict dicts3)
-  where
-    mk_dummy_dict (clas, ty)
-      = Dict uniq clas ty (mk_inst_origin clas ty)
+ | FreeIfTautological    -- Return as free iff it's tautological; 
+                         -- if not, return as irreducible
 
-    uniq = panic "tcSimplifyThetas:uniq"
+data NoInstanceAction
+  = Stop               -- Fail; no error message
+                       -- (Only used when tautology checking.)
 
-    unmk_dummy_dict (Dict _ clas ty _) = (clas, ty)
+  | 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}
 
-@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
-used with \tr{default} declarations.  We are only interested in
-whether it worked or not.
-
-\begin{code}
-tcSimplifyCheckThetas :: InstOrigin            -- context; for error msg
-               -> [(Class, TauType)]   -- Simplify this
-               -> TcM ()
 
-tcSimplifyCheckThetas origin theta
-  = let
-       dicts = map mk_dummy_dict theta
-    in
-        -- Do the business (this is just the heart of "tcSimpl")
-    elimTyCons False (\tv -> False) [] dicts    `thenTc`       \ _ ->
 
-    returnTc ()
+\begin{code}
+type RedState s
+  = (Avails s,         -- What's available
+     [Inst s],         -- Insts for which try_me returned Free
+     [Inst s]          -- Insts for which try_me returned DontReduce
+    )
+
+type Avails s = FiniteMap (Inst s) (Avail s)
+
+data Avail s
+  = Avail
+       (TcIdOcc s)     -- The "main Id"; that is, the Id for the Inst that 
+                       -- caused this avail to be put into the finite map in the first place
+                       -- It is this Id that is bound to the RHS.
+
+       (RHS s)         -- The RHS: an expression whose value is that Inst.
+                       -- The main Id should be bound to this RHS
+
+       [TcIdOcc s]     -- Extra Ids that must all be bound to the main Id.
+                       -- At the end we generate a list of bindings
+                       --       { i1 = main_id; i2 = main_id; i3 = main_id; ... }
+
+data RHS s
+  = NoRhs              -- Used for irreducible dictionaries,
+                       -- which are going to be lambda bound, or for those that are
+                       -- suppplied as "given" when checking againgst a signature.
+                       --
+                       -- NoRhs is also used for Insts like (CCallable f)
+                       -- where no witness is required.
+
+  | Rhs                -- Used when there is a RHS 
+       (TcExpr s)       
+       Bool            -- True => the RHS simply selects a superclass dictionary
+                       --         from a subclass dictionary.
+                       -- False => not so.  
+                       -- This is useful info, because superclass selection
+                       -- is cheaper than building the dictionary using its dfun,
+                       -- and we can sometimes replace the latter with the former
+
+  | PassiveScSel       -- Used for as-yet-unactivated RHSs.  For example suppose we have
+                       -- an (Ord t) dictionary; then we put an (Eq t) entry in
+                       -- the finite map, with an PassiveScSel.  Then if the
+                       -- the (Eq t) binding is ever *needed* we make it an Rhs
+       (TcExpr s)
+       [Inst s]        -- List of Insts that are free in the RHS.
+                       -- If the main Id is subsequently needed, we toss this list into
+                       -- the needed-inst pool so that we make sure their bindings
+                       -- will actually be produced.
+                       --
+                       -- Invariant: these Insts are already in the finite mapping
+
+
+pprAvails avails = vcat (map pp (eltsFM avails))
   where
-    mk_dummy_dict (clas, ty)
-      = Dict uniq clas ty origin
+    pp (Avail main_id rhs ids)
+      = ppr main_id <> colon <+> brackets (ppr ids) <+> pprRhs rhs
 
-    uniq = panic "tcSimplifyCheckThetas:uniq"
+pprRhs NoRhs = text "<no rhs>"
+pprRhs (Rhs rhs b) = ppr rhs
+pprRhs (PassiveScSel rhs is) = text "passive" <+> ppr rhs
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection[elimTyCons]{@elimTyCons@}
+\subsection[reduce]{@reduce@}
 %*                                                                     *
 %************************************************************************
 
+The main entry point for context reduction is @reduceContext@:
+
 \begin{code}
-elimTyCons :: Bool                             -- True <=> Don't simplify const insts
-          -> (TyVar -> Bool)                   -- Free tyvar predicate
-          -> [Inst]                            -- Given
-          -> [Inst]                            -- Wanted
-          -> TcM ([Inst],                      -- Free
-                  [(Inst, TypecheckedExpr)],   -- Bindings
-                  [Inst]                       -- Remaining wanteds; no dups;
-                                               -- dicts only (no Methods)
-              )
+reduceContext :: SDoc -> (Inst s -> WhatToDo)
+             -> [Inst s]       -- Given
+             -> [Inst s]       -- Wanted
+             -> TcM s (TcDictBinds s, 
+                       [Inst s],               -- Free
+                       [Inst s])               -- Irreducible
+
+reduceContext str try_me givens wanteds
+  =     -- Zonking first
+    mapNF_Tc zonkInst givens   `thenNF_Tc` \ givens ->
+    mapNF_Tc zonkInst wanteds  `thenNF_Tc` \ wanteds ->
+
+{-
+    pprTrace "reduceContext" (vcat [
+            text "----------------------",
+            str,
+            text "given" <+> ppr givens,
+            text "wanted" <+> ppr wanteds,
+            text "----------------------"
+            ]) $
+-}
+        -- Build the Avail mapping from "givens"
+    foldlNF_Tc addGiven emptyFM givens         `thenNF_Tc` \ avails ->
+
+        -- Do the real work
+    reduce try_me wanteds (avails, [], [])     `thenTc` \ (avails, frees, irreds) ->
+
+       -- Extract the bindings from avails
+    let
+       binds = foldFM add_bind EmptyMonoBinds avails
+
+       add_bind _ (Avail main_id rhs ids) binds
+         = foldr add_synonym (add_rhs_bind rhs binds) ids
+        where
+          add_rhs_bind (Rhs rhs _) binds = binds `AndMonoBinds` VarMonoBind main_id rhs 
+          add_rhs_bind other       binds = binds
+
+          -- Add the trivial {x = y} bindings
+          -- The main Id can end up in the list when it's first added passively
+          -- and then activated, so we have to filter it out.  A bit of a hack.
+          add_synonym id binds
+            | id /= main_id = binds `AndMonoBinds` VarMonoBind id (HsVar main_id)
+            | otherwise     = binds
+    in
+{-
+    pprTrace ("reduceContext1") (vcat [
+            text "----------------------",
+            str,
+            text "given" <+> ppr givens,
+            text "wanted" <+> ppr wanteds,
+            text "----", 
+            text "avails" <+> pprAvails avails,
+            text "free" <+> ppr frees,         
+            text "irreds" <+> ppr irreds,              
+            text "----------------------"
+            ]) $
+-}
+    returnTc (binds, frees, irreds)
 \end{code}
 
-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.
+The main context-reduction function is @reduce@.  Here's its game plan.
 
-When we do @eTC givens (wanted:wanteds)@ [some details omitted], we...
-
-    (1) first look up @wanted@; this gives us one binding to heave in:
-           wanted = rhs
+\begin{code}
+reduce :: (Inst s -> WhatToDo)
+       -> [Inst s]
+       -> RedState s
+       -> TcM s (RedState s)
+\end{code}
 
-    (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!
+@reduce@ is passed
+     try_me:   given an inst, this function returns
+                 Reduce       reduce this
+                 DontReduce   return this in "irreds"
+                 Free         return this in "frees"
 
-    (3) we simplify the remaining @wanteds@ (recursive call), giving
-       us yet more bindings.
+     wanteds:  The list of insts to reduce
+     state:    An accumulating parameter of type RedState 
+               that contains the state of the algorithm
 
-The final arrangement of the {\em non-recursive} bindings is
+  It returns a RedState.
 
-    let <simpler-wanted-binds> in
-    let wanted = rhs          in
-    let <yet-more-bindings> ...
 
 \begin{code}
-elimTyCons dont_squash_consts is_free_tv givens wanteds
-  = eTC givens wanteds
+    -- Base case: we're done!
+reduce try_me [] state = returnTc state
+
+reduce try_me (wanted:wanteds) state@(avails, frees, irreds)
+
+    -- It's the same as an existing inst, or a superclass thereof
+  | wanted `elemFM` avails
+  = reduce try_me wanteds (activate avails wanted, frees, irreds)
+
+    -- It should be reduced
+  | case try_me_result of { ReduceMe _ -> True; _ -> False }
+  = lookupInst wanted        `thenNF_Tc` \ lookup_result ->
+
+    case lookup_result of
+      GenInst wanteds' rhs -> use_instance wanteds' rhs
+      SimpleInst rhs       -> use_instance []       rhs
+
+      NoInstance ->    -- No such instance! 
+                      -- Decide what to do based on the no_instance_action requested
+                case no_instance_action of
+                  Stop        -> failTc        -- Fail
+                  AddToIrreds -> add_to_irreds -- Add the offending insts to the irreds
+
+    -- It's free and this isn't a top-level binding, so just chuck it upstairs
+  | case try_me_result of { Free -> True; _ -> False }
+  =     -- First, see if the inst can be reduced to a constant in one step
+    lookupInst wanted    `thenNF_Tc` \ lookup_result ->
+    case lookup_result of
+       SimpleInst rhs -> use_instance [] rhs
+       other         -> add_to_frees
+
+    -- It's free and this is a top level binding, so
+    -- check whether it's a tautology or not
+  | case try_me_result of { FreeIfTautological -> True; _ -> False }
+  =     -- Try for tautology
+    tryTc 
+         -- If tautology trial fails, add to irreds
+         (addGiven avails wanted      `thenNF_Tc` \ avails' ->
+          returnTc (avails', frees, wanted:irreds))
+
+         -- If tautology succeeds, just add to frees
+         (reduce try_me_taut [wanted] (avails, [], [])         `thenTc_`
+          returnTc (avails, wanted:frees, irreds))
+                                                               `thenTc` \ state' ->
+    reduce try_me wanteds state'
+
+
+    -- It's irreducible (or at least should not be reduced)
+  | otherwise
+  = ASSERT( case try_me_result of { DontReduce -> True; other -> False } )
+        -- See if the inst can be reduced to a constant in one step
+    lookupInst wanted    `thenNF_Tc` \ lookup_result ->
+    case lookup_result of
+       SimpleInst rhs -> use_instance [] rhs
+       other          -> add_to_irreds
+
   where
-    eTC :: [Inst] -> [Inst]
-       -> TcM ([Inst], [(Inst, TypecheckedExpr)], [Inst])
-
-    eTC _ [] = returnTc ([], [], [])
-
-    eTC givens (wanted:wanteds) = try givens wanted wanteds
-                                     (extractTyVarsFromInst wanted)
-                                     (find_equiv givens wanted)
-       -- find_equiv looks in "givens" for an inst equivalent to "wanted"
-       -- This is used only in Case 2 below; it's like a guard which also
-       -- returns a result.
-
-    try :: [Inst] -> Inst -> [Inst] -> [TyVar] -> (Maybe Inst)
-       -> TcM ([Inst], [(Inst, TypecheckedExpr)], [Inst])
-
-    -- Case 0: same as existing dict, so build a simple binding
-    try givens wanted wanteds tvs_of_wanted (Just this)
-     = eTC givens wanteds      `thenTc` \ (frees, binds, wanteds') ->
-       let 
-         -- Create a new binding iff it's needed
-         new_binds | instBindingRequired wanted = (wanted, Var (mkInstId this)):binds
-                   | otherwise                  = binds
-       in
-       returnTc (frees, new_binds, wanteds')
-
-    -- 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
-    try givens wanted wanteds tvs_of_wanted _ | null tvs_of_wanted
-      = simplify_it dont_squash_consts {- If dont_squash_consts is true,
-                                         simplify only if trival -}
-                   givens wanted wanteds
-
-    -- Case 2: constrains free vars only, so fling it out the top in free_ids
-    try givens wanted wanteds tvs_of_wanted _
-      | all is_free_tv tvs_of_wanted
-      = eTC (wanted:givens) wanteds    `thenTc` \ (frees, binds, wanteds') ->
-       returnTc (wanted:frees, binds, wanteds')
-
-    -- Case 3: is a dict constraining only a tyvar,
-    -- so return it as part of the "wanteds" result
-    try givens wanted wanteds tvs_of_wanted _
-      | isTyVarDict wanted
-      = eTC (wanted:givens) wanteds    `thenTc` \ (frees, binds, wanteds') ->
-       returnTc (frees, binds, wanted:wanteds')
-
-    -- Case 4: is not a simple dict, so look up in instance environment
-    try givens wanted wanteds tvs_of_wanted _
-      = simplify_it False {- Simplify even if not trivial -}
-                   givens wanted wanteds
-
-    simplify_it only_if_trivial givens wanted wanteds
-      = if not (instBindingRequired wanted) then
-               -- No binding required for this chap, so squash right away
-          lookupNoBindInst_Tc wanted   `thenTc` \ simpler_wanteds ->
-
-          eTC givens simpler_wanteds   `thenTc` \ (frees1, binds1, wanteds1) ->
-          let
-              new_givens = [new_given | (new_given,rhs) <- binds1]
-               -- Typically binds1 is empty
-          in
-          eTC givens wanteds           `thenTc` \ (frees2, binds2, wanteds2) ->
-
-          returnTc (frees1 ++ frees2,
-                    binds1 ++ binds2,
-                    wanteds1 ++ wanteds2)
-
-       else    -- An binding is required for this inst
-       lookupInst_Tc wanted    `thenTc` \ (rhs, simpler_wanteds) ->
-
-        if (only_if_trivial && not_var rhs) then
-          -- Ho ho!  It isn't trivial to simplify "wanted",
-          -- because the rhs isn't a simple variable.  The flag
-          -- dont_squash_consts tells us to give up now and
-          -- just fling it out the top.
-          eTC (wanted:givens) wanteds  `thenTc` \ (frees, binds, wanteds') ->
-          returnTc (wanted:frees, binds, wanteds')
-       else
-          -- Aha! Either it's easy, or dont_squash_consts is
-          -- False, so we must do it right here.
-
-          eTC givens simpler_wanteds   `thenTc` \ (frees1, binds1, wanteds1) ->
-          let
-              new_givens = [new_given | (new_given,rhs) <- binds1]
-          in
-          eTC (new_givens ++ [wanted] ++ wanteds1 ++ givens) wanteds
-                                  `thenTc` \ (frees2, binds2, wanteds2) ->
-          returnTc (frees1 ++ frees2,
-                    binds1 ++ [(wanted, rhs)] ++ binds2,
-                    wanteds1 ++ wanteds2)
-      where
-       not_var :: TypecheckedExpr -> Bool
-       not_var (Var _) = False
-       not_var other   = True
-
-    find_equiv :: [Inst] -> Inst -> Maybe Inst
-       -- Look through the argument list for an inst which is
-       -- equivalent to the second arg.
-
-    find_equiv []            wanted = Nothing
-    find_equiv (given:givens) wanted
-      | wanted `matchesInst` given = Just given
-      | otherwise                 = find_equiv givens wanted
+       -- The three main actions
+    add_to_frees  = reduce try_me wanteds (avails, wanted:frees, irreds)
+
+    add_to_irreds = addGiven avails wanted             `thenNF_Tc` \ avails' ->
+                   reduce try_me wanteds (avails',  frees, wanted:irreds)
+
+    use_instance wanteds' rhs = addWanted avails wanted rhs    `thenNF_Tc` \ avails' ->
+                               reduce try_me (wanteds' ++ wanteds) (avails', frees, irreds)
+
+
+    try_me_result              = try_me wanted
+    ReduceMe no_instance_action = try_me_result
+
+    -- The try-me to use when trying to identify tautologies
+    -- It blunders on reducing as much as possible
+    try_me_taut inst = ReduceMe Stop   -- No error recovery
 \end{code}
 
 
+\begin{code}
+activate :: Avails s -> Inst s -> Avails s
+        -- Activate the binding for Inst, ensuring that a binding for the
+        -- wanted Inst will be generated.
+        -- (Activate its parent if necessary, recursively).
+        -- Precondition: the Inst is in Avails already
+
+activate avails wanted
+  | not (instBindingRequired wanted) 
+  = avails
+
+  | otherwise
+  = case lookupFM avails wanted of
+
+      Just (Avail main_id (PassiveScSel rhs insts) ids) ->
+              foldl activate avails' insts      -- Activate anything it needs
+            where
+              avails' = addToFM avails wanted avail'
+              avail'  = Avail main_id (Rhs rhs True) (wanted_id : ids) -- Activate it
+
+      Just (Avail main_id other_rhs ids) -> -- Just add to the synonyms list
+              addToFM avails wanted (Avail main_id other_rhs (wanted_id : ids))
+
+      Nothing -> panic "activate"
+  where
+      wanted_id = instToId wanted
+    
+addWanted avails wanted rhs_expr
+  = ASSERT( not (wanted `elemFM` avails) )
+    returnNF_Tc (addToFM avails wanted avail)
+       -- NB: we don't add the thing's superclasses too!
+       -- Why not?  Because addWanted is used when we've successfully used an
+       -- instance decl to reduce something; e.g.
+       --      d:Ord [a] = dfunOrd (d1:Eq [a]) (d2:Ord a)
+       -- Note that we pass the superclasses to the dfun, so they will be "wanted".
+       -- If we put the superclasses of "d" in avails, then we might end up
+       -- expressing "d1" in terms of "d", which would be a disaster.
+  where
+    avail = Avail (instToId wanted) rhs []
+
+    rhs | instBindingRequired wanted = Rhs rhs_expr False      -- Not superclass selection
+       | otherwise                  = NoRhs
+
+addGiven :: Avails s -> Inst s -> NF_TcM s (Avails s)
+addGiven avails given
+  =     -- ASSERT( not (given `elemFM` avails) )
+        -- This assertion isn' necessarily true.  It's permitted
+        -- to given a redundant context in a type signature (eg (Ord a, Eq a) => ...)
+        -- and when typechecking instance decls we generate redundant "givens" too.
+    addAvail avails given avail
+  where
+    avail = Avail (instToId given) NoRhs []
+
+addAvail avails wanted avail
+  = addSuperClasses (addToFM avails wanted avail) wanted
+
+addSuperClasses :: Avails s -> Inst s -> NF_TcM s (Avails s)
+               -- Add all the superclasses of the Inst to Avails
+               -- Invariant: the Inst is already in Avails.
+
+addSuperClasses avails dict
+  | not (isDict dict)
+  = returnNF_Tc avails
+
+  | otherwise  -- It is a dictionary
+  = tcInstTheta env sc_theta           `thenNF_Tc` \ sc_theta' ->
+    foldlNF_Tc add_sc avails (zipEqual "addSuperClasses" sc_theta' sc_sels)
+  where
+    (clas, tys) = getDictClassTys dict
+    
+    (tyvars, sc_theta, sc_sels, _, _) = classBigSig clas
+    env       = zipTyVarEnv tyvars tys
+
+    add_sc avails ((super_clas, super_tys), sc_sel)
+      = newDictFromOld dict super_clas super_tys       `thenNF_Tc` \ super_dict ->
+        let
+          sc_sel_rhs = DictApp (TyApp (HsVar (RealId sc_sel)) 
+                                      tys)
+                               [instToId dict]
+       in
+        case lookupFM avails super_dict of
+
+            Just (Avail main_id (Rhs rhs False {- not sc selection -}) ids) ->
+                 -- Already there, but not as a superclass selector
+                 -- No need to look at its superclasses; since it's there
+                 --    already they must be already in avails
+                 -- However, we must remember to activate the dictionary
+                 -- from which it is (now) generated
+                 returnNF_Tc (activate avails' dict)
+               where
+                 avails' = addToFM avails super_dict avail
+                 avail   = Avail main_id (Rhs sc_sel_rhs True) ids     -- Superclass selection
+       
+            Just (Avail _ _ _) -> returnNF_Tc avails
+                 -- Already there; no need to do anything
+
+            Nothing ->
+                 -- Not there at all, so add it, and its superclasses
+                 addAvail avails super_dict avail
+               where
+                 avail   = Avail (instToId super_dict) 
+                                 (PassiveScSel sc_sel_rhs [dict])
+                                 []
+\end{code}
+
 %************************************************************************
 %*                                                                     *
-\subsection[elimSCs]{@elimSCs@}
+\subsection[simple]{@Simple@ versions}
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-elimSCs :: [Inst]                              -- Given; no dups
-       -> [Inst]                               -- Wanted; no dups; all dictionaries, all
-                                               -- constraining just a type variable
-       -> NF_TcM ([(Inst,TypecheckedExpr)],    -- Bindings
-                  [Inst])                      -- Minimal wanted set
-
-elimSCs givens wanteds
-  = -- Sort the wanteds so that subclasses occur before superclasses
-    elimSCs_help
-       [dict | dict@(Dict _ _ _ _) <- givens]  -- Filter out non-dictionaries
-       (sortSC wanteds)
+Much simpler versions when there are no bindings to make!
 
-elimSCs_help :: [Inst]                         -- Given; no dups
-            -> [Inst]                          -- Wanted; no dups;
-            -> NF_TcM ([(Inst,TypecheckedExpr)],-- Bindings
-                       [Inst])                 -- Minimal wanted set
+@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.
 
-elimSCs_help given [] = returnNF_Tc ([], [])
+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.
 
-elimSCs_help givens (wanted@(Dict _ wanted_class wanted_ty wanted_orig):wanteds)
-  = case (trySC givens wanted_class wanted_ty) of
+\begin{code}
+tcSimplifyThetas :: (Class -> ClassInstEnv)            -- How to find the ClassInstEnv
+                -> ThetaType                           -- Wanted
+                -> TcM s ThetaType                     -- Needed; of the form C a b c
+                                                       -- where a,b,c are type variables
 
-      Nothing -> -- No superclass relnship found
-                elimSCs_help (wanted:givens) wanteds `thenNF_Tc` \ (binds, wanteds') ->
-                returnNF_Tc (binds, wanted:wanteds')
+tcSimplifyThetas inst_mapper wanteds
+  = reduceSimple inst_mapper [] wanteds                `thenNF_Tc` \ irreds ->
+    let
+       -- Check that the returned dictionaries are of the form (C a b c)
+       bad_guys = [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}
 
-      Just (given, classes) -> -- Aha! There's a superclass relnship
+@tcSimplifyCheckThetas@ just checks class-type constraints, essentially;
+used with \tr{default} declarations.  We are only interested in
+whether it worked or not.
 
-       -- Build intermediate dictionaries
-       let
-           theta = [ (clas, wanted_ty) | clas <- classes ]
-       in
-       newDicts wanted_orig theta              `thenNF_Tc` \ intermediates ->
+\begin{code}
+tcSimplifyCheckThetas :: ThetaType     -- Given
+                     -> ThetaType      -- Wanted
+                     -> TcM s ()
+
+tcSimplifyCheckThetas givens wanteds
+  = reduceSimple classInstEnv givens wanteds    `thenNF_Tc`    \ irreds ->
+    if null irreds then
+       returnTc ()
+    else
+       mapNF_Tc addNoInstErr irreds            `thenNF_Tc_`
+       failTc
+\end{code}
 
-       -- Deal with the recursive call
-       elimSCs_help (wanted : (intermediates ++ givens)) wanteds
-                                               `thenNF_Tc` \ (binds, wanteds') ->
 
-       -- 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
-       let
-           new_binds = mk_binds wanted wanted_class (intermediates ++ [given]) []
-       in
-       returnNF_Tc (new_binds ++ binds, wanteds')
-  where
-    mk_binds :: Inst                           -- Define this
-            -> Class                           -- ...whose class is this
-            -> [Inst]                          -- In terms of this sub-class chain
-            -> [(Inst, TypecheckedExpr)]       -- Push the binding on front of these
-            -> [(Inst, TypecheckedExpr)]
-
-    mk_binds dict clas [] binds_so_far = binds_so_far
-    mk_binds dict clas (dict_sub@(Dict _ dict_sub_class ty _):dicts_sub) binds_so_far
-      = mk_binds dict_sub dict_sub_class dicts_sub (new_bind:binds_so_far)
-      where
-       new_bind = (dict, DictApp (TyApp (Var (getSuperDictSelId dict_sub_class clas))
-                                        [ty])
-                                 [mkInstId dict_sub])
-
-
-trySC :: [Inst]                                -- Givens
-      -> Class -> UniType              -- Wanted
-      -> Maybe (Inst, [Class])         -- Nothing if no link; Just (given, classes)
-                                       -- if wanted can be given in terms of given, with
-                                       -- intermediate classes specified
-trySC givens wanted_class wanted_ty
-  = case subclass_relns of
-        [] -> Nothing
-        ((given, classes, _): _) -> Just (given, classes)
+\begin{code}
+type AvailsSimple = FiniteMap (Class, [TauType]) Bool
+                   -- True  => irreducible 
+                   -- False => given, or can be derived from a given or from an irreducible
+
+reduceSimple :: (Class -> ClassInstEnv) 
+            -> ThetaType               -- Given
+            -> ThetaType               -- Wanted
+            -> NF_TcM s ThetaType      -- Irreducible
+
+reduceSimple inst_mapper givens wanteds
+  = reduce_simple inst_mapper givens_fm wanteds        `thenNF_Tc` \ givens_fm' ->
+    returnNF_Tc [ct | (ct,True) <- fmToList givens_fm']
   where
-    subclass_relns :: [(Inst, [Class], Int)]   -- Subclass of wanted,
-                                                -- intervening classes,
-                                                -- and number of intervening classes
-                                                -- Sorted with shortest link first
-    subclass_relns = sortLt reln_lt (catMaybes (map find_subclass_reln givens))
+    givens_fm     = foldl addNonIrred emptyFM givens
 
-    reln_lt :: (Inst, [Class], Int) -> (Inst, [Class], Int) -> Bool
-    (_,_,n1) `reln_lt` (_,_,n2) = n1 < n2
+reduce_simple :: (Class -> ClassInstEnv) 
+             -> AvailsSimple
+             -> ThetaType
+             -> NF_TcM s AvailsSimple
 
-    find_subclass_reln given@(Dict _ given_class given_ty _)
-        | wanted_ty == given_ty
-        = case (wanted_class `isSuperClassOf` given_class) of
+reduce_simple inst_mapper givens [] 
+  =         -- Finished, so pull out the needed ones
+    returnNF_Tc givens
 
-                Just classes -> Just (given,
-                                      classes,
-                                      length classes)
+reduce_simple inst_mapper givens (wanted@(clas,tys) : wanteds)
+  | wanted `elemFM` givens
+  = reduce_simple inst_mapper givens wanteds
 
-                Nothing      -> Nothing
+  | otherwise
+  = lookupSimpleInst (inst_mapper clas) clas tys       `thenNF_Tc` \ maybe_theta ->
 
-        | otherwise = Nothing
+    case maybe_theta of
+      Nothing ->    reduce_simple inst_mapper (addIrred    givens wanted) wanteds
+      Just theta -> reduce_simple inst_mapper (addNonIrred givens wanted) (theta ++ wanteds)
 
+addIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
+addIrred givens ct
+  = addSCs (addToFM givens ct True) ct
 
-sortSC :: [Inst]    -- Expected to be all dicts (no MethodIds), all of
-                   -- which constrain type variables
-       -> [Inst]    -- Sorted with subclasses before superclasses
+addNonIrred :: AvailsSimple -> (Class, [TauType]) -> AvailsSimple
+addNonIrred givens ct
+  = addSCs (addToFM givens ct False) ct
 
-sortSC dicts = sortLt lt dicts
-  where
-    (Dict _ c1 ty1 _) `lt` (Dict _ c2 ty2 _)
-       = tv1 `ltTyVar` tv2 ||
-       (tv1 `eqTyVar` tv2 && maybeToBool (c2 `isSuperClassOf` c1))
-       where
-       tv1 = getTyVar "sortSC" ty1
-       tv2 = getTyVar "sortSC" ty2
-\end{code}
+addSCs givens ct@(clas,tys)
+ = foldl add givens sc_theta
+ where
+   (tyvars, sc_theta_tmpl, _, _, _) = classBigSig clas
+   sc_theta = instantiateThetaTy (zipTyVarEnv tyvars tys) sc_theta_tmpl
+
+   add givens ct = 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}
 
 %************************************************************************
 %*                                                                     *
@@ -567,36 +787,229 @@ there, they would have unresolvable references to @f@.
 We pass in an @init_lie@ of @Insts@ and a list of locally-bound @Ids@.
 For each method @Inst@ in the @init_lie@ that mentions one of the
 @Ids@, we create a binding.  We return the remaining @Insts@ (in an
-@LIE@), as well as the @Binds@ generated.
+@LIE@), as well as the @HsBinds@ generated.
 
 \begin{code}
-bindInstsOfLocalFuns ::        LIE -> [Id] -> NF_TcM (LIE, TypecheckedMonoBinds)
+bindInstsOfLocalFuns ::        LIE s -> [TcIdBndr s] -> TcM s (LIE s, TcMonoBinds s)
 
 bindInstsOfLocalFuns init_lie local_ids
-  = let
-       insts = unMkLIE init_lie
+  = reduceContext (text "bindInsts" <+> ppr local_ids)
+                 try_me [] (bagToList init_lie)        `thenTc` \ (binds, frees, irreds) ->
+    ASSERT( null irreds )
+    returnTc (mkLIE frees, binds)
+  where
+    local_id_set = mkIdSet local_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 local_id_set inst = ReduceMe AddToIrreds
+               | otherwise                     = Free
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
+\section[Disambig]{Disambiguation of overloading}
+%*                                                                     *
+%************************************************************************
+
+
+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}
+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}
+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.
+
+So here is the function which does the work.  It takes the ambiguous
+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.
+
+
+@tcSimplifyTop@ is called once per module to simplify
+all the constant and ambiguous Insts.
+
+\begin{code}
+tcSimplifyTop :: LIE s -> TcM s (TcDictBinds s)
+tcSimplifyTop wanted_lie
+  = reduceContext (text "tcSimplTop") try_me [] wanteds        `thenTc` \ (binds1, frees, irreds) ->
+    ASSERT( null frees )
+
+    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:_) = isEmptyTyVarSet (tyVarsOfInst d `intersectTyVarSets` non_std_tyvars)
+       non_std_tyvars          = unionManyTyVarSets (map tyVarsOfInst non_stds)
+
+               -- Collect together all the bad guys
+       bad_guys = non_stds ++ concat std_bads
     in
-    bind_insts insts [] EmptyMonoBinds
+
+       -- Disambiguate the ones that look feasible
+    mapTc disambigGroup std_oks                `thenTc` \ binds_ambig ->
+
+       -- And complain about the ones that don't
+    mapNF_Tc complain bad_guys         `thenNF_Tc_`
+
+    returnTc (binds1 `AndMonoBinds` andMonoBinds binds_ambig)
   where
-    bind_insts :: [Inst]               -- Insts to mangle
-               -> [Inst]               -- accum. Insts to return
-               -> TypecheckedMonoBinds -- accum. Binds to return
-               -> NF_TcM (LIE, TypecheckedMonoBinds)
-
-    bind_insts [] acc_insts acc_binds
-      = returnNF_Tc (mkLIE acc_insts, acc_binds)
-
-    bind_insts (inst@(Method uniq id tys orig):insts) acc_insts acc_binds
-      | id `is_elem` local_ids
-      = noFailTc (lookupInst_Tc inst)  `thenNF_Tc` \ (expr, dict_insts) ->
-       let
-           bind =  VarMonoBind (mkInstId inst) expr
-       in
-       bind_insts insts (dict_insts ++ acc_insts) (bind `AndMonoBinds` acc_binds)
+    wanteds    = bagToList wanted_lie
+    try_me inst        = ReduceMe AddToIrreds
 
-    bind_insts (some_other_inst:insts) acc_insts acc_binds
-       -- Either not a method, or a method instance for an id not in local_ids
-      = bind_insts insts (some_other_inst:acc_insts) acc_binds
+    d1 `cmp_by_tyvar` d2 = get_tv d1 `compare` get_tv d2
+
+    complain d | isEmptyTyVarSet (tyVarsOfInst d) = addTopInstanceErr d
+              | otherwise                        = addAmbigErr tyVarsOfInst d
+
+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
+the same type variable.
+
+ADR Comment 20/6/94: I've changed the @CReturnable@ case to default to
+@()@ instead of @Int@.  I reckon this is the Right Thing to do since
+the most common use of defaulting is code like:
+\begin{verbatim}
+       _ccall_ foo     `seqPrimIO` bar
+\end{verbatim}
+Since we're not using the result of @foo@, the result if (presumably)
+@void@.
+
+\begin{code}
+disambigGroup :: [Inst s]      -- All standard classes of form (C a)
+             -> TcM s (TcDictBinds s)
+
+disambigGroup dicts
+  |  any isNumericClass classes        -- Guaranteed all standard classes
+  =    -- THE DICTS OBEY THE DEFAULTABLE CONSTRAINT
+       -- SO, TRY DEFAULT TYPES IN ORDER
+
+       -- Failure here is caused by there being no type in the
+       -- default list which can satisfy all the ambiguous classes.
+       -- For example, if Real a is reqd, but the only type in the
+       -- default list is Int.
+    tcGetDefaultTys                    `thenNF_Tc` \ default_tys ->
+    let
+      try_default []   -- No defaults work, so fail
+       = failTc
+
+      try_default (default_ty : default_tys)
+       = tryTc (try_default default_tys) $     -- If default_ty fails, we try
+                                               -- default_tys instead
+         tcSimplifyCheckThetas [] thetas       `thenTc` \ _ ->
+         returnTc default_ty
+        where
+         thetas = classes `zip` repeat [default_ty]
+    in
+       -- See if any default works, and if so bind the type variable to it
+       -- If not, add an AmbigErr
+    recoverTc (complain dicts `thenNF_Tc_` returnTc EmptyMonoBinds)    $
+
+    try_default default_tys                    `thenTc` \ chosen_default_ty ->
+
+       -- Bind the type variable and reduce the context, for real this time
+    tcInstType emptyTyVarEnv chosen_default_ty         `thenNF_Tc` \ chosen_default_tc_ty ->   -- Tiresome!
+    unifyTauTy chosen_default_tc_ty (mkTyVarTy tyvar)  `thenTc_`
+    reduceContext (text "disambig" <+> ppr dicts)
+                 try_me [] dicts       `thenTc` \ (binds, frees, ambigs) ->
+    ASSERT( null frees && null ambigs )
+    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
+  = complain dicts     `thenNF_Tc_`
+    returnTc EmptyMonoBinds
+
+  where
+    complain    = addAmbigErrs tyVarsOfInst
+    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}
+
+
+
+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}
+genCantGenErr insts    -- Can't generalise these Insts
+  = sep [ptext SLIT("Cannot generalise these overloadings (in a _ccall_):"), 
+        nest 4 (pprInstsInFull insts)
+       ]
+
+addAmbigErrs ambig_tv_fn dicts = mapNF_Tc (addAmbigErr ambig_tv_fn) dicts
+
+addAmbigErr ambig_tv_fn dict
+  = tcAddSrcLoc (instLoc dict) $
+    addErrTc (sep [text "Ambiguous type variable(s)",
+                  hsep (punctuate comma (map (quotes . ppr) ambig_tvs)),
+                  nest 4 (text "in the constraint" <+> quotes (pprInst dict)),
+                  nest 4 (pprOrigin dict)])
+  where
+    ambig_tvs = tyVarSetToList (ambig_tv_fn dict)
+
+-- Used for top-level irreducibles
+addTopInstanceErr dict
+  = tcAddSrcLoc (instLoc dict)                $
+    addErrTc (sep [ptext SLIT("No instance for") <+> quotes (pprInst dict),
+                  nest 4 $ parens $ pprOrigin dict])
+
+addNoInstanceErr str givens dict
+  = tcAddSrcLoc (instLoc dict) $
+    addErrTc (sep [sep [ptext SLIT("Could not deduce") <+> quotes (pprInst dict),
+                       nest 4 $ parens $ pprOrigin dict],
+                  nest 4 $ ptext SLIT("from the context") <+> pprInsts givens]
+             $$
+             ptext SLIT("Probable cause:") <+> 
+             vcat [ptext SLIT("missing") <+> quotes (pprInst dict) <+> ptext SLIT("in") <+> str,
+                   if all_tyvars then empty else
+                   ptext SLIT("or missing instance declaration for") <+> quotes (pprInst dict)]
+    )
+  where
+    all_tyvars = all isTyVarTy tys
+    (_, tys)   = getDictClassTys dict
 
-    is_elem = isIn "bindInstsOfLocalFuns"
+-- Used for the ...Thetas variants; all top level
+addNoInstErr (c,ts)
+  = addErrTc (ptext SLIT("No instance for") <+> quotes (pprConstraint c ts))
 \end{code}