The EqvWF_Build instance messes up with typeclass resolution

[YaZko]

The EqvWF_Build instance appears to lead astray typeclass resolution when performing unrelated rewrites.
Consider the following code snippet relying on itrees:

From ITree Require Import
     ITree Eq.Eq.

Goal forall {E R1 R2} (RR : R1 -> R2 -> Prop) (t1 t1': itree E R1) (t2 : itree E R2),
    eutt eq t1 t1' ->
    eutt RR t1 t2 ->
    False.
  intros * EQ1 EQ2.
  rewrite EQ1 in EQ2. (* Instantaneous *)
  Undo.

  Require Import ExtLib.Programming.Eqv.
  Fail Timeout 5 rewrite EQ1 in EQ2. (* Appears to loop, had it run a few minutes without success *)

  Remove Hints EqvWF_Build : typeclass_instances.

  rewrite EQ1 in EQ2. (* Instantaneous again *)
Abort.