Let’s say I have a relation R : nat -> nat -> nat -> Prop, which forms a PER in the first and second argument, i.e.
Instance RPER c : PER (fun a b => R a b c) := ...
Is there a way for Coq to be smart enough to figure out this is the right instance for R a b c?
I guess one obvious way is to give a definition for (fun a b => R a b c) and set it opaque during typeclass resolution, but this is not very convenient, as I truly want the PER tactics to work out of the box.
Not an answer to your question, but often when typeclass search can’t figure something out but it’s only a restricted setting, e.g. for a fixed R, you can useHint Extern in the typeclass_instances database and plug some custom Ltac there which uses the instance you defined