Zulip Chat Archive

Stream: general

Topic: inferring instance variables


view this post on Zulip 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?

view this post on Zulip Kenny Lau (May 08 2020 at 07:06):

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

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 07:09):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 08 2020 at 07:20):

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

view this post on Zulip 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?

view this post on Zulip 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