Skip to content

Commit

Permalink
Merge b737a4 into the 7.6 branch, curing Trac #7748
Browse files Browse the repository at this point in the history 
The caching of goals in the constraint solver led to a
equality-constraint loop even in a really simple program!

    commit b737a45
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Fri Aug 31 10:05:03 2012 +0100

    More simplifications to the constraint solver

    * 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 Apr 16, 2013
1 parent 04fefe8 commit 3ed9baf
Show file tree
Hide file tree
Showing 4 changed files with 66 additions and 85 deletions.
27 changes: 13 additions & 14 deletions compiler/typecheck/TcCanonical.lhs
View file
Expand Up @@ -39,7 +39,7 @@ import Util
import TysWiredIn ( eqTyCon )
import Data.Maybe ( isJust, fromMaybe )
import Data.Maybe ( fromMaybe )
-- import Data.List ( zip4 )
\end{code}

Expand Down Expand Up @@ -849,7 +849,7 @@ emitKindConstraint ct
xdecomp x = [mkEvKindCast x (evTermCoercion kev)]
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 @@ -1181,14 +1181,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 @@ -1221,19 +1221,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
18 changes: 9 additions & 9 deletions compiler/typecheck/TcInteract.lhs
View file
Expand Up @@ -391,7 +391,7 @@ kick_out_rewritable ct is@(IS { inert_cans =
, 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
fl = cc_ev ct
Expand Down Expand Up @@ -774,8 +774,8 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
-- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
; ctevs <- xCtFlavor_cache False fl2 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
; ctevs <- xCtFlavor fl2 [mkTcEqPred xi2 xi1] xev
-- See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
; add_to_work d2 ctevs
; irWorkItemConsumed "FunEq/FunEq" }
Expand All @@ -792,8 +792,8 @@ doInteractWithInert ii@(CFunEqCan { cc_ev = fl1, cc_fun = tc1
-- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
; ctevs <- xCtFlavor_cache False fl1 [mkTcEqPred xi2 xi1] xev
-- Why not simply xCtFlavor? See Note [Cache-caused loops]
; ctevs <- xCtFlavor fl1 [mkTcEqPred xi2 xi1] xev
-- See Note [Cache-caused loops]
-- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
; add_to_work d1 ctevs
Expand Down Expand Up @@ -1455,8 +1455,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 @@ -1514,8 +1514,7 @@ doTopReactFunEq fl tc args xi d
-- Found a top-level instance
do { -- Add it to the solved goals
unless (isDerived fl) $
do { addSolvedFunEq fl
; addToSolved fl }
do { addSolvedFunEq fl }
; let coe_ax = famInstAxiom famInst
; succeed_with (mkTcAxInstCo coe_ax rep_tys)
Expand All @@ -1524,6 +1523,7 @@ doTopReactFunEq fl tc args xi d
succeed_with :: TcCoercion -> TcType -> TcS TopInteractResult
succeed_with coe rhs_ty
= do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
; traceTcS ("doTopReactFunEq ") (ppr ctevs)
; case ctevs of
[ctev] -> updWorkListTcS $ extendWorkListEq $
CNonCanonical { cc_ev = ctev
Expand Down
104 changes: 43 additions & 61 deletions compiler/typecheck/TcSMonad.lhs
View file
Expand Up @@ -38,19 +38,18 @@ module TcSMonad (
wrapErrTcS, wrapWarnTcS,
-- Getting and setting the flattening cache
getFlatCache, updFlatCache, addToSolved, addSolvedFunEq,
getFlatCache, updFlatCache, addSolvedDict, addSolvedFunEq,
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 @@ -383,6 +382,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 @@ -520,7 +525,7 @@ data InertSet
, inert_solved_funeqs :: FamHeadMap CtEvidence -- Of form co :: F xis ~ xi
-- No Deriveds
, inert_solved :: PredMap CtEvidence -- All others
, inert_solved_dicts :: PredMap CtEvidence -- All others
-- These two fields constitute a cache of solved (only!) constraints
-- See Note [Solved constraints]
-- - Constraints of form (F xis ~ xi) live in inert_solved_funeqs,
Expand All @@ -544,10 +549,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 @@ -558,19 +561,9 @@ emptyInert
, inert_irreds = emptyCts }
, inert_frozen = emptyCts
, inert_flat_cache = FamHeadMap emptyTM
, inert_solved = PredMap emptyTM
, inert_solved_dicts = PredMap emptyTM
, inert_solved_funeqs = FamHeadMap emptyTM }
updSolvedSet :: InertSet -> CtEvidence -> InertSet
updSolvedSet is item
= 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) }
updInertSet :: InertSet -> Ct -> InertSet
-- Add a new inert element to the inert set.
Expand Down Expand Up @@ -629,22 +622,24 @@ updInertSetTcS item
; traceTcS "updInertSetTcs }" $ 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
; modifyInertTcS (\is -> ((), updSolvedSet is 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 :: CtEvidence -> TcS ()
addSolvedFunEq fun_eq
= modifyInertTcS $ \inert -> ((), upd_inert inert)
= updInertTcS upd_inert
where
upd_inert inert
= let slvd = unFamHeadMap (inert_solved_funeqs inert)
Expand All @@ -664,7 +659,13 @@ modifyInertTcS upd
; wrapTcS (TcM.writeTcRef is_var new_inert)
; return a }
updInertTcS :: (InertSet -> InertSet) -> TcS ()
-- Modify the inert set with the supplied function
updInertTcS upd
= do { is_var <- getTcSInertsRef
; curr_inert <- wrapTcS (TcM.readTcRef is_var)
; let new_inert = upd curr_inert
; wrapTcS (TcM.writeTcRef is_var new_inert) }
splitInertsForImplications :: InertSet -> ([Ct],InertSet)
-- Converts the Wanted of the original inert to Given and removes
Expand Down Expand Up @@ -696,7 +697,7 @@ splitInertsForImplications is
, inert_dicts = dicts
}
, inert_frozen = _frozen
, inert_solved = solved
, inert_solved_dicts = solved
, inert_flat_cache = flat_cache
, inert_solved_funeqs = funeq_cache
})
Expand All @@ -711,7 +712,7 @@ splitInertsForImplications is
-- At some point, I used to flush all the solved, in
-- fear of evidence loops. But I think we are safe,
-- flushing is why T3064 had become slower
, inert_solved = solved -- PredMap emptyTM
, inert_solved_dicts = solved -- PredMap emptyTM
, inert_flat_cache = flat_cache -- FamHeadMap emptyTM
, inert_solved_funeqs = funeq_cache -- FamHeadMap emptyTM
}
Expand Down Expand Up @@ -787,7 +788,7 @@ extractRelevantInerts wi
lookupInInerts :: InertSet -> TcPredType -> Maybe CtEvidence
-- Is this exact predicate type cached in the solved or canonicals of the InertSet
lookupInInerts (IS { inert_solved = solved, inert_cans = ics }) pty
lookupInInerts (IS { inert_solved_dicts = solved, inert_cans = ics }) pty
= case lookupInSolved solved pty of
Just ctev -> return ctev
Nothing -> lookupInInertCans ics pty
Expand Down Expand Up @@ -1505,29 +1506,17 @@ 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 _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
xCtFlavor (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
= ASSERT( equalLength ptys (ev_decomp xev tm) )
zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
-- See Note [Bind new Givens immediately]
xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
xCtFlavor (Wanted { 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 _ (Derived { ctev_wloc = wl }) ptys _xev
xCtFlavor (Derived { ctev_wloc = wl }) ptys _xev
= do { ders <- mapM (newDerived wl) ptys
; return (catMaybes ders) }
Expand All @@ -1536,6 +1525,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 a new identity (flavor) for new_pred;
Expand All @@ -1558,29 +1550,23 @@ Main purpose: create a new identity (flavor) for new_pred;
Solved NEVER HAPPENS
-}
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
-> 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 (Derived { ctev_wloc = wl }) pty_new _co
rewriteCtFlavor (Derived { ctev_wloc = wl }) pty_new _co
= newDerived wl pty_new
rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
rewriteCtFlavor (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
= do { new_ev <- newGivenEvVar gl pty_new new_tm -- See Note [Bind new Givens immediately]
; return (Just new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo
rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co
rewriteCtFlavor ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, ctev_pred = pty_old }) pty_new co
| isTcReflCo co -- If just reflexivity then you may re-use the same variable
= return (Just (if pty_old `eqType` pty_new
then ctev
Expand All @@ -1591,10 +1577,6 @@ rewriteCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar, cte
| otherwise
= do { new_evar <- newWantedEvVar wl pty_new
; 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
2 changes: 1 addition & 1 deletion compiler/typecheck/TcSimplify.lhs
View file
Expand Up @@ -946,7 +946,7 @@ shadowIPs gs m
_ -> False
purgeShadowed is = is { inert_cans = purgeCans (inert_cans is)
, inert_solved = purgeSolved (inert_solved is)
, inert_solved_dicts = purgeSolved (inert_solved_dicts is)
}
purgeDicts = snd . partitionCCanMap isShadowedCt
Expand Down

0 comments on commit 3ed9baf

Please sign in to comment.