Search for typeclass with Qq

Stream: general

[Markus de Medeiros]

This question is kind of vague, I'm very new to metaprogramming so I'm really just trying to get a sense of what solutions are out there.

I have a typeclass IntoWand ... X Y Z, and I'm writing a tactic where I need one of these instances for a fixed X Z : T but where I don't necessarily know Y. After I get a candidate forY, there's a short string of tactics I need to execute to try and finish the proof. Now I think I may be able come up with some heuristics to find possible values of Y, but I'm wondering if the typeclass system could help in this case:

• Is there any (efficient) way to do backtracking search over the space of possible instantiations for Y where synthInstanceQ q(IntoWand ... X Y Z)works?
• Is there any way to just look for first instance where synthInstanceQ q(IntoWand ... X _ Z) works?
• Right now Y is not an outParam (although Z is), but could try changing that. Can synthInstanceQ make use of outParams to do this kind of searching?

[Mario Carneiro]

synthInstance doesn't play well with tactics generally. You can't just get into the middle of the backtracking search. That said, I think it might not be impossible to write something like that which uses synthInstance internals... I think you want Y to be an outParam for this kind of use

[Aaron Liu]

If you have an outParam, you can just pass a metavariable and synthInstance will (hopefully) fill in its value for you

[Markus de Medeiros]

Thanks!