apply with typeclass instances

Stream: new members

[Bhavik Mehta]

Is there a variant of apply which creates new goals for any missing type class instances?

[Reid Barton]

it randomly seems to do this sometimes already, usually in circumstances where the new goals can be solved by apply_instance...

[Reid Barton]

I assume you're using a recent Lean? there was some issue with apply and type classes but it was fixed a fairly long time ago

[Reid Barton]

"fixed" possibly meaning we replaced a heuristic with a much better but maybe still not always correct heuristic, I'm not sure.

[Bhavik Mehta]

Yeah I'm on 3.9.0 right now - I did have the impression that this used to happen as well but I can't be sure

[Bhavik Mehta]

I think the new goal I want isn't solved by apply_instance

[Reid Barton]

Probably not, given that apply (1) isn't finding the instance, (2) isn't creating a new goal.

[Reid Barton]

Maybe just use haveI or letI first?

[Bhavik Mehta]

Yeah that's probably the most sensible solution, just thought I'd check first! Thanks

[Reid Barton]

Also, while apply is difficult, I seem to recall that exact or refine might have an option for this

[Reid Barton]

Or its default behavior might do what you want

[Bhavik Mehta]

The default behaviour for both of those doesn't do what I want

[Reid Barton]

Oh, I see there's apply_with

[Reid Barton]

apply_with blah { instances := ff } maybe

[Bhavik Mehta]

I find it slightly surprising that using @ and term mode, leaving the missing instance as _ gives the error failed to synthesize type class instance instead of saying couldn't synthesize term

[Bhavik Mehta]

Reid Barton said:

apply_with blah { instances := ff } maybe

This doesn't seem to work for me...

[Bhavik Mehta]

haveI probably is the best thing to do here

[Reid Barton]

I've also noticed that it seems kind of random what happens with this. I encountered this just yesterday with refine I think.

[Bhavik Mehta]

Oh hang on, the apply_with thing works when I don't use @

[Reid Barton]

I gave refine a pretty complicated expression involving _ inside a lambda and stuff, no idea if that was relevant.

[Bhavik Mehta]

Bhavik Mehta said:

Oh hang on, the apply_with thing works when I don't use @

apply_with (preserves_hpb over.forget) { instances := ff } , does create the new goal, apply_with (preserves_hpb over.forget t) { instances := ff } doesn't

[Bhavik Mehta]

and the instances doesn't need to be mentioned at all actually

[Bhavik Mehta]

It seems like it's something to do with where the instance is in the declaration

[Reid Barton]

I would believe that

[Mario Carneiro]

My hacky workaround to this issue is to use refine @foo _ _ (id _) bar

[Mario Carneiro]

where the id is on the typeclass I want to prove

[Mario Carneiro]

@Bhavik Mehta

[Bhavik Mehta]

Cool, thanks!

[Bhavik Mehta]

It turned out my thing should have been inferred anyway, and I just didn't have the right imports