Meta_desugared Sequence lost during typechecking/normalization

[mtzguido]

@msprotz reports that we are not getting sequences in resugared code, see e.g. this:

module Sequence

let f () = ()

let test () =
  f ();
  f ()

$ ./bin/fstar.exe --dump_module Sequence Sequence.fst 
Module after desugaring:
module Sequence
Declarations: [
let f _ = ()
let test _ =
  Sequence.f ();
  Sequence.f ()
]
Exports: [
let f _ = ()
let test _ =
  Sequence.f ();
  Sequence.f ()
]

Module before type checking:
module Sequence
Declarations: [
let f _ = ()
let test _ =
  Sequence.f ();
  Sequence.f ()
]
Exports: [
let f _ = ()
let test _ =
  Sequence.f ();
  Sequence.f ()
]

Module after type checking:
module Sequence
Declarations: [
let f _ = ()
let test _ =
  [@@ FStar.Pervasives.inline_let ]let _ = Sequence.f () in
  Sequence.f ()
]
Exports: [
let f _ = ()
let test _ =
  [@@ FStar.Pervasives.inline_let ]let _ = Sequence.f () in
  Sequence.f ()
]

(Warning 274) Implicitly opening fstar. namespace shadows (sequence -> Sequence.fst), rename Sequence.fst to avoid conflicts
Verified module: Sequence
All verification conditions discharged successfully

I tried fixing it here but it leads to weird regressions, so making a note.

[msprotz]

Thanks for trying Guido. The use-case is to debug terms produced by a tactic, and when it's not obvious why a term is well-typed, the only workflow I have is to print the term, copy/paste it into a buffer, and then try to run it in interactive mode. This resugaring issue is only one of many other issues that make processing printed terms difficult. Others include incorrectly-prefixed constructors, fully qualified references to the current module (which generate dependency loops in batch mode), and for a long while incorrect printing of machine integers, although maybe that is fixed now? Let me know if you want issues filed for the other problems. Thanks!