Fixing inconsistencies in inspect_ln

[aseemr]

Problem

Gabriel Ebner (@gebner) noticed that the reflection inspect_ln API compresses unification variables using the union-find graph in the typechecker. This means it is not a total function, and indeed can be used to prove assertions that are not valid at runtime:

let t = inspect_ln (pack_ln (Tv_uvar u)) in
unify u tunit;
let t' = inspect_ln (pack_ln (Tv_uvar u)) in
assert (t == t')

@nikswamy suggested that inspect_ln should not do this compression of uvars.

While working on this, I noticed another quirk. The Tv_Uvar node in the reflection AST has an int index. In inspect_ln we use Syntax.Unionfind.uvar_id to fill in this field. However, uvar_id returns the id of the root of the union-find tree that the uvar belongs to. This can evolve as the union-find graph evolves, and indeed we can write examples to exploit it:

let u1, u2 = uvar_env (top_env ()) (`unit) in
match inspect_ln u1, inspect_ln u2 with
| Tv_Uvar n1 _ , Tv_UVar n2 _ ->
  unify u1 u2;
  (match inspect_ln u1, inspect_ln u2 with
   | Tv_UVar n1' , Tv_UVar n2' _ ->
     assert (n1 == n1' /\ n2 == n2')  // This is not true when the tactic runs, as can be seen in a dump

This PR has the following fixes:

• Don't compress uvars in inspect_ln. However, we still need to push down delayed substitutions. So, the PR adds a new API compress_subst to FStar.Syntax.Subst.
• Use uvars's own id for Tv_UVar.
• A collect_app API in FStar.Tactics.Derived that uses inspect internally.

The second change is done for both inspect_ln and inspect. Otherwise, inspect is unchanged.

Impact on clients

This change breaks some code patterns in the existing code. For example, the steel tactic was doing something like this:

match T.inspect t with
| Tv_App _ _ -> let hd, args = R.collect_app t in
                        ...

Where R.collect_app internally calls into R.inspect_ln to get the head constructor of t.

When t is a uvar, this is problematic, since T.inspect will compress the uvar and may return Tv_App, while R.inspect_ln will return Tv_UVar.

To sort out this confusion, the PR renames R.collect_app to R.collect_app_ln and introduces a T.collect_app that uses inspect internally.

Changing R.collect_app in the steel tactic to T.collect_app restored it.

The other changes were just related to renaming of R.collect_app to R.collect_app_ln. If the client code was in Tac already, I changed R.collect_app to T.collect_app, else to R.collect_app_ln.

No changes are required in Everest, outside of F*.

[aseemr]

A correction: it requires a small patch to HACL* to change some R.inspect_ln calls to T.inspect in Test.Lowstarize.fst.

[mtzguido]

This looks great to me. I'm just adding a test for it and relocating collect_app into Tactics.SyntaxHelpers. Fine with merging as soon as HACL takes the fix.