RFC: Named arguments should not make explicit arguments implicit except for structure parameters

[kmill]

Summary

Remove the general anyNamedArgDependsOnCurrent feature from the app elaborator that was added in a5ab59a and instead address #1851 by making specifically structure projection notation enable it for the self named argument.

Supersedes RFC #5386.

Motivation

The app elaborator has a feature (added in a5ab59a) where every explicit parameter that is depended upon by a named argument becomes an implicit parameter. We will call this feature argument suppression via named arguments for the purpose of this RFC.

There are two motivations for it.

The first motivation is that when there are no positional arguments remaining, every remaining parameter that is depended upon by a named argument is fully determined by that named argument, so there is no sense in requiring that such an argument be supplied. For example, given Nat.le_of_lt : (a b : Nat) → (h : a < b) → a ≤ b, one would be tempted to write Nat.le_of_lt (h := pf), and it would be inconvenient to need to supply a and b as well. Additionally, such arguments are not suitable for the eta expansion feature, where each missing explicit argument creates an "eta argument" — an argument that is lambda abstracted — since this would result in a type-incorrect term.

The second motivation is to make projection notation for structures more uniform. For background, recall that for a structure such as

structure S (α β : Type) where
  f : α → β

the field projection S.f has a type of the form {α β : Type} → (self : S α β) → α → β. The parameters before self are the structure parameters, which are always fully determined by the type of self. Similarly, for a class such as

class C (α β : Type) where
  f : β

the field projection C.f has a type of the form (α : Type) → {β : Type} → [self : C α β] → β. Notice that in this case the first structure parameter is explicit since it cannot be inferred from any other explicit arguments or from the return type, and it is needed for typeclass inference of the self parameter.

For x : S, the projection notation x.f is elaborated as if it were S.f (self := x), using named arguments. Similarly, when inst : C, then inst.f is elaborated as if it were C.f (self := inst). Named arguments are the mechanism by which the elaborator provides a value for self, which works even when it is an implicit argument.

In issue #1851 it was noticed that elaborating inst.f as C.f (self := inst) led to confusing behavior, since the structure parameters needed to still be supplied. This was fixed by generalizing the argument suppression via named arguments feature to apply to all arguments, even if there are still positional arguments to process. This addresses the issue because the structure parameters are always depended upon by the self parameter, so they become implicit. The result is that for inst : C α β the projection inst.f elaborates as @C.f α β inst.

However, this leads to other confusions. Named arguments in general suppress all explicit parameters depending on them, not just in the structure projection case. For example, in issue #1867 there is unintuitive behavior with using a named argument for an instance parameter. The general issue is that it is unclear to the user which parameters depend on implicit parameters — after all, they do not appear in the source text! — so it can be hard to predict what will happen. Furthermore when it does occur, the only mitigation when it is unwanted is to use named arguments for the suppressed explicit parameters.

The argument suppression via named arguments feature also has a counterintuitive interaction with explicit mode ("@ mode"), pointed out on Zulip. The assumption of explicit mode is that each argument should be provided explicitly. Argument suppression via named arguments is however still enabled in explicit mode since the implementation of explicit mode is, essentially, that each parameter becomes explicit (with a special case for _ arguments for instance implicit parameters). Since they are explicit, argument suppression via named arguments applies. For an example counterintuitive behavior, in @C.f (self := inst) the α parameter becomes implicit since the self parameter depends on it. We believe users would expect to need to write @C.f (self := inst) α in explicit mode.

Guide-level explanation

(Rough draft with key information) Projection notation (also known as field notation or dot notation) is a convenient object-oriented-like way to apply projection functions to a term. (... examples ...)

In the simplest case, x.f resolves to S.f x, where S is a structure and f is a field of S. If f is located in a parent structure, then Lean will automatically insert parent projections. (... examples ...)

In particular, the notation x.f resolves as S.f (self := p x) where p (optional) is the projection to the parent structure S.

Classes are a kind of structure as well, and projection notation can be used on class instances. However, classes are different from normal structures in that the self parameter of field projections is instance implicit rather than explicit. In this case, inst.f resolves to C.f _ ... _ (self := inst), where there is one placeholder _ per explicit class parameter that isn't itself supplied using a named argument.

In a section on named arguments:

Migration: In Lean pre-v4.XX.0, using named arguments would make every explicit argument it depends on to become implicit, even in explicit mode. This feature was made more restrictive, and you may need to insert some number of positional _ or (_) arguments to adapt to the change. Using _ should usually work, but (_) may be necessary in explicit mode for instance implicit arguments that are non-canonical.

Reference-level explanation

(... explanation of elaboration of normal applications ...)

When processing parameters, if there are no more positional arguments, then every subsequent explicit parameter...

• ... in ellipsis mode is treated as an implicit parameter
• ... that is depended upon by an explicit argument is treated as an implicit argument, and otherwise as an eta argument.
• ... in normal mode, when the resulting function type has opt params or auto params, is treated as an eta argument
  Otherwise, the application is finalized.

When processing parameters, if there are more positional arguments, but the current parameter is explicit and there is a named argument tagged with suppressDeps that depends on it, then it is treated as an implicit argument.

(... in section on projections ...) Projection notation x.f for structure projections resolves as S.f (self := x) where the named argument is tagged with suppressDeps.

Drawbacks

Users may be making use of this feature for named arguments. Kevin Buzzard for example was using it in explicit mode to avoid needing to supply "obvious" _s. It should be said that Kevin said he was making progress with which arguments to fill in next with guess-and-check, not intentionally.

Floris van Doorn thinks that making class structure parameters implicit in projections can still lead to confusion.

Rationale

• As issue passing instances to named arguments turns explicit args into implicit #1867 shows, users have been surprised by the argument suppression via named arguments feature, and they often feel like it is an elaboration bug.
• The generalized argument suppression via named arguments feature is motivated by the specific use case of not supplying structure parameters in instance projections. We can easily implement this precise feature.
• The argument suppression via named arguments feature in the specific case when there are no more explicit arguments is motivated by convenience. It might be confusing needing to add _s, but it's also confusing when such a named argument application doesn't elaborate. At least the _s only need to be added to the end.
• Since there is no such thing as explicit mode projection notation, the suppressDeps solution for projection notation immediately improves named argument handling for explicit mode, making explicit mode more predictable. It keeps the invariant that each argument (be it positional or named) corresponds to one parameter. It is hard to predict which arguments are suppressed, especially ones that are originally implicit arguments as they do not generally appear in the syntax.
• We might have considered making argument suppression via named arguments apply to any named argument for a self parameter. However, users can write C.f (self := inst) (using the above example C), which would surprisingly omit a parameter.
• Users can specify the exact expression they want for every argument in explicit mode. Argument suppression via named arguments leads to terms that might not definitionally be in the correct form — there are some mathlib examples where this causes typeclass inference failure.
• Generalized field notation uses a separate "lval resolution" procedure, and it uses either positional or named arguments, preferring positional when possible. This meant that argument suppression via named arguments only applied for underapplied generalized field notation. Removing argument suppression via named arguments makes generalized field notation elaboration less confusing.
• The pretty printer is not aware of argument suppression via named arguments, and the pp.analyze option can cause round-tripping issues because of this. Removing the feature fixes this. Note that projection notation notation is disabled for instances, so this RFC has no effect on pretty printing instance projections.
• Lean 3 resolved argument-free structure projections in the way described by this RFC.

In the issue #1867, Mario Carniero suggests another implementation that tries to preserve argument suppression via named arguments. That would entail a relatively large refactor since (1) the elaborator does not keep track of the actual order of named vs positional arguments, just an array for each and (2) the elaborator processes in parameter order, not argument order.

Unresolved questions and future possibilities

• There is some disagreement about whether Dot notation with typeclass instances issue #1851 is an issue. Floris van Doorn suggests the fix is for the user to use _s for the explicit structure parameters.
• Generalized field notation will not omit any arguments, meaning user-defined "fields" will elaborate with different behavior. Should users be expected to use only implicit arguments for structure parameters? Should they be willing to accept that _s can be necessary for generalized projections? Or should generalized field notation compute what the "structure parameters" are and omit them for consistency?

Community Feedback

This RFC comes from discussion on the Lean Zulip pointing out a bug in the interaction between how _ is handled in explicit mode for instance implicit arguments and argument suppression via named arguments. The PR #5283 fixes it with the assumption that we want the feature to be enabled in explicit mode, but there was feedback to disable argument suppression via named arguments in explicit mode. This led to RFC #5386, and there was more feedback supporting disabling the feature more widely. There is some support to disable the feature entirely.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[kmill]

It turns out the implementation I suggested here has a big drawback, which is that inserting placeholders for explicit structure parameters means that those structure parameters can't be provided using named arguments. Also, using named arguments for them would lead to those placeholders being shifted to the next explicit arguments!

I see three options:

1. Add a flag to NamedArg that turns on argument suppression for just that named argument. Edit: the RFC was updated with this one.
2. Change the interface to elabAppArgs to accept an (ftype? : Option Expr) argument, so that way the structure parameters can be made implicit. (Users of this interface may also want to use this to change parameter names.)
3. Revert the feature entirely.

[kmill]

Completed by #5283.