RFC: show expected type in instance declarations

[alok]

Proposal

(This may be more appropriate in the vscode-lean4 repo?)

In the pic above, putting the cursor on toString does not show the expected type, but hovering does. However, for defs that are not instance implementations, putting the cursor on the identifier will show the expected type as in the following picture.

I propose that it show should the expected type even in instance declarations.

• User Experience: How does this feature improve the user experience?

Easier to see what a function is doing, and anyway hovering shows that type info.

• Beneficiaries: Which Lean users and projects benefit most from this feature/change?

New users, people who don't want to keep stuff in their head.

• Maintainability: Will this change streamline code maintenance or simplify its structure?

Dunno.