named arguments of dependent functions

Stream: lean4

[Floris van Doorn]

(this issue was found and minimized by @Sven Manthe)

The failure in the first example below is counterintuitive to me. Is this the intended behavior?

structure D where
structure C (x : D) where
def f (x : D) (y : C x) := 0
example := f {} (y := {}) --fails
example := f (x := {}) (y := {}) --works
example := f (x := {}) {} --works
example := f {} {} --works

-- if our function is not dependent, all four cases work
def g (x y : D) := 0
example := g {} (y := {}) --works
example := g (x := {}) (y := {}) --works
example := g (x := {}) {} --works
example := g {} {} --works

The behavior seems to be:

named arguments are processed first, and all dependent arguments (even the explicit ones) before named arguments are already inserted as metavariables.

The fact that dependent arguments are already inserted as metavariables is counterintuitive to me, and is undesirable if y is an implicit argument (e.g. a type-class argument) and x is explicit, and you want to specify y explicitly. In that case, if you also want to give x explicitly, you are required to also write x as a named argument.

[Bhavik Mehta]

I just came across this as well, and I agree it's counterintuitive. It's also not mentioned in the docs for implicit arguments and giving them explicitly.

def foo : Prop := False
def foo_d : Decidable foo := instDecidableFalse
def decide' (p : Prop) {_h : Decidable p} : Bool := decide p

#check decide' foo (_h := foo_d)

Here's the example I came up with - the final line doesn't typecheck and I expected it should.

[Floris van Doorn]

I just realized this is already reported as lean4#1867. Please upvote that issue if you have encountered this.

[Kyle Miller]

Recently I came across this comment explaining this behavior in the app elaborator: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/App.lean#L547-L570

If a named argument depends on an explicit argument, that explicit argument becomes an implicit argument.

It seems like the justification for this is for dot notation, which is implemented using the transformation x.f -> X.f (self := x). Perhaps this explicit->implicit conversion should only occur for this particular named argument?

[Floris van Doorn]

Yes, I also read that comment yesterday, when clicking some links from lean4#1867.
Honestly, I don't see why this special case was implemented. I.e. why don't we just keep explicit arguments explicit, even when a later dependent argument is given?
It might be marginally useful sometimes, allowing you to omit the occasional underscore, but it is confusing, and I don't think the trade-off is worth it. This is a uncommon pattern that many users will not be familiar with. Case in point: a student of mine came to me with a type mismatch error caused by this, and I didn't know what was going on, despite having encountered it before.
Furthermore, giving the dependent argument doesn't necessarily specify the type completely, so the explicit-turned-implicit argument regularly still needs to be given.

Lastly, the issue lean4#1851 reads a bit like @Tomas Skrivan just forgot to put an underscore in their code.

-- on Lean from 2022-10-27
class Approx {α : Type} (a : α) (X : Type) : Type where
  val : X

variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]

/-
application type mismatch
  @Approx.val ?m.97 (Approx.val ?m.102) ?m.107 f
argument
  f
has type
  Approx f' (X → Y) : Type
but is expected to have type
  Approx (Approx.val x') ?m.107 : Type
-/
#check f.val x.val

/-
Approx.val f' (Approx.val x') : Y
-/
#check f.val _ x.val

[Floris van Doorn]

To comment directly on your suggestion: I don't like the idea of having different behavior for x.f compared to X.f (self := x). I think they are similar enough.