Invisible goals are sometimes not highlighted

[Lysxia]

Normally invisible goals are shown by highlighting the functions where they are located, but I seem to have run into a case where that isn't the case. I don't have a really small test case but I have a self-contained project (only using stdlib, though it will take a minute or two to load) to hopefully reproduce it:

# The bug-report branch of this repository
git clone https://gitlab.com/lysxia/gradual-eff --branch bug-report

nvim gradual-eff/src/L2/Sim.lagda.md  # Load cornelis: the invisible goals are not highlighted

agda gradual-eff/src/L2/Sim.lagda.md  # Call agda on the command line to get the locations
# Unsolved metas at the following locations:
#   /home/sam/code/agda/gradual-eff/src/L2/Sim.lagda.md:118,50-56
#   /home/sam/code/agda/gradual-eff/src/L2/Sim.lagda.md:118,58-64
#   /home/sam/code/agda/gradual-eff/src/L2/Sim.lagda.md:119,77-80

[isovector]

I don't think this is an issue in cornelis. I can reproduce it in nvim run from the terminal, but not in neovide (a gui on top of nvim):

[isovector]

That being said, we could generate a location list for all holes / unsolved metas.

[isovector]

Just kidding. I can reproduce it in neovide, but I'm not sure what changed!

[isovector]

It looks like this highlighting happens ~20s after the main highlighting.

[isovector]

I've confirmed this is an upstream problem by watching the output from agda.

We emit a IOTCM "/home/sandy/.src/gradual-eff/src/L2/Sim.lagda.md" NonInteractive Direct ( Cmd_load "/home/sandy/.src/gradual-eff/src/L2/Sim.lagda.md" [] ), at 2022-10-17 10:14:28, and the responses are streamed out:

2022-10-17 10:14:28 JSON> {"status":{"checked":false...
2022-10-17 10:14:28 {"kind":"ClearRunningInfo"}
2022-10-17 10:14:28 {"kind":"ClearHighlighting"...
2022-10-17 10:14:29 {"kind":"RunningInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...
2022-10-17 10:14:59 {"kind":"HighlightingInfo"...

2022-10-17 10:15:20 {"kind":"HighlightingInfo"...
2022-10-17 10:15:20 {"kind":"HighlightingInfo"...
2022-10-17 10:15:20 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"kind":"HighlightingInfo"...
2022-10-17 10:15:21 {"status":{"checked":false...
2022-10-17 10:15:21 {"kind":"DisplayInfo"...
2022-10-17 10:15:21 {"kind":"InteractionPoints"...

I've left a linebreak where agda responds with more output after 20 seconds, which is where the unsolved meta highlighting comes from.

[isovector]

"Fixed" in 80b981c by giving the spans of the invisible goals. The highlighting issue itself is a bug upstream in agda.

[Lysxia]

Awesome, thanks!