Looking into this a bit.

I don't understand how this change could fix the behavior reported in the Pulse issue.

If we enter a symbol in the id_info_table with range = dummyRange, then unless the IDE issues a lookup request with a range equal to the dummy file, with row 0, and some column, I would expect FStar.TypeChecker.Common.id_info_at_pos to return None.

Thereafter, QueryHelper.symlookup should fall back and rely on info_of_lid_str to lookup the symbol in the environment rather than the id_info_table and this could succeed, though it is possible that this returns a symbol with the dummyRange.

So, while I think this change is ok and in fact preferable to not enter symbols with the dummyRange in the id_info_table, I'm not sure this will actually fix the symptom you're observing. Do you think it does? Can you explain why?

Yeah, you're completely right. I'm not sure why I thought the issue went away with this patch.

Part of my confusion is that the range contains two ranges: the range of the use site, as well as the range of the definition site. My intention was to ignore id infos where the definition site is a dummy range. But on second thought this would also throw away useful information (the fully-qualified identifier). The check as implemented in this PR compares both ranges though, which indeed doesn't do anything useful.

I have added a small test case in the fstar-vscode-assistant issue. After some more investigation, I believe that this is a general issue with spliced definitions. The sigelt view doesn't contain ranges, so splices are not required to set it. (And there doesn't seem to be an exposed function to set ranges either.)