inferring instance variables

Stream: general

[Johan Commelin]

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]

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

[Yury G. Kudryashov]

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

[Gabriel Ebner]

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]

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

[Yury G. Kudryashov]

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

[Chris Hughes]

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]

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