fix: improve handling of _s for inst implicit arguments in explicit…

… `@` mode

This PR does two things:
1. Recall that in explicit mode, a `_` in place of an instance implicit argument still does instance synthesis (one can use `(_)` instead to turn it into a true implicit argument). There has been missing terminfo for such arguments. Now hovering will display the synthesized expression and its type.
2. Recall that when there are named arguments, every explicit argument the named arguments depend on become implicit. This was interacting badly with instance arguments in explicit mode, since the `_` special casing mentioned above was not respecting this rule. Now it respects this rule.

This PR is operating under the assumption that the named argument feature in item 2 is meant to be active in explicit mode. An alternative to item 2 would be to turn the feature off in explicit mode.

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,47 @@ 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 remain instance 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, 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
+        ```
+        -/
+        discard <| mkInstMVar (← getArgExpectedType)
+        main
+      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