Brandon Moore (Mar 11 2021 at 20:30): Brandon Moore (Mar 11 2021 at 20:30):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?
Gaëtan Gilbert (Mar 11 2021 at 20:46):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
Brandon Moore (Mar 17 2021 at 15:52):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.
Matthieu Sozeau (Mar 19 2021 at 12:01):! is better, but it does precludes solving Proper ? f, which can come up during resolution.
Last updated: Oct 13 2024 at 01:02 UTC