make sure explicit mode disables suppressDeps

src/Lean/Elab/App.lean

@@ -146,7 +146,7 @@ structure State where
   -/
   etaArgs              : Array Expr   := #[]
   /-- Missing explicit arguments, from dependencies of named arguments. These cannot be eta arguments. -/
-  missingExplicit      : Array Expr   := #[]
+  missingExplicits     : Array Expr   := #[]
   /-- Metavariables that we need to set the error context using the application being built. -/
   toSetErrorCtx        : Array MVarId := #[]
   /-- Metavariables for the instance implicit arguments that have already been processed. -/
@@ -380,10 +380,10 @@ private def finalize : M Expr := do
   -- Register the error context of implicits
   for mvarId in s.toSetErrorCtx do
     registerMVarErrorImplicitArgInfo mvarId ref e
-  unless s.missingExplicit.isEmpty do
-    let mes := s.missingExplicit.map fun e => m!"{indentExpr e}"
+  unless s.missingExplicits.isEmpty do
+    let mes := s.missingExplicits.map fun e => m!"{indentExpr e}"
     logError m!"insufficient number of arguments, \
-      missing {s.missingExplicit.size} explicit argument(s) that are dependencies of a named argument.\n\n\
+      missing {s.missingExplicits.size} explicit argument(s) that are dependencies of a named argument.\n\n\
       Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. \
       These are the inferred missing arguments:\
       {MessageData.joinSep mes.toList ""}"
@@ -420,7 +420,10 @@ private def finalize : M Expr := do
   synthesizeAppInstMVars
   return e
 
-/-- Returns a named argument with `suppressDeps == true` that depends on the next argument, otherwise `none`. -/
+/--
+Returns a named argument that depends on the next argument, otherwise `none`.
+If `onlySuppressDeps` is true, then only returns such a named argument with `suppressDeps` true.
+-/
 private def anyNamedArgDependsOnCurrent? (onlySuppressDeps := true) : M (Option NamedArg) := do
   let s ← get
   if s.namedArgs.any (·.suppressDeps || !onlySuppressDeps) then
@@ -547,7 +550,7 @@ mutual
       mkFreshExprMVar argType
     modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! }
     if missingExplicit then
-      modify fun s => { s with missingExplicit := s.missingExplicit.push arg }
+      modify fun s => { s with missingExplicits := s.missingExplicits.push arg }
     addNewArg argName arg
     main
 
@@ -628,7 +631,7 @@ mutual
             However, they can safely be turned into implicit arguments for elaboration.
             This is an error unless the named argument is meant to suppress dependencies.
             -/
-            addImplicitArg argName (missingExplicit := !arg.suppressDeps)
+            addImplicitArg argName (missingExplicit := (← read).explicit || !arg.suppressDeps)
           else if (← read).ellipsis then
             addImplicitArg argName
           else