Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : master
http://hackage.haskell.org/trac/ghc/changeset/545bb79667ebcbf5e776f76518cf68b4d507e7f5 >--------------------------------------------------------------- commit 545bb79667ebcbf5e776f76518cf68b4d507e7f5 Author: Simon Peyton Jones <simo...@microsoft.com> Date: Tue Nov 6 16:12:39 2012 +0000 Refine the "kick-out" predicate for CTyVarEq Consider Work item: k ~ * Inert item: (a::k) ~ Int Then we must kick out the inert item! We weren't doing that, something I discovered when fixing Trac #7384. Discussed with Dimitrios, and we wrote a long comment Note [Delicate equality kick-out] to explain. >--------------------------------------------------------------- compiler/typecheck/TcInteract.lhs | 67 +++++++++++++++++++++--------------- 1 files changed, 39 insertions(+), 28 deletions(-) diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index a75890f..3facc1e 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -335,13 +335,17 @@ kickOutRewritable new_flav new_tv -- constraints that mention type variables whose -- kinds could contain this variable! - kick_out_eq inert_ct = kick_out_ct inert_ct && - not (ctFlavour inert_ct `canRewrite` new_flav) - -- 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) because of point (8) of - -- See Note [Detailed InertCans Invariants] - -- and Note [Delicate equality kick-out] + kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev }) + = (new_flav `canRewrite` inert_flav) -- See Note [Delicate equality kick-out] + && (new_tv `elemVarSet` kind_vars || -- (1) + (not (inert_flav `canRewrite` new_flav) && -- (2) + new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv))) + where + inert_flav = ctEvFlavour ev + kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet` + tyVarsOfType (typeKind rhs) + + kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct) \end{code} Note [Kick out insolubles] @@ -355,27 +359,34 @@ outer type constructors match. 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. Example: - - 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). 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 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]. +When adding an equality (a ~ xi), we kick out an inert type-variable +equality (b ~ phi) in two cases + +(1) If the new tyvar can rewrite the kind LHS or RHS of the inert + equality. Example: + Work item: [W] k ~ * + Inert: [W] (a:k) ~ ty + [W] (b:*) ~ c :: k + We must kick out those blocked inerts so that we rewrite them + and can subsequently unify. + +(2) If the new tyvar can + Work item: [G] a ~ b + Inert: [W] b ~ [a] + Now at this point the work item cannot be further rewritten by the + inert (due to the weaker inert flavor). But we can't add the work item + as-is because the inert set would then have a cyclic substitution, + when rewriting a wanted type mentioning 'a'. So we must kick the inert out. + + We have to do this only if the inert *cannot* rewrite the work item; + it it can, then the work item will have been fully rewritten by the + inert during canonicalisation. So for example: + Work item: [W] a ~ Int + Inert: [W] b ~ [a] + No need to kick out the inert, beause the inert substitution is not + necessarily idemopotent. See Note [Non-idempotent inert substitution]. + +See also point (8) of Note [Detailed InertCans Invariants] \begin{code} data SPSolveResult = SPCantSolve _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
