iApply applies lemmas without resolving typeclass constraints
Consider this example:
From iris.algebra Require Import excl.
From iris.proofmode Require Import proofmode.
From iris.base_logic Require Import lib.iprop lib.own.
From iris.prelude Require Import options.
Class spin_lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
Local Existing Instance lock_tokG.
Definition spin_lockΣ : gFunctors := #[GFunctor (exclR unitO)].
Global Instance subG_spin_lockΣ {Σ} : subG spin_lockΣ Σ → spin_lockG Σ.
Proof. solve_inG. Qed.
Lemma test `{!spin_lockG Σ} (P Q : iProp Σ) :
P -∗ P -∗ Q.
Proof. Admitted.
Lemma test2 {Σ} (P Q : iProp Σ) :
P -∗ Q.
Proof.
iIntros "HP".
iApply (test with "HP").
I would expect the iApply
to fail, since the test
lemma needs spin_lockG
which is not present. Instead, it succeeds and creates a shelved goal. This is a pretty bad user experience since the shelved goal is easy to miss, so it is likely that one will continue in this proof not realizing that one has applied an impossible lemma. This can also cause very strange follow-on effects since the unresolved evar can cause unification failures and other hard-to-diagnose issues.