diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 7f2dd662285cc29e5ab0ecb0b204a5defdac8dcc..34e7843f69fb953f95963622d5b1fcd8c6049978 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)