## 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: May 13 2021 at 19:20 UTC