[Mouseover pop-up] show type above error

[fpvandoorn]

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.

[mhuisi]

I don't think that we can adjust this. The order of content in hovers is hardcoded in VS Code:
https://github.com/microsoft/vscode/blob/d374d10eea0154ce74b5cafe64d3e0096dd58717/src/vs/editor/contrib/hover/browser/markerHoverParticipant.ts#L57
https://github.com/microsoft/vscode/blob/d374d10eea0154ce74b5cafe64d3e0096dd58717/src/vs/editor/contrib/hover/browser/contentHover.ts#L55