Crash with tactics, variable not found

[mtzguido]

module Bug

open FStar.Tactics.V2

assume val token (g:env) : Type0
assume val check (g:env) : Tac (option (token g))

let test1 () : Tac unit =
  let r = check (cur_env()) in
  ()

Bug.fst(6,46-6,47): (Error 230) Variable "g#418" not found (see also Bug.fst(6,18-6,19)) 

Using a separate letbinding for the cur_env call works.

[aseemr]

This seems like a reasonable error (perhaps not so much for the error message) ... what's the type of r in this code. With an explicit binding, we can write the type, but with the code as written I don't think we can.

[mtzguido]

We now get a good message after #3105 (though the wrapping is unfortunate)

* Error 56 at Bug2981.fst(9,10-9,27):
  - Bound variable
    'g#73'
    escapes because of impure applications in the type of
    'check'
  - Add explicit let-bindings to avoid this

1 error was reported (see above)