fix: hovers and docstrings for (co)inductive types (#10738)

This PR fixes a regression introduced by #10307, where hovering the name of an inductive type or constructor in its own declaration didn't show the docstring. In the process, a bug in docstring handling for coinductive types was discovered and also fixed. Tests are added to prevent the regression from repeating in the future.
2025-10-15 11:32:11 +02:00 · 2025-10-15 11:32:11 +02:00 · 45df6fcd37
commit 45df6fcd37
parent 4077bf2c05
3 changed files with 145 additions and 7 deletions
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@ -1123,7 +1123,6 @@ Term.withoutSavingRecAppSyntax do
 private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext :=
  withElaboratedHeaders vars elabs fun vars elabs rs scopeLevelNames => do
    let res ← mkInductiveDeclCore addAndFinalizeInductiveDecl vars elabs rs scopeLevelNames
-    addTermInfoViews <| elabs.map (·.view)
    return res

 private def mkAuxConstructions (declNames : Array Name) : TermElabM Unit := do
@ -1147,10 +1146,6 @@ def updateViewWithFunctorName (view : InductiveView) : InductiveView :=
  let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (addFunctorPostfix ctor.declName.getPrefix)})
  {view with declName := addFunctorPostfix view.declName, ctors := newCtors}

-def updateViewRemovingFunctorName (view : InductiveView) : InductiveView :=
-  let newCtors := view.ctors.map (fun ctor => {ctor with declName := ctor.declName.updatePrefix (removeFunctorPostfix ctor.declName.getPrefix)})
-  {view with declName := addFunctorPostfix view.declName, ctors := newCtors}
-
 private def elabInductiveViews (vars : Array Expr) (elabs : Array InductiveElabStep1) : TermElabM FinalizeContext := do
  let view0 := elabs[0]!.view
  let ref := view0.ref
@ -1275,9 +1270,11 @@ private def elabInductiveViewsPostprocessing (views : Array InductiveView) (res
      unless (views.any (·.isCoinductive)) do
        Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation

+  -- Term info is added here so that docstrings are maximally available in the environment for hovers
+  runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views
+
 private def elabInductiveViewsPostprocessingCoinductive (views : Array InductiveView)
     : CommandElabM Unit := do
-  let views := views.map updateViewRemovingFunctorName
  let view0 := views[0]!
  let ref := view0.ref

@ -1299,6 +1296,9 @@ private def elabInductiveViewsPostprocessingCoinductive (views : Array Inductive
      unless (views.any (·.isCoinductive)) do
        Term.applyAttributesAt view.declName view.modifiers.attrs .afterCompilation

+  -- Term info is added here so that docstrings are maximally available in the environment for hovers
+  runTermElabM fun _ => Term.withDeclName view0.declName <| withRef ref <| addTermInfoViews views
+
 def InductiveViewToCoinductiveElab (e : InductiveElabStep1) : CoinductiveElabData where
  declId := e.view.declId
  declName := e.view.declName
@ -1321,7 +1321,6 @@ def elabInductives (inductives : Array (Modifiers × Syntax)) : CommandElabM Uni
      elabFlatInductiveViews vars flatElabs
      discard <| flatElabs.mapM fun e => MetaM.run' do mkSumOfProducts e.view.declName
      elabCoinductive (flatElabs.map InductiveViewToCoinductiveElab)
-      addTermInfoViews <| elabs.map (·.view)
    elabInductiveViewsPostprocessingCoinductive (elabs.map (·.view))
  else
    let res ← runTermElabM fun vars => do
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@ -306,3 +306,43 @@ since it needs the environment with the generated `_eval.match_1` matcher.
 -/
 #eval (default : Nat) matches .succ ..
                      --^ textDocument/hover
+
+/--
+These are docs
+-/
+structure S where
+        --^ textDocument/hover
+  /-- So are these -/
+  mk ::
+--^ textDocument/hover
+  /-- And these -/
+  x : Nat
+--^ textDocument/hover
+
+#check { x := 5 : S }
+       --^ textDocument/hover
+                --^ textDocument/hover
+
+/-- Docs -/
+inductive S' where
+        --^ textDocument/hover
+  /-- More docs -/
+  | mk (x : Nat)
+  --^ textDocument/hover
+
+#check (.mk 5 : S')
+       --^ textDocument/hover
+              --^ textDocument/hover
+
+/-- An infinite sequence -/
+coinductive InfSeq (r : α → α → Prop) : α → Prop where
+          --^ textDocument/hover
+  /-- Take a step -/
+  | step : r a b → InfSeq r b → InfSeq r a
+     --^ textDocument/hover
+
+#check InfSeq
+     --^ textDocument/hover
+
+#check InfSeq.step
+     --^ textDocument/hover
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@ -657,3 +657,102 @@
 {"start": {"line": 306, "character": 6},
  "end": {"line": 306, "character": 38}},
 "contents": {"value": "```lean\nBool\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 312, "character": 10}}
+{"range":
+ {"start": {"line": 312, "character": 10},
+  "end": {"line": 312, "character": 11}},
+ "contents":
+ {"value": "```lean\nS : Type\n```\n***\nThese are docs\n", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 315, "character": 2}}
+{"range":
+ {"start": {"line": 315, "character": 2}, "end": {"line": 315, "character": 4}},
+ "contents":
+ {"value": "```lean\nS.mk (x : ℕ) : S\n```\n***\nSo are these ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 318, "character": 2}}
+{"range":
+ {"start": {"line": 318, "character": 2}, "end": {"line": 318, "character": 3}},
+ "contents":
+ {"value": "```lean\nS.x (self : S) : ℕ\n```\n***\nAnd these ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 321, "character": 9}}
+{"range":
+ {"start": {"line": 321, "character": 9},
+  "end": {"line": 321, "character": 10}},
+ "contents":
+ {"value": "```lean\nx : ℕ\n```\n***\nAnd these ", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 321, "character": 18}}
+{"range":
+ {"start": {"line": 321, "character": 18},
+  "end": {"line": 321, "character": 19}},
+ "contents":
+ {"value": "```lean\nS : Type\n```\n***\nThese are docs\n", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 326, "character": 10}}
+{"range":
+ {"start": {"line": 326, "character": 10},
+  "end": {"line": 326, "character": 12}},
+ "contents":
+ {"value": "```lean\nS' : Type\n```\n***\nDocs ", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 329, "character": 4}}
+{"range":
+ {"start": {"line": 329, "character": 4}, "end": {"line": 329, "character": 6}},
+ "contents":
+ {"value": "```lean\nS'.mk (x : ℕ) : S'\n```\n***\nMore docs ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 332, "character": 9}}
+{"range":
+ {"start": {"line": 332, "character": 8},
+  "end": {"line": 332, "character": 11}},
+ "contents":
+ {"value": "```lean\nS'.mk (x : ℕ) : S'\n```\n***\nMore docs ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 332, "character": 16}}
+{"range":
+ {"start": {"line": 332, "character": 16},
+  "end": {"line": 332, "character": 18}},
+ "contents":
+ {"value": "```lean\nS' : Type\n```\n***\nDocs ", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 337, "character": 12}}
+{"range":
+ {"start": {"line": 337, "character": 12},
+  "end": {"line": 337, "character": 18}},
+ "contents":
+ {"value":
+  "```lean\nInfSeq.{u_1} {α : Sort u_1} (r : α → α → Prop) : α → Prop\n```\n***\nAn infinite sequence ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 340, "character": 7}}
+{"range":
+ {"start": {"line": 340, "character": 4}, "end": {"line": 340, "character": 8}},
+ "contents":
+ {"value":
+  "```lean\nInfSeq.step.{u_1} {α : Sort u_1} (r : α → α → Prop) {a b : α} : r a b → InfSeq r b → InfSeq r a\n```\n***\nTake a step ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 343, "character": 7}}
+{"range":
+ {"start": {"line": 343, "character": 7},
+  "end": {"line": 343, "character": 13}},
+ "contents":
+ {"value":
+  "```lean\nInfSeq.{u_1} {α : Sort u_1} (r : α → α → Prop) : α → Prop\n```\n***\nAn infinite sequence ",
+  "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hover.lean"},
+ "position": {"line": 346, "character": 7}}
+{"range":
+ {"start": {"line": 346, "character": 7},
+  "end": {"line": 346, "character": 18}},
+ "contents":
+ {"value":
+  "```lean\nInfSeq.step.{u_1} {α : Sort u_1} (r : α → α → Prop) {a b : α} : r a b → InfSeq r b → InfSeq r a\n```\n***\nTake a step ",
+  "kind": "markdown"}}