Extraction: local letrecs with Tac effect cause error

[amosr]

Something is weird with local letrecs and Tac effect. The following program won't extract:

module ExtractTacRec

module Tac = FStar.Tactics.V2

let rec_crash (fv: Tac.fv): Tac.Tac unit =
  let rec go (attrs: list unit): Tac.Tac unit =
    match attrs with
    | [] -> ()
    | hd :: tl ->
      go tl
  in
  // this let is critical: the example works without it, or if it's moved up
  let nm = Tac.inspect_fv fv in
  go []

I extracted it with bin/fstar.exe tests/extraction/ExtractTacRec.fst --codegen Plugin --extract ExtractTacRec --odir out_x --z3version 4.13.3 which gives the following error:

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("This should not happen (should have been handled at Tm_abs level for effect FStar.Tactics.Effect.TAC)")

Running with --debug SMTEncodingReify,Extraction,ExtractionNorm, the following looks suspicious to me:

Reified body reify (let rec go attrs =
      match attrs with
      | [] -> ()
      | _ :: tl -> go tl
    in
    let nm = FStar.Stubs.Reflection.V2.Builtins.inspect_fv fv in
    go []) 
to reify (let rec go attrs =
      match attrs with
      | [] -> ()
      | _ :: tl -> go tl
    in
    let nm = FStar.Stubs.Reflection.V2.Builtins.inspect_fv fv in
    go [])

I don't know, but should reify (let rec go ... = e in e') reduce to let rec go ... = reify e in reify e'?

If I comment out the let nm = Tac.inspect_fv fv line, then extraction does succeed, but the reify still looks suspect to me:

Reified body reify (let rec go attrs =
      match attrs with
      | [] -> ()
      | _ :: tl -> go tl
    in
    go []) 
to reify (let rec go attrs =
      match attrs with
      | [] -> ()
      | _ :: tl -> go tl
    in
    go [])

I'll keep digging to see if I can fix it myself, but any guidance / thoughts / references would be appreciated.

@nikswamy