Tm_meta is dropped throughout extraction

[msprotz]

At some point during @nikswamy 's work to normalize pure computations within effectful terms, the Tm_meta annotations were dropped. Specifically, those that indicate let-mutable constructs are no longer there at extraction time, meaning that let mutable is broken for the purposes of Low*.

[msprotz]

Here's a testcase:

diff --git a/src/extraction/term.fs b/src/extraction/term.fs
index 815f303..37e76c3 100644
--- a/src/extraction/term.fs
+++ b/src/extraction/term.fs
@@ -755,6 +755,7 @@ and term_as_mlexpr' (g:env) (top:term) : (mlexpr * e_tag * mlty) =
           ml_unit, E_PURE, ml_unit_ty

         | Tm_meta (t, Meta_desugared Mutable_alloc) ->
+            failwith "Found!";
             // the lack of as-patterns makes this a little bit heavy
             begin match term_as_mlexpr' g t with
             | { expr = MLE_Let ((NonRec, flags, bodies), continuation);
diff --git a/src/parser/tosyntax.fs b/src/parser/tosyntax.fs
index 45a1215..2a0cd9b 100644
--- a/src/parser/tosyntax.fs
+++ b/src/parser/tosyntax.fs
@@ -825,7 +825,7 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term =
               mk <| Tm_let((false, [mk_lb (Inl x, x.sort, t1)]), Subst.close [S.mk_binder x] body)
           end in
         if is_mutable
-        then mk <| Tm_meta (tm, Meta_desugared Mutable_alloc)
+        then (Util.print_string "!!! GENERATED !!!\n"; mk <| Tm_meta (tm, Meta_desugared Mutable_alloc))
         else tm
       in

Apply the following diff (cd FStar && patch -p1 < path-to-this-diff). Then cd kremlin/test and make Mutable.exe KOPTS=-verbose.

This displays, among many other messages related to not extracting polymorphic functions:

⚡ Calling F*
✔ [F*,extract]
!!! GENERATED !!!

Meaning that the given Tm_meta node is generated, but then the failwith that's supposed to abort as soon as it's found on the other end is never triggered.

[mtzguido]

Is this still relevant? let mutable itself is gone but don't know if any other Tm_meta annotations are still relevant to extraction

[aseemr]

Closing this issue since we don't have a concrete repro, we can file new issue(s) in case.