RFC: change how named arguments suppress explicit parameters

Stream: lean4

[Kyle Miller]

The RFC is lean4#5397

Summary: Currently every explicit parameter that is depended upon by a named argument is elaborated as an implicit argument. This has been a confusing feature, as evidenced by questions on Zulip and the reported issues, but there are still some places where it is useful.

• We would preserve this feature for explicit parameters that haven't been supplied an argument. This happens when there is a named argument for a parameter that occurs after such an explicit parameter. In that case, normally the explicit argument would become an eta argument (it gets lambda abstracted after the application is elaborated), but that would result in a type-incorrect expression if the explicit argument is depended-upon. Instead, we can just elaborate it as an implicit parameter. There are plenty of examples in Batteries/Mathlib that make use of this. I already explored making this be an error, but I found the resulting errors to be more baffling than just letting it elaborate.
• Internally, the way x.f elaborates when f is a field of a structure is as S.f (self := x). Sometimes structure parameters are explicit, and in this specific case we would have the self argument continue to cause all the structure parameters (the collection of parameters it depends on) to be implicit. Without this exception, while you might be able to write x.f (due to the first bullet), if you wanted to supply any additional arguments a b c you might have to write x.f _ _ a b c, with one _ per explicit structure parameter.

[Kyle Miller]

This RFC was motivated by this Zulip thread. I had explored disabling the explicit parameter suppression completely, but the feature from the first bullet point is difficult to live without, for example in writing rw [lem (h := foo)] when lem has explicit arguments that h depends on.

[Kyle Miller]

There is a reference implementation at lean4#5283. This did not require any changes to Batteries, but you can evaluate the impact on Mathlib.

[Kyle Miller]

Pinging @Kevin Buzzard, @Mario Carneiro, @Floris van Doorn, @Yaël Dillies, who have commented so far.

[Floris van Doorn]

The fact that the feature still exists when no more arguments are given seems reasonable. What is the new output of the following (the current output is shown in comment):

def foo (x y z : Nat) : Nat := x + y + z
#check foo (z := 3) _ -- fun y => foo ?m.76 y 3 : Nat → Nat

The output of the following is unchanged?

#check foo (z := 3) -- fun x y => foo x y 3 : Nat → Nat → Nat
#check Sigma.mk (snd := 1) -- ⟨?m.118, 1⟩ : Sigma ?m.115
#check Prod.mk (snd := 1) -- fun fst => (fst, 1) : ?m.144 → ?m.144 × Nat

(I just realized that there is a difference between the last two examples: one of them is a function, the other an element of a sigma-type.)

[Floris van Doorn]

Kyle Miller said:

Sometimes structure parameters are explicit [arguments of projections]

Just checking: this only (sometimes) happens for classes, right? For non-class structures, projections never have parameters as explicit arguments, I believe.

[Kyle Miller]

All of your examples have the exact same output. A difference is that now you can include the _ in

#check Sigma.mk (snd := 1) _ -- ⟨?m.119, 1⟩ : Sigma ?m.116

In current lean this produces a "function expected" error. The new behavior makes the trailing _ optional because its a dependency (vs required to be omitted). Changing that 1 to Nat.zero (1 obscures the following issue since it's waiting on an OfNat instance) if you try to turn fst into an eta argument like fun x => Sigma.mk x Nat.zero, this has a type error on Nat.zero.

Floris van Doorn said:

Just checking: this only (sometimes) happens for classes, right?

Yes, correct. Non-class structures always have an explicit self parameter, so all the type parameters are implicit.

[Kyle Miller]

I forgot to mention the history of this feature: This ability to omit trailing dependencies of named arguments comes from around 2020, and the fix for lean4#1851 comes from around 2022. The RFC is essentially "revert to the 2020 behavior and re-implement the 2022 behavior for only the self parameter for projection notation".

[Floris van Doorn]

Kyle Miller said:

All of your examples have the exact same output.

Right, because I didn't actually make the arguments dependent. I'm happy with the new behavior described in this RFC.