RFC: Named arguments in explicit mode should not be able to make parameters become implicit

[kmill]

Summary

Modify argument processing in the app elaborator so that the anyNamedArgDependsOnCurrent feature is disabled in explicit mode.

Motivation

The app elaborator has a feature 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. A motivation for it is to make projection notation more convenient. When S is a structure with field S.f, then the elaborator makes use of the fact that the main parameter for the field is named self, elaborating the projection notation x.f as S.f (self := x).

For structures such as classes, the self parameter is not explicit, and in that case structure parameters might be explicit due to the fact that they cannot be inferred from other parameters or the result type. Without special support, elaboration can lead to counterintuitive behavior. For example, in the following code block the projection C.val has n as an explicit parameter. This means that a straightforward implementation of projection notation would require the user to write inst.val n (or inst.val _) even though n can be inferred immediately from inst. However, due to argument suppression via named arguments, users can simply write inst.val:

class C (n : Nat) (α : Type) where
  val : α

variable (n : Nat) (α : Type) [inst : C n α]

set_option pp.explicit true
#check (C.val n : α)  -- @C.val n α inst : α
#check inst.val       -- @C.val n α inst : α

Side note: Named arguments in general suppress all explicit parameters depending on them, not just in the structure projection case. It should also be noted that generalized field notation might or might not be affected by this feature, since "lval resolution" for generalized field notation tries to use positional arguments if possible, falling back to named arguments when it is not. This inconsistency is not the subject of this RFC.

The argument suppression via named arguments feature has a counterintuitive interaction with explicit mode ("@ mode"). 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 to instance implicit parameters). Since they are explicit, argument suppression via named arguments applies.

For example, in the following the n parameter becomes implicit since the self parameter depends on it.

#check @C.val (self := inst) -- @C.val n α inst : α

We believe users would expect to need to write @C.val (self := inst) n in explicit mode.

Guide-level explanation

(Rough draft with key information) Sometimes we want to be able to pass values to implicit parameters in function applications. Named arguments can be used for arguments of all binder types, even implicit parameters. For example (... example ...)

Another way is to enter explicit mode with the @ prefix. In this mode, every parameter is treated as if it were an explicit parameter. (... example ...)

Named arguments can be paired with explicit mode, which can be a convenient way to ensure an argument is being given to the correct parameter amidst a sea of arguments. (... example ...) This can also be used with a trailing .. to automatically insert the correct number of _'s at the end of an application.

For normal applications, named arguments have a feature where each explicit argument that a named argument depends on will become implicit automatically. These arguments can be inferred from the type of the named argument, so they are not strictly needed, which saves needing to write _s for such arguments. For explicit mode this feature is disabled.

Migration: In Lean pre-v4.XX.0, explicit mode had this feature enabled. You may need to insert some number of positional _ or (_) arguments to adapt to the change. Using _ should usually work, but (_) may be necessary for instance implicit arguments that are non-canonical.

Reference-level explanation

(... explanation of elaboration of normal applications, including the argument suppression via named arguments feature ...)

In explicit mode, parameters are processed one at a time according to the following:

• If the next parameter is instance implicit and the next positional argument is _, then the parameter is elaborated as an instance implicit argument and the _ is consumed.
• Otherwise, the next parameter is elaborated as if it were explicit while disabling the argument suppression via named arguments feature.

Drawbacks

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

Rationale

• The argument suppression via named arguments feature is motivated by projection notation. There is no such thing as explicit mode for projection notation, so it makes sense that it should not be enabled in explicit mode.
• This makes 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.
• Users can specify the exact expression they want for every argument. 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.
• The pretty printer is not aware of argument suppression via named arguments. If explicit mode delaboration were to have a feature to use named arguments in certain circumstances, then it would need to be made aware of it. (This does need to be fixed for normal mode delaboration. This is out of scope of this RFC.)

Unresolved questions and future possibilities

• Should the argument suppression via named arguments feature be generally enabled? Or should it instead be enabled only for projection notation?
• Should it also be enabled for generalized field notation in all cases?

Community Feedback

This RFC comes from discussion on the Lean Zulip. There is 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. However, there is support in the Zulip thread to disable it in explicit mode.

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]

Superseded by #5397.