coqc infinite loop in type class resolution

Description of the problem

Compiling this program makes coqc go into an infinite loop.

Note that there is a "bug" in the program because I commented out `(Equivalence F).

This will make coqc search forever for which Equivalence instance it should
use in foo.

Require Import Setoid.
Require Import RelationClasses. (* for Equivalence  *)

Definition equ {T} {e} `(Equivalence T e) := e.
Notation "f == g" := (equ _ f g)  (at level 80).

Class Op (A:Type) := op : A -> A -> A.

Class C F  `(Op F) (* `(Equivalence F) *) :=
{
    foo : forall a b , op a b == op a b;
}.

Coq Version

I installed v8.15.1 with nix.

[nix-shell]$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.12.1

I also tried 8.14.1 and 8.13.1 with the same result.
And I just (July 16, 2022) tried it with master, i.e. 8.17+alpha 672b1443441df4e4777c4d2f7f6fb953bd97544a , and it still has the same problem.

Start by compiling the minimal program in the issue with coqc and confirm that type class resolution does not terminate. Investigate the type class resolution path involved in the Equivalence and Op instances; done means the reproducer terminates rather than looping indefinitely.