+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
+--
+-- -- 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) = partitionGivenEqInsts 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 (addBind 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 = addBind 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 = addBind binds w rhs
+ where
+ w_id = instToId w
+
+ add_given avails w = extendAvailEnv avails w (Given (instToId w))
+\end{code}
+
+
+Note [No superclasses for Stop]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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.
+
+\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