passing instances to named arguments turns explicit args into implicit

[digama0]

structure Bla : Type
class Foo (x : Bla) (y : Int) : Prop
opaque Bla.bla (x : Bla) (y : Int) [foo : Foo x y] : Nat

variable (x : Bla) (y : Int) (f : β → β)
#check x.bla y (foo := ⟨⟩) -- fails
#check x.bla (y := y) (foo := ⟨⟩) -- fails
-- function expected at
--   Bla.bla ?m.87500 ?m.87503
-- term has type
--   Nat

This is a recent regression caused by a5ab59a (the fix for #1851), and came up in the std4 nightly bump leanprover-community/batteries#31.

Here is a proposal for how to handle app args that should fix both this issue and #1851:

• Process the arguments in left-to-right order, starting with the one before the dot.
• The argument before the dot triggers dot-notation lookup and always goes in for the argument of that function of the correct type.
• Whenever filling an argument, all arguments it depends on are marked as implicit.
• If you encounter a regular argument, it goes in for the first unfilled explicit argument.
• If you encounter a named argument, it goes in for that argument (and also marks all args it depends on as implicit if they are not already filled).
• When you run out of arguments, all unfilled implicit arguments up to the first semi-implicit or explicit argument are replaced with _ and the rest are reverted.

(I believe the only difference from current behavior being suggested here is that named parameters should be processed in order with explicit args rather than all at the beginning.)

This has the following behavior:

• x.bla y (foo := ⟨⟩) turns into @Bla.foo x y ⟨⟩
• x.bla (foo := ⟨⟩) y is an error, because the y argument was made implicit
• x.bla (y := y) (foo := ⟨⟩) and x.foo (foo := ⟨⟩) (y := y) both work
• x.bla works and has type ∀ (y : Int) [foo : Foo x y], Nat

and using the example from #1851:

• f.val works and results in @Approx.val (α → β) f' (X → Y) f : X → Y
• f.val x.val is an over-application because f.val has already filled all the explicit arguments, so this is handled as (f.val) x.val which works

[kmill]

This issue was reported by Terry Tao in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Set.2EtoFinset.20without.20Fintype.20or.20Set.2EFinite/near/418374814

He found he had to write

noncomputable def Set.toFinset' {α: Type*} (s: Set α) : Finset α :=
  dite (h := Classical.dec (Set.Finite s)) Set.Finite.toFinset (fun _ ↦ ∅)

instead of

noncomputable def Set.toFinset' {α: Type*} (s: Set α) : Finset α :=
  dite (Set.Finite s) (h := Classical.dec (Set.Finite s)) Set.Finite.toFinset (fun _ ↦ ∅)

[kmill]

Jireh Loreaux reported a similar error, but this wasn't for an instance argument, but an argument that depends on previous explicit arguments. https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/behavior.20of.20.60.28arg.20.3A.3D.20sorry.29.60.20syntax/near/421895074

theorem foo (n m : Nat) (h : m = n) : m = n := h

example (n m : Nat) (h' : m = n) : m = n :=
  foo (h := h') -- succeeds, even without `n` and `m` passed to `foo`

example (n m : Nat) (h' : m = n) : m = n :=
  foo _ _ (h := h') -- fails ("function expected" from too many arguments)

example (n m : Nat) (h' : m = n) : m = n :=
  foo _ _ h' -- succeeds

[fpvandoorn]

This was also reported in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/named.20arguments.20of.20dependent.20functions/near/443147810

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

[fpvandoorn]

Another user was confused by this behavior here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.40foo.20.28A.20.3A.3D.20bar.29.20_.20_/near/468564862

Related RFC #5386 and PR #5283

I argued here that I'm in favor of turning of the feature "argument suppression via named arguments".

[kmill]

It looks like this issue is fixed now due to #5283.