Local mutually recursive functions diverge in tactics

[amosr]

Hi,
I just noticed that using let .. and .. for mutually recursive functions, inside a top-level function, was causing my proof to diverge. It seems OK if I lift them up to top-level mutually recursive functions, or inline the recursion to make it a single locally-recursive definition.

Here is a small example that hangs for me:

module TacticRecursion

module T = FStar.Tactics

let visit_terms (t: T.term): T.Tac unit =
  let rec tm (t: T.term): T.Tac unit = match T.inspect_unascribe t with
    | T.Tv_Match sc _ brs ->
      // do work then recurse...
      T.iter br brs;
      tm sc
    | _ -> ()
  and br (b: T.branch): T.Tac unit = tm (snd b)
  in tm t

let nothing (): unit =
  assert (true) by (
    visit_terms (`true)
  )

[mtzguido]

Hi Amos, thanks for the report. Something fishy is definitely happening here. See for instance this, that does not fail:

let visit_terms () : T.Tac unit =
  let rec tm (): T.Tac unit =
    T.fail "fail"
  and unused () : T.Tac unit =
    ()
  in tm ()

let nothing (): unit =
  assert (True) by (
    visit_terms ()
  )

Looking into it.

[mtzguido]

Should be fixed now! Turned out to be a rather scary-looking normalization bug. Thanks again for the clear report!

[amosr]

That was quick! Thanks Guido