Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : ghc-new-flavor
http://hackage.haskell.org/trac/ghc/changeset/5802ebddd133f4744f5a05539a73166654a6fc76 >--------------------------------------------------------------- commit 5802ebddd133f4744f5a05539a73166654a6fc76 Author: Dimitrios.Vytiniotis <[email protected]> Date: Mon Apr 2 16:34:36 2012 +0100 Dropping the idempotence restriction on the inert substitution, for efficiency. More documentation to follow. >--------------------------------------------------------------- compiler/typecheck/TcInteract.lhs | 93 ++++++++++--------------------------- 1 files changed, 24 insertions(+), 69 deletions(-) diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index f2e193f..879a8f4 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -55,7 +55,7 @@ import qualified Data.Traversable as Traversable import Data.Maybe ( isJust ) import Control.Monad( when, unless ) -import Pair ( pSnd ) +import Pair () import UniqFM import FastString ( sLit ) import DynFlags @@ -316,9 +316,10 @@ kickOutRewritableInerts ct rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution -> TyVarEnv Ct -- All the inert equalities -> TcS (TyVarEnv Ct) -- The new inert equalities -rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs --- The goal: traverse the inert equalities and rewrite some of them, dropping some others --- back to the worklist. This is delicate, see Note [Delicate equality kick-out] +rewriteInertEqsFromInertEq (subst_tv, _subst_co, subst_fl) ieqs +-- The goal: traverse the inert equalities and throw some of them back to the worklist +-- if you have to rewrite and recheck them for occurs check errors. +-- This is delicate, see Note [Delicate equality kick-out] = do { mieqs <- Traversable.mapM do_one ieqs ; traceTcS "Original inert equalities:" (ppr ieqs) ; let flatten_justs elem venv @@ -330,63 +331,18 @@ rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs where do_one ct | subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct) - -- Annoyingly inefficient, but we can't simply check - -- that isReflCo co because of cached solved ReflCo evidence. = if fl `canRewrite` subst_fl then - -- If also the inert can rewrite the subst it's totally safe - -- to rewrite on the spot - do { - -{- DV: I thought this might work but not because you don't have the full knowledge of the - implications (just the worklist). And it's a bit tedious. SPJ and I discussed about breaking - the 'idempotent substitution' invariant to be a little more lazy. -} - - -- DV: Very experimental! - -- If it's a given equality and its LHS does not appear in the worklist - -- there is no point in rewriting him. In fact there is not point in keeping him, - -- at all, is there? - worklist_tvs <- getTcSWorkListTvs - ; if isGiven (cc_flavor ct) && not (tyVarsOfCt ct `elemVarSet` worklist_tvs) then - return Nothing - else do { - ct' <- rewrite_on_the_spot ct - ; return $ Just ct' } - } + -- If also the inert can rewrite the subst then there is no danger of + -- occurs check errors sor keep it there. No need to rewrite the inert equality + -- (as we did in the past): See Note [Non-idempotent inert substitution] + return (Just ct) + -- used to be: rewrite_on_the_spot ct >>= ( return . Just ) else -- We have to throw inert back to worklist for occurs checks - do { updWorkListTcS (extendWorkListEq ct) - ; return Nothing } + updWorkListTcS (extendWorkListEq ct) >> return Nothing | otherwise -- Just keep it there - = return $ Just ct + = return (Just ct) where - -- We have that: subst_co :: subst_tv ~ tau - -- An an old inert: tv ~ rhs - -- That we want to rewrite on-the-spot to tv ~ rhs[tau/subst_tv] fl = cc_flavor ct - tv = cc_tyvar ct - rhs = cc_rhs ct - - rewrite_on_the_spot ct - = do { let rhs_co = liftTcCoSubstWith [subst_tv] [subst_co] rhs - eq_co = mkTcTyConAppCo eqTyCon $ - [ mkTcReflCo (defaultKind $ typeKind rhs) - , mkTcReflCo (mkTyVarTy tv) - , mkTcSymCo rhs_co ] - new_rhs = pSnd (tcCoercionKind rhs_co) - new_eq_pred = mkTcEqPred (mkTyVarTy tv) new_rhs - -- eq_co :: (tv ~ rhs[s/x]) ~ (tv ~ rhs[x]) - - ; mb_fl <- rewriteCtFlavor fl new_eq_pred eq_co - ; case mb_fl of - Just new_fl -> return $ - ct {cc_flavor=new_fl,cc_rhs=new_rhs} - Nothing -> -- Weird, rewritten constraint was solved - -- before -- I am uncertain about what to do - pprPanic "Interesting: \ - rewrote inert equality to existing!" $ - vcat [ text "original ="<+>ppr ct - , text "new eqpred ="<+>ppr new_eq_pred ] - } - kick_out_rewritable :: Ct -> InertSet @@ -451,25 +407,24 @@ Note [Delicate equality kick-out] Delicate: When kicking out rewritable constraints, it would be safe to simply kick out all rewritable equalities, but instead we only kick out those -that, when rewritten, may result in occur-check errors. We rewrite the -rest on the spot. Example: +that, when rewritten, may result in occur-check errors. Example: - WorkItem = [S] a ~ b + WorkItem = [G] a ~ b Inerts = { [W] b ~ [a] } Now at this point the work item cannot be further rewritten by the -inert (due to the weaker inert flavor), so we are examining if we can -instead rewrite the inert from the workitem. But if we rewrite it on -the spot we have to recanonicalize because of the danger of occurs -errors. On the other hand if the inert flavor was just as powerful or -more powerful than the workitem flavor, the work-item could not have -reached this stage (because it would have already been rewritten by -the inert). +inert (due to the weaker inert flavor). Instead the workitem can +rewrite the inert leading to potential occur check errors. So we must +kick the inert out. On the other hand, if the inert flavor was as +powerful or more powerful than the workitem flavor, the work-item could +not have reached this stage (because it would have already been +rewritten by the inert). The coclusion is: we kick out the 'dangerous' equalities that may -require recanonicalization (occurs checks) and the rest we rewrite -unconditionally without further checks, on-the-spot with function -rewriteInertEqsFromInertEq. +require recanonicalization (occurs checks) and the rest we keep +there in the inerts without further checks. +In the past we used to rewrite-on-the-spot those equalities that we keep in, +but this is no longer necessary see Note [Non-idempotent inert substitution]. \begin{code} data SPSolveResult = SPCantSolve _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
