Commit 8dc6da83 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Comments only

parent 8c5fe53b
......@@ -714,7 +714,10 @@ Note that inertness is not the same as idempotence. To apply S to a
type, you may have to apply it recursive. But inertness does
guarantee that this recursive use will terminate.
---------- The main theorem --------------
Note [Extending the inert equalities]
This is the main theorem!
Suppose we have a "work item"
a -fw-> t
and an inert generalised substitution S,
......@@ -724,6 +727,9 @@ guarantee that this recursive use will terminate.
(T3) a not in t -- No occurs check in the work item
(K1) for every (a -fs-> s) in S, then not (fw >= fs)
Reason: the work item is fully rewritten by S, hence not (fs >= fw)
but if (fw >= fs) then the work item could rewrite
the inert item
(K2) for every (b -fs-> s) in S, where b /= a, then
(K2a) not (fs >= fs)
......@@ -740,11 +746,16 @@ guarantee that this recursive use will terminate.
then the extended substition T = S+(a -fw-> t)
is an inert generalised substitution.
Conditions (T1-T3) are established by the canonicaliser
Conditions (K1-K3) are established by TcSMonad.kickOutRewriteable
The idea is that
* (T1-2) are guaranteed by exhaustively rewriting the work-item
with S(fw,_).
* T3 is guaranteed by a simple occurs-check on the work item.
This is done during canonicalisation, in canEqTyVar;
(invariant: a CTyEqCan never has an occurs check).
* (K1-3) are the "kick-out" criteria. (As stated, they are really the
"keep" criteria.) If the current inert S contains a triple that does
......@@ -761,6 +772,12 @@ The idea is that
us to kick out an inert wanted that mentions a, because of (K2a). This
is a common case, hence good not to kick out.
* Lemma (L2): if not (fw >= fw), then K1-K3 all hold.
Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
and so K1-K3 hold. Intuitivel, since fw can't rewrite anything,
adding it cannot cause any loops
This is a common case, because Wanteds cannot rewrite Wanteds.
* Lemma (L1): The conditions of the Main Theorem imply that there is no
(a -fs-> t) in S, s.t. (fs >= fw).
Proof. Suppose the contrary (fs >= fw). Then because of (T1),
......@@ -1304,6 +1321,7 @@ kickOutRewritable :: CtFlavourRole -- Flavour and role of the equality that is
-- take the substitution into account
kickOutRewritable new_fr new_tv ics@(IC { inert_funeqs = funeqmap })
| not (new_fr `eqCanRewriteFR` new_fr)
-- Lemma (L2) in Note [Extending the inert equalities]
= if isFlattenTyVar new_tv
then (emptyWorkList { wl_funeqs = feqs_out }, ics { inert_funeqs = feqs_in })
else (emptyWorkList, ics)
......@@ -1356,8 +1374,8 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs = tv_eqs
(insols_out, insols_in) = partitionBag kick_out_ct insols
-- Kick out even insolubles; see Note [Kick out insolubles]
can_rewrite :: CtEvidence -> Bool
can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole
fr_can_rewrite :: CtEvidence -> Bool
fr_can_rewrite = (new_fr `eqCanRewriteFR`) . ctEvFlavourRole
kick_out_ct :: Ct -> Bool
kick_out_ct ct = kick_out_ctev (ctEvidence ct)
......@@ -1368,12 +1386,12 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs = tv_eqs
kick_out_fe _ = False -- Can't happen
kick_out_ctev :: CtEvidence -> Bool
kick_out_ctev ev = can_rewrite ev
kick_out_ctev ev = fr_can_rewrite ev
&& new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
-- See Note [Kicking out inert constraints]
kick_out_irred :: Ct -> Bool
kick_out_irred ct = can_rewrite (cc_ev ct)
kick_out_irred ct = fr_can_rewrite (cc_ev ct)
&& new_tv `elemVarSet` closeOverKinds (TcM.tyVarsOfCt ct)
-- See Note [Kicking out Irreds]
......@@ -1386,23 +1404,23 @@ kickOutRewritable new_fr new_tv (IC { inert_eqs = tv_eqs
(eqs_in, eqs_out) = partition keep_eq eqs
-- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
-- Implements criteria K1-K3 in Note [Extending the inert equalities]
keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
, cc_eq_rel = eq_rel })
| tv == new_tv
= not (can_rewrite ev) -- (K1)
= not (fr_can_rewrite ev) -- (K1)
| otherwise
= check_k2 && check_k3
ev_fr = ctEvFlavourRole ev
check_k2 = not (ev_fr `eqCanRewriteFR` ev_fr)
|| not (new_fr `eqCanRewriteFR` ev_fr)
|| (ev_fr `eqCanRewriteFR` new_fr)
|| not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
fs = ctEvFlavourRole ev
check_k2 = not (fs `eqCanRewriteFR` fs) -- (K2a)
|| (fs `eqCanRewriteFR` new_fr) -- (K2b)
|| not (new_fr `eqCanRewriteFR` fs) -- (K2c)
|| not (new_tv `elemVarSet` tyVarsOfType rhs_ty) -- (K2d)
| new_fr `eqCanRewriteFR` ev_fr
| new_fr `eqCanRewriteFR` fs
= case eq_rel of
NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
ReprEq -> not (isTyVarExposed new_tv rhs_ty)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment