`Require Import Coq.Sorting.Permutation.` slows down `rewrite_strat` > 10x

This is a followup on https://github.com/coq/coq/issues/15596, but this time focusing on Require Import, because the fix for https://github.com/coq/coq/issues/15596 only addressed Require.

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

(*
Require Import Coq.Sorting.Permutation.
*)

Local Hint Rewrite Nat.add_0_r : mydb.

Goal forall
    (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.
  intros.
  Time rewrite_strat (topdown (hints mydb)) in A.

Uncommenting the Require Import Coq.Sorting.Permutation. slows down rewrite_strat by > 10x, to ca 3 seconds.

A workaround is

Global Remove Hints Permutation.Permutation_cons Permutation.Permutation_app' :
  typeclass_instances.

However, if I try to minimize the slowness by replacing Require Import Coq.Sorting.Permutation. with just the signatures of the two trouble-making instances, there's no slowdown:

Require Import Coq.Classes.Morphisms.

Definition Permutation{A: Type}: list A -> list A -> Prop. Admitted.

Local Instance Permutation_cons A :
 Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A).
Admitted.

Local Instance Permutation_app' A :
 Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A).
Admitted.

There seems to be some interesting performance issue in the interaction between rewrite_strat and typeclass search looking for morphisms.

Start by reproducing the provided rewrite_strat example with and without Require Import Coq.Sorting.Permutation, then read the linked issue #15596 and pull request #15597. Investigate the interaction between rewrite_strat and morphism typeclass search; done means identifying the regression and providing a fix that removes the reported slowdown without relying on the workaround.