X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcSimplify.lhs;h=bed09325acde46c7fa3d695f4a4bfb732ca49a07;hp=292c2314fd19395f98f0017259d1382c06d77819;hb=HEAD;hpb=1d051fbc5df6586298357580fd48de1a51e645b4

diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 292c231..bed0932 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,387 +1,452 @@
-%
-% (c) The University of Glasgow 2006
-% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-%
-
-TcSimplify
-
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
-module TcSimplify (
-	tcSimplifyInfer, tcSimplifyInferCheck,
-	tcSimplifyCheck, tcSimplifyRestricted,
-	tcSimplifyRuleLhs, tcSimplifyIPs, 
-	tcSimplifySuperClasses,
-	tcSimplifyTop, tcSimplifyInteractive,
-	tcSimplifyBracket, tcSimplifyCheckPat,
-
-	tcSimplifyDeriv, tcSimplifyDefault,
-	bindInstsOfLocalFuns, bindIrreds,
-
-        misMatchMsg
-    ) where
+module TcSimplify( 
+       simplifyInfer,
+       simplifyDefault, simplifyDeriv, 
+       simplifyRule, simplifyTop, simplifyInteractive
+  ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-} TcUnify( unifyType )
-import HsSyn
-
+import HsSyn	       
 import TcRnMonad
-import Inst
-import TcEnv
-import InstEnv
-import TcGadt
-import TcType
+import TcErrors
 import TcMType
-import TcIface
-import TcTyFuns
-import TypeRep
+import TcType 
+import TcSMonad 
+import TcInteract
+import Inst
+import Id	( evVarPred )
+import Unify	( niFixTvSubst, niSubstTvSet )
 import Var
-import Name
-import NameSet
-import Class
-import FunDeps
-import PrelInfo
-import PrelNames
-import Type
-import TysWiredIn
-import ErrUtils
-import BasicTypes
 import VarSet
-import VarEnv
-import Module
-import FiniteMap
+import VarEnv 
+import Coercion
+import TypeRep
+
+import Name
+import NameEnv	( emptyNameEnv )
 import Bag
-import Outputable
-import Maybes
 import ListSetOps
 import Util
-import UniqSet
-import SrcLoc
-import DynFlags
-
-import Data.List
+import PrelInfo
+import PrelNames
+import Class		( classKey )
+import BasicTypes       ( RuleName, TopLevelFlag, isTopLevel )
+import Control.Monad    ( when )
+import Outputable
+import FastString
 \end{code}
 
 
-%************************************************************************
-%*									*
-\subsection{NOTES}
-%*									*
-%************************************************************************
-
-	--------------------------------------
-	Notes on functional dependencies (a bug)
-	--------------------------------------
-
-Consider this:
-
-	class C a b | a -> b
-	class D a b | a -> b
-
-	instance D a b => C a b	-- Undecidable 
-				-- (Not sure if it's crucial to this eg)
-	f :: C a b => a -> Bool
-	f _ = True
-	
-	g :: C a b => a -> Bool
-	g = f
-
-Here f typechecks, but g does not!!  Reason: before doing improvement,
-we reduce the (C a b1) constraint from the call of f to (D a b1).
-
-Here is a more complicated example:
-
-| > class Foo a b | a->b
-| >
-| > class Bar a b | a->b
-| >
-| > data Obj = Obj
-| >
-| > instance Bar Obj Obj
-| >
-| > instance (Bar a b) => Foo a b
-| >
-| > foo:: (Foo a b) => a -> String
-| > foo _ = "works"
-| >
-| > runFoo:: (forall a b. (Foo a b) => a -> w) -> w
-| > runFoo f = f Obj
-| 
-| *Test> runFoo foo
-| 
-| <interactive>:1:
-|     Could not deduce (Bar a b) from the context (Foo a b)
-|       arising from use of `foo' at <interactive>:1
-|     Probable fix:
-|         Add (Bar a b) to the expected type of an expression
-|     In the first argument of `runFoo', namely `foo'
-|     In the definition of `it': it = runFoo foo
-| 
-| Why all of the sudden does GHC need the constraint Bar a b? The
-| function foo didn't ask for that... 
-
-The trouble is that to type (runFoo foo), GHC has to solve the problem:
-
-	Given constraint	Foo a b
-	Solve constraint	Foo a b'
-
-Notice that b and b' aren't the same.  To solve this, just do
-improvement and then they are the same.  But GHC currently does
-	simplify constraints
-	apply improvement
-	and loop
-
-That is usually fine, but it isn't here, because it sees that Foo a b is
-not the same as Foo a b', and so instead applies the instance decl for
-instance Bar a b => Foo a b.  And that's where the Bar constraint comes
-from.
-
-The Right Thing is to improve whenever the constraint set changes at
-all.  Not hard in principle, but it'll take a bit of fiddling to do.  
-
-Note [Choosing which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are about to do a generalisation step.  We have in our hand
-
-	G	the environment
-	T	the type of the RHS
-	C	the constraints from that RHS
-
-The game is to figure out
-
-	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
-
-	forall Q. Cq => T
-
-and float the constraints Ct further outwards.
-
-Here are the things that *must* be true:
-
- (A)	Q intersect fv(G) = EMPTY			limits how big Q can be
- (B)	Q superset fv(Cq union T) \ oclose(fv(G),C)	limits how small Q can be
-
- (A) says we can't quantify over a variable that's free in the environment. 
- (B) says we must quantify over all the truly free variables in T, else 
-     we won't get a sufficiently general type.  
-
-We do not *need* to quantify over any variable that is fixed by the
-free vars of the environment G.
-
-	BETWEEN THESE TWO BOUNDS, ANY Q WILL DO!
-
-Example:	class H x y | x->y where ...
-
-	fv(G) = {a}	C = {H a b, H c d}
-			T = c -> b
-
-	(A)  Q intersect {a} is empty
-	(B)  Q superset {a,b,c,d} \ oclose({a}, C) = {a,b,c,d} \ {a,b} = {c,d}
-
-	So Q can be {c,d}, {b,c,d}
-
-In particular, it's perfectly OK to quantify over more type variables
-than strictly necessary; there is no need to quantify over 'b', since
-it is determined by 'a' which is free in the envt, but it's perfectly
-OK to do so.  However we must not quantify over 'a' itself.
-
-Other things being equal, however, we'd like to quantify over as few
-variables as possible: smaller types, fewer type applications, more
-constraints can get into Ct instead of Cq.  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.
+*********************************************************************************
+*                                                                               * 
+*                           External interface                                  *
+*                                                                               *
+*********************************************************************************
 
+\begin{code}
+simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
+-- Simplify top-level constraints
+-- Usually these will be implications,
+-- but when there is nothing to quantify we don't wrap
+-- in a degenerate implication, so we do that here instead
+simplifyTop wanteds 
+  = simplifyCheck (SimplCheck (ptext (sLit "top level"))) wanteds
+
+------------------
+simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
+simplifyInteractive wanteds 
+  = simplifyCheck SimplInteractive wanteds
+
+------------------
+simplifyDefault :: ThetaType	-- Wanted; has no type variables in it
+                -> TcM ()	-- Succeeds iff the constraint is soluble
+simplifyDefault theta
+  = do { wanted <- newFlatWanteds DefaultOrigin theta
+       ; _ignored_ev_binds <- simplifyCheck (SimplCheck (ptext (sLit "defaults"))) 
+                                            (mkFlatWC wanted)
+       ; return () }
+\end{code}
 
 
--------------------------------------
-	Note [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 here's 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.
+*********************************************************************************
+*                                                                                 * 
+*                            Deriving
+*                                                                                 *
+***********************************************************************************
 
-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.
+\begin{code}
+simplifyDeriv :: CtOrigin
+              -> PredType
+	      -> [TyVar]	
+	      -> ThetaType		-- Wanted
+	      -> TcM ThetaType	-- Needed
+-- Given  instance (wanted) => C inst_ty 
+-- Simplify 'wanted' as much as possibles
+-- Fail if not possible
+simplifyDeriv orig pred tvs theta 
+  = do { tvs_skols <- tcInstSkolTyVars tvs -- Skolemize
+      	 	-- The constraint solving machinery 
+		-- expects *TcTyVars* not TyVars.  
+		-- We use *non-overlappable* (vanilla) skolems
+		-- See Note [Overlap and deriving]
+
+       ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
+             subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
+	     doc = parens $ ptext (sLit "deriving") <+> parens (ppr pred)
+
+       ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
+
+       ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
+       ; (residual_wanted, _binds)
+             <- runTcS (SimplInfer doc) NoUntouchables $
+                solveWanteds emptyInert (mkFlatWC wanted)
+
+       ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
+                         -- See Note [Exotic derived instance contexts]
+             get_good :: WantedEvVar -> Either PredType WantedEvVar
+             get_good wev | validDerivPred p = Left p
+                          | otherwise        = Right wev
+                          where p = evVarOfPred wev
+
+       ; reportUnsolved (residual_wanted { wc_flat = bad })
+
+       ; let min_theta = mkMinimalBySCs (bagToList good)
+       ; return (substTheta subst_skol min_theta) }
+\end{code}
 
+Note [Overlap and deriving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider some overlapping instances:
+  data Show a => Show [a] where ..
+  data Show [Char] where ...
+
+Now a data type with deriving:
+  data T a = MkT [a] deriving( Show )
+
+We want to get the derived instance
+  instance Show [a] => Show (T a) where...
+and NOT
+  instance Show a => Show (T a) where...
+so that the (Show (T Char)) instance does the Right Thing
+
+It's very like the situation when we're inferring the type
+of a function
+   f x = show [x]
+and we want to infer
+   f :: Show [a] => a -> String
+
+BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
+             the context for the derived instance. 
+	     Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
+
+Note [Exotic derived instance contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In a 'derived' instance declaration, we *infer* the context.  It's a
+bit unclear what rules we should apply for this; the Haskell report is
+silent.  Obviously, constraints like (Eq a) are fine, but what about
+	data T f a = MkT (f a) deriving( Eq )
+where we'd get an Eq (f a) constraint.  That's probably fine too.
 
-Can we ever be *certain* about ambiguity?  Yes: if there's a constraint
+One could go further: consider
+	data T a b c = MkT (Foo a b c) deriving( Eq )
+	instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
 
-	c in C such that fv(c) intersect (fv(G) union fv(T)) = EMPTY
+Notice that this instance (just) satisfies the Paterson termination 
+conditions.  Then we *could* derive an instance decl like this:
 
-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?
+	instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
+even though there is no instance for (C Int a), because there just
+*might* be an instance for, say, (C Int Bool) at a site where we
+need the equality instance for T's.  
 
-	class K x
-	class H x y | x -> y
-	instance H x y => K (x,y)
+However, this seems pretty exotic, and it's quite tricky to allow
+this, and yet give sensible error messages in the (much more common)
+case where we really want that instance decl for C.
 
-Is this type ambiguous?
-	forall a b. (K (a,b), Eq b) => a -> a
+So for now we simply require that the derived instance context
+should have only type-variable constraints.
 
-Urk.  The (Eq b) looks "definitely ambiguous" but it isn't.  What we are after
-is a "bubble" that's a set of constraints
+Here is another example:
+	data Fix f = In (f (Fix f)) deriving( Eq )
+Here, if we are prepared to allow -XUndecidableInstances we
+could derive the instance
+	instance Eq (f (Fix f)) => Eq (Fix f)
+but this is so delicate that I don't think it should happen inside
+'deriving'. If you want this, write it yourself!
+
+NB: if you want to lift this condition, make sure you still meet the
+termination conditions!  If not, the deriving mechanism generates
+larger and larger constraints.  Example:
+  data Succ a = S a
+  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
+
+Note the lack of a Show instance for Succ.  First we'll generate
+  instance (Show (Succ a), Show a) => Show (Seq a)
+and then
+  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
+and so on.  Instead we want to complain of no instance for (Show (Succ a)).
+
+The bottom line
+~~~~~~~~~~~~~~~
+Allow constraints which consist only of type variables, with no repeats.
+
+*********************************************************************************
+*                                                                                 * 
+*                            Inference
+*                                                                                 *
+***********************************************************************************
 
-	Cq = Ca union Cq'  st  fv(Ca) intersect (fv(Cq') union fv(T) union fv(G)) = EMPTY
+\begin{code}
+simplifyInfer :: TopLevelFlag
+              -> Bool                  -- Apply monomorphism restriction
+              -> [(Name, TcTauType)]   -- Variables to be generalised,
+                                       -- and their tau-types
+              -> WantedConstraints
+              -> TcM ([TcTyVar],    -- Quantify over these type variables
+                      [EvVar],      -- ... and these constraints
+                      TcEvBinds)    -- ... binding these evidence variables
+simplifyInfer top_lvl apply_mr name_taus wanteds
+  | isEmptyWC wanteds
+  = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
+       ; zonked_taus <- zonkTcTypes (map snd name_taus)
+       ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
+       ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
+       ; return (qtvs, [], emptyTcEvBinds) }
 
-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-ambiguous can then float out, and get smashed at top level
-(which squashes out the constants, like Eq (T a) above)
+  | otherwise
+  = do { zonked_wanteds <- zonkWC wanteds
+       ; zonked_taus    <- zonkTcTypes (map snd name_taus)
+       ; gbl_tvs        <- tcGetGlobalTyVars
+
+       ; traceTc "simplifyInfer {"  $ vcat
+             [ ptext (sLit "apply_mr =") <+> ppr apply_mr
+             , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
+             , ptext (sLit "wanted =") <+> ppr zonked_wanteds
+             ]
+
+             -- Step 1
+             -- Make a guess at the quantified type variables
+	     -- Then split the constraints on the baisis of those tyvars
+	     -- to avoid unnecessarily simplifying a class constraint
+	     -- See Note [Avoid unecessary constraint simplification]
+       ; let zonked_tau_tvs = get_tau_tvs zonked_taus
+             proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
+                          zonked_tau_tvs `minusVarSet` gbl_tvs
+             (perhaps_bound, surely_free)
+                        = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
+
+       ; traceTc "simplifyInfer proto"  $ vcat
+             [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
+             , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
+             , ptext (sLit "surely_fref =") <+> ppr surely_free
+             ]
+
+       ; emitFlats surely_free
+       ; traceTc "sinf"  $ vcat
+             [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
+             , ptext (sLit "surely_free   =") <+> ppr surely_free
+             ]
+
+            -- Step 2 
+       	    -- Now simplify the possibly-bound constraints
+       ; (simpl_results, tc_binds0)
+           <- runTcS (SimplInfer (ppr (map fst name_taus))) NoUntouchables $
+              simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
+
+       ; when (insolubleWC simpl_results)  -- Fail fast if there is an insoluble constraint
+              (do { reportUnsolved simpl_results; failM })
+
+            -- Step 3 
+            -- Split again simplified_perhaps_bound, because some unifications 
+            -- may have happened, and emit the free constraints. 
+       ; gbl_tvs        <- tcGetGlobalTyVars
+       ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
+       ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
+       ; let init_tvs 	     = zonked_tau_tvs `minusVarSet` gbl_tvs
+             mr_qtvs  	     = init_tvs `minusVarSet` constrained_tvs
+             constrained_tvs = tyVarsOfEvVarXs zonked_simples
+             qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
+             (final_qtvs, (bound, free))
+                | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
+                | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
+       ; emitFlats free
+
+       ; if isEmptyVarSet final_qtvs && isEmptyBag bound
+         then ASSERT( isEmptyBag (wc_insol simpl_results) )
+              do { traceTc "} simplifyInfer/no quantification" empty
+                 ; emitImplications (wc_impl simpl_results)
+                 ; return ([], [], EvBinds tc_binds0) }
+         else do
+
+            -- Step 4, zonk quantified variables 
+       { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
+       ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
+                        | (name, ty) <- name_taus ]
+                        -- Don't add the quantified variables here, because
+                        -- they are also bound in ic_skols and we want them to be
+                        -- tidied uniformly
+             skol_info = InferSkol poly_ids
+
+       ; gloc <- getCtLoc skol_info
+       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
+
+            -- Step 5
+            -- Minimize `bound' and emit an implication
+       ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
+       ; ev_binds_var <- newTcEvBinds
+       ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
+       ; lcl_env <- getLclTypeEnv
+       ; let implic = Implic { ic_untch    = NoUntouchables
+                             , ic_env      = lcl_env
+                             , ic_skols    = mkVarSet qtvs_to_return
+                             , ic_given    = minimal_bound_ev_vars
+                             , ic_wanted   = simpl_results { wc_flat = bound }
+                             , ic_insol    = False
+                             , ic_binds    = ev_binds_var
+                             , ic_loc      = gloc }
+       ; emitImplication implic
+       ; traceTc "} simplifyInfer/produced residual implication for quantification" $
+             vcat [ ptext (sLit "implic =") <+> ppr implic
+                       -- ic_skols, ic_given give rest of result
+                  , ptext (sLit "qtvs =") <+> ppr final_qtvs
+                  , ptext (sLit "spb =") <+> ppr zonked_simples
+                  , ptext (sLit "bound =") <+> ppr bound ]
+
+
+
+       ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
+  where
+    get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
+                | otherwise          = exactTyVarsOfTypes
+     -- See Note [Silly type synonym] in TcType
+\end{code}
 
 
-	--------------------------------------
-		Notes on principal types
-	--------------------------------------
+Note [Minimize by Superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 
-    class C a where
-      op :: a -> a
+When we quantify over a constraint, in simplifyInfer we need to
+quantify over a constraint that is minimal in some sense: For
+instance, if the final wanted constraint is (Eq alpha, Ord alpha),
+we'd like to quantify over Ord alpha, because we can just get Eq alpha
+from superclass selection from Ord alpha. This minimization is what
+mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
+to check the original wanted.
 
-    f x = let g y = op (y::Int) in True
+\begin{code}
+simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
+simplifyWithApprox wanted
+ = do { traceTcS "simplifyApproxLoop" (ppr wanted)
 
-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
+      ; results <- solveWanteds emptyInert wanted
 
+      ; let (residual_implics, floats) = approximateImplications (wc_impl results)
 
-	--------------------------------------
-	The need for forall's in constraints
-	--------------------------------------
+        -- If no new work was produced then we are done with simplifyApproxLoop
+      ; if insolubleWC results || isEmptyBag floats
+        then return results
 
-[Exchange on Haskell Cafe 5/6 Dec 2000]
+        else solveWanteds emptyInert
+                (WC { wc_flat = floats `unionBags` wc_flat results
+                    , wc_impl = residual_implics
+                    , wc_insol = emptyBag }) }
 
-  class C t where op :: t -> Bool
-  instance C [t] where op x = True
+approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
+-- Extracts any nested constraints that don't mention the skolems
+approximateImplications impls
+  = do_bag (float_implic emptyVarSet) impls
+  where 
+    do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
+    do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
+    plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
+    plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
+
+    float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
+    float_implic skols imp
+      = (unitBag (imp { ic_wanted = wanted' }), floats)
+      where
+        (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
 
-  p y = (let f :: c -> Bool; f x = op (y >> return x) in f, y ++ [])
-  q y = (y ++ [], let f :: c -> Bool; f x = op (y >> return x) in f)
+    float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
+      = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
+      where
+        (flat',   floats1) = do_bag (float_flat   skols) flat
+        (implic', floats2) = do_bag (float_implic skols) implic
 
-The definitions of p and q differ only in the order of the components in
-the pair on their right-hand sides.  And yet:
+    float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
+    float_flat skols wev
+      | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
+      | otherwise                                 = (unitBag wev, emptyBag)
+\end{code}
 
-  ghc and "Typing Haskell in Haskell" reject p, but accept q;
-  Hugs rejects q, but accepts p;
-  hbc rejects both p and q;
-  nhc98 ... (Malcolm, can you fill in the blank for us!).
+\begin{code}
+-- (growX gbls wanted tvs) grows a seed 'tvs' against the 
+-- X-constraint 'wanted', nuking the 'gbls' at each stage
+-- It's conservative in that if the seed could *possibly*
+-- grow to include a type variable, then it does
+
+growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
+growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
+
+growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
+growWantedEVs gbl_tvs ws tvs
+  | isEmptyBag ws = tvs
+  | otherwise     = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
+
+--------  Helper functions, do not do fixpoint ------------------------
+growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
+growWC gbl_tvs wc = growImplics gbl_tvs             (wc_impl wc) .
+                    growPreds   gbl_tvs evVarOfPred (wc_flat wc) .
+                    growPreds   gbl_tvs evVarOfPred (wc_insol wc)
+
+growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
+growImplics gbl_tvs implics tvs
+  = foldrBag grow_implic tvs implics
+  where
+    grow_implic implic tvs
+      = grow tvs `minusVarSet` ic_skols implic
+      where
+        grow = growWC gbl_tvs (ic_wanted implic) .
+               growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
+               -- We must grow from givens too; see test IPRun
 
-The type signature for f forces context reduction to take place, and
-the results of this depend on whether or not the type of y is known,
-which in turn depends on which component of the pair the type checker
-analyzes first.  
+growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
+growPreds gbl_tvs get_pred items tvs
+  = foldrBag extend tvs items
+  where
+    extend item tvs = tvs `unionVarSet`
+                      (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
+
+--------------------
+quantifyMe :: TyVarSet      -- Quantifying over these
+	   -> WantedEvVar
+	   -> Bool	    -- True <=> quantify over this wanted
+quantifyMe qtvs wev
+  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
+  | otherwise	  = tyVarsOfPred pred `intersectsVarSet` qtvs
+  where
+    pred = evVarOfPred wev
+\end{code}
 
-Solution: if y::m a, float out the constraints
-	Monad m, forall c. C (m c)
-When m is later unified with [], we can solve both constraints.
+Note [Avoid unecessary constraint simplification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When inferring the type of a let-binding, with simplifyInfer,
+try to avoid unnecessariliy simplifying class constraints.
+Doing so aids sharing, but it also helps with delicate 
+situations like
+   instance C t => C [t] where ..
+   f :: C [t] => ....
+   f x = let g y = ...(constraint C [t])... 
+         in ...
+When inferring a type for 'g', we don't want to apply the
+instance decl, because then we can't satisfy (C t).  So we
+just notice that g isn't quantified over 't' and partition
+the contraints before simplifying.
 
+This only half-works, but then let-generalisation only half-works.
 
-	--------------------------------------
-		Notes on implicit parameters
-	--------------------------------------
 
 Note [Inheriting implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -409,2381 +474,818 @@ BOTTOM LINE: when *inferring types* you *must* quantify
 over implicit parameters. See the predicate isFreeWhenInferring.
 
 
-Note [Implicit parameters and ambiguity] 
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Only a *class* predicate can give rise to ambiguity
-An *implicit parameter* cannot.  For example:
-	foo :: (?x :: [a]) => Int
-	foo = length ?x
-is fine.  The call site will suppply a particular 'x'
-
-Furthermore, the type variables fixed by an implicit parameter
-propagate to the others.  E.g.
-	foo :: (Show a, ?x::[a]) => Int
-	foo = show (?x++?x)
-The type of foo looks ambiguous.  But it isn't, because at a call site
-we might have
-	let ?x = 5::Int in foo
-and all is well.  In effect, implicit parameters are, well, parameters,
-so we can take their type variables into account as part of the
-"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
-
-
-Question 2: type signatures
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-BUT WATCH OUT: When you supply a type signature, we can't force you
-to quantify over implicit parameters.  For example:
-
-	(?x + 1) :: Int
-
-This is perfectly reasonable.  We do not want to insist on
-
-	(?x + 1) :: (?x::Int => Int)
-
-That would be silly.  Here, the definition site *is* the occurrence site,
-so the above strictures don't apply.  Hence the difference between
-tcSimplifyCheck (which *does* allow implicit paramters to be inherited)
-and tcSimplifyCheckBind (which does not).
-
-What about when you supply a type signature for a binding?
-Is it legal to give the following explicit, user type 
-signature to f, thus:
-
-	f :: Int -> Int
-	f x = (x::Int) + ?y
-
-At first sight this seems reasonable, but it has the nasty property
-that adding a type signature changes the dynamic semantics.
-Consider this:
-
-	(let f x = (x::Int) + ?y
- 	 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)
-
-Indeed, simply inlining f (at the Haskell source level) would change the
-dynamic semantics.
-
-Nevertheless, as Launchbury says (email Oct 01) we can't really give the
-semantics for a Haskell program without knowing its typing, so if you 
-change the typing you may change the semantics.
+*********************************************************************************
+*                                                                                 * 
+*                             RULES                                               *
+*                                                                                 *
+***********************************************************************************
 
-To make things consistent in all cases where we are *checking* against
-a supplied signature (as opposed to inferring a type), we adopt the
-rule: 
-
-	a signature does not need to quantify over implicit params.
-
-[This represents a (rather marginal) change of policy since GHC 5.02,
-which *required* an explicit signature to quantify over all implicit
-params for the reasons mentioned above.]
-
-But that raises a new question.  Consider 
-
-	Given (signature)	?x::Int
-	Wanted (inferred)	?x::Int, ?y::Bool
-
-Clearly we want to discharge the ?x and float the ?y out.  But
-what is the criterion that distinguishes them?  Clearly it isn't
-what free type variables they have.  The Right Thing seems to be
-to float a constraint that
-	neither mentions any of the quantified type variables
-	nor any of the quantified implicit parameters
-
-See the predicate isFreeWhenChecking.
-
-
-Question 3: monomorphism
-~~~~~~~~~~~~~~~~~~~~~~~~
-There's a nasty corner case when the monomorphism restriction bites:
-
-	z = (x::Int) + ?y
-
-The argument above suggests that we *must* generalise
-over the ?y parameter, to get
-	z :: (?y::Int) => Int,
-but the monomorphism restriction says that we *must not*, giving
-	z :: Int.
-Why does the momomorphism restriction say this?  Because if you have
-
-	let z = x + ?y in z+z
-
-you might not expect the addition to be done twice --- but it will if
-we follow the argument of Question 2 and generalise over ?y.
-
-
-Question 4: top level
-~~~~~~~~~~~~~~~~~~~~~
-At the top level, monomorhism makes no sense at all.
-
-    module Main where
-	main = let ?x = 5 in print foo
-
-	foo = woggle 3
-
-	woggle :: (?x :: Int) => Int -> Int
-	woggle y = ?x + y
-
-We definitely don't want (foo :: Int) with a top-level implicit parameter
-(?x::Int) becuase there is no way to bind it.  
-
-
-Possible choices
-~~~~~~~~~~~~~~~~
-(A) Always generalise over implicit parameters
-    Bindings that fall under the monomorphism restriction can't
-	be generalised
-
-    Consequences:
-	* Inlining remains valid
-	* No unexpected loss of sharing
-	* But simple bindings like
-		z = ?y + 1
-	  will be rejected, unless you add an explicit type signature
-	  (to avoid the monomorphism restriction)
-		z :: (?y::Int) => Int
-		z = ?y + 1
-	  This seems unacceptable
-
-(B) Monomorphism restriction "wins"
-    Bindings that fall under the monomorphism restriction can't
-	be generalised
-    Always generalise over implicit parameters *except* for bindings
-	that fall under the monomorphism restriction
-
-    Consequences
-	* Inlining isn't valid in general
-	* No unexpected loss of sharing
-	* Simple bindings like
-		z = ?y + 1
-	  accepted (get value of ?y from binding site)
-
-(C) Always generalise over implicit parameters
-    Bindings that fall under the monomorphism restriction can't
-	be generalised, EXCEPT for implicit parameters
-    Consequences
-	* Inlining remains valid
-	* Unexpected loss of sharing (from the extra generalisation)
-	* Simple bindings like
-		z = ?y + 1
-	  accepted (get value of ?y from occurrence sites)
-
-
-Discussion
-~~~~~~~~~~
-None of these choices seems very satisfactory.  But at least we should
-decide which we want to do.
-
-It's really not clear what is the Right Thing To Do.  If you see
-
-	z = (x::Int) + ?y
-
-would you expect the value of ?y to be got from the *occurrence sites*
-of 'z', or from the valuue of ?y at the *definition* of 'z'?  In the
-case of function definitions, the answer is clearly the former, but
-less so in the case of non-fucntion definitions.   On the other hand,
-if we say that we get the value of ?y from the definition site of 'z',
-then inlining 'z' might change the semantics of the program.
-
-Choice (C) really says "the monomorphism restriction doesn't apply
-to implicit parameters".  Which is fine, but remember that every
-innocent binding 'x = ...' that mentions an implicit parameter in
-the RHS becomes a *function* of that parameter, called at each
-use of 'x'.  Now, the chances are that there are no intervening 'with'
-clauses that bind ?y, so a decent compiler should common up all
-those function calls.  So I think I strongly favour (C).  Indeed,
-one could make a similar argument for abolishing the monomorphism
-restriction altogether.
-
-BOTTOM LINE: we choose (B) at present.  See tcSimplifyRestricted
-
-
-
-%************************************************************************
-%*									*
-\subsection{tcSimplifyInfer}
-%*									*
-%************************************************************************
-
-tcSimplify is called when we *inferring* a type.  Here's the overall game plan:
-
-    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'.)
-
-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.
-
-For the guts, we need a loop, that alternates context reduction and
-improvement with unification.  E.g. Suppose we have
-
-	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)
-
-If we need to unify anything, we rattle round the whole thing all over
-again.
-
-
-\begin{code}
-tcSimplifyInfer
-	:: SDoc
-	-> TcTyVarSet		-- fv(T); type vars
-	-> [Inst]		-- Wanted
-	-> TcM ([TcTyVar],	-- Tyvars to quantify (zonked and quantified)
-		[Inst],		-- Dict Ids that must be bound here (zonked)
-		TcDictBinds)	-- Bindings
-	-- Any free (escaping) Insts are tossed into the environment
-\end{code}
-
-
-\begin{code}
-tcSimplifyInfer doc tau_tvs wanted
-  = do	{ tau_tvs1 <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
-	; wanted'  <- mappM zonkInst wanted	-- Zonk before deciding quantified tyvars
-	; gbl_tvs  <- tcGetGlobalTyVars
-	; let preds1   = fdPredsOfInsts wanted'
-	      gbl_tvs1 = oclose preds1 gbl_tvs
-	      qtvs     = grow preds1 tau_tvs1 `minusVarSet` gbl_tvs1
-			-- See Note [Choosing which variables to quantify]
-
-		-- To maximise sharing, remove from consideration any 
-		-- constraints that don't mention qtvs at all
-	; let (free, bound) = partition (isFreeWhenInferring qtvs) wanted'
-	; extendLIEs free
-
-		-- To make types simple, reduce as much as possible
-	; traceTc (text "infer" <+> (ppr preds1 $$ ppr (grow preds1 tau_tvs1) $$ ppr gbl_tvs $$ 
-		   ppr gbl_tvs1 $$ ppr free $$ ppr bound))
-	; (irreds1, binds1) <- tryHardCheckLoop doc bound
-
-		-- Note [Inference and implication constraints]
-	; let want_dict d = tyVarsOfInst d `intersectsVarSet` qtvs
-	; (irreds2, binds2) <- approximateImplications doc want_dict irreds1
-
-		-- Now work out all over again which type variables to quantify,
-		-- exactly in the same way as before, but starting from irreds2.  Why?
-		-- a) By now improvment may have taken place, and we must *not*
-		--    quantify over any variable free in the environment
-		--    tc137 (function h inside g) is an example
-		--
-		-- b) Do not quantify over constraints that *now* do not
-		--    mention quantified type variables, because they are
-		--    simply ambiguous (or might be bound further out).  Example:
-		--    	f :: Eq b => a -> (a, b)
-		--    	g x = fst (f x)
-		--    From the RHS of g we get the MethodInst f77 :: alpha -> (alpha, beta)
-		--    We decide to quantify over 'alpha' alone, but free1 does not include f77
-		--    because f77 mentions 'alpha'.  Then reducing leaves only the (ambiguous)
-		--    constraint (Eq beta), which we dump back into the free set
-		--    See test tcfail181
-		--
-		-- c) irreds may contain type variables not previously mentioned,
-		--    e.g.  instance D a x => Foo [a] 
-		--	    wanteds = Foo [a]
-		--       Then after simplifying we'll get (D a x), and x is fresh
-		-- 	 We must quantify over x else it'll be totally unbound
-	; tau_tvs2 <- zonkTcTyVarsAndFV (varSetElems tau_tvs1)
-	; gbl_tvs2 <- zonkTcTyVarsAndFV (varSetElems gbl_tvs1)
-		-- Note that we start from gbl_tvs1
-		-- We use tcGetGlobalTyVars, then oclose wrt preds2, because
-		-- we've already put some of the original preds1 into frees
-		-- E.g. 	wanteds = C a b	  (where a->b)
-		--		gbl_tvs = {a}
-		--		tau_tvs = {b}
-		-- Then b is fixed by gbl_tvs, so (C a b) will be in free, and
-		-- irreds2 will be empty.  But we don't want to generalise over b!
-	; let preds2 = fdPredsOfInsts irreds2	-- irreds2 is zonked
-	      qtvs   = grow preds2 tau_tvs2 `minusVarSet` oclose preds2 gbl_tvs2
-	; let (free, irreds3) = partition (isFreeWhenInferring qtvs) irreds2
-	; extendLIEs free
-
-		-- Turn the quantified meta-type variables into real type variables
-	; qtvs2 <- zonkQuantifiedTyVars (varSetElems qtvs)
-
-		-- We can't abstract over any remaining unsolved 
-		-- implications so instead just float them outwards. Ugh.
-	; let (q_dicts0, implics) = partition isAbstractableInst irreds3
-	; loc <- getInstLoc (ImplicOrigin doc)
-	; implic_bind <- bindIrreds loc qtvs2 q_dicts0 implics
-
-		-- Prepare equality instances for quantification
-	; let (q_eqs0,q_dicts) = partition isEqInst q_dicts0
-	; q_eqs <- mappM finalizeEqInst q_eqs0
-
-	; return (qtvs2, q_eqs ++ q_dicts, binds1 `unionBags` binds2 `unionBags` implic_bind) }
-	-- NB: when we are done, we might have some bindings, but
-	-- the final qtvs might be empty.  See Note [NO TYVARS] below.
-
-approximateImplications :: SDoc -> (Inst -> Bool) -> [Inst] -> TcM ([Inst], TcDictBinds)
--- Note [Inference and implication constraints]
--- Given a bunch of Dict and ImplicInsts, try to approximate the implications by
---	- fetching any dicts inside them that are free
---	- using those dicts as cruder constraints, to solve the implications
---	- returning the extra ones too
-
-approximateImplications doc want_dict irreds
-  | null extra_dicts 
-  = return (irreds, emptyBag)
-  | otherwise
-  = do	{ extra_dicts' <- mapM cloneDict extra_dicts
-	; tryHardCheckLoop doc (extra_dicts' ++ irreds) }
-		-- By adding extra_dicts', we make them 
-		-- available to solve the implication constraints
-  where 
-    extra_dicts = get_dicts (filter isImplicInst irreds)
-
-    get_dicts :: [Inst] -> [Inst]	-- Returns only Dicts
-	-- Find the wanted constraints in implication constraints that satisfy
-	-- want_dict, and are not bound by forall's in the constraint itself
-    get_dicts ds = concatMap get_dict ds
-
-    get_dict d@(Dict {}) | want_dict d = [d]
-		         | otherwise   = []
-    get_dict (ImplicInst {tci_tyvars = tvs, tci_wanted = wanteds})
-	= [ d | let tv_set = mkVarSet tvs
-	      , d <- get_dicts wanteds 
-	      , not (tyVarsOfInst d `intersectsVarSet` tv_set)]
-    get_dict i@(EqInst {}) | want_dict i = [i]
-			   | otherwise   = [] 
-    get_dict other = pprPanic "approximateImplications" (ppr other)
-\end{code}
-
-Note [Inference and implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
-Suppose we have a wanted implication constraint (perhaps arising from
-a nested pattern match) like
-	C a => D [a]
-and we are now trying to quantify over 'a' when inferring the type for
-a function.  In principle it's possible that there might be an instance
-	instance (C a, E a) => D [a]
-so the context (E a) would suffice.  The Right Thing is to abstract over
-the implication constraint, but we don't do that (a) because it'll be
-surprising to programmers and (b) because we don't have the machinery to deal
-with 'given' implications.
-
-So our best approximation is to make (D [a]) part of the inferred
-context, so we can use that to discharge the implication. Hence
-the strange function get_dictsin approximateImplications.
-
-The common cases are more clear-cut, when we have things like
-	forall a. C a => C b
-Here, abstracting over (C b) is not an approximation at all -- but see
-Note [Freeness and implications].
- 
-See Trac #1430 and test tc228.
-
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyInferCheck is used when we know the constraints we are to simplify
--- against, but we don't know the type variables over which we are going to quantify.
--- This happens when we have a type signature for a mutually recursive group
-tcSimplifyInferCheck
-	 :: InstLoc
-	 -> TcTyVarSet		-- fv(T)
-	 -> [Inst]		-- Given
-	 -> [Inst]		-- Wanted
-	 -> TcM ([TyVar],	-- Fully zonked, and quantified
-		 TcDictBinds)	-- Bindings
-
-tcSimplifyInferCheck loc tau_tvs givens wanteds
-  = do	{ traceTc (text "tcSimplifyInferCheck <-" <+> ppr wanteds)
-      	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-
-	-- Figure out which type variables to quantify 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.
-	; let all_tvs = varSetElems (tau_tvs `unionVarSet` tyVarsOfInsts givens)
-	; all_tvs <- zonkTcTyVarsAndFV all_tvs
-	; gbl_tvs <- tcGetGlobalTyVars
-	; let qtvs = varSetElems (all_tvs `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
-
-	; qtvs' <- zonkQuantifiedTyVars qtvs
-
-		-- Now we are back to normal (c.f. tcSimplCheck)
-	; implic_bind <- bindIrreds loc qtvs' givens irreds
-
-	; traceTc (text "tcSimplifyInferCheck ->" <+> ppr (implic_bind))
-	; return (qtvs', binds `unionBags` implic_bind) }
-\end{code}
-
-Note [Squashing methods]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Be careful if you want to float methods more:
-	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)
-may continue to float out!
-
-
-Note [NO TYVARS]
-~~~~~~~~~~~~~~~~~
-	class Y a b | a -> b where
-	    y :: a -> X b
-	
-	instance Y [[a]] a where
-	    y ((x:_):_) = X x
-	
-	k :: X a -> X a -> X a
-
-	g :: Num a => [X a] -> [X a]
-	g xs = h xs
-	    where
-	    h ys = ys ++ map (k (y [[0]])) xs
-
-The excitement comes when simplifying the bindings for h.  Initially
-try to simplify {y @ [[t1]] t2, 0 @ t1}, with initial qtvs = {t2}.
-From this we get t1:=:t2, but also various bindings.  We can't forget
-the bindings (because of [LOOP]), but in fact t1 is what g is
-polymorphic in.  
-
-The net effect of [NO TYVARS] 
-
-\begin{code}
-isFreeWhenInferring :: TyVarSet -> Inst	-> Bool
-isFreeWhenInferring qtvs inst
-  =  isFreeWrtTyVars qtvs inst	-- Constrains no quantified vars
-  && isInheritableInst inst	-- and no implicit parameter involved
-				--   see Note [Inheriting implicit parameters]
-
-{-	No longer used (with implication constraints)
-isFreeWhenChecking :: TyVarSet	-- Quantified tyvars
-	 	   -> NameSet	-- Quantified implicit parameters
-		   -> Inst -> Bool
-isFreeWhenChecking qtvs ips inst
-  =  isFreeWrtTyVars qtvs inst
-  && isFreeWrtIPs    ips inst
--}
-
-isFreeWrtTyVars qtvs inst = tyVarsOfInst inst `disjointVarSet` qtvs
-isFreeWrtIPs     ips inst = not (any (`elemNameSet` ips) (ipNamesOfInst inst))
-\end{code}
-
-
-%************************************************************************
-%*									*
-\subsection{tcSimplifyCheck}
-%*									*
-%************************************************************************
-
-@tcSimplifyCheck@ is used when we know exactly the set of variables
-we are going to quantify over.  For example, a class or instance declaration.
-
-\begin{code}
------------------------------------------------------------
--- tcSimplifyCheck is used when checking expression type signatures,
--- class decls, instance decls etc.
-tcSimplifyCheck	:: InstLoc
-	 	-> [TcTyVar]		-- Quantify over these
-	 	-> [Inst]		-- Given
-	 	-> [Inst]		-- Wanted
-	 	-> TcM TcDictBinds	-- Bindings
-tcSimplifyCheck loc qtvs givens wanteds 
-  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do	{ traceTc (text "tcSimplifyCheck")
-      	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-	; implic_bind <- bindIrreds loc qtvs givens irreds
-	; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
--- tcSimplifyCheckPat is used for existential pattern match
-tcSimplifyCheckPat :: InstLoc
-	 	   -> [CoVar] -> Refinement
-	 	   -> [TcTyVar]		-- Quantify over these
-	 	   -> [Inst]		-- Given
-	 	   -> [Inst]		-- Wanted
-	 	   -> TcM TcDictBinds	-- Bindings
-tcSimplifyCheckPat loc co_vars reft qtvs givens wanteds
-  = ASSERT( all isTcTyVar qtvs && all isSkolemTyVar qtvs )
-    do	{ traceTc (text "tcSimplifyCheckPat")
-      	; (irreds, binds) <- gentleCheckLoop loc givens wanteds
-	; implic_bind <- bindIrredsR loc qtvs co_vars reft 
-				    givens irreds
-	; return (binds `unionBags` implic_bind) }
-
------------------------------------------------------------
-bindIrreds :: InstLoc -> [TcTyVar]
-	   -> [Inst] -> [Inst]
-	   -> TcM TcDictBinds
-bindIrreds loc qtvs givens irreds 
-  = bindIrredsR loc qtvs [] emptyRefinement givens irreds
-
-bindIrredsR :: InstLoc -> [TcTyVar] -> [CoVar]
-	    -> Refinement -> [Inst] -> [Inst]
-	    -> TcM TcDictBinds	
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
-bindIrredsR loc qtvs co_vars reft givens irreds
-  | null irreds
-  = return emptyBag
-  | otherwise
-  = do	{ let givens' = filter isDict givens
-		-- The givens can include methods
-		-- See Note [Pruning the givens in an implication constraint]
-
-	   -- If there are no 'givens' *and* the refinement is empty
-	   -- (the refinement is like more givens), then it's safe to 
-	   -- partition the 'wanteds' by their qtvs, thereby trimming irreds
-	   -- See Note [Freeness and implications]
-	; irreds' <- if null givens' && isEmptyRefinement reft
-	     	     then do
-	     	    	{ let qtv_set = mkVarSet qtvs
-	     	    	      (frees, real_irreds) = partition (isFreeWrtTyVars qtv_set) irreds
-	     	    	; extendLIEs frees
-	     	    	; return real_irreds }
-	     	     else return irreds
-	
-	; let all_tvs = qtvs ++ co_vars	-- Abstract over all these
-	; (implics, bind) <- makeImplicationBind loc all_tvs reft givens' irreds'
-			-- This call does the real work
-			-- If irreds' is empty, it does something sensible
-	; extendLIEs implics
-	; return bind } 
-
-
-makeImplicationBind :: InstLoc -> [TcTyVar] -> Refinement
-		    -> [Inst] -> [Inst]
-		    -> TcM ([Inst], TcDictBinds)
--- Make a binding that binds 'irreds', by generating an implication
--- constraint for them, *and* throwing the constraint into the LIE
--- The binding looks like
---	(ir1, .., irn) = f qtvs givens
--- where f is (evidence for) the new implication constraint
---	f :: forall qtvs. {reft} givens => (ir1, .., irn)
--- qtvs includes coercion variables
---
--- This binding must line up the 'rhs' in reduceImplication
-makeImplicationBind loc all_tvs reft
-		    givens 	-- Guaranteed all Dicts (TOMDO: true?)
-		    irreds
- | null irreds			-- If there are no irreds, we are done
- = return ([], emptyBag)
- | otherwise			-- Otherwise we must generate a binding
- = do	{ uniq <- newUnique 
-	; span <- getSrcSpanM
-	; let (eq_givens, dict_givens) = partition isEqInst givens
-	      eq_tyvar_cos =  map TyVarTy $ uniqSetToList $ tyVarsOfTypes $ map eqInstType eq_givens
-	; let name = mkInternalName uniq (mkVarOcc "ic") span
-	      implic_inst = ImplicInst { tci_name = name, tci_reft = reft,
-					 tci_tyvars = all_tvs, 
-					 tci_given = (eq_givens ++ dict_givens),
-					 tci_wanted = irreds, tci_loc = loc }
-	; let   -- only create binder for dict_irreds
-	      (eq_irreds, dict_irreds) = partition isEqInst irreds
-              n_dict_irreds = length dict_irreds
-	      dict_irred_ids = map instToId dict_irreds
-	      tup_ty = mkTupleTy Boxed n_dict_irreds (map idType dict_irred_ids)
-	      pat = TuplePat (map nlVarPat dict_irred_ids) Boxed tup_ty
-	      rhs = L span (mkHsWrap co (HsVar (instToId implic_inst)))
-	      co  = mkWpApps (map instToId dict_givens) <.> mkWpTyApps eq_tyvar_cos <.> mkWpTyApps (mkTyVarTys all_tvs)
-	      bind | [dict_irred_id] <- dict_irred_ids  = VarBind dict_irred_id rhs
-		   | otherwise        = PatBind { pat_lhs = L span pat, 
-				                  pat_rhs = unguardedGRHSs rhs, 
-				      	          pat_rhs_ty = tup_ty,
-				      	          bind_fvs = placeHolderNames }
-	; -- pprTrace "Make implic inst" (ppr (implic_inst,irreds,dict_irreds,tup_ty)) $
-	  return ([implic_inst], unitBag (L span bind)) }
-
------------------------------------------------------------
-tryHardCheckLoop :: SDoc
-	     -> [Inst]			-- Wanted
-	     -> TcM ([Inst], TcDictBinds)
-
-tryHardCheckLoop doc wanteds
-  = do { (irreds,binds,_) <- checkLoop (mkRedEnv doc try_me []) wanteds
-       ; return (irreds,binds)
-       }
-  where
-    try_me inst = ReduceMe AddSCs
-	-- Here's the try-hard bit
-
------------------------------------------------------------
-gentleCheckLoop :: InstLoc
-	       -> [Inst]		-- Given
-	       -> [Inst]		-- Wanted
-	       -> TcM ([Inst], TcDictBinds)
-
-gentleCheckLoop inst_loc givens wanteds
-  = do { (irreds,binds,_) <- checkLoop env wanteds
-       ; return (irreds,binds)
-       }
-  where
-    env = mkRedEnv (pprInstLoc inst_loc) try_me givens
-
-    try_me inst | isMethodOrLit inst = ReduceMe AddSCs
-		| otherwise	     = Stop
-	-- When checking against a given signature 
-	-- we MUST be very gentle: Note [Check gently]
-\end{code}
-
-Note [Check gently]
-~~~~~~~~~~~~~~~~~~~~
-We have to very careful about not simplifying too vigorously
-Example:  
-  data T a where
-    MkT :: a -> T [a]
-
-  f :: Show b => T b -> b
-  f (MkT x) = show [x]
-
-Inside the pattern match, which binds (a:*, x:a), we know that
-	b ~ [a]
-Hence we have a dictionary for Show [a] available; and indeed we 
-need it.  We are going to build an implication contraint
-	forall a. (b~[a]) => Show [a]
-Later, we will solve this constraint using the knowledg e(Show b)
-	
-But we MUST NOT reduce (Show [a]) to (Show a), else the whole
-thing becomes insoluble.  So we simplify gently (get rid of literals
-and methods only, plus common up equal things), deferring the real
-work until top level, when we solve the implication constraint
-with tryHardCheckLooop.
-
-
-\begin{code}
------------------------------------------------------------
-checkLoop :: RedEnv
-	  -> [Inst]			-- Wanted
-	  -> TcM ([Inst], TcDictBinds,
-	          [Inst]) 		-- needed givens
--- Precondition: givens are completely rigid
--- Postcondition: returned Insts are zonked
-
-checkLoop env wanteds
-  = go env wanteds []
-  where go env wanteds needed_givens
-	  = do {  -- We do need to zonk the givens; cf Note [Zonking RedEnv]
-                ; env'     <- zonkRedEnv env
-		; wanteds' <- zonkInsts  wanteds
-	
-		; (improved, binds, irreds, more_needed_givens) <- reduceContext env' wanteds'
-
-		; let all_needed_givens = needed_givens ++ more_needed_givens
-	
-		; if not improved then
-	 	     return (irreds, binds, all_needed_givens)
-		  else do
-	
-		-- If improvement did some unification, we go round again.
-		-- We start again with irreds, not wanteds
-		-- Using an instance decl might have introduced a fresh type variable
-		-- which might have been unified, so we'd get an infinite loop
-		-- if we started again with wanteds!  See Note [LOOP]
-		{ (irreds1, binds1, all_needed_givens1) <- go env' irreds all_needed_givens
-		; return (irreds1, binds `unionBags` binds1, all_needed_givens1) } }
-\end{code}
-
-Note [Zonking RedEnv]
-~~~~~~~~~~~~~~~~~~~~~
-It might appear as if the givens in RedEnv are always rigid, but that is not
-necessarily the case for programs involving higher-rank types that have class
-contexts constraining the higher-rank variables.  An example from tc237 in the
-testsuite is
-
-  class Modular s a | s -> a
-
-  wim ::  forall a w. Integral a 
-                        => a -> (forall s. Modular s a => M s w) -> w
-  wim i k = error "urk"
-
-  test5  ::  (Modular s a, Integral a) => M s a
-  test5  =   error "urk"
-
-  test4   =   wim 4 test4'
-
-Notice how the variable 'a' of (Modular s a) in the rank-2 type of wim is
-quantified further outside.  When type checking test4, we have to check
-whether the signature of test5 is an instance of 
-
-  (forall s. Modular s a => M s w)
-
-Consequently, we will get (Modular s t_a), where t_a is a TauTv into the
-givens. 
-
-Given the FD of Modular in this example, class improvement will instantiate
-t_a to 'a', where 'a' is the skolem from test5's signatures (due to the
-Modular s a predicate in that signature).  If we don't zonk (Modular s t_a) in
-the givens, we will get into a loop as improveOne uses the unification engine
-TcGadt.tcUnifyTys, which doesn't know about mutable type variables.
-
-
-Note [LOOP]
-~~~~~~~~~~~
-	class If b t e r | b t e -> r
-	instance If T t e t
-	instance If F t e e
-	class Lte a b c | a b -> c where lte :: a -> b -> c
-	instance Lte Z b T
-	instance (Lte a b l,If l b a c) => Max a b c
-
-Wanted:	Max Z (S x) y
-
-Then we'll reduce using the Max instance to:
-	(Lte Z (S x) l, If l (S x) Z y)
-and improve by binding l->T, after which we can do some reduction
-on both the Lte and If constraints.  What we *can't* do is start again
-with (Max Z (S x) y)!
-
-
-
-%************************************************************************
-%*									*
-		tcSimplifySuperClasses
-%*									*
-%************************************************************************
-
-Note [SUPERCLASS-LOOP 1]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We have to be very, very careful when generating superclasses, lest we
-accidentally build a loop. Here's an example:
-
-  class S a
-
-  class S a => C a where { opc :: a -> a }
-  class S b => D b where { opd :: b -> b }
-  
-  instance C Int where
-     opc = opd
-  
-  instance D Int where
-     opd = opc
-
-From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
-Simplifying, we may well get:
-	$dfCInt = :C ds1 (opd dd)
-	dd  = $dfDInt
-	ds1 = $p1 dd
-Notice that we spot that we can extract ds1 from dd.  
-
-Alas!  Alack! We can do the same for (instance D Int):
-
-	$dfDInt = :D ds2 (opc dc)
-	dc  = $dfCInt
-	ds2 = $p1 dc
-
-And now we've defined the superclass in terms of itself.
-
-Solution: never generate a superclass selectors at all when
-satisfying the superclass context of an instance declaration.
-
-Two more nasty cases are in
-	tcrun021
-	tcrun033
-
-\begin{code}
-tcSimplifySuperClasses 
-	:: InstLoc 
-	-> [Inst]	-- Given 
-	-> [Inst]	-- Wanted
-	-> TcM TcDictBinds
-tcSimplifySuperClasses loc givens sc_wanteds
-  = do	{ traceTc (text "tcSimplifySuperClasses")
-	; (irreds,binds1,_) <- checkLoop env sc_wanteds
-	; let (tidy_env, tidy_irreds) = tidyInsts irreds
-	; reportNoInstances tidy_env (Just (loc, givens)) tidy_irreds
-	; return binds1 }
-  where
-    env = mkRedEnv (pprInstLoc loc) try_me givens
-    try_me inst = ReduceMe NoSCs
-	-- Like tryHardCheckLoop, but with NoSCs
-\end{code}
-
-
-%************************************************************************
-%*									*
-\subsection{tcSimplifyRestricted}
-%*									*
-%************************************************************************
-
-tcSimplifyRestricted infers which type variables to quantify for a 
-group of restricted bindings.  This isn't trivial.
-
-Eg1:	id = \x -> x
-	We want to quantify over a to get id :: forall a. a->a
-	
-Eg2:	eq = (==)
-	We do not want to quantify over a, because there's an Eq a 
-	constraint, so we get eq :: a->a->Bool	(notice no forall)
-
-So, assume:
-	RHS has type 'tau', whose free tyvars are tau_tvs
-	RHS has constraints 'wanteds'
-
-Plan A (simple)
-  Quantify over (tau_tvs \ ftvs(wanteds))
-  This is bad. The constraints may contain (Monad (ST s))
-  where we have 	instance Monad (ST s) where...
-  so there's no need to be monomorphic in s!
-
-  Also the constraint might be a method constraint,
-  whose type mentions a perfectly innocent tyvar:
-	  op :: Num a => a -> b -> a
-  Here, b is unconstrained.  A good example would be
-	foo = op (3::Int)
-  We want to infer the polymorphic type
-	foo :: forall b. b -> b
-
-
-Plan B (cunning, used for a long time up to and including GHC 6.2)
-  Step 1: Simplify the constraints as much as possible (to deal 
-  with Plan A's problem).  Then set
-	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
-  Step 2: Now simplify again, treating the constraint as 'free' if 
-  it does not mention qtvs, and trying to reduce it otherwise.
-  The reasons for this is to maximise sharing.
-
-  This fails for a very subtle reason.  Suppose that in the Step 2
-  a constraint (Foo (Succ Zero) (Succ Zero) b) gets thrown upstairs as 'free'.
-  In the Step 1 this constraint might have been simplified, perhaps to
-  (Foo Zero Zero b), AND THEN THAT MIGHT BE IMPROVED, to bind 'b' to 'T'.
-  This won't happen in Step 2... but that in turn might prevent some other
-  constraint (Baz [a] b) being simplified (e.g. via instance Baz [a] T where {..}) 
-  and that in turn breaks the invariant that no constraints are quantified over.
-
-  Test typecheck/should_compile/tc177 (which failed in GHC 6.2) demonstrates
-  the problem.
-
-
-Plan C (brutal)
-  Step 1: Simplify the constraints as much as possible (to deal 
-  with Plan A's problem).  Then set
-	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-  Return the bindings from Step 1.
-  
-
-A note about Plan C (arising from "bug" reported by George Russel March 2004)
-Consider this:
-
-      instance (HasBinary ty IO) => HasCodedValue ty
-
-      foo :: HasCodedValue a => String -> IO a
-
-      doDecodeIO :: HasCodedValue a => () -> () -> IO a
-      doDecodeIO codedValue view  
-        = let { act = foo "foo" } in  act
-
-You might think this should work becuase the call to foo gives rise to a constraint
-(HasCodedValue t), which can be satisfied by the type sig for doDecodeIO.  But the
-restricted binding act = ... calls tcSimplifyRestricted, and PlanC simplifies the
-constraint using the (rather bogus) instance declaration, and now we are stuffed.
-
-I claim this is not really a bug -- but it bit Sergey as well as George.  So here's
-plan D
-
-
-Plan D (a variant of plan B)
-  Step 1: Simplify the constraints as much as possible (to deal 
-  with Plan A's problem), BUT DO NO IMPROVEMENT.  Then set
-	qtvs = tau_tvs \ ftvs( simplify( wanteds ) )
-
-  Step 2: Now simplify again, treating the constraint as 'free' if 
-  it does not mention qtvs, and trying to reduce it otherwise.
-
-  The point here is that it's generally OK to have too few qtvs; that is,
-  to make the thing more monomorphic than it could be.  We don't want to
-  do that in the common cases, but in wierd cases it's ok: the programmer
-  can always add a signature.  
-
-  Too few qtvs => too many wanteds, which is what happens if you do less
-  improvement.
-
-
-\begin{code}
-tcSimplifyRestricted 	-- Used for restricted binding groups
-			-- i.e. ones subject to the monomorphism restriction
-	:: SDoc
-	-> TopLevelFlag
-	-> [Name]		-- Things bound in this group
-	-> TcTyVarSet		-- Free in the type of the RHSs
-	-> [Inst]		-- Free in the RHSs
-	-> TcM ([TyVar],	-- Tyvars to quantify (zonked and quantified)
-		TcDictBinds)	-- Bindings
-	-- tcSimpifyRestricted returns no constraints to
-	-- quantify over; by definition there are none.
-	-- They are all thrown back in the LIE
-
-tcSimplifyRestricted doc top_lvl bndrs tau_tvs wanteds
-	-- Zonk everything in sight
-  = do	{ traceTc (text "tcSimplifyRestricted")
-	; wanteds' <- zonkInsts wanteds
-
-   	-- 'ReduceMe': Reduce as far as we can.  Don't stop at
-	-- dicts; the idea is to get rid of as many type
-	-- variables as possible, and we don't want to stop
-	-- at (say) Monad (ST s), because that reduces
-	-- immediately, with no constraint on s.
-	--
-	-- BUT do no improvement!  See Plan D above
-	-- HOWEVER, some unification may take place, if we instantiate
-	-- 	    a method Inst with an equality constraint
-	; let env = mkNoImproveRedEnv doc (\i -> ReduceMe AddSCs)
-	; (_imp, _binds, constrained_dicts, _) <- reduceContext env wanteds'
-
-	-- Next, figure out the tyvars we will quantify over
-	; tau_tvs' <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
-	; gbl_tvs' <- tcGetGlobalTyVars
-	; constrained_dicts' <- zonkInsts constrained_dicts
-
-	; let qtvs1 = tau_tvs' `minusVarSet` oclose (fdPredsOfInsts constrained_dicts) gbl_tvs'
-				-- As in tcSimplifyInfer
-
-		-- Do not quantify over constrained type variables:
-		-- this is the monomorphism restriction
-	      constrained_tvs' = tyVarsOfInsts constrained_dicts'
-	      qtvs = qtvs1 `minusVarSet` constrained_tvs'
-	      pp_bndrs = pprWithCommas (quotes . ppr) bndrs
-
-	-- Warn in the mono
-	; warn_mono <- doptM Opt_WarnMonomorphism
-	; warnTc (warn_mono && (constrained_tvs' `intersectsVarSet` qtvs1))
-		 (vcat[ ptext SLIT("the Monomorphism Restriction applies to the binding")
-				<> plural bndrs <+> ptext SLIT("for") <+> pp_bndrs,
-			ptext SLIT("Consider giving a type signature for") <+> pp_bndrs])
-
-	; traceTc (text "tcSimplifyRestricted" <+> vcat [
-		pprInsts wanteds, pprInsts constrained_dicts',
-		ppr _binds,
-		ppr constrained_tvs', ppr tau_tvs', ppr qtvs ])
-
-	-- The first step may have squashed more methods than
-	-- necessary, so try again, this time more gently, knowing the exact
-	-- set of type variables to quantify over.
-	--
-	-- We quantify only over constraints that are captured by qtvs;
-	-- these will just be a subset of non-dicts.  This in contrast
-	-- to normal inference (using isFreeWhenInferring) in which we quantify over
-	-- all *non-inheritable* constraints too.  This implements choice
-	-- (B) under "implicit parameter and monomorphism" above.
-	--
-	-- Remember that we may need to do *some* simplification, to
-	-- (for example) squash {Monad (ST s)} into {}.  It's not enough
-	-- just to float all constraints
-	--
-	-- At top level, we *do* squash methods becuase we want to 
-	-- expose implicit parameters to the test that follows
-	; let is_nested_group = isNotTopLevel top_lvl
-	      try_me inst | isFreeWrtTyVars qtvs inst,
-			   (is_nested_group || isDict inst) = Stop
-		          | otherwise  	         = ReduceMe AddSCs
-	      env = mkNoImproveRedEnv doc try_me
-	; (_imp, binds, irreds, _) <- reduceContext env wanteds'
-
-	-- See "Notes on implicit parameters, Question 4: top level"
-	; ASSERT( all (isFreeWrtTyVars qtvs) irreds )	-- None should be captured
-	  if is_nested_group then
-		extendLIEs irreds
-	  else do { let (bad_ips, non_ips) = partition isIPDict irreds
-		  ; addTopIPErrs bndrs bad_ips
-		  ; extendLIEs non_ips }
-
-	; qtvs' <- zonkQuantifiedTyVars (varSetElems qtvs)
-	; return (qtvs', binds) }
-\end{code}
-
-
-%************************************************************************
-%*									*
-		tcSimplifyRuleLhs
-%*									*
-%************************************************************************
+Note [Simplifying RULE lhs constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+On the LHS of transformation rules we only simplify only equalities,
+but not dictionaries.  We want to keep dictionaries unsimplified, to
+serve as the available stuff for the RHS of the rule.  We *do* want to
+simplify equalities, however, to detect ill-typed rules that cannot be
+applied.
 
-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.
+Implementation: the TcSFlags carried by the TcSMonad controls the
+amount of simplification, so simplifyRuleLhs just sets the flag
+appropriately.
 
 Example.  Consider the following left-hand side of a rule
-	
 	f (x == y) (y > z) = ...
-
 If we typecheck this expression we get constraints
-
 	d1 :: Ord a, d2 :: Eq a
-
 We do NOT want to "simplify" to the LHS
-
 	forall x::a, y::a, z::a, d1::Ord a.
 	  f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-
 Instead we want	
-
 	forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
 	  f ((==) d2 x y) ((>) d1 y z) = ...
 
 Here is another example:
-
 	fromIntegral :: (Integral a, Num b) => a -> b
 	{-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
-
 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
 we *dont* want to get
-
 	forall dIntegralInt.
 	   fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-
 because the scsel will mess up RULE matching.  Instead we want
-
 	forall dIntegralInt, dNumInt.
 	  fromIntegral Int Int dIntegralInt dNumInt = id Int
 
 Even if we have 
-
 	g (x == y) (y == z) = ..
-
 where the two dictionaries are *identical*, we do NOT WANT
-
 	forall x::a, y::a, z::a, d1::Eq a
 	  f ((==) d1 x y) ((>) d1 y z) = ...
-
 because that will only match if the dict args are (visibly) equal.
 Instead we want to quantify over the dictionaries separately.
 
-In short, tcSimplifyRuleLhs must *only* squash LitInst and MethInts, leaving
-all dicts unchanged, with absolutely no sharing.  It's simpler to do this
-from scratch, rather than further parameterise simpleReduceLoop etc
-
-\begin{code}
-tcSimplifyRuleLhs :: [Inst] -> TcM ([Inst], TcDictBinds)
-tcSimplifyRuleLhs wanteds
-  = go [] emptyBag wanteds
-  where
-    go dicts binds []
-	= return (dicts, binds)
-    go dicts binds (w:ws)
-	| isDict w
-	= go (w:dicts) binds ws
-	| otherwise
-	= do { w' <- zonkInst w  -- So that (3::Int) does not generate a call
-				 -- to fromInteger; this looks fragile to me
-	     ; lookup_result <- lookupSimpleInst w'
-	     ; case lookup_result of
-		 GenInst ws' rhs -> 
-                   go dicts (addInstToDictBind binds w rhs) (ws' ++ ws)
-		 NoInstance	 -> pprPanic "tcSimplifyRuleLhs" (ppr w)
-	  }
-\end{code}
-
-tcSimplifyBracket is used when simplifying the constraints arising from
-a Template Haskell bracket [| ... |].  We want to check that there aren't
-any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
-Show instance), but we aren't otherwise interested in the results.
-Nor do we care about ambiguous dictionaries etc.  We will type check
-this bracket again at its usage site.
-
-\begin{code}
-tcSimplifyBracket :: [Inst] -> TcM ()
-tcSimplifyBracket wanteds
-  = do	{ tryHardCheckLoop doc wanteds
-	; return () }
-  where
-    doc = text "tcSimplifyBracket"
-\end{code}
-
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.  
 
-%************************************************************************
-%*									*
-\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.
-
-Actually, the constraints from B might improve the types in ?x. For example
-
-	f :: (?x::Int) => Char -> Char
-	let ?x = 3 in f 'c'
-
-then the constraint (?x::Int) arising from the call to f will
-force the binding for ?x to be of type Int.
-
-\begin{code}
-tcSimplifyIPs :: [Inst]		-- The implicit parameters bound here
-	      -> [Inst]		-- Wanted
-	      -> TcM TcDictBinds
-	-- We need a loop so that we do improvement, and then
-	-- (next time round) generate a binding to connect the two
-	-- 	let ?x = e in ?x
-	-- Here the two ?x's have different types, and improvement 
-	-- makes them the same.
-
-tcSimplifyIPs given_ips wanteds
-  = do	{ wanteds'   <- zonkInsts wanteds
-	; given_ips' <- zonkInsts given_ips
-		-- Unusually for checking, we *must* zonk the given_ips
-
-	; let env = mkRedEnv doc try_me given_ips'
-	; (improved, binds, irreds, _) <- reduceContext env wanteds'
-
-	; if not improved then 
-		ASSERT( all is_free irreds )
-		do { extendLIEs irreds
-		   ; return binds }
-	  else
-		tcSimplifyIPs given_ips wanteds }
-  where
-    doc	   = text "tcSimplifyIPs" <+> ppr given_ips
-    ip_set = mkNameSet (ipNamesOfInsts given_ips)
-    is_free inst = isFreeWrtIPs ip_set inst
-
-	-- Simplify any methods that mention the implicit parameter
-    try_me inst | is_free inst = Stop
-		| otherwise    = ReduceMe NoSCs
-\end{code}
-
-
-%************************************************************************
-%*									*
-\subsection[binds-for-local-funs]{@bindInstsOfLocalFuns@}
-%*									*
-%************************************************************************
-
-When doing a binding group, we may have @Insts@ of local functions.
-For example, we might have...
-\begin{verbatim}
-let f x = x + 1	    -- orig local function (overloaded)
-    f.1 = f Int	    -- two instances of f
-    f.2 = f Float
- in
-    (f.1 5, f.2 6.7)
-\end{verbatim}
-The point is: we must drop the bindings for @f.1@ and @f.2@ here,
-where @f@ is in scope; those @Insts@ must certainly not be passed
-upwards towards the top-level.	If the @Insts@ were binding-ified up
-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 @HsBinds@ generated.
-
-\begin{code}
-bindInstsOfLocalFuns ::	[Inst] -> [TcId] -> TcM TcDictBinds
--- Simlifies only MethodInsts, and generate only bindings of form 
---	fm = f tys dicts
--- We're careful not to even generate bindings of the form
---	d1 = d2
--- You'd think that'd be fine, but it interacts with what is
--- arguably a bug in Match.tidyEqnInfo (see notes there)
-
-bindInstsOfLocalFuns wanteds local_ids
-  | null overloaded_ids
-	-- Common case
-  = extendLIEs wanteds		`thenM_`
-    returnM emptyLHsBinds
-
-  | otherwise
-  = do	{ (irreds, binds,_) <- checkLoop env for_me
-	; extendLIEs not_for_me	
-	; extendLIEs irreds
-	; return binds }
-  where
-    env = mkRedEnv doc try_me []
-    doc		     = text "bindInsts" <+> ppr local_ids
-    overloaded_ids   = filter is_overloaded local_ids
-    is_overloaded id = isOverloadedTy (idType id)
-    (for_me, not_for_me) = partition (isMethodFor overloaded_set) wanteds
-
-    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 | isMethod inst = ReduceMe NoSCs
-		| otherwise	= Stop
-\end{code}
-
-
-%************************************************************************
-%*									*
-\subsection{Data types for the reduction mechanism}
-%*									*
-%************************************************************************
-
-The main control over context reduction is here
+HOWEVER, under a nested implication things are different
+Consider
+  f :: (forall a. Eq a => a->a) -> Bool -> ...
+  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
+       f b True = ...
+    #=}
+Here we *must* solve the wanted (Eq a) from the given (Eq a)
+resulting from skolemising the agument type of g.  So we 
+revert to SimplCheck when going under an implication.  
 
 \begin{code}
-data RedEnv 
-  = RedEnv { red_doc	:: SDoc			-- The context
-	   , red_try_me :: Inst -> WhatToDo
-	   , red_improve :: Bool		-- True <=> do improvement
-	   , red_givens :: [Inst]		-- All guaranteed rigid
-						-- Always dicts
-						-- but see Note [Rigidity]
-	   , red_stack  :: (Int, [Inst])	-- Recursion stack (for err msg)
-						-- See Note [RedStack]
-  }
-
--- Note [Rigidity]
--- The red_givens are rigid so far as cmpInst is concerned.
--- There is one case where they are not totally rigid, namely in tcSimplifyIPs
---	let ?x = e in ...
--- Here, the given is (?x::a), where 'a' is not necy a rigid type
--- But that doesn't affect the comparison, which is based only on mame.
-
--- Note [RedStack]
--- The red_stack pair (n,insts) pair is just used for error reporting.
--- 'n' is always the depth of the stack.
--- The 'insts' 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.
-
-
-mkRedEnv :: SDoc -> (Inst -> WhatToDo) -> [Inst] -> RedEnv
-mkRedEnv doc try_me givens
-  = RedEnv { red_doc = doc, red_try_me = try_me,
-	     red_givens = givens, red_stack = (0,[]),
-	     red_improve = True }	
-
-mkNoImproveRedEnv :: SDoc -> (Inst -> WhatToDo) -> RedEnv
--- Do not do improvement; no givens
-mkNoImproveRedEnv doc try_me
-  = RedEnv { red_doc = doc, red_try_me = try_me,
-	     red_givens = [], red_stack = (0,[]),
-	     red_improve = True }	
-
-data WhatToDo
- = ReduceMe WantSCs	-- Try to reduce this
-			-- If there's no instance, add the inst to the 
-			-- irreductible ones, but don't produce an error 
-			-- message of any kind.
-			-- It might be quite legitimate such as (Eq a)!
-
- | Stop		-- Return as irreducible unless it can
-			-- be reduced to a constant in one step
-			-- Do not add superclasses; see 
-
-data WantSCs = NoSCs | AddSCs	-- Tells whether we should add the superclasses
-				-- of a predicate when adding it to the avails
-	-- The reason for this flag is entirely the super-class loop problem
-	-- Note [SUPER-CLASS LOOP 1]
-
-zonkRedEnv :: RedEnv -> TcM RedEnv
-zonkRedEnv env 
-  = do { givens' <- mappM zonkInst (red_givens env)
-       ; return $ env {red_givens = givens'}
-       }
+simplifyRule :: RuleName 
+             -> [TcTyVar]		-- Explicit skolems
+             -> WantedConstraints	-- Constraints from LHS
+             -> WantedConstraints	-- Constraints from RHS
+             -> TcM ([EvVar], 		-- LHS dicts
+                     TcEvBinds,		-- Evidence for LHS
+                     TcEvBinds)		-- Evidence for RHS
+-- See Note [Simplifying RULE lhs constraints]
+simplifyRule name tv_bndrs lhs_wanted rhs_wanted
+  = do { loc        <- getCtLoc (RuleSkol name)
+       ; zonked_lhs <- zonkWC lhs_wanted
+       ; let untch = NoUntouchables
+	     	 -- We allow ourselves to unify environment 
+		 -- variables; hence *no untouchables*
+
+       ; (lhs_results, lhs_binds)
+              <- runTcS (SimplRuleLhs name) untch $
+                 solveWanteds emptyInert zonked_lhs
+
+       ; traceTc "simplifyRule" $
+         vcat [ text "zonked_lhs"   <+> ppr zonked_lhs 
+              , text "lhs_results" <+> ppr lhs_results
+              , text "lhs_binds"    <+> ppr lhs_binds 
+              , text "rhs_wanted"   <+> ppr rhs_wanted ]
+
+
+       -- Don't quantify over equalities (judgement call here)
+       ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
+                                         (wc_flat lhs_results)
+             lhs_dicts    = map evVarOf (bagToList dicts)
+                                 -- Dicts and implicit parameters
+
+           -- Fail if we have not got down to unsolved flats
+       ; ev_binds_var <- newTcEvBinds
+       ; emitImplication $ Implic { ic_untch  = untch
+                                  , ic_env    = emptyNameEnv
+                                  , ic_skols  = mkVarSet tv_bndrs
+                                  , ic_given  = lhs_dicts
+                                  , ic_wanted = lhs_results { wc_flat = eqs }
+                                  , ic_insol  = insolubleWC lhs_results
+                                  , ic_binds  = ev_binds_var
+                                  , ic_loc    = loc }
+
+	     -- Notice that we simplify the RHS with only the explicitly
+	     -- introduced skolems, allowing the RHS to constrain any 
+	     -- unification variables.
+	     -- Then, and only then, we call zonkQuantifiedTypeVariables
+	     -- Example   foo :: Ord a => a -> a
+	     --		  foo_spec :: Int -> Int
+	     --		  {-# RULE "foo"  foo = foo_spec #-}
+	     --	    Here, it's the RHS that fixes the type variable
+
+	     -- So we don't want to make untouchable the type
+	     -- variables in the envt of the RHS, because they include
+	     -- the template variables of the RULE
+
+	     -- Hence the rather painful ad-hoc treatement here
+       ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
+       ; let doc = ptext (sLit "rhs of rule") <+> doubleQuotes (ftext name)
+       ; rhs_binds1 <- simplifyCheck (SimplCheck doc) $
+            WC { wc_flat = emptyBag
+               , wc_insol = emptyBag
+               , wc_impl = unitBag $
+                    Implic { ic_untch   = NoUntouchables
+                            , ic_env    = emptyNameEnv
+                            , ic_skols  = mkVarSet tv_bndrs
+                            , ic_given  = lhs_dicts
+                            , ic_wanted = rhs_wanted
+                            , ic_insol  = insolubleWC rhs_wanted
+                            , ic_binds  = rhs_binds_var
+                            , ic_loc    = loc } }
+       ; rhs_binds2 <- readTcRef evb_ref
+
+       ; return ( lhs_dicts
+                , EvBinds lhs_binds 
+                , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
 \end{code}
 
 
-%************************************************************************
-%*									*
-\subsection[reduce]{@reduce@}
-%*									*
-%************************************************************************
-
-Note [Ancestor Equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-During context reduction, we add to the wanted equalities also those
-equalities that (transitively) occur in superclass contexts of wanted
-class constraints.  Consider the following code
-
-  class a ~ Int => C a
-  instance C Int
-
-If (C a) is wanted, we want to add (a ~ Int), which will be discharged by
-substituting Int for a.  Hence, we ultimately want (C Int), which we
-discharge with the explicit instance.
+*********************************************************************************
+*                                                                                 * 
+*                                 Main Simplifier                                 *
+*                                                                                 *
+***********************************************************************************
 
 \begin{code}
-reduceContext :: RedEnv
-	      -> [Inst]			-- Wanted
-	      -> TcM (ImprovementDone,
-		      TcDictBinds,	-- Dictionary bindings
-		      [Inst],		-- Irreducible
-		      [Inst])		-- Needed givens
-
-reduceContext env wanteds
-  = do	{ traceTc (text "reduceContext" <+> (vcat [
-	     text "----------------------",
-	     red_doc env,
-	     text "given" <+> ppr (red_givens env),
-	     text "wanted" <+> ppr wanteds,
-	     text "----------------------"
-	     ]))
-
-	; let givens 		 	  = red_givens env
-	      (given_eqs0, given_dicts0)  = partition isEqInst givens
-	      (wanted_eqs0, wanted_dicts) = partition isEqInst wanteds
-
-          -- We want to add as wanted equalities those that (transitively) 
-          -- occur in superclass contexts of wanted class constraints.
-          -- See Note [Ancestor Equalities]
-	; ancestor_eqs <- ancestorEqualities wanted_dicts
-        ; let wanted_eqs = wanted_eqs0 ++ ancestor_eqs
-	; traceTc $ text "reduceContext: ancestor eqs" <+> ppr ancestor_eqs
-
-	  -- 1. Normalise the *given* *equality* constraints
-	; (given_eqs, eliminate_skolems) <- normaliseGivenEqs given_eqs0
-
-	  -- 2. Normalise the *given* *dictionary* constraints
-	  --    wrt. the toplevel and given equations
-	; (given_dicts, given_binds) <- normaliseGivenDicts given_eqs 
-                                                            given_dicts0
-
-	  -- 3. Solve the *wanted* *equation* constraints
-	; eq_irreds0 <- solveWantedEqs given_eqs wanted_eqs 
-
-	  -- 4. Normalise the *wanted* equality constraints with respect to
-	  --    each other 
-	; eq_irreds <- normaliseWantedEqs eq_irreds0
-
-          -- 5. Build the Avail mapping from "given_dicts"
-	; init_state <- foldlM addGiven emptyAvails given_dicts
-
-          -- 6. Solve the *wanted* *dictionary* constraints
-	  --    This may expose some further equational constraints...
-	; wanted_dicts' <- zonkInsts wanted_dicts
-	; avails <- reduceList env wanted_dicts' init_state
-	; (binds, irreds0, needed_givens) <- extractResults avails wanted_dicts'
-	; traceTc $ text "reduceContext extractresults" <+> vcat
-		      [ppr avails,ppr wanted_dicts',ppr binds,ppr needed_givens]
-
-	  -- 7. Normalise the *wanted* *dictionary* constraints
-	  --    wrt. the toplevel and given equations
-	; (irreds1,normalise_binds1) <- normaliseWantedDicts given_eqs irreds0
-
-	  -- 8. Substitute the wanted *equations* in the wanted *dictionaries*
-	; (irreds,normalise_binds2) <- substEqInDictInsts eq_irreds irreds1
-		
-	  -- 9. eliminate the artificial skolem constants introduced in 1.
-	; eliminate_skolems	
-
-	  -- If there was some FD improvement,
-	  -- or new wanted equations have been exposed,
-	  -- we should have another go at solving.
-	; let improved = availsImproved avails 
-			 || (not $ isEmptyBag normalise_binds1)
-			 || (not $ isEmptyBag normalise_binds2)
-			 || (any isEqInst irreds)
-
-	; traceTc (text "reduceContext end" <+> (vcat [
-	     text "----------------------",
-	     red_doc env,
-	     text "given" <+> ppr (red_givens env),
-	     text "wanted" <+> ppr wanteds,
-	     text "----",
-	     text "avails" <+> pprAvails avails,
-	     text "improved =" <+> ppr improved,
-	     text "irreds = " <+> ppr irreds,
-	     text "binds = " <+> ppr binds,
-	     text "needed givens = " <+> ppr needed_givens,
-	     text "----------------------"
-	     ]))
-
-	; return (improved, 
-                  given_binds `unionBags` normalise_binds1 
-                              `unionBags` normalise_binds2 
-                              `unionBags` binds, 
-                  irreds ++ eq_irreds, 
-                  needed_givens) 
-        }
-
-tcImproveOne :: Avails -> Inst -> TcM ImprovementDone
-tcImproveOne avails inst
-  | not (isDict inst) = return False
-  | otherwise
-  = do	{ inst_envs <- tcGetInstEnvs
-	; let eqns = improveOne (classInstances inst_envs)
-				(dictPred inst, pprInstArising inst)
-				[ (dictPred p, pprInstArising p)
-				| p <- availsInsts avails, isDict p ]
-		-- 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
-	; traceTc (text "improveOne" <+> ppr inst)
-	; unifyEqns eqns }
-
-unifyEqns :: [(Equation,(PredType,SDoc),(PredType,SDoc))] 
-	  -> TcM ImprovementDone
-unifyEqns [] = return False
-unifyEqns eqns
-  = do	{ traceTc (ptext SLIT("Improve:") <+> vcat (map pprEquationDoc eqns))
-        ; mappM_ unify eqns
-	; return True }
-  where
-    unify ((qtvs, pairs), what1, what2)
-	 = addErrCtxtM (mkEqnMsg what1 what2)	$
-	   tcInstTyVars (varSetElems qtvs)	`thenM` \ (_, _, tenv) ->
-	   mapM_ (unif_pr tenv) pairs
-    unif_pr tenv (ty1,ty2) =  unifyType (substTy tenv ty1) (substTy tenv ty2)
-
-pprEquationDoc (eqn, (p1,w1), (p2,w2)) = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
-
-mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
-  = do	{ pred1' <- zonkTcPredType pred1; pred2' <- zonkTcPredType pred2
-	; let { pred1'' = tidyPred tidy_env pred1'; pred2'' = tidyPred tidy_env pred2' }
-	; let msg = vcat [ptext SLIT("When using functional dependencies to combine"),
-			  nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
-			  nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
-	; return (tidy_env, msg) }
-\end{code}
-
-The main context-reduction function is @reduce@.  Here's its game plan.
+simplifyCheck :: SimplContext
+	      -> WantedConstraints	-- Wanted
+              -> TcM (Bag EvBind)
+-- Solve a single, top-level implication constraint
+-- e.g. typically one created from a top-level type signature
+-- 	    f :: forall a. [a] -> [a]
+--          f x = rhs
+-- We do this even if the function has no polymorphism:
+--    	    g :: Int -> Int
+
+--          g y = rhs
+-- (whereas for *nested* bindings we would not create
+--  an implication constraint for g at all.)
+--
+-- Fails if can't solve something in the input wanteds
+simplifyCheck ctxt wanteds
+  = do { wanteds <- zonkWC wanteds
+
+       ; traceTc "simplifyCheck {" (vcat
+             [ ptext (sLit "wanted =") <+> ppr wanteds ])
+
+       ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
+                                 solveWanteds emptyInert wanteds
+
+       ; traceTc "simplifyCheck }" $
+         ptext (sLit "unsolved =") <+> ppr unsolved
+
+       ; reportUnsolved unsolved
+
+       ; return ev_binds }
+
+----------------
+solveWanteds :: InertSet                            -- Given
+             -> WantedConstraints
+             -> TcS WantedConstraints
+solveWanteds inert wanted
+  = do { (unsolved_flats, unsolved_implics, insols)
+             <- solve_wanteds inert wanted
+       ; return (WC { wc_flat = keepWanted unsolved_flats   -- Discard Derived
+                    , wc_impl = unsolved_implics
+                    , wc_insol = insols }) }
+
+solve_wanteds :: InertSet                            -- Given
+              -> WantedConstraints
+              -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
+-- solve_wanteds iterates when it is able to float equalities
+-- out of one or more of the implications
+solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
+  = do { traceTcS "solveWanteds {" (ppr wanted)
+
+                 -- Try the flat bit
+                 -- Discard from insols all the derived/given constraints
+                 -- because they will show up again when we try to solve
+                 -- everything else.  Solving them a second time is a bit
+                 -- of a waste, but the code is simple, and the program is
+                 -- wrong anyway!
+       ; let all_flats = flats `unionBags` keepWanted insols
+       ; inert1 <- solveInteractWanted inert (bagToList all_flats)
+
+       ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
+
+       ; bb <- getTcEvBindsBag
+       ; tb <- getTcSTyBindsMap
+       ; traceTcS "solveWanteds }" $
+                 vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
+                      , text "unsolved_implics =" <+> ppr unsolved_implics
+                      , text "current evbinds  =" <+> vcat (map ppr (varEnvElts bb))
+                      , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
+                      ]
+
+       ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
+                -- See Note [Solving Family Equations]
+                -- NB: remaining_flats has already had subst applied
+
+       ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
+
+       ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
+                , mapBag (substImplication subst) unsolved_implics
+                , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
 
-\begin{code}
-reduceList :: RedEnv -> [Inst] -> Avails -> TcM Avails
-reduceList env@(RedEnv {red_stack = (n,stk)}) wanteds state
-  = do 	{ dopts <- getDOpts
-#ifdef DEBUG
-	; if n > 8 then
-		dumpTcRn (hang (ptext SLIT("Interesting! Context reduction stack depth") <+> int n) 
-			     2 (ifPprDebug (nest 2 (pprStack stk))))
-	  else return ()
-#endif
-	; if n >= ctxtStkDepth dopts then
-	    failWithTc (reduceDepthErr n stk)
-	  else
-	    go wanteds state }
   where
-    go []     state = return state
-    go (w:ws) state = do { traceTc (text "reduceList " <+> ppr (w:ws) <+> ppr state)
-			 ; state' <- reduce (env {red_stack = (n+1, w:stk)}) w state
-			 ; go ws state' }
-
-    -- Base case: we're done!
-reduce env wanted avails
-    -- It's the same as an existing inst, or a superclass thereof
-  | Just avail <- findAvail avails wanted
-  = do { traceTc (text "reduce: found " <+> ppr wanted)
-       ; returnM avails	
-       }
-
-  | otherwise
-  = do	{ traceTc (text "reduce" <+> ppr avails <+> ppr wanted)
-	; case red_try_me env wanted of {
-	    Stop -> try_simple (addIrred NoSCs);
-			-- See Note [No superclasses for Stop]
-
-	    ReduceMe want_scs -> do	-- It should be reduced
-		{ (avails, lookup_result) <- reduceInst env avails wanted
-		; case lookup_result of
-		    NoInstance -> addIrred want_scs avails wanted
-			     -- Add it and its superclasses
-		    	     
-		    GenInst [] rhs -> addWanted want_scs avails wanted rhs []
-
-		    GenInst wanteds' rhs 
-			  -> do	{ avails1 <- addIrred NoSCs avails wanted
-				; avails2 <- reduceList env wanteds' avails1
-				; addWanted want_scs avails2 wanted rhs wanteds' } }
-		-- Temporarily do addIrred *before* the reduceList, 
-		-- which has the effect of adding the thing we are trying
-		-- to prove to the database before trying to prove the things it
-		-- needs.  See note [RECURSIVE DICTIONARIES]
-		-- NB: we must not do an addWanted before, because that adds the
-		--     superclasses too, and that can lead to a spurious loop; see
-		--     the examples in [SUPERCLASS-LOOP]
-		-- So we do an addIrred before, and then overwrite it afterwards with addWanted
-    } }
+    simpl_loop :: Int
+               -> InertSet
+               -> Bag Implication
+               -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
+    simpl_loop n inert implics
+      | n>10
+      = trace "solveWanteds: loop" $	                -- Always bleat
+        do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
+           ; let (_, unsolved_cans) = extractUnsolved inert
+           ; return (unsolved_cans, implics) }
+
+      | otherwise
+      = do { traceTcS "solveWanteds: simpl_loop start {" $
+                 vcat [ text "n =" <+> ppr n
+                      , text "implics =" <+> ppr implics
+                      , text "inert   =" <+> ppr inert ]
+           
+           ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
+                     -- unsolved_cans contains either Wanted or Derived!
+
+           ; (implic_eqs, unsolved_implics) 
+                  <- solveNestedImplications just_given_inert unsolved_cans implics
+
+                -- Apply defaulting rules if and only if there
+		-- no floated equalities.  If there are, they may
+		-- solve the remaining wanteds, so don't do defaulting.
+           ; improve_eqs <- if not (isEmptyBag implic_eqs)
+			    then return implic_eqs
+                            else applyDefaultingRules just_given_inert unsolved_cans
+
+           ; traceTcS "solveWanteds: simpl_loop end }" $
+                 vcat [ text "improve_eqs      =" <+> ppr improve_eqs
+                      , text "unsolved_flats   =" <+> ppr unsolved_cans
+                      , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
+           ; (improve_eqs_already_in_inert, inert_with_improvement)
+               <- solveInteract inert improve_eqs 
+
+           ; if improve_eqs_already_in_inert then
+                 return (unsolved_cans, unsolved_implics)
+             else 
+                 simpl_loop (n+1) inert_with_improvement 
+                                         -- Contain unsolved_cans and the improve_eqs
+                                  unsolved_implics
+           }
+
+givensFromWanteds :: SimplContext -> CanonicalCts -> Bag FlavoredEvVar
+-- Extract the Wanted ones from CanonicalCts and conver to
+-- Givens; not Given/Solved, see Note [Preparing inert set for implications]
+givensFromWanteds _ctxt = foldrBag getWanted emptyBag
   where
-  	-- First, see if the inst can be reduced to a constant in one step
-	-- Works well for literals (1::Int) and constant dictionaries (d::Num Int)
-	-- Don't bother for implication constraints, which take real work
-    try_simple do_this_otherwise
-      = do { res <- lookupSimpleInst wanted
-	   ; case res of
-	        GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
-	        other	       -> do_this_otherwise avails wanted }
-\end{code}
-
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-But the above isn't enough.  Suppose 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] from Ord [a], and then add the
-superclasses of C [a] to avails.  But we must not overwrite the binding
-for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
-build a loop! 
-
-Here's another variant, immortalised in tcrun020
-	class Monad m => C1 m
-	class C1 m => C2 m x
-	instance C2 Maybe Bool
-For the instance decl we need to build (C1 Maybe), and it's no good if
-we run around and add (C2 Maybe Bool) and its superclasses to the avails 
-before we search for C1 Maybe.
-
-Here's another example 
- 	class Eq b => Foo a b
-	instance Eq a => Foo [a] a
-If we are reducing
-	(Foo [t] t)
-
-we'll first deduce that it holds (via the instance decl).  We must not
-then overwrite the Eq t constraint with a superclass selection!
-
-At first I had a gross hack, whereby I simply did not add superclass constraints
-in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
-becuase it lost legitimate superclass sharing, and it still didn't do the job:
-I found a very obscure program (now tcrun021) in which improvement meant the
-simplifier got two bites a the cherry... so something seemed to be an Stop
-first time, but reducible next time.
-
-Now we implement the Right Solution, which is to check for loops directly 
-when adding superclasses.  It's a bit like the occurs check in unification.
-
-
-Note [RECURSIVE DICTIONARIES]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider 
-    data D r = ZeroD | SuccD (r (D r));
-    
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-    
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])).  Here's how we go:
-
-	d1 : Eq (D [])
-
-by instance decl, holds if
-	d2 : Eq [D []]
-	where 	d1 = dfEqD d2
-
-by instance decl of Eq, holds if
-	d3 : D []
-	where	d2 = dfEqList d3
-		d1 = dfEqD d2
-
-But now we can "tie the knot" to give
-
-	d3 = d1
-	d2 = dfEqList d3
-	d1 = dfEqD d2
-
-and it'll even run!  The trick is to put the thing we are trying to prove
-(in this case Eq (D []) into the database before trying to prove its
-contributing clauses.
-	
-
-%************************************************************************
-%*									*
-		Reducing a single constraint
-%*									*
-%************************************************************************
-
-\begin{code}
----------------------------------------------
-reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst env avails (ImplicInst { tci_tyvars = tvs, tci_reft = reft, tci_loc = loc,
-				    tci_given = extra_givens, tci_wanted = wanteds })
-  = reduceImplication env avails reft tvs extra_givens wanteds loc
-
-reduceInst env avails other_inst
-  = do	{ result <- lookupSimpleInst other_inst
-	; return (avails, result) }
-\end{code}
-
-Note [Equational Constraints in Implication Constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-An equational constraint is of the form 
-	Given => Wanted 
-where Given and Wanted may contain both equational and dictionary
-constraints. The delay and reduction of these two kinds of constraints
-is distinct:
-
--) In the generated code, wanted Dictionary constraints are wrapped up in an
-   implication constraint that is created at the code site where the wanted
-   dictionaries can be reduced via a let-binding. This let-bound implication
-   constraint is deconstructed at the use-site of the wanted dictionaries.
-
--) While the reduction of equational constraints is also delayed, the delay
-   is not manifest in the generated code. The required evidence is generated
-   in the code directly at the use-site. There is no let-binding and deconstruction
-   necessary. The main disadvantage is that we cannot exploit sharing as the
-   same evidence may be generated at multiple use-sites. However, this disadvantage
-   is limited because it only concerns coercions which are erased.
-
-The different treatment is motivated by the different in representation. Dictionary
-constraints require manifest runtime dictionaries, while equations require coercions
-which are types.
-
-\begin{code}
----------------------------------------------
-reduceImplication :: RedEnv
-		 -> Avails
-		 -> Refinement	-- May refine the givens; often empty
-		 -> [TcTyVar]	-- Quantified type variables; all skolems
-		 -> [Inst]	-- Extra givens; all rigid
-		 -> [Inst]	-- Wanted
-		 -> InstLoc
-		 -> TcM (Avails, LookupInstResult)
-\end{code}
-
-Suppose we are simplifying the constraint
-	forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens',
-and refinment 'reft'.
-
-Note that
-  * The refinement is often empty
-
-  * The 'extra givens' need not mention any of the quantified type variables
-	e.g. 	forall {}. Eq a => Eq [a]
-		forall {}. C Int => D (Tree Int)
-
-    This happens when you have something like
-	data T a where
-	  T1 :: Eq a => a -> T a
-
-	f :: T a -> Int
-	f x = ...(case x of { T1 v -> v==v })...
-
-\begin{code}
-	-- ToDo: should we instantiate tvs?  I think it's not necessary
-	--
-	-- Note on coercion variables:
-	--
-	--	The extra given coercion variables are bound at two different sites:
-	--	-) in the creation context of the implication constraint	
-	--		the solved equational constraints use these binders
-	--
-	--	-) at the solving site of the implication constraint
-	--		the solved dictionaries use these binders		
-	--		these binders are generated by reduceImplication
-	--
-reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
-  = do	{ 	-- Add refined givens, and the extra givens
-		-- Todo fix this 
-	  (refined_red_givens,refined_avails)
-		<- if isEmptyRefinement reft then return (red_givens env,orig_avails)
-		   else foldlM (addRefinedGiven reft) ([],orig_avails) (red_givens env)
-
-		-- Solve the sub-problem
-	; let try_me inst = ReduceMe AddSCs	-- Note [Freeness and implications]
-	      env' = env { red_givens = refined_red_givens ++ extra_givens ++ availsInsts orig_avails
-			 , red_try_me = try_me }
-
-	; traceTc (text "reduceImplication" <+> vcat
-			[ ppr orig_avails,
-			  ppr (red_givens env), ppr extra_givens, 
-			  ppr reft, ppr wanteds])
-	; (irreds,binds,needed_givens0) <- checkLoop env' wanteds
-        ; let needed_givens1 = [ng | ng <- needed_givens0, notElem ng extra_givens]
-
-		-- Note [Reducing implication constraints]
-		-- Tom -- update note, put somewhere!
-
-	; traceTc (text "reduceImplication result" <+> vcat
-			[ppr irreds, ppr binds, ppr needed_givens1])
--- 	; avails <- reduceList env' wanteds avails
+    getWanted :: CanonicalCt -> Bag FlavoredEvVar -> Bag FlavoredEvVar
+    getWanted cc givens
+      | pushable_wanted cc
+      = let given = mkEvVarX (cc_id cc) (mkGivenFlavor (cc_flavor cc) UnkSkol)
+        in given `consBag` givens     -- and not mkSolvedFlavor,
+                                      -- see Note [Preparing inert set for implications]
+      | otherwise = givens
+
+    pushable_wanted :: CanonicalCt -> Bool 
+    pushable_wanted cc 
+      | not (isCFrozenErr cc) 
+      , isWantedCt cc 
+      = isEqPred (evVarPred (cc_id cc)) -- see Note [Preparing inert set for implications]
+      | otherwise = False 
+ 
+solveNestedImplications :: InertSet -> CanonicalCts
+                        -> Bag Implication
+                        -> TcS (Bag FlavoredEvVar, Bag Implication)
+solveNestedImplications just_given_inert unsolved_cans implics
+  | isEmptyBag implics
+  = return (emptyBag, emptyBag)
+  | otherwise 
+  = do {  -- See Note [Preparing inert set for implications]
+	  -- Push the unsolved wanteds inwards, but as givens
+             
+       ; simpl_ctx <- getTcSContext 
+
+       ; let pushed_givens    = givensFromWanteds simpl_ctx unsolved_cans
+             tcs_untouchables = filterVarSet isFlexiTcsTv $
+                                tyVarsOfEvVarXs pushed_givens
+             -- See Note [Extra TcsTv untouchables]
+
+       ; traceTcS "solveWanteds: preparing inerts for implications {"  
+                  (vcat [ppr tcs_untouchables, ppr pushed_givens])
+
+       ; (_, inert_for_implics) <- solveInteract just_given_inert pushed_givens 
+
+       ; traceTcS "solveWanteds: } now doing nested implications {" $
+         vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
+              , text "implics =" <+> ppr implics ]
+
+       ; (implic_eqs, unsolved_implics)
+           <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
+
+       ; traceTcS "solveWanteds: done nested implications }" $
+                  vcat [ text "implic_eqs ="       <+> ppr implic_eqs
+                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
+
+       ; return (implic_eqs, unsolved_implics) }
+
+solveImplication :: TcTyVarSet                -- Untouchable TcS unification variables
+                 -> InertSet                  -- Given
+                 -> Implication               -- Wanted
+                 -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
+                         Bag Implication)     -- Unsolved rest (always empty or singleton)
+-- Returns: 
+--  1. A bag of floatable wanted constraints, not mentioning any skolems, 
+--     that are of the form unification var = type
 -- 
--- 		-- Extract the binding
--- 	; (binds, irreds) <- extractResults avails wanteds
-	; (refinement_binds,needed_givens) <- extractLocalResults refined_avails needed_givens1
-	; traceTc (text "reduceImplication local results" <+> vcat
-			[ppr refinement_binds, ppr needed_givens])
-
-	; -- extract superclass binds
-	  --  (sc_binds,_) <- extractResults avails []
--- 	; traceTc (text "reduceImplication sc_binds" <+> vcat
---			[ppr sc_binds, ppr avails])
---  
-
-		-- We always discard the extra avails we've generated;
-		-- but we remember if we have done any (global) improvement
---	; let ret_avails = avails
-	; let ret_avails = orig_avails
---	; let ret_avails = updateImprovement orig_avails avails
-
-	; traceTc (text "reduceImplication condition" <+> ppr ((isEmptyLHsBinds binds) || (null irreds)))
-
---	Porgress is no longer measered by the number of bindings
---	; if isEmptyLHsBinds binds then 	-- No progress
-	; if (isEmptyLHsBinds binds) && (not $ null irreds) then 
-		return (ret_avails, NoInstance)
-	  else do
-	{ 
-	; (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
-			-- This binding is useless if the recursive simplification
-			-- made no progress; but currently we don't try to optimise that
-			-- case.  After all, we only try hard to reduce at top level, or
-			-- when inferring types.
-
-	; let	dict_wanteds = filter (not . isEqInst) wanteds
-		(extra_eq_givens, extra_dict_givens) = partition isEqInst extra_givens
-		dict_ids = map instToId extra_dict_givens 
-		-- TOMDO: given equational constraints bug!
-		--  we need a different evidence for given
-		--  equations depending on whether we solve
-		--  dictionary constraints or equational constraints
-		eq_tyvars = uniqSetToList $ tyVarsOfTypes $ map eqInstType extra_eq_givens
-		-- dict_ids = map instToId extra_givens
-		co  = mkWpTyLams tvs <.> mkWpTyLams eq_tyvars <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` refinement_binds `unionBags` bind)
-		rhs = mkHsWrap co payload
-	        loc = instLocSpan inst_loc
-		payload | [dict_wanted] <- dict_wanteds = HsVar (instToId dict_wanted)
-			| otherwise = ExplicitTuple (map (L loc . HsVar . instToId) dict_wanteds) Boxed
-
-	
-	; traceTc (text "reduceImplication ->"  <+> vcat
-			[ ppr ret_avails,
-			  ppr implic_insts])
-		-- If there are any irreds, we back off and return NoInstance
-	; return (ret_avails, GenInst (implic_insts ++ needed_givens) (L loc rhs))
-  	} 
-    }
-\end{code}
-
-Note [Reducing implication constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are trying to simplify
-	(Ord a, forall b. C a b => (W [a] b, D c b))
-where
-	instance (C a b, Ord a) => W [a] b
-When solving the implication constraint, we'll start with
-	Ord a -> Irred
-in the Avails.  Then we add (C a b -> Given) and solve. Extracting
-the results gives us a binding for the (W [a] b), with an Irred of 
-(Ord a, D c b).  Now, the (Ord a) comes from "outside" the implication,
-but the (D d b) is from "inside".  So we want to generate a Rhs binding
-like this
-
-	ic = /\b \dc:C a b). (df a b dc do, ic' b dc)
-	   depending on
-		do :: Ord a
-		ic' :: forall b. C a b => D c b
-
-The 'depending on' part of the Rhs is important, because it drives
-the extractResults code.
-
-The "inside" and "outside" distinction is what's going on with 'inner' and
-'outer' in reduceImplication
-
-
-Note [Freeness and implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's hard to say when an implication constraint can be floated out.  Consider
-	forall {} Eq a => Foo [a]
-The (Foo [a]) doesn't mention any of the quantified variables, but it
-still might be partially satisfied by the (Eq a). 
-
-There is a useful special case when it *is* easy to partition the 
-constraints, namely when there are no 'givens'.  Consider
-	forall {a}. () => Bar b
-There are no 'givens', and so there is no reason to capture (Bar b).
-We can let it float out.  But if there is even one constraint we
-must be much more careful:
-	forall {a}. C a b => Bar (m b)
-because (C a b) might have a superclass (D b), from which we might 
-deduce (Bar [b]) when m later gets instantiated to [].  Ha!
-
-Here is an even more exotic example
-	class C a => D a b
-Now consider the constraint
-	forall b. D Int b => C Int
-We can satisfy the (C Int) from the superclass of D, so we don't want
-to float the (C Int) out, even though it mentions no type variable in
-the constraints!
-
-Note [Pruning the givens in an implication constraint]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are about to form the implication constraint
-	forall tvs.  Eq a => Ord b
-The (Eq a) cannot contribute to the (Ord b), because it has no access to
-the type variable 'b'.  So we could filter out the (Eq a) from the givens.
-
-Doing so would be a bit tidier, but all the implication constraints get
-simplified away by the optimiser, so it's no great win.   So I don't take
-advantage of that at the moment.
-
-If you do, BE CAREFUL of wobbly type variables.
-
-
-%************************************************************************
-%*									*
-		Avails and AvailHow: the pool of evidence
-%*									*
-%************************************************************************
-
-
-\begin{code}
-data Avails = Avails !ImprovementDone !AvailEnv
-
-type ImprovementDone = Bool	-- True <=> some unification has happened
-				-- so some Irreds might now be reducible
-				-- keys that are now 
-
-type AvailEnv = FiniteMap Inst AvailHow
-data AvailHow
-  = IsIrred 		-- Used for irreducible dictionaries,
-			-- which are going to be lambda bound
-
-  | Given TcId 		-- Used for dictionaries for which we have a binding
-			-- e.g. those "given" in a signature
-
-  | Rhs 		-- Used when there is a RHS
-	(LHsExpr TcId) 	-- The RHS
-	[Inst]		-- Insts free in the RHS; we need these too
-
-instance Outputable Avails where
-  ppr = pprAvails
-
-pprAvails (Avails imp avails)
-  = vcat [ ptext SLIT("Avails") <> (if imp then ptext SLIT("[improved]") else empty)
-	 , nest 2 (vcat [sep [ppr inst, nest 2 (equals <+> ppr avail)]
-			| (inst,avail) <- fmToList avails ])]
-
-instance Outputable AvailHow where
-    ppr = pprAvail
-
--------------------------
-pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred	= text "Irred"
-pprAvail (Given x)   	= text "Given" <+> ppr x
-pprAvail (Rhs rhs bs)   = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
-
--------------------------
-extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
-extendAvailEnv env inst avail = addToFM env inst avail
-
-findAvailEnv :: AvailEnv -> Inst -> Maybe AvailHow
-findAvailEnv env wanted = lookupFM env wanted
-	-- NB 1: the Ord instance of Inst compares by the class/type info
-	--  *not* by unique.  So
-	--	d1::C Int ==  d2::C Int
-
-emptyAvails :: Avails
-emptyAvails = Avails False emptyFM
-
-findAvail :: Avails -> Inst -> Maybe AvailHow
-findAvail (Avails _ avails) wanted = findAvailEnv avails wanted
-
-elemAvails :: Inst -> Avails -> Bool
-elemAvails wanted (Avails _ avails) = wanted `elemFM` avails
-
-extendAvails :: Avails -> Inst -> AvailHow -> TcM Avails
--- Does improvement
-extendAvails avails@(Avails imp env) inst avail 
-  = do	{ imp1 <- tcImproveOne avails inst	-- Do any improvement
-	; return (Avails (imp || imp1) (extendAvailEnv env inst avail)) }
-
-availsInsts :: Avails -> [Inst]
-availsInsts (Avails _ avails) = keysFM avails
-
-availsImproved (Avails imp _) = imp
-
-updateImprovement :: Avails -> Avails -> Avails
--- (updateImprovement a1 a2) sets a1's improvement flag from a2
-updateImprovement (Avails _ avails1) (Avails imp2 _) = Avails imp2 avails1
-\end{code}
-
-Extracting the bindings from a bunch of Avails.
-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
-
-\begin{code}
-extractResults :: Avails
-	       -> [Inst]		-- Wanted
-	       -> TcM (	TcDictBinds, 	-- Bindings
-			[Inst],		-- Irreducible ones
-			[Inst])		-- Needed givens, i.e. ones used in the bindings
-
-extractResults (Avails _ avails) wanteds
-  = go avails emptyBag [] [] wanteds
-  where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst] -> [Inst]
-	-> TcM (TcDictBinds, [Inst], [Inst])
-    go avails binds irreds givens [] 
-      = returnM (binds, irreds, givens)
-
-    go avails binds irreds givens (w:ws)
-      = case findAvailEnv avails w of
-	  Nothing -> pprTrace "Urk: extractResults" (ppr w) $
-		     go avails binds irreds givens ws
-
-	  Just (Given id) 
-		| id == w_id -> go avails binds irreds (w:givens) ws 
-		| otherwise  -> 
-                  go avails (addInstToDictBind binds w (nlHsVar id)) irreds 
-                     (update_id w  id:givens) ws
-		-- The sought Id can be one of the givens, via a superclass chain
-		-- and then we definitely don't want to generate an x=x binding!
-
-	  Just IsIrred -> go (add_given avails w) binds (w:irreds) givens ws
-		-- The add_given handles the case where we want (Ord a, Eq a), and we
-		-- don't want to emit *two* Irreds for Ord a, one via the superclass chain
-		-- This showed up in a dupliated Ord constraint in the error message for 
-		--	test tcfail043
-
-	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds givens (ws' ++ ws)
-			     where	
-				new_binds = addInstToDictBind binds w rhs
-      where
-	w_id = instToId w	
-	update_id m@(Method{}) id = m {tci_id = id}
-        update_id w            id = w {tci_name = idName id} 
-
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
-
-extractLocalResults :: Avails
-	       -> [Inst]		-- Wanted
-	       -> TcM (	TcDictBinds, 	-- Bindings
-			[Inst])		-- Needed givens, i.e. ones used in the bindings
-
-extractLocalResults (Avails _ avails) wanteds
-  = go avails emptyBag [] wanteds
-  where
-    go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
-	-> TcM (TcDictBinds, [Inst])
-    go avails binds givens [] 
-      = returnM (binds, givens)
-
-    go avails binds givens (w:ws)
-      = case findAvailEnv avails w of
-	  Nothing -> -- pprTrace "Urk: extractLocalResults" (ppr w) $
-		     go avails binds givens ws
-
-	  Just IsIrred ->
-		     go avails binds givens ws
-
-	  Just (Given id) 
-		| id == w_id -> go avails binds (w:givens) ws 
-		| otherwise  -> go avails binds (w{tci_name=idName id}:givens) ws
-		-- The sought Id can be one of the givens, via a superclass chain
-		-- and then we definitely don't want to generate an x=x binding!
-
-	  Just (Rhs rhs ws') -> go (add_given avails w) new_binds givens (ws' ++ ws)
-			     where	
-				new_binds = addInstToDictBind binds w rhs
-      where
-	w_id = instToId w	
+--  2. Maybe a unsolved implication, empty if entirely solved! 
+-- 
+-- Precondition: everything is zonked by now
+solveImplication tcs_untouchables inert
+     imp@(Implic { ic_untch  = untch 
+                 , ic_binds  = ev_binds
+                 , ic_skols  = skols 
+                 , ic_given  = givens
+                 , ic_wanted = wanteds
+                 , ic_loc    = loc })
+  = nestImplicTcS ev_binds (untch, tcs_untouchables) $
+    recoverTcS (return (emptyBag, emptyBag)) $
+       -- Recover from nested failures.  Even the top level is
+       -- just a bunch of implications, so failing at the first
+       -- one is bad
+    do { traceTcS "solveImplication {" (ppr imp) 
+
+         -- Solve flat givens
+       ; given_inert <- solveInteractGiven inert loc givens 
+
+         -- Simplify the wanteds
+       ; (unsolved_flats, unsolved_implics, insols)
+             <- solve_wanteds given_inert wanteds
+
+       ; let (res_flat_free, res_flat_bound)
+                 = floatEqualities skols givens unsolved_flats
+             final_flat = keepWanted res_flat_bound
+
+       ; let res_wanted = WC { wc_flat = final_flat
+                             , wc_impl = unsolved_implics
+                             , wc_insol = insols }
+             res_implic = unitImplication $
+                          imp { ic_wanted = res_wanted
+                              , ic_insol  = insolubleWC res_wanted }
+
+       ; traceTcS "solveImplication end }" $ vcat
+             [ text "res_flat_free =" <+> ppr res_flat_free
+             , text "res_implic =" <+> ppr res_implic ]
+
+       ; return (res_flat_free, res_implic) }
+
+
+floatEqualities :: TcTyVarSet -> [EvVar]
+                -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
+-- Post: The returned FlavoredEvVar's are only Wanted or Derived
+-- and come from the input wanted ev vars or deriveds 
+floatEqualities skols can_given wantders
+  | hasEqualities can_given = (emptyBag, wantders)
+          -- Note [Float Equalities out of Implications]
+  | otherwise = partitionBag is_floatable wantders
+  
 
-    add_given avails w = extendAvailEnv avails w (Given (instToId w))
+  where is_floatable :: FlavoredEvVar -> Bool
+        is_floatable (EvVarX cv _fl)
+          | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
+        is_floatable _flev = False
+
+        tvs_under_fsks :: Type -> TyVarSet
+        -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
+        tvs_under_fsks (TyVarTy tv)     
+          | not (isTcTyVar tv)               = unitVarSet tv
+          | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
+          | otherwise                        = unitVarSet tv
+        tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
+        tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
+        tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
+        tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
+        tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
+        	     	       	      -- can mention type variables!
+          | isTyVar tv		      = inner_tvs `delVarSet` tv
+          | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
+                                        inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
+          where
+            inner_tvs = tvs_under_fsks ty
+
+        predTvs_under_fsks :: PredType -> TyVarSet
+        predTvs_under_fsks (IParam _ ty)    = tvs_under_fsks ty
+        predTvs_under_fsks (ClassP _ tys)   = unionVarSets (map tvs_under_fsks tys)
+        predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
 \end{code}
 
-
-Note [No superclasses for Stop]
+Note [Preparing inert set for implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Before solving the nested implications, we convert any unsolved flat wanteds
+to givens, and add them to the inert set.  Reasons:
+
+  a) In checking mode, suppresses unnecessary errors.  We already have
+     on unsolved-wanted error; adding it to the givens prevents any 
+     consequential errors from showing up
+
+  b) More importantly, in inference mode, we are going to quantify over this
+     constraint, and we *don't* want to quantify over any constraints that
+     are deducible from it.
+
+  c) Flattened type-family equalities must be exposed to the nested
+     constraints.  Consider
+	F b ~ alpha, (forall c.  F b ~ alpha)
+     Obviously this is soluble with [alpha := F b].  But the
+     unification is only done by solveCTyFunEqs, right at the end of
+     solveWanteds, and if we aren't careful we'll end up with an
+     unsolved goal inside the implication.  We need to "push" the
+     as-yes-unsolved (F b ~ alpha) inwards, as a *given*, so that it
+     can be used to solve the inner (F b
+     ~ alpha).  See Trac #4935.
+
+  d) There are other cases where interactions between wanteds that can help
+     to solve a constraint. For example
+
+  	class C a b | a -> b
+
+  	(C Int alpha), (forall d. C d blah => C Int a)
+
+     If we push the (C Int alpha) inwards, as a given, it can produce
+     a fundep (alpha~a) and this can float out again and be used to
+     fix alpha.  (In general we can't float class constraints out just
+     in case (C d blah) might help to solve (C Int a).)
+
+The unsolved wanteds are *canonical* but they may not be *inert*,
+because when made into a given they might interact with other givens.
+Hence the call to solveInteract.  Example:
+
+ Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 
+
+We were not able to solve (a ~w [beta]) but we can't just assume it as
+given because the resulting set is not inert. Hence we have to do a
+'solveInteract' step first. 
+
+Finally, note that we convert them to [Given] and NOT [Given/Solved].
+The reason is that Given/Solved are weaker than Givens and may be discarded.
+As an example consider the inference case, where we may have, the following 
+original constraints: 
+     [Wanted] F Int ~ Int
+             (F Int ~ a => F Int ~ a)
+If we convert F Int ~ Int to [Given/Solved] instead of Given, then the next 
+given (F Int ~ a) is going to cause the Given/Solved to be ignored, casting 
+the (F Int ~ a) insoluble. Hence we should really convert the residual 
+wanteds to plain old Given. 
+
+We need only push in unsolved equalities both in checking mode and inference mode: 
+
+  (1) In checking mode we should not push given dictionaries in because of
+example LongWayOverlapping.hs, where we might get strange overlap
+errors between far-away constraints in the program.  But even in
+checking mode, we must still push type family equations. Consider:
+
+   type instance F True a b = a 
+   type instance F False a b = b
+
+   [w] F c a b ~ gamma 
+   (c ~ True) => a ~ gamma 
+   (c ~ False) => b ~ gamma
+
+Since solveCTyFunEqs happens at the very end of solving, the only way to solve
+the two implications is temporarily consider (F c a b ~ gamma) as Given (NB: not 
+merely Given/Solved because it has to interact with the top-level instance 
+environment) and push it inside the implications. Now, when we come out again at
+the end, having solved the implications solveCTyFunEqs will solve this equality.
+
+  (2) In inference mode, we recheck the final constraint in checking mode and
+hence we will be able to solve inner implications from top-level quantified
+constraints nonetheless.
+
+
+Note [Extra TcsTv untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we decide not to reduce an Inst -- the 'WhatToDo' --- we still
-add it to avails, so that any other equal Insts will be commoned up
-right here.  However, we 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.
+Furthemore, we record the inert set simplifier-generated unification
+variables of the TcsTv kind (such as variables from instance that have
+been applied, or unification flattens). These variables must be passed
+to the implications as extra untouchable variables. Otherwise we have
+the danger of double unifications. Example (from trac ticket #4494):
+
+   (F Int ~ uf)  /\  (forall a. C a => F Int ~ beta) 
+
+In this example, beta is touchable inside the implication. The first
+solveInteract step leaves 'uf' ununified. Then we move inside the
+implication where a new constraint
+       uf  ~  beta  
+emerges. We may spontaneously solve it to get uf := beta, so the whole
+implication disappears but when we pop out again we are left with (F
+Int ~ uf) which will be unified by our final solveCTyFunEqs stage and
+uf will get unified *once more* to (F Int).
+
+The solution is to record the TcsTvs (i.e. the simplifier-generated
+unification variables) that are generated when solving the flats, and
+make them untouchables for the nested implication. In the example
+above uf would become untouchable, so beta would be forced to be
+unified as beta := uf.
+
+NB: A consequence is that every simplifier-generated TcsTv variable
+    that gets floated out of an implication becomes now untouchable
+    next time we go inside that implication to solve any residual
+    constraints. In effect, by floating an equality out of the
+    implication we are committing to have it solved in the outside.
+
+Note [Float Equalities out of Implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+We want to float equalities out of vanilla existentials, but *not* out 
+of GADT pattern matches. 
 
-\begin{code}
-addWanted :: WantSCs -> Avails -> Inst -> LHsExpr TcId -> [Inst] -> TcM Avails
-addWanted want_scs avails wanted rhs_expr wanteds
-  = addAvailAndSCs want_scs avails wanted avail
-  where
-    avail = Rhs rhs_expr wanteds
-
-addGiven :: Avails -> Inst -> TcM Avails
-addGiven avails given = addAvailAndSCs AddSCs avails given (Given (instToId given))
-	-- Always add superclasses for 'givens'
-	--
-	-- No ASSERT( not (given `elemAvails` avails) ) because in an instance
-	-- decl for Ord t we can add both Ord t and Eq t as 'givens', 
-	-- so the assert isn't true
-
-addRefinedGiven :: Refinement -> ([Inst], Avails) -> Inst -> TcM ([Inst], Avails)
-addRefinedGiven reft (refined_givens, avails) given
-  | isDict given	-- We sometimes have 'given' methods, but they
-			-- are always optional, so we can drop them
-  , let pred = dictPred given
-  , isRefineablePred pred	-- See Note [ImplicInst rigidity]
-  , Just (co, pred) <- refinePred reft pred
-  = do 	{ new_given <- newDictBndr (instLoc given) pred
-	; let rhs = L (instSpan given) $
-		    HsWrap (WpCo co) (HsVar (instToId given))
-	; avails <- addAvailAndSCs AddSCs avails new_given (Rhs rhs [given])
-	; return (new_given:refined_givens, avails) }
-	    -- ToDo: the superclasses of the original given all exist in Avails 
-	    -- so we could really just cast them, but it's more awkward to do,
-	    -- and hopefully the optimiser will spot the duplicated work
-  | otherwise
-  = return (refined_givens, avails)
-\end{code}
-
-Note [ImplicInst rigidity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-	C :: forall ab. (Eq a, Ord b) => b -> T a
-	
-	...(case x of C v -> <body>)...
-
-From the case (where x::T ty) we'll get an implication constraint
-	forall b. (Eq ty, Ord b) => <body-constraints>
-Now suppose <body-constraints> itself has an implication constraint 
-of form
-	forall c. <reft> => <payload>
-Then, we can certainly apply the refinement <reft> to the Ord b, becuase it is
-existential, but we probably should not apply it to the (Eq ty) because it may
-be wobbly. Hence the isRigidInst
-
-@Insts@ are ordered by their class/type info, rather than by their
-unique.  This allows the context-reduction mechanism to use standard finite
-maps to do their stuff.  It's horrible that this code is here, rather
-than with the Avails handling stuff in TcSimplify
 
 \begin{code}
-addIrred :: WantSCs -> Avails -> Inst -> TcM Avails
-addIrred want_scs avails irred = ASSERT2( not (irred `elemAvails` avails), ppr irred $$ ppr avails )
-    	      		         addAvailAndSCs want_scs avails irred IsIrred
-
-addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
-addAvailAndSCs want_scs avails inst avail
-  | not (isClassDict inst) = extendAvails avails inst avail
-  | NoSCs <- want_scs	   = extendAvails avails inst avail
-  | otherwise		   = do { traceTc (text "addAvailAndSCs" <+> vcat [ppr inst, ppr deps])
-				; avails' <- extendAvails avails inst avail
-				; addSCs is_loop avails' inst }
-  where
-    is_loop pred = any (`tcEqType` mkPredTy pred) dep_tys
-			-- Note: this compares by *type*, not by Unique
-    deps         = findAllDeps (unitVarSet (instToVar inst)) avail
-    dep_tys	 = map idType (varSetElems deps)
-
-    findAllDeps :: IdSet -> AvailHow -> IdSet
-    -- Find all the Insts that this one depends on
-    -- See Note [SUPERCLASS-LOOP 2]
-    -- Watch out, though.  Since the avails may contain loops 
-    -- (see Note [RECURSIVE DICTIONARIES]), so we need to track the ones we've seen so far
-    findAllDeps so_far (Rhs _ kids) = foldl find_all so_far kids
-    findAllDeps so_far other	    = so_far
-
-    find_all :: IdSet -> Inst -> IdSet
-    find_all so_far kid
-      | isEqInst kid                       = so_far
-      | kid_id `elemVarSet` so_far	   = so_far
-      | Just avail <- findAvail avails kid = findAllDeps so_far' avail
-      | otherwise			   = so_far'
-      where
-	so_far' = extendVarSet so_far kid_id	-- Add the new kid to so_far
-	kid_id = instToId kid
-
-addSCs :: (TcPredType -> Bool) -> Avails -> Inst -> TcM Avails
-	-- Add all the superclasses of the Inst to Avails
-	-- The first param says "dont do this because the original thing
-	--	depends on this one, so you'd build a loop"
-	-- Invariant: the Inst is already in Avails.
-
-addSCs is_loop avails dict
-  = ASSERT( isDict dict )
-    do	{ sc_dicts <- newDictBndrs (instLoc dict) sc_theta'
-	; foldlM add_sc avails (zipEqual "add_scs" sc_dicts sc_sels) }
-  where
-    (clas, tys) = getDictClassTys dict
-    (tyvars, sc_theta, sc_sels, _) = classBigSig clas
-    sc_theta' = filter (not . isEqPred) $
-                  substTheta (zipTopTvSubst tyvars tys) sc_theta
-
-    add_sc avails (sc_dict, sc_sel)
-      | is_loop (dictPred sc_dict) = return avails 	-- See Note [SUPERCLASS-LOOP 2]
-      | is_given sc_dict 	   = return avails
-      | otherwise		   = do { avails' <- extendAvails avails sc_dict (Rhs sc_sel_rhs [dict])
-					; addSCs is_loop avails' sc_dict }
-      where
-	sc_sel_rhs = L (instSpan dict) (HsWrap co_fn (HsVar sc_sel))
-	co_fn	   = WpApp (instToVar dict) <.> mkWpTyApps tys
 
-    is_given :: Inst -> Bool
-    is_given sc_dict = case findAvail avails sc_dict of
-			  Just (Given _) -> True	-- Given is cheaper than superclass selection
-			  other		 -> False	
-
--- From the a set of insts obtain all equalities that (transitively) occur in
--- superclass contexts of class constraints (aka the ancestor equalities). 
---
-ancestorEqualities :: [Inst] -> TcM [Inst]
-ancestorEqualities
-  =   mapM mkWantedEqInst               -- turn only equality predicates..
-    . filter isEqPred                   -- ..into wanted equality insts
-    . bagToList 
-    . addAEsToBag emptyBag              -- collect the superclass constraints..
-    . map dictPred                      -- ..of all predicates in a bag
-    . filter isClassDict
+solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
+-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
+-- See Note [Solving Family Equations]
+-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
+--          where the newly generated equalities (alpha := F xi) have been substituted through.
+solveCTyFunEqs cts
+ = do { untch   <- getUntouchables 
+      ; let (unsolved_can_cts, (ni_subst, cv_binds))
+                = getSolvableCTyFunEqs untch cts
+      ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
+                                          , ppr ni_subst, ppr cv_binds
+                                          ])
+      ; mapM_ solve_one cv_binds
+
+      ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
   where
-    addAEsToBag :: Bag PredType -> [PredType] -> Bag PredType
-    addAEsToBag bag []           = bag
-    addAEsToBag bag (pred:preds)
-      | pred `elemBag` bag = addAEsToBag bag         preds
-      | isEqPred pred      = addAEsToBag bagWithPred preds
-      | isClassPred pred   = addAEsToBag bagWithPred predsWithSCs
-      | otherwise          = addAEsToBag bag         preds
-      where
-        bagWithPred  = bag `snocBag` pred
-        predsWithSCs = preds ++ substTheta (zipTopTvSubst tyvars tys) sc_theta
-        --
-        (tyvars, sc_theta, _, _) = classBigSig clas
-        (clas, tys) 		 = getClassPredTys pred 
+    solve_one (cv,tv,ty) = do { setWantedTyBind tv ty
+                              ; setCoBind cv (mkReflCo ty) }
+
+------------
+type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
+  -- The TvSubstEnv is not idempotent, but is loop-free
+  -- See Note [Non-idempotent substitution] in Unify
+emptyFunEqBinds :: FunEqBinds
+emptyFunEqBinds = (emptyVarEnv, [])
+
+extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
+extendFunEqBinds (tv_subst, cv_binds) cv tv ty
+  = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
+
+------------
+getSolvableCTyFunEqs :: TcsUntouchables
+                     -> CanonicalCts                -- Precondition: all Wanteds or Derived!
+                     -> (CanonicalCts, FunEqBinds)  -- Postcondition: returns the unsolvables
+getSolvableCTyFunEqs untch cts
+  = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
+  where
+    dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
+               -> (CanonicalCts, FunEqBinds)
+    dflt_funeq (cts_in, feb@(tv_subst, _))
+               (CFunEqCan { cc_id = cv
+                          , cc_flavor = fl
+                          , cc_fun = tc
+                          , cc_tyargs = xis
+                          , cc_rhs = xi })
+      | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
+
+      , isTouchableMetaTyVar_InRange untch tv
+           -- And it's a *touchable* unification variable
+
+      , typeKind xi `isSubKind` tyVarKind tv
+         -- Must do a small kind check since TcCanonical invariants 
+         -- on family equations only impose compatibility, not subkinding
+
+      , not (tv `elemVarEnv` tv_subst)
+           -- Check not in extra_binds
+           -- See Note [Solving Family Equations], Point 1
+
+      , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
+           -- Occurs check: see Note [Solving Family Equations], Point 2
+      = ASSERT ( not (isGivenOrSolved fl) )
+        (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
+
+    dflt_funeq (cts_in, fun_eq_binds) ct
+      = (cts_in `extendCCans` ct, fun_eq_binds)
 \end{code}
 
+Note [Solving Family Equations] 
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
+After we are done with simplification we may be left with constraints of the form:
+     [Wanted] F xis ~ beta 
+If 'beta' is a touchable unification variable not already bound in the TyBinds 
+then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
 
-%************************************************************************
-%*									*
-\section{tcSimplifyTop: defaulting}
-%*									*
-%************************************************************************
+When is it ok to do so? 
+    1) 'beta' must not already be defaulted to something. Example: 
 
+           [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
+           [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
+                                       have to report this as unsolved.
 
-@tcSimplifyTop@ is called once per module to simplify all the constant
-and ambiguous Insts.
+    2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
+       set [beta := F xis] only if beta is not among the free variables of xis.
 
-We need to be careful of one case.  Suppose we have
+    3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
+       of type family equations. See Inert Set invariants in TcInteract. 
 
-	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??
+*********************************************************************************
+*                                                                               * 
+*                          Defaulting and disamgiguation                        *
+*                                                                               *
+*********************************************************************************
 
-It's OK: the final zonking stage should zap y to (), which is fine.
-
-
-\begin{code}
-tcSimplifyTop, tcSimplifyInteractive :: [Inst] -> TcM TcDictBinds
-tcSimplifyTop wanteds
-  = tc_simplify_top doc False wanteds
-  where 
-    doc = text "tcSimplifyTop"
-
-tcSimplifyInteractive wanteds
-  = tc_simplify_top doc True wanteds
-  where 
-    doc = text "tcSimplifyInteractive"
-
--- The TcLclEnv should be valid here, solely to improve
--- error message generation for the monomorphism restriction
-tc_simplify_top doc interactive wanteds
-  = do	{ dflags <- getDOpts
-  	; wanteds <- zonkInsts wanteds
-	; mapM_ zonkTopTyVar (varSetElems (tyVarsOfInsts wanteds))
-
-	; traceTc (text "tc_simplify_top 0: " <+> ppr wanteds)
-	; (irreds1, binds1) <- tryHardCheckLoop doc1 wanteds
-	; traceTc (text "tc_simplify_top 1: " <+> ppr irreds1)
-	; (irreds2, binds2) <- approximateImplications doc2 (\d -> True) irreds1
-	; traceTc (text "tc_simplify_top 2: " <+> ppr irreds2)
-
-		-- Use the defaulting rules to do extra unification
-		-- NB: irreds2 are already zonked
-	; (irreds3, binds3) <- disambiguate doc3 interactive dflags irreds2
-
-		-- Deal with implicit parameters
-	; let (bad_ips, non_ips) = partition isIPDict irreds3
-	      (ambigs, others)   = partition isTyVarDict non_ips
-
-	; topIPErrs bad_ips	-- Can arise from   f :: Int -> Int
-				--		    f x = x + ?y
-	; addNoInstanceErrs others
-	; addTopAmbigErrs ambigs	
-
-	; return (binds1 `unionBags` binds2 `unionBags` binds3) }
-  where
-    doc1 = doc <+> ptext SLIT("(first round)")
-    doc2 = doc <+> ptext SLIT("(approximate)")
-    doc3 = doc <+> ptext SLIT("(disambiguate)")
-\end{code}
+Basic plan behind applyDefaulting rules: 
+ 
+ Step 1:  
+    Split wanteds into defaultable groups, `groups' and the rest `rest_wanted' 
+    For each defaultable group, do: 
+      For each possible substitution for [alpha |-> tau] where `alpha' is the 
+      group's variable, do: 
+        1) Make up new TcEvBinds
+        2) Extend TcS with (groupVariable 
+        3) given_inert <- solveOne inert (given : a ~ tau) 
+        4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
+        5) if unsolved == empty then 
+                 sneakyUnify a |-> tau 
+                 write the evidence bins
+                 return (final_inert ++ group_constraints,[]) 
+                      -- will contain the info (alpha |-> tau)!!
+                 goto next defaultable group 
+           if unsolved <> empty then 
+                 throw away evidence binds
+                 try next substitution 
+     If you've run out of substitutions for this group, too bad, you failed 
+                 return (inert,group) 
+                 goto next defaultable group
+ 
+ Step 2: 
+   Collect all the (canonical-cts, wanteds) gathered this way. 
+   - Do a solveGiven over the canonical-cts to make sure they are inert 
+------------------------------------------------------------------------------------------
 
-If a dictionary constrains a type variable which is
-	* 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
-	* 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.
-
-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.
-
-@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}
-disambiguate :: SDoc -> Bool -> DynFlags -> [Inst] -> TcM ([Inst], TcDictBinds)
-	-- Just does unification to fix the default types
-	-- The Insts are assumed to be pre-zonked
-disambiguate doc interactive dflags insts
-  | null insts
-  = return (insts, emptyBag)
-
-  | null defaultable_groups
-  = do	{ traceTc (text "disambigutate, no defaultable groups" <+> vcat [ppr unaries, ppr insts, ppr bad_tvs, ppr defaultable_groups])
-	; return (insts, emptyBag) }
-
+applyDefaultingRules :: InertSet
+                     -> CanonicalCts             -- All wanteds
+                     -> TcS (Bag FlavoredEvVar)  -- All wanteds again!
+-- Return some *extra* givens, which express the 
+-- type-class-default choice
+
+applyDefaultingRules inert wanteds
+  | isEmptyBag wanteds 
+  = return emptyBag
   | otherwise
-  = do 	{  	-- Figure out what default types to use
-	  default_tys <- getDefaultTys extended_defaulting ovl_strings
-
-	; traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
-	; mapM_ (disambigGroup default_tys) defaultable_groups
-
-	-- disambigGroup does unification, hence try again
-	; tryHardCheckLoop doc insts }
-
-  where
-   extended_defaulting = interactive || dopt Opt_ExtendedDefaultRules dflags
-   ovl_strings = dopt Opt_OverloadedStrings dflags
-
-   unaries :: [(Inst, Class, TcTyVar)]  -- (C tv) constraints
-   bad_tvs :: TcTyVarSet  -- Tyvars mentioned by *other* constraints
-   (unaries, bad_tvs_s) = partitionWith find_unary insts 
-   bad_tvs 		= unionVarSets bad_tvs_s
-
-	-- Finds unary type-class constraints
-   find_unary d@(Dict {tci_pred = ClassP cls [ty]})
-	| Just tv <- tcGetTyVar_maybe ty = Left (d,cls,tv)
-   find_unary inst			 = Right (tyVarsOfInst inst)
-
-		-- Group by type variable
-   defaultable_groups :: [[(Inst,Class,TcTyVar)]]
-   defaultable_groups = filter defaultable_group (equivClasses cmp_tv unaries)
-   cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
-
-   defaultable_group :: [(Inst,Class,TcTyVar)] -> Bool
-   defaultable_group ds@((_,_,tv):_)
-	=  isTyConableTyVar tv	-- Note [Avoiding spurious errors]
-	&& not (tv `elemVarSet` bad_tvs)
-	&& defaultable_classes [c | (_,c,_) <- ds]
-   defaultable_group [] = panic "defaultable_group"
-
-   defaultable_classes clss 
-	| extended_defaulting = any isInteractiveClass clss
-	| otherwise 	      = all is_std_class clss && (any is_num_class clss)
-
- 	-- In interactive mode, or with -fextended-default-rules,
-	-- we default Show a to Show () to avoid graututious errors on "show []"
-   isInteractiveClass cls 
-	= is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
-
-   is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-	-- is_num_class adds IsString to the standard numeric classes, 
-	-- when -foverloaded-strings is enabled
-
-   is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
-	-- Similarly is_std_class
-
------------------------
-disambigGroup :: [Type]			-- The default types
-	      -> [(Inst,Class,TcTyVar)]	-- All standard classes of form (C a)
-	      -> TcM ()	-- Just does unification, to fix the default types
-
-disambigGroup default_tys dicts
-  = try_default default_tys
+  = do { untch <- getUntouchables
+       ; tv_cts <- mapM (defaultTyVar untch) $
+                   varSetElems (tyVarsOfCDicts wanteds) 
+
+       ; info@(_, default_tys, _) <- getDefaultInfo
+       ; let groups = findDefaultableGroups info untch wanteds
+       ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
+
+       ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
+                                 , text "Type defaults =" <+> ppr deflt_cts])
+
+       ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
+
+------------------
+defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
+-- defaultTyVar is used on any un-instantiated meta type variables to
+-- default the kind of ? and ?? etc to *.  This is important to ensure
+-- that instance declarations match.  For example consider
+--	instance Show (a->b)
+--	foo x = show (\_ -> True)
+-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
+-- and that won't match the typeKind (*) in the instance decl.  
+-- See test tc217.
+--
+-- We look only at touchable type variables. No further constraints
+-- are going to affect these type variables, so it's time to do it by
+-- hand.  However we aren't ready to default them fully to () or
+-- whatever, because the type-class defaulting rules have yet to run.
+
+defaultTyVar untch the_tv 
+  | isTouchableMetaTyVar_InRange untch the_tv
+  , not (k `eqKind` default_k)
+  = do { ev <- TcSMonad.newKindConstraint the_tv default_k
+       ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
+       ; return (unitBag (mkEvVarX ev (Wanted loc))) }
+  | otherwise            
+  = return emptyBag	 -- The common case
   where
-    (_,_,tyvar) = ASSERT(not (null dicts)) head dicts	-- Should be non-empty
-    classes = [c | (_,c,_) <- dicts]
-
-    try_default [] = return ()
-    try_default (default_ty : default_tys)
-      = tryTcLIE_ (try_default default_tys) $
-    	do { tcSimplifyDefault [mkClassPred clas [default_ty] | clas <- classes]
-		-- This may fail; then the tryTcLIE_ kicks in
-		-- 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.
-
-		-- After this we can't fail
-	   ; warnDefault dicts default_ty
-	   ; unifyType default_ty (mkTyVarTy tyvar) 
-	   ; return () -- TOMDO: do something with the coercion
-	   }
-
-
------------------------
-getDefaultTys :: Bool -> Bool -> TcM [Type]
-getDefaultTys extended_deflts ovl_strings
-  = do	{ mb_defaults <- getDeclaredDefaultTys
-	; case mb_defaults of {
-	   Just tys -> return tys ;	-- User-supplied defaults
-	   Nothing  -> do
-
-	-- No use-supplied default
-	-- Use [Integer, Double], plus modifications
-	{ integer_ty <- tcMetaTy integerTyConName
-	; checkWiredInTyCon doubleTyCon
-	; string_ty <- tcMetaTy stringTyConName
-	; return (opt_deflt extended_deflts unitTy
-			-- Note [Default unitTy]
-			++
-		  [integer_ty,doubleTy]
-			++
-		  opt_deflt ovl_strings string_ty) } } }
+    k = tyVarKind the_tv
+    default_k = defaultKind k
+
+
+----------------
+findDefaultableGroups 
+    :: ( SimplContext 
+       , [Type]
+       , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
+    -> TcsUntouchables	-- Untouchable
+    -> CanonicalCts	-- Unsolved
+    -> [[(CanonicalCt,TcTyVar)]]
+findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) 
+                      untch wanteds
+  | not (performDefaulting ctxt) = []
+  | null default_tys             = []
+  | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
+  where 
+    unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
+    non_unaries :: [CanonicalCt]             -- and *other* constraints
+    
+    (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
+        -- Finds unary type-class constraints
+    find_unary cc@(CDictCan { cc_tyargs = [ty] })
+        | Just tv <- tcGetTyVar_maybe ty
+        = Left (cc, tv)
+    find_unary cc = Right cc  -- Non unary or non dictionary 
+
+    bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
+    bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries 
+
+    cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
+
+    is_defaultable_group ds@((_,tv):_)
+        = isTyConableTyVar tv	-- Note [Avoiding spurious errors]
+        && not (tv `elemVarSet` bad_tvs)
+        && isTouchableMetaTyVar_InRange untch tv 
+        && defaultable_classes [cc_class cc | (cc,_) <- ds]
+    is_defaultable_group [] = panic "defaultable_group"
+
+    defaultable_classes clss 
+        | extended_defaults = any isInteractiveClass clss
+        | otherwise         = all is_std_class clss && (any is_num_class clss)
+
+    -- In interactive mode, or with -XExtendedDefaultRules,
+    -- we default Show a to Show () to avoid graututious errors on "show []"
+    isInteractiveClass cls 
+        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
+
+    is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+    -- is_num_class adds IsString to the standard numeric classes, 
+    -- when -foverloaded-strings is enabled
+
+    is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
+    -- Similarly is_std_class
+
+------------------------------
+disambigGroup :: [Type]                    -- The default types 
+              -> InertSet                  -- Given inert 
+              -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
+	      	 		           --  sharing same type variable
+              -> TcS (Bag FlavoredEvVar)
+
+disambigGroup [] _inert _grp 
+  = return emptyBag
+disambigGroup (default_ty:default_tys) inert group
+  = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
+       ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
+       ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
+             derived_eq = mkEvVarX ev der_flav
+
+       ; success <- tryTcS $
+                    do { (_,final_inert) <- solveInteract inert $ listToBag $
+                                            derived_eq : wanted_ev_vars
+           	       ; let (_, unsolved) = extractUnsolved final_inert                         
+                       ; let wanted_unsolved = filterBag isWantedCt unsolved 
+                                            -- Don't care about Derived's
+                       ; return (isEmptyBag wanted_unsolved) }
+       ; case success of
+           True  ->  -- Success: record the type variable binding, and return
+                    do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
+                       ; traceTcS "disambigGroup succeeded" (ppr default_ty)
+                       ; return (unitBag derived_eq) }
+           False ->    -- Failure: try with the next type
+                    do { traceTcS "disambigGroup failed, will try other default types"
+                                  (ppr default_ty)
+                       ; disambigGroup default_tys inert group } }
   where
-    opt_deflt True  ty = [ty]
-    opt_deflt False ty = []
+    ((the_ct,the_tv):_) = group
+    wanteds             = map fst group
+    wanted_ev_vars :: [FlavoredEvVar]
+    wanted_ev_vars      = map deCanonicalise wanteds
+
+    mk_derived_flavor :: CtFlavor -> CtFlavor
+    mk_derived_flavor (Wanted loc) = Derived loc
+    mk_derived_flavor _ = panic "Asked  to disambiguate given or derived!"
 \end{code}
 
-Note [Default unitTy]
-~~~~~~~~~~~~~~~~~~~~~
-In interative mode (or with -fextended-default-rules) we add () as the first type we
-try when defaulting.  This has very little real impact, except in the following case.
-Consider: 
-	Text.Printf.printf "hello"
-This has type (forall a. IO a); it prints "hello", and returns 'undefined'.  We don't
-want the GHCi repl loop to try to print that 'undefined'.  The neatest thing is to
-default the 'a' to (), rather than to Integer (which is what would otherwise happen;
-and then GHCi doesn't attempt to print the ().  So in interactive mode, we add
-() to the list of defaulting types.  See Trac #1200.
-
 Note [Avoiding spurious errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When doing the unification for defaulting, we check for skolem
@@ -2798,328 +1300,17 @@ we try to unify a with Int (to default it), but find that it's
 already been unified with the rigid variable from g's type sig
 
 
-%************************************************************************
-%*									*
-\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}
-tcSimplifyDeriv :: InstOrigin
-		-> [TyVar]	
-		-> ThetaType		-- Wanted
-	        -> TcM ThetaType	-- Needed
--- Given  instance (wanted) => C inst_ty 
--- Simplify 'wanted' as much as possible
-
-tcSimplifyDeriv orig tyvars theta
-  = do	{ (tvs, _, tenv) <- tcInstTyVars tyvars
-	-- The main loop may do unification, and that may crash if 
-	-- it doesn't see a TcTyVar, so we have to instantiate. Sigh
-	-- ToDo: what if two of them do get unified?
-	; wanteds <- newDictBndrsO orig (substTheta tenv theta)
-	; (irreds, _) <- tryHardCheckLoop doc wanteds
-
-	; let (tv_dicts, others) = partition ok irreds
-	; addNoInstanceErrs others
-	-- See Note [Exotic derived instance contexts] in TcMType
-
-	; let rev_env = zipTopTvSubst tvs (mkTyVarTys tyvars)
-	      simpl_theta = substTheta rev_env (map dictPred tv_dicts)
-		-- This reverse-mapping is a pain, but the result
-		-- should mention the original TyVars not TcTyVars
-
-	; return simpl_theta }
-  where
-    doc = ptext SLIT("deriving classes for a data type")
-
-    ok dict | isDict dict = validDerivPred (dictPred dict)
-	    | otherwise	  = False
-\end{code}
-
 
-@tcSimplifyDefault@ just checks class-type constraints, essentially;
-used with \tr{default} declarations.  We are only interested in
-whether it worked or not.
+*********************************************************************************
+*                                                                               * 
+*                   Utility functions
+*                                                                               *
+*********************************************************************************
 
 \begin{code}
-tcSimplifyDefault :: ThetaType	-- Wanted; has no type variables in it
-		  -> TcM ()
-
-tcSimplifyDefault theta
-  = newDictBndrsO DefaultOrigin theta	`thenM` \ wanteds ->
-    tryHardCheckLoop doc wanteds	`thenM` \ (irreds, _) ->
-    addNoInstanceErrs  irreds	 	`thenM_`
-    if null irreds then
-	returnM ()
-    else
-	failM
-  where
-    doc = ptext SLIT("default declaration")
-\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}
-groupErrs :: ([Inst] -> TcM ())	-- Deal with one group
-	  -> [Inst]		-- The offending Insts
-          -> TcM ()
--- Group together insts with the same origin
--- We want to report them together in error messages
-
-groupErrs report_err [] 
-  = returnM ()
-groupErrs report_err (inst:insts) 
-  = do_one (inst:friends)		`thenM_`
-    groupErrs report_err others
-
-  where
-	-- (It may seem a bit crude to compare the error messages,
-	--  but it makes sure that we combine just what the user sees,
-	--  and it avoids need equality on InstLocs.)
-   (friends, others) = partition is_friend insts
-   loc_msg	     = showSDoc (pprInstLoc (instLoc inst))
-   is_friend friend  = showSDoc (pprInstLoc (instLoc friend)) == loc_msg
-   do_one insts = addInstCtxt (instLoc (head insts)) (report_err insts)
-		-- Add location and context information derived from the Insts
-
--- Add the "arising from..." part to a message about bunch of dicts
-addInstLoc :: [Inst] -> Message -> Message
-addInstLoc insts msg = msg $$ nest 2 (pprInstArising (head insts))
-
-addTopIPErrs :: [Name] -> [Inst] -> TcM ()
-addTopIPErrs bndrs [] 
-  = return ()
-addTopIPErrs bndrs ips
-  = do	{ dflags <- getDOpts
-	; addErrTcM (tidy_env, mk_msg dflags tidy_ips) }
-  where
-    (tidy_env, tidy_ips) = tidyInsts ips
-    mk_msg dflags ips 
-	= vcat [sep [ptext SLIT("Implicit parameters escape from"),
-	        nest 2 (ptext SLIT("the monomorphic top-level binding") 
-					    <> plural bndrs <+> ptext SLIT("of")
-					    <+> pprBinders bndrs <> colon)],
-		nest 2 (vcat (map ppr_ip ips)),
-		monomorphism_fix dflags]
-    ppr_ip ip = pprPred (dictPred ip) <+> pprInstArising ip
-
-topIPErrs :: [Inst] -> TcM ()
-topIPErrs dicts
-  = groupErrs report tidy_dicts
-  where
-    (tidy_env, tidy_dicts) = tidyInsts dicts
-    report dicts = addErrTcM (tidy_env, mk_msg dicts)
-    mk_msg dicts = addInstLoc dicts (ptext SLIT("Unbound implicit parameter") <> 
-				     plural tidy_dicts <+> pprDictsTheta tidy_dicts)
-
-addNoInstanceErrs :: [Inst]	-- Wanted (can include implications)
-		  -> TcM ()	
-addNoInstanceErrs insts
-  = do	{ let (tidy_env, tidy_insts) = tidyInsts insts
-	; reportNoInstances tidy_env Nothing tidy_insts }
-
-reportNoInstances 
-	:: TidyEnv
-	-> Maybe (InstLoc, [Inst])	-- Context
-			-- Nothing => top level
-			-- Just (d,g) => d describes the construct
-			--		 with givens g
-	-> [Inst]	-- What is wanted (can include implications)
-	-> TcM ()	
-
-reportNoInstances tidy_env mb_what insts 
-  = groupErrs (report_no_instances tidy_env mb_what) insts
-
-report_no_instances tidy_env mb_what insts
-  = do { inst_envs <- tcGetInstEnvs
-       ; let (implics, insts1)  = partition isImplicInst insts
-	     (insts2, overlaps) = partitionWith (check_overlap inst_envs) insts1
-             (eqInsts, insts3)  = partition isEqInst insts2
-       ; traceTc (text "reportNoInstances" <+> vcat 
-                       [ppr implics, ppr insts1, ppr insts2])
-       ; mapM_ complain_implic implics
-       ; mapM_ (\doc -> addErrTcM (tidy_env, doc)) overlaps
-       ; groupErrs complain_no_inst insts3 
-       ; mapM_ eqInstMisMatch eqInsts
-       }
-  where
-    complain_no_inst insts = addErrTcM (tidy_env, mk_no_inst_err insts)
-
-    complain_implic inst	-- Recurse!
-      = reportNoInstances tidy_env 
-			  (Just (tci_loc inst, tci_given inst)) 
-			  (tci_wanted inst)
-
-    check_overlap :: (InstEnv,InstEnv) -> Inst -> Either Inst SDoc
-	-- Right msg  => overlap message
-	-- Left  inst => no instance
-    check_overlap inst_envs wanted
-	| not (isClassDict wanted) = Left wanted
-	| otherwise
-	= case lookupInstEnv inst_envs clas tys of
-		-- The case of exactly one match and no unifiers means a
-		-- successful lookup.  That can't happen here, because dicts
-		-- only end up here if they didn't match in Inst.lookupInst
-#ifdef DEBUG
-		([m],[]) -> pprPanic "reportNoInstance" (ppr wanted)
-#endif
-		([], _)  -> Left wanted		-- No match
-		res	 -> Right (mk_overlap_msg wanted res)
-	  where
-	    (clas,tys) = getDictClassTys wanted
-
-    mk_overlap_msg dict (matches, unifiers)
-      = ASSERT( not (null matches) )
-        vcat [	addInstLoc [dict] ((ptext SLIT("Overlapping instances for") 
-					<+> pprPred (dictPred dict))),
-    		sep [ptext SLIT("Matching instances") <> colon,
-    		     nest 2 (vcat [pprInstances ispecs, pprInstances unifiers])],
-		if not (isSingleton matches)
-    		then 	-- Two or more matches
-		     empty
-    		else 	-- One match, plus some unifiers
-		ASSERT( not (null unifiers) )
-		parens (vcat [ptext SLIT("The choice depends on the instantiation of") <+>
-	    		         quotes (pprWithCommas ppr (varSetElems (tyVarsOfInst dict))),
-			      ptext SLIT("To pick the first instance above, use -fallow-incoherent-instances"),
-			      ptext SLIT("when compiling the other instance declarations")])]
-      where
-    	ispecs = [ispec | (ispec, _) <- matches]
-
-    mk_no_inst_err insts
-      | null insts = empty
-
-      | Just (loc, givens) <- mb_what,   -- Nested (type signatures, instance decls)
-	not (isEmptyVarSet (tyVarsOfInsts insts))
-      = vcat [ addInstLoc insts $
-	       sep [ ptext SLIT("Could not deduce") <+> pprDictsTheta insts
-	           , nest 2 $ ptext SLIT("from the context") <+> pprDictsTheta givens]
-	     , show_fixes (fix1 loc : fixes2) ]
-
-      | otherwise	-- Top level 
-      = vcat [ addInstLoc insts $
-	       ptext SLIT("No instance") <> plural insts
-		    <+> ptext SLIT("for") <+> pprDictsTheta insts
-	     , show_fixes fixes2 ]
-
-      where
-    	fix1 loc = sep [ ptext SLIT("add") <+> pprDictsTheta insts
-				 <+> ptext SLIT("to the context of"),
-			 nest 2 (ppr (instLocOrigin loc)) ]
-			 -- I'm not sure it helps to add the location
-			 -- nest 2 (ptext SLIT("at") <+> ppr (instLocSpan loc)) ]
-
-    	fixes2 | null instance_dicts = []
-	       | otherwise	     = [sep [ptext SLIT("add an instance declaration for"),
-				        pprDictsTheta instance_dicts]]
-	instance_dicts = [d | d <- insts, isClassDict d, not (isTyVarDict d)]
-		-- Insts for which it is worth suggesting an adding an instance declaration
-		-- Exclude implicit parameters, and tyvar dicts
-
-	show_fixes :: [SDoc] -> SDoc
-	show_fixes []     = empty
-	show_fixes (f:fs) = sep [ptext SLIT("Possible fix:"), 
-				 nest 2 (vcat (f : map (ptext SLIT("or") <+>) fs))]
-
-addTopAmbigErrs dicts
--- Divide into groups that share a common set of ambiguous tyvars
-  = ifErrsM (return ()) $	-- Only report ambiguity if no other errors happened
-				-- See Note [Avoiding spurious errors]
-    mapM_ report (equivClasses cmp [(d, tvs_of d) | d <- tidy_dicts])
-  where
-    (tidy_env, tidy_dicts) = tidyInsts dicts
-
-    tvs_of :: Inst -> [TcTyVar]
-    tvs_of d = varSetElems (tyVarsOfInst d)
-    cmp (_,tvs1) (_,tvs2) = tvs1 `compare` tvs2
-    
-    report :: [(Inst,[TcTyVar])] -> TcM ()
-    report pairs@((inst,tvs) : _)	-- The pairs share a common set of ambiguous tyvars
-	= mkMonomorphismMsg tidy_env tvs	`thenM` \ (tidy_env, mono_msg) ->
-	  setSrcSpan (instSpan inst) $
-		-- the location of the first one will do for the err message
-	  addErrTcM (tidy_env, msg $$ mono_msg)
-	where
-	  dicts = map fst pairs
-	  msg = sep [text "Ambiguous type variable" <> plural tvs <+> 
-			  pprQuotedList tvs <+> in_msg,
-		     nest 2 (pprDictsInFull dicts)]
-	  in_msg = text "in the constraint" <> plural dicts <> colon
-    report [] = panic "addTopAmbigErrs"
-
-
-mkMonomorphismMsg :: TidyEnv -> [TcTyVar] -> TcM (TidyEnv, Message)
--- There's an error with these Insts; if they have free type variables
--- it's probably caused by the monomorphism restriction. 
--- Try to identify the offending variable
--- ASSUMPTION: the Insts are fully zonked
-mkMonomorphismMsg tidy_env inst_tvs
-  = do	{ dflags <- getDOpts
-	; (tidy_env, docs) <- findGlobals (mkVarSet inst_tvs) tidy_env
-	; return (tidy_env, mk_msg dflags docs) }
-  where
-    mk_msg _ _ | any isRuntimeUnk inst_tvs
-        =  vcat [ptext SLIT("Cannot resolve unknown runtime types:") <+>
-                   (pprWithCommas ppr inst_tvs),
-                ptext SLIT("Use :print or :force to determine these types")]
-    mk_msg _ []   = ptext SLIT("Probable fix: add a type signature that fixes these type variable(s)")
-			-- This happens in things like
-			--	f x = show (read "foo")
-			-- where monomorphism doesn't play any role
-    mk_msg dflags docs 
-	= vcat [ptext SLIT("Possible cause: the monomorphism restriction applied to the following:"),
-		nest 2 (vcat docs),
-		monomorphism_fix dflags]
-
-isRuntimeUnk :: TcTyVar -> Bool
-isRuntimeUnk x | SkolemTv RuntimeUnkSkol <- tcTyVarDetails x = True
-               | otherwise = False
-
-monomorphism_fix :: DynFlags -> SDoc
-monomorphism_fix dflags
-  = ptext SLIT("Probable fix:") <+> vcat
-	[ptext SLIT("give these definition(s) an explicit type signature"),
-	 if dopt Opt_MonomorphismRestriction dflags
-           then ptext SLIT("or use -fno-monomorphism-restriction")
-           else empty]	-- Only suggest adding "-fno-monomorphism-restriction"
-			-- if it is not already set!
-    
-warnDefault ups default_ty
-  = doptM Opt_WarnTypeDefaults  `thenM` \ warn_flag ->
-    addInstCtxt (instLoc (head (dicts))) (warnTc warn_flag warn_msg)
-  where
-    dicts = [d | (d,_,_) <- ups]
-
-	-- Tidy them first
-    (_, tidy_dicts) = tidyInsts dicts
-    warn_msg  = vcat [ptext SLIT("Defaulting the following constraint(s) to type") <+>
-				quotes (ppr default_ty),
-		      pprDictsInFull tidy_dicts]
-
-reduceDepthErr n stack
-  = vcat [ptext SLIT("Context reduction stack overflow; size =") <+> int n,
-	  ptext SLIT("Use -fcontext-stack=N to increase stack size to N"),
-	  nest 4 (pprStack stack)]
-
-pprStack stack = vcat (map pprInstInFull stack)
-\end{code}
+newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
+newFlatWanteds orig theta
+  = do { loc <- getCtLoc orig
+       ; evs <- newWantedEvVars theta
+       ; return (listToBag [EvVarX w loc | w <- evs]) }
+\end{code}
\ No newline at end of file