Slowness of `set_unfold` for `gset`

This issue follows up on iris#232 (closed).

It appears that set_unfold is very slow on goals involving gset. For example, when calling set_unfold on a goal like the following, it takes near half a second.

Lemma slow `{Countable K} (X1 X2 X3 : gset K) :
  X1 ∪ (X2 ∪ X3) = (X1 ∪ X2) ∪ X3.

Interestingly enough, the problem does not appear in the following goal, where set_unfold takes close to no time:

Lemma fast `{FinSet K C, !LeibnizEquiv C} (X1 X2 X3 : C) :
  X1 ∪ (X2 ∪ X3) = (X1 ∪ X2) ∪ X3.

So, clearly set_unfold is doing inefficient things in combination with gset.

After a bit of trial and error, it appears that the elem_of operation on gset is the culprit. Type class search, as used in the implementation of set_unfold tries to unfold stuff there. If I make elem_of type class opaque, the performance improves significantly.

I tried a bunch of stuff:

• Make elem_of type class opaque. If we go this route, I believe we should make all operational type classes opaque. That would be a good thing, so we less often rely on stuff that's accidentally convertible (by breaking abstractions). I tried this, see https://gitlab.mpi-sws.org/iris/stdpp/tree/robbert/tc_opaque This causes quite a bit of breakage in Iris as expected. More annoyingly, the performance implications on Iris are unclear https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=7cd65053a1a3e8665f4270c2f6857a18cb41fb69&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Ftc_opaque&var-commit2=5e9d94b31f671e2e1e771789fb1fd92f86856166&var-config2=coq-8.9.0&var-group=(.)%2F%5B%5E%2F%5D&var-metric=instructions Random stuff gets slower, random stuff gets faster.
• Make just mapset_elem_of or gset_elem_of type class opaque. This appears to not fix the issue.
• Seal mapset_elem_of. This appears to not fix the issue.

Some experiments

From stdpp Require Import gmap.

Lemma fast `{FinSet K C, !LeibnizEquiv C} (X1 X2 X3 : C) :
  X1 ∪ (X2 ∪ X3) = (X1 ∪ X2) ∪ X3.
Proof.
  Time set_unfold.
  (* Finished transaction in 0.032 secs (0.031u,0.s) (successful) *)
Abort.

Lemma slow `{Countable K} (X1 X2 X3 : gset K) :
  X1 ∪ (X2 ∪ X3) = (X1 ∪ X2) ∪ X3.
Proof.
  Time set_unfold.
  (* Finished transaction in 0.382 secs (0.373u,0.s) (successful) *)
Restart.
  Typeclasses Opaque elem_of.
  Time set_unfold.
  (* Finished transaction in 0.03 secs (0.029u,0.s) (successful) *)
  Typeclasses Transparent elem_of. (* undo *)
Restart.
  Typeclasses Opaque gset_elem_of.
  Time set_unfold.
  (* Finished transaction in 0.253 secs (0.252u,0.s) (successful) *)
Restart.
  Typeclasses Opaque mapset.mapset_elem_of.
  Time set_unfold.
  (* Finished transaction in 0.366 secs (0.357u,0.s) (successful)
     WTF this is even slower? *)
Admitted.

Lemma fast_big `{FinSet K C, !LeibnizEquiv C} (X1 X2 X3 : C) :
  X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 =
  X1 ∪ X2 ∪ X3 ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 ∪
  X1 ∪ X2 ∪ X3 ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2.
Proof.
  Time set_unfold.
  (* Finished transaction in 0.135 secs (0.131u,0.s) (successful) *)
Admitted.

Lemma slow_big `{Countable K} (X1 X2 X3 : gset K) :
  X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 =
  X1 ∪ X2 ∪ X3 ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2 ∪
  X1 ∪ X2 ∪ X3 ∪ X1 ∪ X2 ∪ X1 ∪ (X2 ∪ X3) ∪ X1 ∪ X2.
Proof.
  Time set_unfold.
  (* Finished transaction in 1.839 secs (1.836u,0.004s) (successful) *)
Restart.
  Typeclasses Opaque elem_of.
  Time set_unfold.
  (* Finished transaction in 0.157 secs (0.148u,0.s) (successful) *)
Admitted.