import FiniteMap
import Bag
import Outputable
+import Maybes
import ListSetOps
import Util
import SrcLoc
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 getImplicWanteds.
+the strange function get_dictsin approximateImplications.
The common cases are more clear-cut, when we have things like
forall a. C a => C b
ppr reft, ppr wanteds, ppr avails ])
; avails <- reduceList env' wanteds avails
- -- Extract the binding
+ -- Extract the results
+ -- Note [Reducing implication constraints]
; (binds, irreds) <- extractResults avails wanteds
-
+ ; let (outer, inner) = partition (isJust . findAvail orig_avails) irreds
+
; traceTc (text "reduceImplication result" <+> vcat
- [ ppr irreds, ppr binds])
+ [ ppr outer, ppr inner, ppr binds])
-- 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
+ ; if isEmptyLHsBinds binds && null outer then -- No progress
return (ret_avails, NoInstance)
else do
- { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens irreds
+ { (implic_insts, bind) <- makeImplicationBind inst_loc tvs reft extra_givens inner
; let dict_ids = map instToId extra_givens
co = mkWpTyLams tvs <.> mkWpLams dict_ids <.> WpLet (binds `unionBags` bind)
payload | [wanted] <- wanteds = HsVar (instToId wanted)
| 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))
+ ; return (ret_avails, GenInst (implic_insts ++ outer) (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
type AvailEnv = FiniteMap Inst AvailHow
data AvailHow
- = IsIrred TcId -- Used for irreducible dictionaries,
+ = IsIrred -- Used for irreducible dictionaries,
-- which are going to be lambda bound
| Given TcId -- Used for dictionaries for which we have a binding
-------------------------
pprAvail :: AvailHow -> SDoc
-pprAvail (IsIrred x) = text "Irred" <+> ppr x
+pprAvail IsIrred = text "Irred"
pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = text "Rhs" <+> ppr rhs <+> braces (ppr bs)
+pprAvail (Rhs rhs bs) = text "Rhs" <+> sep [ppr rhs, braces (ppr bs)]
-------------------------
extendAvailEnv :: AvailEnv -> Inst -> AvailHow -> AvailEnv
go avails binds irreds (w:ws)
= case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go avails binds irreds ws
+ Nothing -> pprTrace "Urk: extractResults" (ppr w) $
+ go avails binds irreds ws
Just (Given id)
| id == w_id -> 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!
- Just (IsIrred id)
- | id == w_id -> go (add_given avails w) binds (w:irreds) ws
- | otherwise -> go avails (addBind binds w_id (nlHsVar id)) irreds ws
+ Just IsIrred -> go (add_given avails w) binds (w:irreds) 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
\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 (instToId irred))
+ addAvailAndSCs want_scs avails irred IsIrred
addAvailAndSCs :: WantSCs -> Avails -> Inst -> AvailHow -> TcM Avails
addAvailAndSCs want_scs avails inst avail
= return (insts, emptyBag)
| null defaultable_groups
- = do { traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ = do { traceTc (text "disambiguate1" <+> vcat [ppr insts, ppr unaries, ppr bad_tvs, ppr defaultable_groups])
; return (insts, emptyBag) }
| otherwise
= do { -- Figure out what default types to use
default_tys <- getDefaultTys extended_defaulting ovl_strings
- ; traceTc (text "disambigutate" <+> vcat [ppr unaries, ppr bad_tvs, ppr defaultable_groups])
+ ; 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