Inlay Goals in IDE

Stream: lean4

[Manu Bhat]

I know it was previously discussed why inlay hints are currently put off, the reasons of which make sense.

However even if not implemented for a while, here is a proof of concept showing the possible benefits of having inlay goals displayed in an IDE to stir up some discussion. I believe this could especially be more helpful for beginners. Does anyone have any thoughts?

image.png
image.png

In this implementation, type hints are given for expressions such as #check, #eval and the current target type is displayed on blank lines.

[Alex J. Best]

I use inlay type hints and argument names in other languages and find them very useful. I think they would be very useful for Lean also. Its a shame to hear that they are broken somehow.
The pylance extension in particular has some great features like double clicking on the inlay hint to insert the hint into the file. This allows you to write the code in a lazy way see that it is correctly typed and then insert the type hints rapidly, whether this is more or less appropriate for Lean than python I find it hard to say.

[Patrick Massot]

You can already get the first example without inlay hint. I think it’s enabled by default in neovim, and I got it from the error lens extension when I was using VSCode.

[Shanghe Chen]

Hi I made an initial attempt to display the type for some definitions, which is a typical use case for inlay hints. However, I still cannot distinguish between definitions that already have type annotations and those that omit them. I am wondering if it’s still possible with regular expressions or if I should use a parser. Currently, the semantic tokens do not seem to help here as they appear to be quite coarse.
5F68DD04-51B0-4370-B3C5-2EC293DD29BC.jpg

[Edward van de Meent]

I don't think this is possible with a regular expression (not regEx), because you can't match brackets. Using regEx is likely to result in ugly/unidiomatic code because of this, so I'd say the best way to go about this is to somehow leverage leans parser to do this for you