viewing types of ctrl-space suggestions in VS Code

Stream: general

[Kevin Buzzard]

I often use ctrl-space to give me suggestions for the lemma I'm looking for. But the output is totally weird to me. Frequently I do not see the full type of the suggested lemma, VS Code cuts it off after a few lines. In the gif example attached, you can see that sometimes 5 lines are displayed and sometimes two. Can I persuade VS Code to just tell me the type of the lemma, rather than just giving me the list of typeclasses in the input and then truncating after two lines? You can see in the video that sometimes VS Code displays 2 lines, and somtimes 5, and I can see no rhyme or reason for the choice. I would like to see "as much as possible" and there is clearly room to display this. I can hover over the output to see the full type but the font size is too tiny for me to read and I don't know how to increase it, and I don't really want to hover anyway, I just want to see the output on the font size I've selected. Am I making sense? Why is VS Code sometimes only displaying two lines of output and sometimes 5? Concrete example: why can't I see the full type of finsum_mem_congr?

autocomplete2.gif

[Aaron Liu]

The relevant setting category is Editor › Suggest but I can't find the setting

[David Ledvinka]

I had a similar issue. I assume someone likely has a better solution but if not I found you can drag on the size of the right hand box so that it is big enough to see any (or most) type declarations. It will keep that size until you quit the editor (I am not sure if there is a way to save it).
vscode.png

[Marc Huisinga]

I think the reason that VS Code cuts this information off in this way is that it retains the line breaks in code blocks and then just omits all characters on the same line that exceed the width of the box. AFAIK there's no good way to configure this other than increasing the size of the box (even the auto-completion font size setting doesn't seem to affect it).

I've played around a bit with the VS Code API to see whether there is something we can do to improve the way it renders this, e.g. by moving the type from the "detail" field to the "documentation" field, but all of the alternatives are even worse.

We could drop the full implicit prefix so that type classes don't show up in the type, if that is a desired change (lean4#7676). It's not perfectly clear to me that type class dependencies are never of interest, though.

[Shreyas Srinivas]

We had a similar discussion w.r.t to the loogle extension. The conclusion iirc was that typeclass instances matter but implicits don’t

[Shreyas Srinivas]

Adding anything to the description makes it cluttered. But I think vscode doesn’t trim white spaces at the end of the description. I used it to sneak in an empty new line to improve vertical spacing between the options

[Shreyas Srinivas]

Ofc this is a brittle way to improve the UI since vscode devs could change this behaviour any day

[Marc Huisinga]

Shreyas Srinivas said:

Adding anything to the description makes it cluttered. But I think vscode doesn’t trim white spaces at the end of the description. I used it to sneak in an empty new line to improve vertical spacing between the options

There is no issue with vertical separation here and we are not talking about VS Code's QuickPick UI, but its auto-completion UI.