- = do { traceTc (text "reduce" <+> ppr wanted $$ ppr avails)
- ; case red_try_me env wanted of {
- Stop -> try_simple (addIrred NoSCs);
- -- See Note [No superclasses for Stop]
-
- ReduceMe -> do -- It should be reduced
- { (avails, lookup_result) <- reduceInst env avails wanted
- ; case lookup_result of
- NoInstance -> addIrred AddSCs avails wanted
- -- Add it and its superclasses
-
- GenInst [] rhs -> addWanted AddSCs avails wanted rhs []
-
- GenInst wanteds' rhs
- -> do { avails1 <- addIrred NoSCs avails wanted
- ; avails2 <- reduceList env wanteds' avails1
- ; addWanted AddSCs 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
- } }
- 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 []
- _ -> do_this_otherwise avails wanted }
-\end{code}
-
-
-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.
-
-Note [SUPERCLASS-LOOP 2]
-~~~~~~~~~~~~~~~~~~~~~~~~
-We need to be careful when adding "the constaint we are trying to prove".
-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.
-
-
-
-%************************************************************************
-%* *
- Reducing a single constraint
-%* *
-%************************************************************************
-
-\begin{code}
----------------------------------------------
-reduceInst :: RedEnv -> Avails -> Inst -> TcM (Avails, LookupInstResult)
-reduceInst _ avails other_inst
- = do { result <- lookupSimpleInst other_inst
- ; return (avails, result) }
-\end{code}
-
-Note [Equational Constraints in Implication Constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-An implication 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
- -> Inst
- -> TcM (TcDictBinds, [Inst])
-\end{code}
-
-Suppose we are simplifying the constraint
- forall bs. extras => wanted
-in the context of an overall simplification problem with givens 'givens'.
-
-Note that
- * The '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
- --
- -- 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
-
--------------------------
-pprAvail :: AvailHow -> SDoc
-pprAvail IsIrred = text "Irred"
-pprAvail (Given x) = text "Given" <+> ppr x
-pprAvail (Rhs rhs bs) = sep [text "Rhs" <+> ppr bs,
- nest 2 (ppr rhs)]
-
--------------------------
-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 -> ImprovementDone
-availsImproved (Avails imp _) = imp
-\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}
-type DoneEnv = FiniteMap Inst [Id]
--- Tracks which things we have evidence for
-
-extractResults :: Avails
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, -- Bindings
- [Inst], -- The insts bound by the bindings
- [Inst]) -- Irreducible ones
- -- Note [Reducing implication constraints]
-
-extractResults (Avails _ avails) wanteds
- = go emptyBag [] [] emptyFM wanteds
- where
- go :: TcDictBinds -- Bindings for dicts
- -> [Inst] -- Bound by the bindings
- -> [Inst] -- Irreds
- -> DoneEnv -- Has an entry for each inst in the above three sets
- -> [Inst] -- Wanted
- -> TcM (TcDictBinds, [Inst], [Inst])
- go binds bound_dicts irreds _ []
- = return (binds, bound_dicts, irreds)
-
- go binds bound_dicts irreds done (w:ws)
- | isEqInst w
- = go binds bound_dicts (w:irreds) done' ws
-
- | Just done_ids@(done_id : rest_done_ids) <- lookupFM done w
- = if w_id `elem` done_ids then
- go binds bound_dicts irreds done ws
- else
- go (add_bind (nlHsVar done_id)) bound_dicts irreds
- (addToFM done w (done_id : w_id : rest_done_ids)) ws
-
- | otherwise -- Not yet done
- = case findAvailEnv avails w of
- Nothing -> pprTrace "Urk: extractResults" (ppr w) $
- go binds bound_dicts irreds done ws
-
- Just IsIrred -> go binds bound_dicts (w:irreds) done' ws
-
- Just (Rhs rhs ws') -> go (add_bind rhs) (w:bound_dicts) irreds done' (ws' ++ ws)
-
- Just (Given g) -> go binds' bound_dicts irreds (addToFM done w [g_id]) ws
- where
- g_id = instToId g
- binds' | w_id == g_id = binds
- | otherwise = add_bind (nlHsVar g_id)
- where
- w_id = instToId w
- done' = addToFM done w [w_id]
- add_bind rhs = addInstToDictBind binds w 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 want_scs avails given (Given given)
- where
- want_scs = case instLocOrigin (instLoc given) of
- NoScOrigin -> NoSCs
- _other -> AddSCs
- -- Conditionally add superclasses for 'given'
- -- See Note [Recursive instances and superclases]
-
- -- 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
-\end{code}
-
-\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 _ = 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 "don't 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
- _ -> False
-
--- From the a set of insts obtain all equalities that (transitively) occur in
--- superclass contexts of class constraints (aka the ancestor equalities).