From 3ed9baf44904ad7ca0402f5a1b493a23d9d49253 Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Tue, 16 Apr 2013 07:27:23 +0100 Subject: [PATCH] Merge b737a4 into the 7.6 branch, curing Trac #7748 The caching of goals in the constraint solver led to a equality-constraint loop even in a really simple program! commit b737a45391201fd475b89227ed1d7c9b72b24eea Author: Simon Peyton Jones 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.) --- compiler/typecheck/TcCanonical.lhs | 27 ++++---- compiler/typecheck/TcInteract.lhs | 18 ++--- compiler/typecheck/TcSMonad.lhs | 104 ++++++++++++----------------- compiler/typecheck/TcSimplify.lhs | 2 +- 4 files changed, 66 insertions(+), 85 deletions(-) diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs index b013e258f39a..2ea331006faf 100644 --- a/compiler/typecheck/TcCanonical.lhs +++ b/compiler/typecheck/TcCanonical.lhs @@ -39,7 +39,7 @@ import Util import TysWiredIn ( eqTyCon ) -import Data.Maybe ( isJust, fromMaybe ) +import Data.Maybe ( fromMaybe ) -- import Data.List ( zip4 ) \end{code} @@ -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) @@ -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 @@ -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} diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 2c2dc54c1b09..ee394967fdb2 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -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 @@ -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" } @@ -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 @@ -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 } @@ -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) @@ -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 diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 8adb1d504fd2..2cf47c2828bc 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -38,7 +38,7 @@ module TcSMonad ( wrapErrTcS, wrapWarnTcS, -- Getting and setting the flattening cache - getFlatCache, updFlatCache, addToSolved, addSolvedFunEq, + getFlatCache, updFlatCache, addSolvedDict, addSolvedFunEq, deferTcSForAllEq, @@ -46,11 +46,10 @@ module TcSMonad ( 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, @@ -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 @@ -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, @@ -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 @@ -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. @@ -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) @@ -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 @@ -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 }) @@ -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 } @@ -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 @@ -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) } @@ -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; @@ -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 @@ -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 } diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs index bf407eb52e4a..b45a5ec63932 100644 --- a/compiler/typecheck/TcSimplify.lhs +++ b/compiler/typecheck/TcSimplify.lhs @@ -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