Comments only

1 files 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)