iPoseProof with malformed pm_trm diverges
Some of my Iris students stumbled across this issue: when iPoseProof and derived tactics are given a bad proof mode term, they appear to run forever instead of giving an error. A minimal example:
Lemma test Σ (P : iProp Σ) : P -∗ P.
Proof.
iIntros "P".
iPoseProof ("P" "P") as "H". (* diverges *)
This is a pretty silly example, but it's easy to stumble into if you forget the $!
or with
notation:
Lemma test2 Σ (P : expr -> iProp Σ) (x : nat) : (∀ x, P x) -∗ P #x.
Proof.
iIntros "P".
iPoseProof ("P" #x) as "H". (* diverges *)
This appears to be the case in versions from 3.4.0 to the current dev version (dev.2022-04-07.0.8fa39f7c).