Require Coq.Sorting.Permutation. slows down rewrite_strat by > 10x

[samuelgruetter]

Require Import Coq.Lists.List. Import ListNotations.
Require Import Coq.Arith.PeanoNat.

(*Require Coq.Sorting.Permutation.*)

Local Hint Rewrite Nat.add_0_r : mydb.

Lemma foo 
    (l : list nat)
    (v v0 mscratch: nat)
    (maprep: Type)
    (m: maprep)
    (Array : (nat -> nat -> maprep -> Prop) ->
               nat -> list nat -> nat -> maprep -> Prop)
    (Scalar : nat -> nat -> maprep -> Prop)
    (atAddr : nat -> (nat -> maprep -> Prop) -> maprep -> Prop)
    (A : atAddr mscratch
                (Array Scalar 4
                       ([v0] ++ [v + 0] ++ l)) m)
     : False.
Proof.
  Time rewrite_strat (topdown (hints mydb)) in A.

• On master from Fri Jan 21, uncommenting Require Coq.Sorting.Permutation. increases the time from 0.254 secs to 3.572 secs.
• On 8.15-rc1, uncommenting Require Coq.Sorting.Permutation. increases the time from 0.071 to 26.511 secs.

If I don't need any setoid_rewrite functionality, will this be fixed by #15093, because I could just pass in an empty hint DB for the morphisms?

But for users who do need setoid_rewrite functionality, is there a way to shrink this performance gap? I see that Coq.Sorting.Permutation. contains a lot of global instances, which could/should be made #[export], on the other hand, do these "off-topic" instances really need to slow down rewrite_strat that much?

[Alizter]

cc @mattam82

[SkySkimmer]

permutation_cons and permutation_app' are the problem, the other instances by themselves cause no slowdown.
#15597

[samuelgruetter]

#15597 fixes the issue for users who Require Coq.Sorting.Permutation., but for users who Require Import Coq.Sorting.Permutation., it's still slow. There seems to be some interesting performance issue in the interaction between rewrite_strat and typeclass search looking for morphisms, so I would suggest to keep this issue open (but it seems I don't have the power to reopen it).

[Alizter]

@samuelgruetter Can you open a new issue?