feat: show universe args on hover

We might also want to replace them with fresh vars to make the hover
completely independent of the context, but this change at least avoids
any hidden information.

src/Lean/Server/InfoUtils.lean

@@ -175,11 +175,11 @@ where
         -- types of sorts are funny to look at in widgets, but ultimately not very helpful
         return none
       let tp ← Meta.inferType ti.expr
-      let eFmt ← Lean.withOptions (Lean.pp.fullNames.set . true) do
+      let eFmt ← Lean.withOptions (Lean.pp.fullNames.set · true |> (Lean.pp.universes.set · true)) do
         Meta.ppExpr ti.expr
       let tpFmt ← Meta.ppExpr tp
       -- try not to show too scary internals
-      let fmt := if isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
+      let fmt := if ti.expr.isConst || isAtomicFormat eFmt then f!"{eFmt} : {tpFmt}" else f!"{tpFmt}"
       return some f!"```lean
 {fmt}
 ```"

tests/lean/interactive/hover.lean.expected.out

@@ -80,7 +80,7 @@ null
 {"range":
  {"start": {"line": 93, "character": 8}, "end": {"line": 93, "character": 10}},
  "contents":
- {"value": "```lean\nid : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}}
+ {"value": "```lean\nid.{0} : ∀ {α : Prop}, α → α\n```", "kind": "markdown"}}
 {"textDocument": {"uri": "file://hover.lean"},
  "position": {"line": 93, "character": 10}}
 {"range":