Karamel extraction errors on `noextract` recursive tactic

[amosr]

I came across an error when defining a tactic that uses a local recursive definition as well as repeat. The --codegen krml extraction fails with a "this should not happen" error below. The minimised program is contrived but it happened for a real program, too.

Error message:

$ fstar.exe --codegen krml --odir build/extract/xwt example/bug-reports/ExtractWithTac.fst
Extracted module FStar.Pervasives.Native
...
Extracted module FStar.Tactics
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)")
* Warning 302 at FStar.Tactics.Effect.fsti(178,22-178,28):
  - for expression f () of type 'a, Expected effect Pure; got effect Impure

FAIL

The file ExtractWithTac.fst:

module ExtractWithTac

module T = FStar.Tactics

noextract
let rec_and_repeat (): T.Tac unit =
  let rec go (bs: list unit): T.Tac unit =
    match bs with
    | [] -> ()
    | _ :: bs -> go bs in
  ignore (T.repeat T.revert)

// The original (not-as-contrived) program was:
//
// let clear_all (): T.Tac unit =
//   let open T in
//   let rec go bs: Tac unit = match bs with
//    | [] -> ()
//    | b::bs ->
//     (try
//       T.clear b
//     with err ->
//       ());
//     go bs
//   in
//   ignore (T.repeat T.revert);
//   let bs = T.repeat T.intro in
//   go bs

[nikswamy]

Thanks Amos.

1. noextract is confusing and the documentation on the wiki is out of date and should be updated.

See this: https://github.com/FStarLang/FStar/pull/2090

noextract results in a definition not being extract for --codegen OCaml, but not for --codegen krml

If you really want to skip this for Karamel, you can write

[@@noextract_to "krml"]
let rec_and_repeat ...

We should update the wiki.

2. Regardless of the qualifier, this should extract without crashing. So, thanks for the bug-report ... we should fix that.

[amosr]

Thanks Nik! The noextract_to attribute gets me out of trouble. (I ended up needing both noextract and noextract_to.)

[tahina-pro]

(I ended up needing both noextract and noextract_to.)

Yes, I also recently hit this. I had to read into the source code of FStar.Extraction.ML.Modul: https://github.com/FStarLang/FStar/blob/ff87ff54356a0d79da894383d1715f6f801afd4b/src/extraction/FStar.Extraction.ML.Modul.fst#L699-L720