I ran into a slow rewrite, and have tracked it down to our code having an instance `Proper (R1 ==> R2 ==> prod_relation R1 R2) pair`

, which makes the typeclass search for a `setoid_rewrite`

of this form slow - exponential in the arity of P takes (testing in 8.12.0):

```
Lemma rewriteslow
(A : Type)
(P : A -> A -> A -> (A * A) -> Prop)
(a x y : A)
(H : x = y):
P a a a (a, x).
Time setoid_rewrite H.
```

Here are imports and instances

```
Require Import Setoid Morphisms.
Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
relation (A * B) := fun x y => R1 (fst x) (fst y) /\ R2 (snd x) (snd y).
Global Instance pair_proper' {A} {R1: relation A} {B} {R2 : relation B}:
Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
Proof. firstorder eauto. Qed.
```

I've started to look at `Set Typeclasses Debug`

output. Where should I go from here?

seems related to https://github.com/coq/coq/issues/7916

you can try `Hint Mode Proper ! ! - : typeclass_instances.`

or variants (+ is stricter than ! is stricter than -, - is default), it makes your example go fast but I have no clue about the impact in general

That issue is interesting. The discussion there suggests that `setoid_rewrite`

relies more than I expected on letting typeclass resolution pick what relations to use. That makes setting a mode seems a bit dangerous. I guess your `! ! _`

might not get in the way if the goal usually has the form `Proper (_ ==> _) _`

, and the `==>`

is enough of a head to satisfy the `!`

mode.

! is better, but it does precludes solving Proper ? f, which can come up during resolution.

Last updated: Jun 17 2024 at 22:01 UTC