Remaining uses of autoImplicit in mathlib

Stream: mathlib4

[Michael Rothgang]

Over the recent PRs, the use of autoImplicit in mathlib has shrunk considerably. I think it's feasible to list the remaining uses and discuss them individually. Currently, there are 18 files left in Mathlib which use autoImplicit:

• three only use it for individual declarations
• Data/List/EditDistance/{Bounds,Estimator} and almost all of Data/MLLList are handled in #14896 (and the latter is somewhat deprecated anyway, as I understand it) update: merged now
• 3 files are in Data/Vector: #14885 handles these

• Tactic/Ring/Basic is done in #14709 merged now

• Data/HashMap is fully deprecated (so doesn't really matter either way)

• Control/Random seems to use autoImplicit pervasively: this seems to be a case where actually allowing it could be fine.
• Logic/UnivLE always yields errors in the univLE_of_max instance
• Logic/Basic is simply a huge file

I would like to extend the set_option linter to also complain about autoImplicit being used in Mathlib, effectively enforcing what has been informal policy already. This means disabling the linter on existing usages. Any comments, suggestions, concerns or objections to doing so?

[Yaël Dillies]

Probably @Kim Morrison will be sad

[Patrick Massot]

I am very sad too, but this is too late. This feature of Lean 4 had too many enemies.

[Kevin Buzzard]

I renewed my hatred against it only this week when I mistyped an \MCX as an X in a lean game repo and was bewildered for several minutes, and even went as far as a partial redesign of the entire set-up of my game before I realised my foolish error (I had edited several files to "fix" the problem after misdiagnosing it).

[Damiano Testa]

If Lean had a transient message saying "Hey, this is a new variable!" the first time that it is "introduced", I would probably like it much more.

[Shreyas Srinivas]

Kevin Buzzard said:

I renewed my hatred against it only this week when I mistyped an \MCX as an X in a lean game repo and was bewildered for several minutes, and even went as far as a partial redesign of the entire set-up of my game before I realised my foolish error (I had edited several files to "fix" the problem after misdiagnosing it).

Never had this happen to me, after the first two or three times. I almost always know when I need to check for autoImplicit as a cause when I encounter an error.

[Shreyas Srinivas]

Also, I would never turn off a feature like this in an entire library just because it bothered me. Maybe on a file by file I would turn on a flag and turn it off when I am done. If only there was a way to toggle this feature in the infoview on a per file level, instead of writing the set_option line. EDIT : That has the potential to open a different can of worms about the default setting, but at least it is quicker to tweak.

[Mario Carneiro]

I remember @Sebastian Ullrich demoing a feature which used inlay hints to show autoimplicits, which makes them much noisier / harder to miss. I'm sad that didn't make it in, perhaps it got deprioritized after the initial push (during the Munich meetup IIRC)

[Robert Maxton]

I hadn't realized this was a recent-ish decision. Alas. I personally find it extremely useful at least when writing the file, and had thought its non-use was mostly a matter of clarity when reading the resulting code.

[Joachim Breitner]

Yes, it's still on our wish list, but don't hold your breath, it is rather tricky to implement robustly given CS Code's and the LSP' API, and it's not high priority.

[Shreyas Srinivas]

Mario Carneiro said:

I remember Sebastian Ullrich demoing a feature which used inlay hints to show autoimplicits, which makes them much noisier / harder to miss. I'm sad that didn't make it in, perhaps it got deprioritized after the initial push (during the Munich meetup IIRC)

There was a brief discussion on using inlays to show autoImplicit on zulip discord. We had three ideas:

1. use haskell style inlays in a line above the def.
2. Show it in the infoview when the cursor is on the def using autoImplicit
3. Show a hint when another declaration has an error and an upstream def used autoImplicit. This is better because autoImplicit can show up in errors in downstream declarations.

[Kim Morrison]

Agreeing with the above, that more work (e.g. inlay hints) is needed to restore the glory of autoImplicits, I am not at all sad that Mathlib is becoming uniform here.

1. The big benefit of autoImplicits is in development. For finished files it is a more balanced trade-off for readability.

2. Uniformity in language conventions is really valuable. If we can't have it ecosystem wide, it's still good to improve the internal consistency in mathematics projects.