From 257cd15a00c587543371ad447e446e02a80b8638 Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Fri, 6 Jun 2025 15:07:01 +0200
Subject: [PATCH] fix: wrong signature help after map/filter/etc (#8655)

This PR fixes a bug in the signature help where it would be displayed
for higher-order-functions that are the last argument of another
function.
---
 src/Lean/Server/FileWorker/SignatureHelp.lean |  7 +++
 tests/lean/interactive/signatureHelp.lean     |  8 ++++
 .../signatureHelp.lean.expected.out           | 45 +++++++++++--------
 3 files changed, 41 insertions(+), 19 deletions(-)

diff --git a/src/Lean/Server/FileWorker/SignatureHelp.lean b/src/Lean/Server/FileWorker/SignatureHelp.lean
index ca9fd94685..cfc1835792 100644
--- a/src/Lean/Server/FileWorker/SignatureHelp.lean
+++ b/src/Lean/Server/FileWorker/SignatureHelp.lean
@@ -134,7 +134,14 @@ def findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext)
   -- applications of a `forall` in front of ones that do.
   -- This usually happens when `.termArg` candidates overshadow `.pipeArg` candidates,
   -- but the `.termArg` candidates are not semantically valid left-hand sides of applications.
+  let hasHighPrioCandidate := candidates.any (·.kind.prio > CandidateKind.termArg.prio)
   for candidate in candidates do
+    if candidate.kind matches .termArg && hasHighPrioCandidate then
+      -- If all high prio candidates agree that there is no function application here,
+      -- we trust them instead of falling back to `.termArg` candidates.
+      -- This ensures that no signature help is displayed for a function that is passed as
+      -- the last argument to another function.
+      return none
     if let some signatureHelp ← determineSignatureHelp tree candidate.appStx then
       return some signatureHelp
   return none
diff --git a/tests/lean/interactive/signatureHelp.lean b/tests/lean/interactive/signatureHelp.lean
index 32c929b2b6..a629c5221e 100644
--- a/tests/lean/interactive/signatureHelp.lean
+++ b/tests/lean/interactive/signatureHelp.lean
@@ -85,6 +85,14 @@ def complexFun (f : Nat → Nat → Nat → Nat → Nat) (x : Nat) : Nat := sorr
 #check complexFun (simpleFun  ) -- Signature help of `simpleFun` expected
                            --^ textDocument/signatureHelp
 
+def complexFun' (x : Nat) (f : Nat → Nat → Nat → Nat → Nat) : Nat := sorry
+
+#check complexFun' 0  -- Shortened signature help of `complexFun'` expected
+                   --^ textDocument/signatureHelp
+
+#check complexFun' 0 simpleFun  -- No signature help expected
+                             --^ textDocument/signatureHelp
+
 structure SomeStructure where
   fieldFun (x : Nat) : Nat → Nat
 
diff --git a/tests/lean/interactive/signatureHelp.lean.expected.out b/tests/lean/interactive/signatureHelp.lean.expected.out
index 52760c9dba..0c5b5ac427 100644
--- a/tests/lean/interactive/signatureHelp.lean.expected.out
+++ b/tests/lean/interactive/signatureHelp.lean.expected.out
@@ -90,50 +90,57 @@ null
 {"signatures": [{"label": "{x : Type} → (a b : Nat) → Nat → Nat → Nat"}],
  "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 96, "character": 18}}
-{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0}
+ "position": {"line": 89, "character": 21}}
+{"signatures": [{"label": "(f : Nat → Nat → Nat → Nat → Nat) → Nat"}],
+ "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 99, "character": 20}}
-{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0}
-{"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 102, "character": 22}}
+ "position": {"line": 92, "character": 31}}
 null
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 105, "character": 23}}
+ "position": {"line": 104, "character": 18}}
 {"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 108, "character": 25}}
+ "position": {"line": 107, "character": 20}}
 {"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 111, "character": 16}}
+ "position": {"line": 110, "character": 22}}
+null
+{"textDocument": {"uri": "file:///signatureHelp.lean"},
+ "position": {"line": 113, "character": 23}}
+{"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0}
+{"textDocument": {"uri": "file:///signatureHelp.lean"},
+ "position": {"line": 116, "character": 25}}
+{"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0}
+{"textDocument": {"uri": "file:///signatureHelp.lean"},
+ "position": {"line": 119, "character": 16}}
 {"signatures": [{"label": "(x : Nat) → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 114, "character": 18}}
+ "position": {"line": 122, "character": 18}}
 null
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 117, "character": 21}}
+ "position": {"line": 125, "character": 21}}
 {"signatures": [{"label": "(x : Nat) → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 120, "character": 23}}
+ "position": {"line": 128, "character": 23}}
 null
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 123, "character": 21}}
+ "position": {"line": 131, "character": 21}}
 {"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 126, "character": 23}}
+ "position": {"line": 134, "character": 23}}
 {"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 129, "character": 25}}
+ "position": {"line": 137, "character": 25}}
 null
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 132, "character": 24}}
+ "position": {"line": 140, "character": 24}}
 {"signatures": [{"label": "(x : Nat) → Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 135, "character": 26}}
+ "position": {"line": 143, "character": 26}}
 {"signatures": [{"label": "Nat → Nat"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 138, "character": 37}}
+ "position": {"line": 146, "character": 37}}
 {"signatures": [{"label": "(x : Nat) → SomeStructure"}], "activeSignature": 0}
 {"textDocument": {"uri": "file:///signatureHelp.lean"},
- "position": {"line": 142, "character": 39}}
+ "position": {"line": 150, "character": 39}}
 null