max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: wrong signature help after map/filter/etc (#8655)

Browse source 
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.
This commit is contained in:
Marc Huisinga 2025-06-06 15:07:01 +02:00 • committed by GitHub
parent 5963bc8b8a
commit 257cd15a00
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 41 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Lean/Server/FileWorker/SignatureHelp.lean
View file

@ -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

8
tests/lean/interactive/signatureHelp.lean
View file

@ -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

45
tests/lean/interactive/signatureHelp.lean.expected.out
View file

@ -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