Tactic using anti-quotation for a binder stuck if lax checked

[857b]

The following example verify without any issue when checked in normal mode:

module Main
open FStar.Tactics

let dummy_lemma (x : int) goal (pf : goal) : goal
  = pf

// begin lax
let test_tac_0 () : Tac unit =
  let x = intro () in
  apply (`dummy_lemma (`#x))
// end lax

let test_0 : (x : int) -> squash (x + 1 > x) = _ by (test_tac_0 (); smt ())

let test_tac_1 () : Tac unit =
  let x = intro () in
  let xt = binder_to_term x in
  apply (`dummy_lemma (`#xt))

let test_1 : (x : int) -> squash (x + 1 > x) = _ by (test_tac_1 (); smt ())

However, if one checks the definition of test_tac_0 in lax mode, it get stuck when called from test_0:

F* reported issues in other files: [(#s(fstar-issue warning (#s(fstar-location "FStar.Tactics.Derived.fst" 523 523 45 90)) "Not an embedded term: let _ =
  FStar.Reflection.Builtins.inspect_binder (FStar.Reflection.Builtins.pack_binder (FStar.Reflection.Builtins.pack_bv
            (FStar.Reflection.Data.Mkbv_view \"x\" 10285 (`Prims.int)))
        (FStar.Reflection.Data.Q_Explicit)
        [])
in
(let bv, _ = _ in
  FStar.Tactics.Derived.bv_to_term bv)
<:
FStar.Reflection.Types.term" 266) #s(fstar-issue warning (#s(fstar-location "FStar.Tactics.Effect.fsti" 94 101 2 32)) "Not an embedded tactic result: match FStar.Tactics.Builtins.t_apply true false (`Main.dummy_lemma _) \"(((proofstate)))\" with
| FStar.Tactics.Result.Success a ps' ->
  let ps' =
    FStar.Tactics.Types.set_proofstate_range ps'
      (FStar.Range.prims_to_fstar_range <input>(13,68-13,74))
  in
  (let true = FStar.Tactics.Types.tracepoint ps' in
    (fun _ -> reify (FStar.Tactics.Derived.smt ())) a (FStar.Tactics.Types.decr_depth ps'))
  <:
  FStar.Tactics.Result.__result Prims.unit
| FStar.Tactics.Result.Failed e ps' -> FStar.Tactics.Result.Failed e ps'" 266))]
(Error 228) user tactic failed: ‘Tactic got stuck! Please file a bug report with a minimal reproduction of this issue.
match FStar.Tactics.Builtins.t_apply true false (‘Main.dummy_lemma _) "(((proofstate)))" with
| FStar.Tactics.Result.Success a ps’ ->
  let ps’ =
    FStar.Tactics.Types.set_proofstate_range ps’
      (FStar.Range.prims_to_fstar_range <input>(13,68-13,74))
  in
  (let true = FStar.Tactics.Types.tracepoint ps’ in
    (fun _ -> reify (FStar.Tactics.Derived.smt ())) a (FStar.Tactics.Types.decr_depth ps’))
  <:
  FStar.Tactics.Result.__result Prims.unit
| FStar.Tactics.Result.Failed e ps’ -> FStar.Tactics.Result.Failed e ps’‘
Related location (C-c C-’ to visit, M-, to come back): Main.fst(13,47-13,48)

The problem seems to come from the direct use of a binder (x) in an anti-quotation operator `#. There is no such issue with test_tac_1, which uses an explicit cast binder_to_term.

[W95Psp]

Hi Benjamin, I think your issue is another form of missed coercion as in #2471, which was fixed by @aseemr yesterday! I tried your example @857b with latest F* master, but the coercion is missed in that specific case. @aseemr do think it is easy to fix?

Btw, we can actually see F* is not inserting a binder_to_term in lax mode by printing the terms, i.e.:

module Main
open FStar.Tactics

assume val dummy_lemma: int -> unit

let test = (fun (x: binder) -> `(dummy_lemma (`#x))) <: _ -> Tac _
#push-options "--lax"
let test_lax = (fun (x: binder) -> `(dummy_lemma (`#x))) <: _ -> Tac _
#pop-options

let body_of_sigelt (n: string)
  = match lookup_typ (top_env ()) (explode_qn n) with
    | Some se -> ( match inspect_sigelt se with
                | Sg_Let _ [lb] -> (inspect_lb lb).lb_def
                | _ -> fail "body_of_sigelt: not Sg_Let" )
    | _ -> fail ("body_of_sigelt: "^n^" not found")

let _ = run_tactic (fun () -> 
    let test     = body_of_sigelt (`%test    ) in
    let test_lax = body_of_sigelt (`%test_lax) in
    print (
      "# test: \n" ^ term_to_string test ^
      "\n# test_lax: \n" ^ term_to_string test_lax
    )
)

prints:

# test:
(fun x ->
    let _ = FStar.Tactics.Derived.binder_to_term x in
    `Main.dummy_lemma _)
<:
_: FStar.Reflection.Types.binder -> FStar.Tactics.Effect.Tac FStar.Reflection.Types.term

# test_lax:
(fun _ -> `Main.dummy_lemma _)
<:
_: FStar.Reflection.Types.binder -> FStar.Tactics.Effect.Tac FStar.Reflection.Types.term