## Stream: new members

### Topic: apply with typeclass instances

#### Bhavik Mehta (May 10 2020 at 16:20):

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

#### Reid Barton (May 10 2020 at 16:21):

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

#### Reid Barton (May 10 2020 at 16:21):

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 (May 10 2020 at 16:22):

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

#### Bhavik Mehta (May 10 2020 at 16:22):

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 (May 10 2020 at 16:22):

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

#### Reid Barton (May 10 2020 at 16:23):

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

#### Reid Barton (May 10 2020 at 16:23):

Maybe just use haveI or letI first?

#### Bhavik Mehta (May 10 2020 at 16:23):

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

#### Reid Barton (May 10 2020 at 16:23):

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

#### Reid Barton (May 10 2020 at 16:24):

Or its default behavior might do what you want

#### Bhavik Mehta (May 10 2020 at 16:24):

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

#### Reid Barton (May 10 2020 at 16:25):

Oh, I see there's apply_with

#### Reid Barton (May 10 2020 at 16:26):

apply_with blah { instances := ff } maybe

#### Bhavik Mehta (May 10 2020 at 16:26):

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 (May 10 2020 at 16:27):

Reid Barton said:

apply_with blah { instances := ff } maybe

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

#### Bhavik Mehta (May 10 2020 at 16:27):

haveI probably is the best thing to do here

#### Reid Barton (May 10 2020 at 16:27):

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 (May 10 2020 at 16:28):

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

#### Reid Barton (May 10 2020 at 16:28):

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

#### Bhavik Mehta (May 10 2020 at 16:29):

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 (May 10 2020 at 16:30):

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

#### Bhavik Mehta (May 10 2020 at 16:30):

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

#### Reid Barton (May 10 2020 at 16:36):

I would believe that

#### Mario Carneiro (May 10 2020 at 17:05):

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

#### Mario Carneiro (May 10 2020 at 17:06):

where the id is on the typeclass I want to prove

@Bhavik Mehta

Cool, thanks!

#### Bhavik Mehta (May 10 2020 at 17:07):

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

Last updated: May 12 2021 at 23:13 UTC