+ 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}
+
+\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
+ --
+ -- ToDo: what about improvement? There may be some improvement
+ -- exposed as a result of the simplifications done by reduceList
+ -- which are discarded if we back off.
+ -- This is almost certainly Wrong, but we'll fix it when dealing
+ -- better with equality constraints
+reduceImplication env orig_avails reft tvs extra_givens wanteds inst_loc
+ = do { -- Add refined givens, and the extra givens
+ (refined_red_givens, avails)
+ <- if isEmptyRefinement reft then return (red_givens env, orig_avails)
+ else foldlM (addRefinedGiven reft) ([], orig_avails) (red_givens env)
+ ; avails <- foldlM addGiven avails extra_givens
+
+ -- Solve the sub-problem
+ ; let try_me inst = ReduceMe AddSCs -- Note [Freeness and implications]
+ env' = env { red_givens = refined_red_givens ++ extra_givens
+ , red_try_me = try_me }
+
+ ; traceTc (text "reduceImplication" <+> vcat
+ [ ppr (red_givens env), ppr extra_givens, ppr reft, ppr wanteds ])
+ ; avails <- reduceList env' wanteds avails
+
+ -- Extract the binding (no frees, because try_me never says Free)
+ ; (binds, irreds) <- extractResults avails wanteds
+
+ -- We always discard the extra avails we've generated;
+ -- but we remember if we have done any (global) improvement
+ ; let ret_avails = updateImprovement orig_avails avails
+
+ ; if isEmptyLHsBinds binds then -- No progress
+ 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_ids = map instToId extra_givens
+ co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
+ rhs = mkHsWrap co payload
+ loc = instLocSpan inst_loc
+ payload | isSingleton wanteds = HsVar (instToId (head wanteds))
+ | otherwise = ExplicitTuple (map (L loc . HsVar . instToId) wanteds) Boxed
+
+ -- If there are any irreds, we back off and return NoInstance
+ ; return (ret_avails, GenInst implic_insts (L loc rhs))
+ } }
+\end{code}
+
+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!
+
+%************************************************************************
+%* *
+ 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" <+> 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
+
+extractResults (Avails _ avails) wanteds
+ = go avails emptyBag [] wanteds
+ where
+ go :: AvailEnv -> TcDictBinds -> [Inst] -> [Inst]
+ -> TcM (TcDictBinds, [Inst])
+ go avails binds irreds []
+ = returnM (binds, irreds)
+
+ go avails binds irreds (w:ws)
+ = case findAvailEnv avails w of
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds ws
+
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) ws
+
+ Just (Given id)
+ | id == instToId w
+ -> go avails binds irreds 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!
+
+ | otherwise
+ -> go avails (addBind binds w (nlHsVar id)) irreds ws
+
+ Just (Rhs rhs ws') -> go (add_given avails w) new_binds irreds (ws' ++ ws)
+ where
+ new_binds = addBind binds w rhs
+
+ add_given avails w = extendAvailEnv avails w (Given (instToId w))
+
+addBind binds inst rhs = binds `unionBags` unitBag (L (instSpan inst)
+ (VarBind (instToId inst) rhs))
+\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
+ 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
+ , Just (co, pred) <- refinePred reft (dictPred given)
+ = 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)
+
+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 (instToId 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
+ | 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' = 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 (instToId 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
+\end{code}
+
+%************************************************************************
+%* *