[Mouseover pop-up] show type above error

In VSCode, when mousing over a constant, it shows

• First any errors on that constant
• Below it the type of the constant

Now the error is already easily visible in the Lean Infoview, either in the Messages or All Messages tab. Therefore, when mousing over a term, I am never interested in seeing the error. However, the type of a constant is not as easily accessible elsewhere, and very often I want to see the type of the constant (usually to find out which arguments are explicit).

Therefore my suggestion: show the type of the constant above the error in the mouse-over pop-up. It will save me a bit of scrolling time, because the error is often larger than the pop-up. This is a minor issue, but it happens very frequently.

In the Zulip thread there is significant support.

Start at the VSCode mouseover pop-up entry point and trace how a constant's type and errors are assembled. Use the Lean Infoview Messages and All Messages tabs, along with the linked Zulip discussion, as context. Done means the constant's type appears above its error while preserving the existing error information.