Inconsistency in weakening of modalities in `iApply`

From iris.proofmode Require Import tactics.

Lemma test {PROP : bi} (P Q : PROP) :
  (P -∗ <affine> Q) -∗ Q.
Proof.
  iIntros "H".
  Fail iApply "H". (* fails *)
  iApply ("H" with "[]"). (* works *)

Analysis

What happens is that the first (and failing) iApply directly attempts to find an IntoWand instance to match the conclusion of the wand with the goal. This fails because the only applicable IntoWand instance is:

Global Instance into_wand_wand p q P Q P' :
  FromAssumption q P P' → IntoWand p q (P' -∗ Q) P Q.

There is no FromAssumption for Q, so no weakening of the conclusion is performed.

In the second attempt, iApply will first iSpecialize with the wand. As such, it tries to find an IntoWand instance where the conclusion can be unified with an evar. Then after that, it will use iAssumption, which uses FromAssumption to weaken the modality.

Solution

We probably should add FromAssumption to instances like into_wand_wand. I do not know if this was just an omission, or there's a reason for that. Should try.