Persistent searches can instantiate evars for instance via `big_sepL_nil_persistent`
Already discussed in https://mattermost.mpi-sws.org/iris/pl/yemuustbc7gatximj8uoxq544r, but probably stuck on Strict Resolution
not working:
From iris.base_logic Require Import invariants.
From iris.proofmode Require Import proofmode.
Section inv.
Context `{!invGS_gen hlc Σ}.
Goal ⊢@{iProp Σ} ∃ (l : list nat) A B, A -∗ ([∗list] x ∈ l, B x) -∗ False.
iIntros. iExists _, _, _.
Set Typeclasses Debug.
iIntros.
(*
Result:
hlc: has_lc
Σ: gFunctors
invGS_gen0: invGS_gen hlc Σ
1/1
_ : [∗ list] x ∈ [], ?Goal0 x
--------------------------------------□
_ : ?Goal
--------------------------------------∗
False
*)
(* The TC trace includes the offending part:
1: looking for (Persistent ([∗ list] x ∈ ?Goal, ?Goal1 x)) with backtracking
1.1: simple apply @big_sepL_nil_persistent on
(Persistent ([∗ list] x ∈ ?Goal, ?Goal1 x)), 0 subgoal(s)
1: looking for (Affine ([∗ list] x ∈ [], ?Goal0 x)) with backtracking
1.1: simple apply @big_sepL_nil_affine on
(Affine ([∗ list] x ∈ [], ?Goal0 x)), 0 subgoal(s)
*)