+ -- 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
+ --
+ -- Note [Binders for equalities]
+ -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ -- To reuse the binders of local/given equalities in the binders of
+ -- implication constraints, it is crucial that these given equalities
+ -- always have the form
+ -- cotv :: t1 ~ t2
+ -- where cotv is a simple coercion type variable (and not a more
+ -- complex coercion term). We require that the extra_givens always
+ -- have this form and exploit the special form when generating binders.
+reduceImplication env
+ orig_implic@(ImplicInst { tci_name = name, tci_loc = inst_loc,
+ tci_tyvars = tvs,
+ tci_given = extra_givens, tci_wanted = wanteds
+ })
+ = do { -- Solve the sub-problem
+ ; let try_me _ = ReduceMe -- Note [Freeness and implications]
+ env' = env { red_givens = extra_givens ++ red_givens env
+ , red_doc = sep [ptext (sLit "reduceImplication for")
+ <+> ppr name,
+ nest 2 (parens $ ptext (sLit "within")
+ <+> red_doc env)]
+ , red_try_me = try_me }
+
+ ; traceTc (text "reduceImplication" <+> vcat
+ [ ppr (red_givens env), ppr extra_givens,
+ ppr wanteds])
+ ; (irreds, binds) <- checkLoop env' wanteds
+
+ ; traceTc (text "reduceImplication result" <+> vcat
+ [ppr irreds, ppr binds])
+
+ ; -- extract superclass binds
+ -- (sc_binds,_) <- extractResults avails []
+-- ; traceTc (text "reduceImplication sc_binds" <+> vcat
+-- [ppr sc_binds, ppr avails])
+--
+
+ -- SLPJ Sept 07: what if improvement happened inside the checkLoop?
+ -- Then we must iterate the outer loop too!
+
+ ; didntSolveWantedEqs <- allM wantedEqInstIsUnsolved wanteds
+ -- we solve wanted eqs by side effect!
+
+ -- Progress is no longer measered by the number of bindings
+ -- If there are any irreds, but no bindings and no solved
+ -- equalities, we back off and do nothing
+ ; let backOff = isEmptyLHsBinds binds && -- no new bindings
+ (not $ null irreds) && -- but still some irreds
+ didntSolveWantedEqs -- no instantiated cotv
+
+ ; if backOff then -- No progress
+ return (emptyBag, [orig_implic])
+ else do
+ { (simpler_implic_insts, bind)
+ <- makeImplicationBind inst_loc tvs 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 -- extract Id binders for dicts and CoTyVar binders for eqs;
+ -- see Note [Binders for equalities]
+ (extra_eq_givens, extra_dict_givens) = partition isEqInst
+ extra_givens
+ eq_cotvs = map instToVar extra_eq_givens
+ dict_ids = map instToId extra_dict_givens
+
+ -- Note [Always inline implication constraints]
+ wrap_inline | null dict_ids = idHsWrapper
+ | otherwise = WpInline
+ co = wrap_inline
+ <.> mkWpTyLams tvs
+ <.> mkWpTyLams eq_cotvs
+ <.> mkWpLams dict_ids
+ <.> WpLet (binds `unionBags` bind)
+ rhs = mkLHsWrap co payload
+ loc = instLocSpan inst_loc
+ -- wanted equalities are solved by updating their
+ -- cotv; we don't generate bindings for them
+ dict_bndrs = map (L loc . HsVar . instToId)
+ . filter (not . isEqInst)
+ $ wanteds
+ payload = mkBigLHsTup dict_bndrs
+
+
+ ; traceTc (vcat [text "reduceImplication" <+> ppr name,
+ ppr simpler_implic_insts,
+ text "->" <+> ppr rhs])
+ ; return (unitBag (L loc (VarBind (instToId orig_implic) rhs)),
+ simpler_implic_insts)
+ }
+ }
+reduceImplication _ i = pprPanic "reduceImplication" (ppr i)
+\end{code}
+
+Note [Always inline implication constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose an implication constraint floats out of an INLINE function.
+Then although the implication has a single call site, it won't be
+inlined. And that is bad because it means that even if there is really
+*no* overloading (type signatures specify the exact types) there will
+still be dictionary passing in the resulting code. To avert this,
+we mark the implication constraints themselves as INLINE, at least when
+there is no loss of sharing as a result.
+
+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!
+
+One more example: the constraint
+ class C a => D a b
+ instance (C a, E c) => E (a,c)
+
+ constraint: forall b. D Int b => E (Int,c)
+
+You might think that the (D Int b) can't possibly contribute
+to solving (E (Int,c)), since the latter mentions 'c'. But
+in fact it can, because solving the (E (Int,c)) constraint needs
+dictionaries
+ C Int, E c
+and the (C Int) can be satisfied from the superclass of (D Int b).
+So we must still not float (E (Int,c)) out.
+
+To think about: special cases for unary type classes?
+
+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.
+But BE CAREFUL of the examples above in [Freeness and implications].
+
+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 Inst -- 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 -> SDoc
+pprAvails (Avails imp avails)
+ = vcat [ ptext (sLit "Avails") <> (if imp then ptext (sLit "[improved]") else empty)
+ , nest 2 $ braces $
+ vcat [ sep [ppr inst, nest 2 (equals <+> ppr avail)]
+ | (inst,avail) <- fmToList avails ]]
+
+instance Outputable AvailHow where
+ ppr = pprAvail