Skip to content

Commit

Permalink
More simplifications to the constraint solver
Browse files Browse the repository at this point in the history 
* inert_solved becomes dictionaries-only, inert_solved_dicts

* inert_solved_dicts is used only to cache the result of uses
  of a top level instance declaration, just like inert_solved_funeqs

* That in turn simplifies xCtFlavor and rewriteCtFlavor, because
  they no longer need a "should I cache" parameter.  (Moreover the
  settings for this parameter were very subtle; it's easy to get
  loops if you cache too much.  Caching only top-level instance
  uses is much safer, and eliminates all these subtle cases.)
  • Loading branch information
Simon Peyton Jones committed Aug 31, 2012
1 parent 2b69233 commit b737a45
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 98 deletions.
29 changes: 14 additions & 15 deletions compiler/typecheck/TcCanonical.lhs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
-- for details
module TcCanonical(
canonicalize, occurCheckExpand,
canonicalize, occurCheckExpand, emitWorkNC,
StopOrContinue (..)
) where
Expand All @@ -34,7 +34,7 @@ import TcSMonad
import FastString
import Util
import Maybes( isJust, fromMaybe, catMaybes )
import Maybes( fromMaybe, catMaybes )
\end{code}


Expand Down Expand Up @@ -854,7 +854,7 @@ emitKindConstraint ct -- By now ct is canonical
xdecomp x = [mkEvKindCast x (evTermCoercion kev_tm)]
xev = XEvTerm xcomp xdecomp
; ctevs <- xCtFlavor_cache False fl [mkTcEqPred ty1 ty2] xev
; ctevs <- xCtFlavor fl [mkTcEqPred ty1 ty2] xev
-- Important: Do not cache original as Solved since we are supposed to
-- solve /exactly/ the same constraint later! Example:
-- (alpha :: kappa0)
Expand Down Expand Up @@ -1163,14 +1163,14 @@ canEqLeafTyVarLeftRec :: SubGoalDepth
canEqLeafTyVarLeftRec d fl tv s2 -- fl :: tv ~ s2
= do { traceTcS "canEqLeafTyVarLeftRec" $ pprEq (mkTyVarTy tv) s2
; (xi1,co1) <- flattenTyVar d FMFullFlatten fl tv -- co1 :: xi1 ~ tv
; let is_still_var = isJust (getTyVar_maybe xi1)
; traceTcS "canEqLeafTyVarLeftRec2" $ empty
; let co = mkTcTyConAppCo eqTyCon $ [ mkTcReflCo (defaultKind $ typeKind s2)
, co1, mkTcReflCo s2]
-- co :: (xi1 ~ s2) ~ (tv ~ s2)
; mb <- rewriteCtFlavor_cache (if is_still_var then False else True) fl (mkTcEqPred xi1 s2) co
; mb <- rewriteCtFlavor fl (mkTcEqPred xi1 s2) co
-- NB that rewriteCtFlavor does not cache the result
-- See Note [Caching loops]
; traceTcS "canEqLeafTyVarLeftRec3" $ empty
Expand Down Expand Up @@ -1203,19 +1203,18 @@ canEqLeafTyVarLeft d fl tv s2 -- eqv : tv ~ s2
-- Not reflexivity but maybe an occurs error
{ let occ_check_result = occurCheckExpand tv xi2
xi2' = fromMaybe xi2 occ_check_result
not_occ_err = isJust occ_check_result
-- Delicate: don't want to cache as solved a constraint with occurs error!
co = mkTcTyConAppCo eqTyCon $
[mkTcReflCo (defaultKind $ typeKind s2), mkTcReflCo tv_ty, co2]
; mb <- rewriteCtFlavor_cache not_occ_err fl (mkTcEqPred tv_ty xi2') co
; mb <- rewriteCtFlavor fl (mkTcEqPred tv_ty xi2') co
-- NB that rewriteCtFlavor does not cache the result (as it used to)
-- which would be wrong if the constraint has an occurs error
; case mb of
Just new_fl -> if not_occ_err then
continueWith $
CTyEqCan { cc_ev = new_fl, cc_depth = d
, cc_tyvar = tv, cc_rhs = xi2' }
else
canEqFailure d new_fl
Just new_fl -> case occ_check_result of
Just {} -> continueWith $
CTyEqCan { cc_ev = new_fl, cc_depth = d
, cc_tyvar = tv, cc_rhs = xi2' }
Nothing -> canEqFailure d new_fl
Nothing -> return Stop
} }
\end{code}
Expand Down
24 changes: 10 additions & 14 deletions compiler/typecheck/TcInteract.lhs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -353,7 +353,7 @@ kickOutRewritable new_flav new_tv
, inert_irreds = irs_in }
, inert_frozen = fro_in }
-- NB: Notice that don't rewrite
-- inert_solved, inert_flat_cache and inert_solved_funeqs
-- inert_solved_dicts, and inert_solved_funeqs
-- optimistically. But when we lookup we have to take the
-- subsitution into account
Expand Down Expand Up @@ -731,10 +731,10 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
-- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
; ctevs <- xCtFlavor_cache False ev2 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
-- No caching! See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
; add_to_work d2 ctevs
; emitWorkNC d2 ctevs
; return (IRWorkItemConsumed "FunEq/FunEq") }
| fl2 `canSolve` fl1 && lhss_match
Expand All @@ -749,17 +749,12 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
-- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
; ctevs <- xCtFlavor_cache False ev1 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
; add_to_work d1 ctevs
; emitWorkNC d1 ctevs
; return (IRInertConsumed "FunEq/FunEq") }
where
add_to_work d [ctev] = updWorkListTcS $ extendWorkListEq $
CNonCanonical {cc_ev = ctev, cc_depth = d}
add_to_work _ _ = return ()
lhss_match = tc1 == tc2 && eqTypes args1 args2
co1 = evTermCoercion $ ctEvTerm ev1
co2 = evTermCoercion $ ctEvTerm ev2
Expand Down Expand Up @@ -1421,8 +1416,8 @@ doTopReactDict inerts workItem fl cls xis depth
| isWanted fl
-> do { lkup_inst_res <- matchClassInst inerts cls xis (getWantedLoc fl)
; case lkup_inst_res of
GenInst wtvs ev_term ->
addToSolved fl >> doSolveFromInstance wtvs ev_term
GenInst wtvs ev_term -> do { addSolvedDict fl
; doSolveFromInstance wtvs ev_term }
NoInstance -> return NoTopInt }
| otherwise
-> return NoTopInt }
Expand Down Expand Up @@ -1490,6 +1485,7 @@ doTopReactFunEq ct fl fun_tc args xi d
succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
succeed_with str co rhs_ty -- co :: fun_tc args ~ rhs_ty
= do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
; case ctevs of
[ctev] -> updWorkListTcS $ extendWorkListEq $
CNonCanonical { cc_ev = ctev
Expand Down
108 changes: 39 additions & 69 deletions compiler/typecheck/TcSMonad.lhs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,19 +36,18 @@ module TcSMonad (
wrapErrTcS, wrapWarnTcS,
-- Getting and setting the flattening cache
addToSolved, addSolvedFunEq, getFlattenSkols,
addSolvedDict, addSolvedFunEq, getFlattenSkols,
deferTcSForAllEq,
setEvBind,
XEvTerm(..),
MaybeNew (..), isFresh, freshGoals, getEvTerms,
xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
xCtFlavor, -- Transform a CtEvidence during a step
rewriteCtFlavor, -- Specialized version of xCtFlavor for coercions
newWantedEvVar, instDFunConstraints,
newDerived,
xCtFlavor_cache, rewriteCtFlavor_cache,
-- Creation of evidence variables
setWantedTyBind,
Expand Down Expand Up @@ -396,6 +395,12 @@ instance Outputable a => Outputable (PredMap a) where
instance Outputable a => Outputable (FamHeadMap a) where
ppr (FamHeadMap m) = ppr (foldTM (:) m [])
sizePredMap :: PredMap a -> Int
sizePredMap (PredMap m) = foldTypeMap (\_ x -> x+1) 0 m
sizeFamHeadMap :: FamHeadMap a -> Int
sizeFamHeadMap (FamHeadMap m) = foldTypeMap (\_ x -> x+1) 0 m
ctTypeMapCts :: TypeMap Ct -> Cts
ctTypeMapCts ctmap = foldTM (\ct cts -> extendCts cts ct) ctmap emptyCts
Expand Down Expand Up @@ -544,12 +549,12 @@ data InertSet
-- Always the result of using a top-level family axiom F xis ~ tau
-- No Deriveds
, inert_solved :: PredMap CtEvidence
-- These two fields constitute a cache of solved (only!) constraints
, inert_solved_dicts :: PredMap CtEvidence
-- Of form ev :: C t1 .. tn
-- Always the result of using a top-level instance declaration
-- See Note [Solved constraints]
-- - Superset of inert_solved_funeqs
-- - Used to avoid creating a new EvVar when we have a new goal that we
-- have solvedin the past
-- - Used to avoid creating a new EvVar when we have a new goal
-- that we have solved in the past
-- - Stored not necessarily as fully rewritten
-- (ToDo: rewrite lazily when we lookup)
}
Expand All @@ -571,10 +576,8 @@ instance Outputable InertSet where
ppr is = vcat [ ppr $ inert_cans is
, text "Frozen errors =" <+> -- Clearly print frozen errors
braces (vcat (map ppr (Bag.bagToList $ inert_frozen is)))
, text "Solved and cached" <+>
int (foldTypeMap (\_ x -> x+1) 0
(unPredMap $ inert_solved is)) <+>
text "more constraints" ]
, text "Solved dicts" <+> int (sizePredMap (inert_solved_dicts is))
, text "Solved funeqs" <+> int (sizeFamHeadMap (inert_solved_funeqs is))]
emptyInert :: InertSet
emptyInert
Expand All @@ -585,20 +588,9 @@ emptyInert
, inert_irreds = emptyCts }
, inert_frozen = emptyCts
, inert_fsks = []
, inert_solved = PredMap emptyTM
, inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = FamHeadMap emptyTM }
updSolvedSet :: CtEvidence -> InertSet -> InertSet
updSolvedSet item is
= let pty = ctEvPred item
upd_solved Nothing = Just item
upd_solved (Just _existing_solved) = Just item
-- .. or Just existing_solved? Is this even possible to happen?
in is { inert_solved =
PredMap $
alterTM pty upd_solved (unPredMap $ inert_solved is) }
insertInertItem :: Ct -> InertSet -> InertSet
-- Add a new inert element to the inert set.
insertInertItem item is
Expand Down Expand Up @@ -655,26 +647,25 @@ insertInertItemTcS item
; traceTcS "insertInertItemTcS }" $ empty }
addToSolved :: CtEvidence -> TcS ()
addSolvedDict :: CtEvidence -> TcS ()
-- Add a new item in the solved set of the monad
addToSolved item
addSolvedDict item
| isIPPred (ctEvPred item) -- Never cache "solved" implicit parameters (not sure why!)
= return ()
| otherwise
= do { traceTcS "updSolvedSetTcs {" $
text "Trying to insert new solved item:" <+> ppr item
; updInertTcS (updSolvedSet item)
; traceTcS "updSolvedSetTcs }" $ empty }
= do { traceTcS "updSolvedSetTcs:" $ ppr item
; updInertTcS upd_solved_dicts }
where
upd_solved_dicts is
= is { inert_solved_dicts = PredMap $ alterTM pred upd_solved $
unPredMap $ inert_solved_dicts is }
pred = ctEvPred item
upd_solved _ = Just item
addSolvedFunEq :: Ct -> TcType -> TcS ()
addSolvedFunEq fun_eq fam_ty
= updInertTcS (upd_solved_funeqs . upd_solved)
-- Update both inert_solved and inert_solved_funeqs
-- The former is a superset of the latter
= updInertTcS upd_solved_funeqs
where
upd_solved = updSolvedSet (cc_ev fun_eq)
upd_solved_funeqs inert
= inert { inert_solved_funeqs = insertFamHead (inert_solved_funeqs inert) fam_ty fun_eq }
Expand Down Expand Up @@ -852,7 +843,7 @@ lookupFlatEqn fam_ty
lookupInInerts :: TcPredType -> TcS (Maybe CtEvidence)
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts pty
= do { IS { inert_solved = solved, inert_cans = ics } <- getTcSInerts
= do { IS { inert_solved_dicts = solved, inert_cans = ics } <- getTcSInerts
; case lookupInSolved solved pty of
Just ctev -> return (Just ctev)
Nothing -> return (lookupInInertCans ics pty) }
Expand Down Expand Up @@ -1476,15 +1467,8 @@ xCtFlavor :: CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS [CtEvidence]
xCtFlavor = xCtFlavor_cache True
xCtFlavor_cache :: Bool -- True = if wanted add to the solved bag!
-> CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
-> XEvTerm -- Instructions about how to manipulate evidence
-> TcS [CtEvidence]
xCtFlavor_cache _ (CtGiven { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
xCtFlavor (CtGiven { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
= ASSERT( equalLength ptys (ev_decomp xev tm) )
zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
-- For Givens we make new EvVars and bind them immediately. We don't worry
Expand All @@ -1496,16 +1480,12 @@ xCtFlavor_cache _ (CtGiven { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
-- But that superclass selector can't (yet) appear in a coercion
-- (see evTermCoercion), so the easy thing is to bind it to an Id
xCtFlavor_cache cache ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
xCtFlavor ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
= do { new_evars <- mapM (newWantedEvVar wl) ptys
; setEvBind evar (ev_comp xev (getEvTerms new_evars))
-- Add the now-solved wanted constraint to the cache
; when cache $ addToSolved ctev
; return (freshGoals new_evars) }
xCtFlavor_cache _ (CtDerived { ctev_wloc = wl }) ptys _xev
xCtFlavor (CtDerived { ctev_wloc = wl }) ptys _xev
= do { ders <- mapM (newDerived wl) ptys
; return (catMaybes ders) }
Expand All @@ -1514,6 +1494,9 @@ rewriteCtFlavor :: CtEvidence
-> TcPredType -- new predicate
-> TcCoercion -- new ~ old
-> TcS (Maybe CtEvidence)
-- Returns Just new_fl iff either (i) 'co' is reflexivity
-- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
-- In either case, there is nothing new to do with new_fl
{-
rewriteCtFlavor old_fl new_pred co
Main purpose: create new evidence for new_pred;
Expand All @@ -1534,28 +1517,19 @@ Main purpose: create new evidence for new_pred;
Not Just new_evidence
-}
rewriteCtFlavor = rewriteCtFlavor_cache True
-- Returns Just new_fl iff either (i) 'co' is reflexivity
-- or (ii) 'co' is not reflexivity, and 'new_pred' not cached
-- In either case, there is nothing new to do with new_fl
rewriteCtFlavor_cache :: Bool
-> CtEvidence -- old evidence
-> TcPredType -- new predicate
-> TcCoercion -- new ~ old
-> TcS (Maybe CtEvidence)
-- If derived, don't even look at the coercion
-- NB: this allows us to sneak away with ``error'' thunks for
-- coercions that come from derived ids (which don't exist!)
rewriteCtFlavor_cache _cache (CtDerived { ctev_wloc = wl }) pty_new _co
rewriteCtFlavor (CtDerived { ctev_wloc = wl }) pty_new _co
= newDerived wl pty_new
rewriteCtFlavor_cache _cache (CtGiven { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
rewriteCtFlavor (CtGiven { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
= return (Just (CtGiven { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
where
new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo
rewriteCtFlavor_cache cache ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = old_pred })
rewriteCtFlavor ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = old_pred })
new_pred co
| isTcReflCo co -- If just reflexivity then you may re-use the same variable
= return (Just (if old_pred `eqType` new_pred
Expand All @@ -1570,10 +1544,6 @@ rewriteCtFlavor_cache cache ctev@(CtWanted { ctev_wloc = wl, ctev_evar = evar, c
| otherwise
= do { new_evar <- newWantedEvVar wl new_pred
; setEvBind evar (mkEvCast (getEvTerm new_evar) co)
-- Add the now-solved wanted constraint to the cache
; when cache $ addToSolved ctev
; case new_evar of
Fresh ctev -> return (Just ctev)
_ -> return Nothing }
Expand Down

0 comments on commit b737a45

Please sign in to comment.