inferInstance vs. by infer_instance

Stream: mathlib4

[Michael Stoll]

In #12060, seeing several instances proved via by infer_instance, I replaced the proofs by inferInstance, thinking that the term proof is shorter and likely more efficient than a tactic proof. Then @Yaël Dillies asked me to revert, saying

This change means that any use of those instances comes at the cost of unfolding inferInstance. In general, please use infer_instance the tactic instead of inferInstance the term when defining instances

However, the tactic infer_instance is defined to be exact inferInstance, and some experiments showed that (in terms of heartbeats) the term is at least as efficient as the tactic.

So my question is whether there is a preference for the tactic over the term (and if so, on what grounds).

(It may be the case that in Lean3 there was a difference that no longer exists.)

[Mario Carneiro]

indeed there used to be a difference in lean 3 that no longer exists

[Mario Carneiro]

IMO it's a (minor) regression

[Michael Stoll]

What was better in Lean3?

[Mario Carneiro]

the difference is that apply_instance would directly insert the result of typeclass synthesis, while inferInstance or whatever it was called then is just an identity wrapper with a [x : A] argument which indirectly triggers typeclass synthesis

[Mario Carneiro]

the inferInstance identity function is needless cruft in the proof term

[Michael Stoll]

But apply_instance would need to get the result from somewhere, so how is it different?

[Mario Carneiro]

it would call the typeclass machinery function itself

[Mario Carneiro]

rather than relying on the app elaborator to see a [ ] argument and call the typeclass machinery

[Michael Stoll]

Are there any plans to change the implementation of the tactic infer_instance to recover the old behavior?

[Mario Carneiro]

I don't think it's on anyone's radar

[Michael Stoll]

So should I revert the change anyway, so that we can profit in case somebody does it after all?

[Mario Carneiro]

there is no difference between them, so for now I would say no preference. If we fix it we'll want to make both forms work anyway

[Yaël Dillies]

I'm happy with that

[Michael Stoll]

Can we then get #12060 merged?