fix: named argument that depends on missing explicit argument

src/Lean/Elab/App.lean

@@ -348,6 +348,21 @@ private def addImplicitArg (k : M Expr) : M Expr := do
   addNewArg arg
   k
 
+/- Return true if there is a named argument that depends on the next argument. -/
+private def anyNamedArgDependsOnCurrent : M Bool := do
+  let s ← get
+  if s.namedArgs.isEmpty then
+    return false
+  else
+    forallTelescopeReducing s.fType fun xs _ => do
+      let curr := xs[0]
+      for i in [1:xs.size] do
+        let xDecl ← getLocalDecl xs[i].fvarId!
+        if s.namedArgs.any fun arg => arg.name == xDecl.userName then
+          if (← getMCtx).localDeclDependsOn xDecl curr.fvarId! then
+            return true
+      return false
+
 /-
   Process a `fType` of the form `(x : A) → B x`.
   This method assume `fType` is a function type -/
@@ -383,7 +398,10 @@ private def processExplictArg (k : M Expr) : M Expr := do
       throwError "invalid autoParam, argument must be a constant"
     | _, _, _ =>
       if !s.namedArgs.isEmpty then
-        addEtaArg k
+        if (← anyNamedArgDependsOnCurrent) then
+          addImplicitArg k
+        else
+          addEtaArg k
       else if !s.explicit then
         if (← fTypeHasOptAutoParams) then
           addEtaArg k

tests/lean/missingExplicitWithForwardNamedDep.lean

@@ -0,0 +1,30 @@
+class Foo (α : Type) (β : Type)  where
+  val : Nat
+  a   : α
+  b   : β
+
+#check Foo.val
+
+def valOf [s : Foo α β] : Nat :=
+  s.val
+
+#eval valOf (s := { val := 10, a := true, b := false : Foo Bool Bool })
+
+def valOf2 (α β : Type) [s : Foo α β] : Nat :=
+  s.val
+
+#check valOf2 (s := { val := 10, a := true, b := false : Foo Bool Bool })
+-- valOf2 Bool Bool
+
+def f (x y z : Nat) := x + y + z
+
+#check f (z := 10)
+-- fun (x y : Nat) => f x y 10 : Nat → Nat → Nat
+
+def g {α : Type} (a b : α) := b
+#check g (b := 10)
+-- fun (a : Nat) => g a 10
+
+def h (α : Type) (a b : α) := b
+#check h (b := true)
+-- fun a => h Bool a true

tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out

@@ -0,0 +1,6 @@
+Foo.val : (α β : Type) → [self : Foo α β] → Nat
+10
+valOf2 Bool Bool : Nat
+fun (x y : Nat) => f x y 10 : Nat → Nat → Nat
+fun (a : Nat) => g a 10 : Nat → Nat
+fun (a : Bool) => h Bool a true : Bool → Bool