fix: refine how named arguments suppress explicit arguments

src/Lean/Elab/App.lean

@@ -433,11 +433,13 @@ private def hasArgsToProcess : M Bool := do
   let s ← get
   return !s.args.isEmpty || !s.namedArgs.isEmpty
 
-/-- Return `true` if the next argument at `args` is of the form `_` -/
-private def isNextArgHole : M Bool := do
+/--
+Returns the argument syntax if the next argument at `args` is of the form `_`.
+-/
+private def nextArgHole? : M (Option Syntax) := do
   match (← get).args with
-  | Arg.stx (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true
-  | _ => pure false
+  | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx
+  | _ => pure none
 
 /--
   Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type
@@ -649,20 +651,46 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processInstImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      if (← isNextArgHole) then
+      if (← anyNamedArgDependsOnCurrent) then
+        /-
+        See the note in processExplicitArg about `anyNamedArgDependsOnCurrent`.
+        For consistency, instance implicit arguments should always become implicit if a named argument depends on them.
+        If we do not do this check here, then the `nextArgHole?` branch being before `processExplicitArg`
+        would result in counterintuitive behavior.
+        For example, without this block of code, in the following the `_` is optional.
+        When it is omitted, `processExplicitArg` sees that `h` depends on the `Decidable` instance
+        so makes the `Decidable` instance argument become implicit.
+        When it is `_`, the `nextArgHole?` branch allows it to be present.
+        The third example counterintuitively yields a "function expected" error.
+        ```lean
+        theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry
+
+        variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)
+
+        example : p := @foo (h := h)
+        example : p := @foo (h := h) _
+        example : p := @foo (h := h) inferInstance
+        ```
+        -/
+        addImplicitArg argName
+      else if let some stx ← nextArgHole? then
         /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
-        let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+        let ty ← getArgExpectedType
+        let arg ← mkInstMVar ty
+        addTermInfo' stx arg ty (← getLCtx)
         modify fun s => { s with args := s.args.tail! }
-        addInstMVar arg.mvarId!
-        addNewArg argName arg
         main
       else
         processExplicitArg argName
     else
-      let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+      discard <| mkInstMVar (← getArgExpectedType)
+      main
+  where
+    mkInstMVar (ty : Expr) : M Expr := do
+      let arg ← mkFreshExprMVar ty MetavarKind.synthetic
       addInstMVar arg.mvarId!
       addNewArg argName arg
-      main
+      return arg
 
   /-- Elaborate function application arguments. -/
   partial def main : M Expr := do

tests/lean/interactive/explicitAppInstHole.lean

@@ -0,0 +1,6 @@
+/-!
+# Make sure there is type information on `_` for inst parameters in explicit mode
+-/
+
+example : Nat := @ite _ True _ 1 2
+                           --^ textDocument/hover

tests/lean/interactive/explicitAppInstHole.lean.expected.out

@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file:///explicitAppInstHole.lean"},
+ "position": {"line": 4, "character": 29}}
+{"range":
+ {"start": {"line": 4, "character": 29}, "end": {"line": 4, "character": 30}},
+ "contents":
+ {"value":
+  "```lean\ninstDecidableTrue : Decidable True\n```\n***\nA placeholder term, to be synthesized by unification. \n***\n*import Init.Core*",
+  "kind": "markdown"}}

tests/lean/run/explicitApp.lean

@@ -0,0 +1,27 @@
+/-!
+# Tests for app elaborator in explicit mode
+-/
+
+namespace Test1
+
+/-!
+Named arguments in explicit mode cause arguments it depends on to become implicit.
+However, inst implicit arguments had odd behavior with `_`, since supplying `_` would override
+the fact that it should be implicit.
+-/
+
+theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry
+
+variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)
+
+example : p := @foo (h := h)
+/--
+error: function expected at
+  foo h
+term has type
+  p
+-/
+#guard_msgs in
+example : p := @foo (h := h) _
+
+end Test1