From c95100e8fd7e9c72297b1dee39676be1033c39df Mon Sep 17 00:00:00 2001
From: Marc Huisinga <mhuisi@protonmail.com>
Date: Mon, 25 Aug 2025 10:47:14 +0200
Subject: [PATCH] fix: de-prioritize `PartialTermInfo` in hover info selection
 (#10047)

This PR ensures that hovering over `match` displays the type of the
match.
---
 src/Lean/Server/InfoUtils.lean                      | 7 +++++++
 tests/lean/interactive/hoverMatch.lean              | 6 ++++++
 tests/lean/interactive/hoverMatch.lean.expected.out | 8 ++++++++
 3 files changed, 21 insertions(+)
 create mode 100644 tests/lean/interactive/hoverMatch.lean
 create mode 100644 tests/lean/interactive/hoverMatch.lean.expected.out

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 3aab2c98cd..7a533c6167 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -251,6 +251,8 @@ structure HoverableInfoPrio where
   size : Nat
   -- Prefer results for constants over variables (which overlap at declaration names)
   isVariableInfo : Bool
+  -- Prefer non-partial infos over partial infos
+  isPartialTermInfo : Bool
   deriving BEq
 
 instance : Ord HoverableInfoPrio where
@@ -267,6 +269,10 @@ instance : Ord HoverableInfoPrio where
       return .lt
     if ! i1.isVariableInfo && i2.isVariableInfo then
       return .gt
+    if i1.isPartialTermInfo && ! i2.isPartialTermInfo then
+      return .lt
+    if ! i1.isPartialTermInfo && i2.isPartialTermInfo then
+      return .gt
     return .eq
 
 instance : LE HoverableInfoPrio := leOfOrd
@@ -300,6 +306,7 @@ partial def InfoTree.hoverableInfoAtM? [Monad m] (t : InfoTree) (hoverPos : Stri
       isHoverPosOnStop := r.stop == hoverPos
       size := (r.stop - r.start).byteIdx
       isVariableInfo := info matches .ofTermInfo { expr := .fvar .., .. }
+      isPartialTermInfo := info matches .ofPartialTermInfo ..
     }
     let result := { ctx, info, children }
     return some (priority, result)
diff --git a/tests/lean/interactive/hoverMatch.lean b/tests/lean/interactive/hoverMatch.lean
new file mode 100644
index 0000000000..f723ce777c
--- /dev/null
+++ b/tests/lean/interactive/hoverMatch.lean
@@ -0,0 +1,6 @@
+-- Hovering on `match` displays the type
+example :=
+  match true with
+  --^ textDocument/hover
+  | true => true
+  | false => false
diff --git a/tests/lean/interactive/hoverMatch.lean.expected.out b/tests/lean/interactive/hoverMatch.lean.expected.out
new file mode 100644
index 0000000000..5e5e9c6214
--- /dev/null
+++ b/tests/lean/interactive/hoverMatch.lean.expected.out
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file:///hoverMatch.lean"},
+ "position": {"line": 2, "character": 4}}
+{"range":
+ {"start": {"line": 2, "character": 2}, "end": {"line": 5, "character": 18}},
+ "contents":
+ {"value":
+  "```lean\nBool\n```\n***\nPattern matching. `match e, ... with | p, ... => f | ...` matches each given\nterm `e` against each pattern `p` of a match alternative. When all patterns\nof an alternative match, the `match` term evaluates to the value of the\ncorresponding right-hand side `f` with the pattern variables bound to the\nrespective matched values.\nIf used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available\nwithin `f`.\n\nWhen not constructing a proof, `match` does not automatically substitute variables\nmatched on in dependent variables' types. Use `match (generalizing := true) ...` to\nenforce this.\n\nSyntax quotations can also be used in a pattern match.\nThis matches a `Syntax` value against quotations, pattern variables, or `_`.\n\nQuoted identifiers only match identical identifiers - custom matching such as by the preresolved\nnames only should be done explicitly.\n\n`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.\nFor users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they\nshould participate in matching.\nFor example, in\n```lean\nsyntax \"c\" (\"foo\" <|> \"bar\") ...\n```\n`foo` and `bar` are indistinguishable during matching, but in\n```lean\nsyntax foo := \"foo\"\nsyntax \"c\" (foo <|> \"bar\") ...\n```\nthey are not.\n",
+  "kind": "markdown"}}