## 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.
```