From 8dc6da83f43ceb5e595e00fc454111720fe02ec3 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones
Date: Tue, 24 Nov 2015 13:25:51 +0000
Subject: [PATCH] Comments only
---
compiler/typecheck/TcSMonad.hs | 44 ++++++++++++++++++++++++----------
1 file changed, 31 insertions(+), 13 deletions(-)
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 7f2dd66228..34e7843f69 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -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
where
(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
where
- 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)
check_k3
- | 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)
--
2.25.4