Repeatedly failing `Affine` typeclass search can slow down `iFrame`
During patching iron for !1017 (merged), I ran into a situation similar to this (exaggerated to make effect more visible):
Lemma test_iFrame_affinely_3 P Q :
let i := 50 in (* controls amount of [Affine] searches *)
let j := 50 in (* controls hardness of an individual [Affine] search*)
let rep :=
fun n R T =>
([∗ list] P ∈ ((repeat R n) ++ [T]), P)%I
in
rep j (<affine> Q) Q ⊢ rep i (<affine> P) (<affine> P) ∗ rep j (<affine> Q) Q.
Proof.
iIntros (i j rep) "Hrep".
time iFrame "Hrep". (* 3.2 seconds *)
Undo 1.
time (iSplitR; last iFrame). (* 0.005 seconds *)
Abort.
The problematic Frame
instance is frame_affinely
, which attempts to show that the framed hypothesis is Affine
whenever the <affine>
modality occurs in the goal. One possible solution is to replace the Affine
condition with QuickAffine
in frame_affinely
:
Lemma frame_affinely_alt p R P Q Q' :
TCOr (TCEq p true) (classes_make.QuickAffine R) →
Frame p R P Q → classes_make.MakeAffinely Q Q' →
Frame p R (<affine> P) Q'. (* Default cost > 1 *)
Proof.
rewrite /classes_make.QuickAffine.
case; apply _.
Qed.
Remove Hints class_instances_frame.frame_affinely : typeclass_instances.
Existing Instance frame_affinely_alt.
(* speeds up the first iFrame to 0.3 seconds *)