Preprocess tactic is not able to reconstruct terms involving records/structs

[amosr]

Hi, I just noticed that preprocess_with does not deal well with records. A record constructor { x = 0; y = 1} generates a term like __dummy__ 0 1. If we inspect then re-pack that application, then they don't seem to be re-packed correctly.

Test case:

module Test.VisitRecord

module Tac = FStar.Tactics

type record = { x: int; y: int; }

[@@Tac.preprocess_with (Tac.visit_tm (fun i -> i))]
let visit_record_nok (add: int): record =
  { x = 0; y = 1 }

The above preprocess tactic should just be an identity transform, but I get the error:

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Invalid_argument("List.combine: list lengths differ")
Raised at Stdlib.invalid_arg in file "stdlib.ml", line 30, characters 20-45
Called from FStar_TypeChecker_TcTerm.tc_maybe_toplevel_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 3180, characters 20-106
Called from FStar_Compiler_Util.record_time in file "fstar-lib/FStar_Compiler_Util.ml", line 26, characters 14-18
Called from FStar_TypeChecker_TcTerm.tc_term in file "fstar-lib/generated/FStar_TypeChecker_TcTerm.ml", line 1674, characters 9-1023
...

I'm not certain, but it seems to be specific to the preprocessing. I have a splice that takes apart record applications and recreates them fine.

I can also recreate the problem without visit:

let rec tac_rec_inspect (t: Tac.term): Tac.Tac Tac.term =
  match Tac.inspect t with
  | Tac.Tv_Abs bv tm ->
    Tac.print "+ abs";
    let tm = tac_rec_inspect tm in
    Tac.print "- abs";
    Tac.pack (Tac.Tv_Abs bv tm)

  | Tac.Tv_App hd (arg, q) ->
    Tac.print "+ app";
    let hd = tac_rec_inspect hd in
    let arg = tac_rec_inspect arg in
    Tac.print "- app";
    Tac.pack (Tac.Tv_App hd (arg, q))

  | ti ->
    Tac.print ("leaf: " ^ Tac.term_to_string (quote ti));
    ti

[@@Tac.preprocess_with (fun t -> tac_rec_inspect t)]
let inspect_record_nok (add: int) =
  { x = 0; y = 1 }

(Low priority for me, just wanted to log it before I forgot)