fix: hovers and docstrings for (co)inductive types

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.

Author: david-christiansen

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
@@ -1275,9 +1274,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 +1300,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 +1325,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

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

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"}}