Zulip Chat Archive

Stream: general

Topic: inferring instance variables

Johan Commelin (May 08 2020 at 07:05):

At some point in time, we would replace a whole bunch of [ring R] by {_inst : ring R} because it would save us a type class search. Do I understand correctly that this is no longer necessary in lean-3.x.c for high values of x?

Kenny Lau (May 08 2020 at 07:06):

what do you mean by replace [ring R] with {_inst : ring R}?

Yury G. Kudryashov (May 08 2020 at 07:09):

See, e.g., algebra/group/hom.

Gabriel Ebner (May 08 2020 at 07:17):

There are two cases:

  1. Type class instances: here the issue was mainly performance. Lean used to synthesize arguments in [] even if they were inferable via unification. This is fixed now.
  2. Regular definitions. Here the "issue" is that Lean tries to synthesize arguments in [] eagerly. This is typically a good idea. But you run into problems if the inferred instance is not definitionally equal to the one you have in your goal. I don't think this will change. An example of this is quotient.mk' vs quotient.mk.

Johan Commelin (May 08 2020 at 07:19):

@Gabriel Ebner Thanks for the explanation. So in general, we don't need so many {_inst : ring R}s anymore, right?

Yury G. Kudryashov (May 08 2020 at 07:20):

I remember a recent PR adding {_inst : ring R}s because of (2).

Chris Hughes (May 08 2020 at 07:57):

There are a few places where there is fintype or decidable are in curly brackets because of diamond problems with these classes after rewrites. Is this no longer necessary?

Gabriel Ebner (May 08 2020 at 08:40):

The {h : fintype ...} and {h : decidable ...} issue is exactly number 2. These are still necessary, and I don't think this will change.

Last updated: Aug 03 2023 at 10:10 UTC