fix: refine how named arguments suppress explicit arguments

[kmill]

Note: Most of the implementation of this PR is at #5512 due to a bad rebase before merging.

Recall that currently named arguments suppress all explicit parameters that are dependencies. This PR limits this feature to only apply to true structure projections, except in the case where it is triggered when there are no more positional arguments. This preserves the primary reason for generalizing this feature (issue #1851), while removing the generalized feature, which has led to numerous confusions (issue #1867). This also fixes a bug pointed out on Zulip where in @ mode, instance implicit parameter dependencies to named arguments would be suppressed unless the next positional argument was _.

More detail:

• The NamedArg structure now has a suppressDeps : Bool field. It is set to true for the self argument in structure projections. If there is such a NamedArg, explicit parameters that are dependencies to the named argument are turned into implicit arguments. The consequence is that all structure projections are treated as if their type parameters are implicit, even for class projections. This flag is not used for generalized field notation.
• We preserve the suppression feature when there are no positional arguments remaining. This feature pre-dates the fix to issue Dot notation with typeclass instances issue #1851, and it is useful when combining named arguments and the eta expansion feature, since dependencies of named arguments cannot be turned into eta arguments. Plus, there are examples of the form rw [lem (h := foo)] where lem has explicit arguments that h depends on.
• For instance implicit parameters in explicit mode, now _ arguments register terminfo and are hoverable.
• Now .. is respected in explicit mode.

This implements RFC #5397. The suppressDeps flag suggests a future possibility of a named argument syntax that can suppress dependencies.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-08 19:35:15) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1b6572726fe2418266c5205bda4f0d5573e20229 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 20:06:48)

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-08 21:01:51) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-24 08:07:28) View Log

[kmill]

Originally this PR conservatively changed how _ worked for instance arguments in explicit mode. Now it changes how named arguments suppress dependencies in general, starting from a4af20a.

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-24 08:25:52) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-24 22:22:09) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-24 22:51:22) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5283 build failed against this PR. (2024-09-24 23:11:27) View Log

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5283 has successfully built against this PR. (2024-09-25 02:10:52) View Log