Elaboration of optional parameters does not take into account expected type

[kmill]

Description

When using a function that has optional parameters, it can sometimes be surprising how eager optional parameters are filled in when arguments could come from the expected type.

Steps to Reproduce

In the following, one might expect the first example to work. Instead, one needs to write fun n => f n or (f ·) to inhibit filling in the optional parameter.

def f (n : Nat := 0) : Nat := n

example : Nat → Nat := f
/-
type mismatch
  f
has type
  Nat : Type
but is expected to have type
  Nat → Nat : Type
-/

example : Nat → Nat := (f ·) -- ok

Versions

Lean 4.11.0 nightly from 7/22/2024

Additional Information

It is unclear whether this first example should work, or whether expected-type-directed optional parameters would lead to worse confusion, but I wanted to file an issue to record a momentary surprise I had recently.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

Thanks for logging this issue. In the current system, this should be considered by design. If we see evidence for such a change that outweighs that against, an RFC would be the next step.

[kmill]

I'll leave just a couple more thoughts here:

In the current system, there is a single class of optional parameter, positional parameters with default values. I see there being two different use cases for optional parameters: (1) filling in positional parameters with contextually relevant default values (like for example optional parameters to constructors) and (2) configuration (like for example boolean flags to monadic functions). If there were a distinction between these two types, then it would make sense for type-1 parameters to take the expected type into account, since they would be more like implicit parameters that can optionally be supplied positionally, and arguably if they're not present they could be taken from the expected type. Type-2 parameters though should not be, and I believe it would be very confusing if they were.

So, an RFC would also have to take into account separating these types of optional parameters.

Incidentally, if there were also non-positional optional parameters like in Python (ones that must be set using named arguments), then that would naturally distinguish these two use cases.