Zulip Chat Archive

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

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

@Bhavik Mehta

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

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: Dec 20 2023 at 11:08 UTC