Fixing the need to use --ide_id_info_off in Steel and Pulse

[nikswamy]

Particularly in Steel and Pulse files, when using fstar-mode.el or with fstar-vscode-assistant, one would need to use --ide_id_info_off to avoid having F* crash when it enters types in the IDE's symbol lookup table.

This has puzzled me for a long time and the need to use the flag is also annoying.

The problem

In some places we do let tx = UF.new_transaction(); typecheck some stuff; UF.rollback tx

Typechecking the stuff in between can add new symbols to the IDE id table and those symbols may mention uvars in the unionfind graph associated with tx.

But, when the tx is rolled back, those uvars are left dangling, although they are still in this table.

Later, when we complete checking the enclosing top-level declaration, we scan this table promoting all id info there (by normalizing all types in the id table and moving them to another sub-table), but there we encounter this dangling uvar and crash.

The fix

The fix is in two parts.

1. First, the symbol table is just for info purposes and is not needed for correctness. So, rather than crashing if an unresolved uvar is found, I check if an unresolved uvar is present, and if so simply remove the entry from the table; Otherwise, normalize and move it as before. This should be a global defensive fix, but at the cost of losing information in the table.

2. In Pulse, this particular pattern of rolling back the UF graph happens at every callback to the typechecker. So, in FStar.Tactics.V2.Basic.refl_typing_builtin_wrapper I now promote entries in the symbol table at each callback before rolling back the UF graph. That allows us to keep useful symbol info.

If we wanted to retain all symbols in non-Pulse scenarios, we'd have to track down all uses of this transaction rollback pattern and apply a similar patch as in refl_typing_builtin_wrapper.

Evaluation

I have tested that Pulse files that were using this ide_id_info_off for use in the editor no longer need to do so.

I have also checked that some steel files that were using this option (e.g., OWGCounter) also no longer need to do so, @R1kM , you might be interested to check if this PR helps remove that option in other Steel developments.