Commit 545bb796 authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 4dade857
......@@ -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
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment