diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 072823f33581..0a1192137b93 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -650,10 +650,10 @@ mutual
       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.
+        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, in the following the `_` is optional.
+        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.
@@ -668,8 +668,7 @@ mutual
         example : p := @foo (h := h) inferInstance
         ```
         -/
-        discard <| mkInstMVar (← getArgExpectedType)
-        main
+        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 ty ← getArgExpectedType