[commit: ghc] ghc-new-flavor: Dropping the idempotence restriction on the inert substitution, (5802ebd)
dimitris at microsoft.com
dimitris at microsoft.com
Tue Apr 3 14:30:43 CEST 2012
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 <dimitris at microsoft.com>
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
More information about the Cvs-ghc
mailing list