Opening this so that I don't forget about it. The following example (thanks @Blaisorblade) should show the current, unwanted behavior so I should probably add this as a test case:
Lemma foo {M} : ⊢ ∃ (P : uPred M), P -∗ (∀ (x : nat), ⌜ x = x ⌝) ∗ P.
Proof.
iExists ?[P]. (* [iExists _.] also works. *)
iIntros "P". iSplit.
iIntros (x).
Fail iApply "P".
iAssumption.
Show.
(*
M : ucmraT
============================
"P" : False
--------------------------------------∗
False
*)