Weird transient issue in steel, gensym collision?

[mtzguido]

This has been happening on and off for a bit, where some seemingly innocuous changes to F* trigger this bug again, but trying to minimize it makes it disappear in pure Heisenbug fashion. I am using this issue to make a note and save some hashes where it does happen.

For F* hash https://github.com/FStarLang/FStar/commit/3ed3c98d39ce028c31c5908a38bc68ad5098f563 and steel hash 876bf9343a3fa4b8ab2e3b26e3574c7a445c3cd8, trying to build steel gives the following two errors:

* Error 228 at Steel.ST.GhostReference.fsti(171,10-171,16):
  - Tactic failed
  - apply_lemma failed
  - Cannot instantiate lemma: FStar.Tactics.V2.Logic.fa_intro_lem
    with postcondition:
      forall (x: Steel.Effect.Common.vprop).
        Steel.Effect.Common.equiv x (*?u2498*) _ ==> (*?u2490*) _
    to match goal:
      Prims.squash (forall (x1: Steel.Effect.Common.vprop).
            Steel.Effect.Common.equiv x1 x ==>
            Steel.Effect.Common.equiv x1
              (Steel.Effect.Common.VStar x Steel.Effect.Common.emp))

* Error 228 at Steel.Array.fsti(102,2-102,21):
  - Tactic failed
  - apply_lemma failed
  - Cannot instantiate lemma: FStar.Tactics.V2.Logic.fa_intro_lem
    with postcondition:
      forall (x: Steel.Effect.Common.vprop).
        Steel.Effect.Common.equiv x (Steel.Effect.Common.VStar x (*?u272*) _) ==>
        (*?u260*) _
    to match goal:
      Prims.squash (forall (x2: Steel.Effect.Common.vprop).
            Steel.Effect.Common.equiv x2 (Steel.Effect.Common.VStar x x) ==>
            Steel.Effect.Common.equiv x2 (Steel.Effect.Common.VStar x x))

Seemingly for no reason, as nothing really changed in F* to affect it. However almost any random change in those files makes it succeed, e.g. this diff:

diff --git a/lib/steel/Steel.Array.fsti b/lib/steel/Steel.Array.fsti
index 753869e7..e0d13841 100644
--- a/lib/steel/Steel.Array.fsti
+++ b/lib/steel/Steel.Array.fsti
@@ -90,6 +90,8 @@ val intro_varrayp
       aselp a p h' == s
     )

+let f x = x
+
 let intro_varray
   (#opened: _) (#elt: Type) (a: array elt) (s: Seq.seq elt)
 : SteelGhost unit opened
diff --git a/lib/steel/Steel.ST.GhostReference.fsti b/lib/steel/Steel.ST.GhostReference.fsti
index ee9c3610..8679383a 100644
--- a/lib/steel/Steel.ST.GhostReference.fsti
+++ b/lib/steel/Steel.ST.GhostReference.fsti
@@ -144,6 +144,8 @@ val free (#a:Type0)
       (pts_to r full_perm v)
       (fun _ -> emp)

+let f x = x
+
 /// Executes a code block with a ghost reference temporarily
 /// allocated. This function is declared in the `STF` effect so
 /// that the pre- and post-resources can be properly inferred by the

I think the problem is possibly a variable collision due to some bad scoping, and the let f x = x affects the gensym slightly to avoid it.