Frame instance for multiset union can interact badly with instantiating existential quantifiers

This is problematic:

From iris.proofmode Require Import proofmode.

Section test.
  Context {PROP : bi}.

  Lemma multiset_problem (P : PROP) : P ⊢ ∃ (X : gmultiset nat), [∗ mset] y ∈ X, False.
  Proof.
    iIntros "HP".
    Fail Timeout 2 iFrame "HP".
  Abort.
End test.

This happens because there is the following frame instance for framing inside a multiset union:

Global Instance frame_big_sepMS_disj_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
  Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
  Frame p R ([∗ mset] y ∈ X1 ⊎ X2, Φ y) Q | 2.
Proof. by rewrite /Frame big_sepMS_disj_union. Qed.

In our multiset_problem example, this instance will instantiate the evar ?X with a union ?X1 ⊎ ?X2. After two more steps, we encounter almost the same goal, and Frame instance search will loop.

The instances for [∗ list] do not suffer from this problem, since they are guarded by an IsCons or IsApp typeclass with proper Hint Modes.
To fix this, we could use the same approach: guard frame_big_sepMS_disj_union with a new class IsUnion.

Encountered by @janno @lepigre