From 9f4075be723d8f426ba6bde4aee3390047279b12 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 27 Sep 2024 13:14:29 -0700
Subject: [PATCH] fix: refine how named arguments suppress explicit arguments
 (#5283)

Recall that currently named arguments suppress all explicit parameters
that are dependencies. This PR limits this feature to only apply to true
structure projections, except in the case where it is triggered when
there are no more positional arguments. This preserves the primary
reason for generalizing this feature (issue #1851), while removing the
generalized feature, which has led to numerous confusions (issue #1867).
This also fixes a bug pointed out [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.40foo.20.28A.20.3A.3D.20bar.29.20_.20_/near/468564862)
where in `@` mode, instance implicit parameter dependencies to named
arguments would be suppressed unless the next positional argument was
`_`.

More detail:
* The `NamedArg` structure now has a `suppressDeps : Bool` field. It is
set to `true` for the `self` argument in structure projections. If there
is such a `NamedArg`, explicit parameters that are dependencies to the
named argument are turned into implicit arguments. The consequence is
that *all* structure projections are treated as if their type parameters
are implicit, even for class projections. This flag is *not* used for
generalized field notation.
* We preserve the suppression feature when there are no positional
arguments remaining. This feature pre-dates the fix to issue #1851, and
it is useful when combining named arguments and the eta expansion
feature, since dependencies of named arguments cannot be turned into eta
arguments. Plus, there are examples of the form `rw [lem (h := foo)]`
where `lem` has explicit arguments that `h` depends on.
* For instance implicit parameters in explicit mode, now `_` arguments
register terminfo and are hoverable.
* Now `..` is respected in explicit mode.

This implements RFC #5397. The `suppressDeps` flag suggests a future
possibility of a named argument syntax that can suppress dependencies.
---
 src/Lean/Elab/App.lean                        | 48 +++++++++++++++----
 .../lean/interactive/explicitAppInstHole.lean |  6 +++
 .../explicitAppInstHole.lean.expected.out     |  8 ++++
 tests/lean/run/explicitApp.lean               | 27 +++++++++++
 4 files changed, 79 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/interactive/explicitAppInstHole.lean
 create mode 100644 tests/lean/interactive/explicitAppInstHole.lean.expected.out
 create mode 100644 tests/lean/run/explicitApp.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index d7caaa78c365..9cd48c4519d9 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/tests/lean/interactive/explicitAppInstHole.lean b/tests/lean/interactive/explicitAppInstHole.lean
new file mode 100644
index 000000000000..96f5abb08db6
--- /dev/null
+++ b/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
diff --git a/tests/lean/interactive/explicitAppInstHole.lean.expected.out b/tests/lean/interactive/explicitAppInstHole.lean.expected.out
new file mode 100644
index 000000000000..5b8f04d000f9
--- /dev/null
+++ b/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"}}
diff --git a/tests/lean/run/explicitApp.lean b/tests/lean/run/explicitApp.lean
new file mode 100644
index 000000000000..188575def36e
--- /dev/null
+++ b/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