From 5f96a9fc4dbf0deae280eaf0a5bbd293fe9ec6c2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 19 Dec 2021 11:03:15 +0100
Subject: [PATCH] fix: do not show type of sort in hover

Fixes #896
---
 src/Lean/Server/InfoUtils.lean                 | 3 +++
 tests/lean/interactive/hover.lean              | 3 +++
 tests/lean/interactive/hover.lean.expected.out | 8 ++++++++
 3 files changed, 14 insertions(+)

diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index f98799cfda..dfc2cd375a 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -171,6 +171,9 @@ where
   fmtTerm? : MetaM (Option Format) := do
     match i with
     | Info.ofTermInfo ti =>
+      if ti.expr.isSort then
+        -- 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
         Meta.ppExpr ti.expr
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index 580c7cc8ef..ddca593abe 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -134,3 +134,6 @@ instance : ToString Nat := ⟨toString⟩
 --^ textDocument/hover
 instance f : ToString Nat := ⟨toString⟩
        --^ textDocument/hover
+
+example : Type 0 := Nat
+        --^ textDocument/hover
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 5df3cf0caf..f27157338f 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/tests/lean/interactive/hover.lean.expected.out
@@ -159,3 +159,11 @@ null
   "end": {"line": 134, "character": 10}},
  "contents":
  {"value": "```lean\nBar.f : ToString Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 137, "character": 10}}
+{"range":
+ {"start": {"line": 137, "character": 10},
+  "end": {"line": 137, "character": 16}},
+ "contents":
+ {"value": "A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ",
+  "kind": "markdown"}}