Proofs made using `unshelve` are forgotten afterward

[TWal]

See the following minimal example

open FStar.Tactics

assume val predicate: int -> Type0
// If we add the SMTPat, then `test` succeed
assume val predicate_is_true_lemma: x:int -> Lemma (predicate x) //[SMTPat (predicate x)]

// The dumps allow us to see that the tactic is called correctly in every case
val prove_predicate: unit -> Tac unit
let prove_predicate () =
  dump "goal";
  apply_lemma (`predicate_is_true_lemma);
  dump "goal solved"

assume val test_function1: x:int -> squash (predicate x) -> int

// Subtyping check failed; expected type squash (predicate 42); got type unit;
[@@expect_failure]
let test: int = (_ by (
  let proof = uvar_env (top_env ()) (Some (`(squash (predicate 42)))) in
  unshelve proof;
  focus (fun () ->
    prove_predicate ()
  );
  exact (mk_e_app (`test_function1) [(`42); proof])
))

// Found by Lucas Franceschino
let test_workaround: int = (_ by (
  exact (mk_e_app (`test_function1) [(`42); (`(synth_by_tactic prove_predicate))])
))

The workaround is a bit weird because the tactic generates a term, which then executes another tactic.

[W95Psp]

After a bit of debugging, it appears that what is going on in the issue of @TWal is that the unification variable loses its refinement. When solving the goal with prove_predicate, at some point, the unification variable is retyped as unit, with it's refinement (predicate x) as an additional proof obligation.

Here are some examples showing a bit more this behavior:

open FStar.Tactics

// (Some utilities)
// Are two term equal?
let eq_term t1 t2 = compare_term t1 t2 = FStar.Order.Eq
// Asserts the string representation of a term matches a given string 
let assert_term_is (t: term) (s: string): Tac unit =
  let t = term_to_string t in
  if t = s then ()
  else fail ("[assert_eq_string]: expected [" ^ s ^ "], but got [" ^ t ^ " ]")
// Same thing for multiple terms
let assert_terms_are (t: list term) (s: list string): Tac unit
  = if List.Tot.length t = List.Tot.length s
    then iter (fun (t, s) -> assert_term_is t s) (zip t s)
    else fail "[assert_terms_are] mismatch lengths"
// Same thing for proof states
let assert_ps_is (s: list string): Tac unit
  = assert_terms_are (List.Tot.map goal_type (goals ())) s

// First, we solve a goal [x:'a{ref x}] using [exact] with a value that has the exact type [x:'a{ref x}]
// This work correctly, the unification variable [uv] carries the refinement after the goal being solved
let f1 (ref: 'a -> Type0) (wit: 'a {ref wit})
  = assert True by (
  let t = quote (x:'a {ref x}) in
  let uv = uvar_env (cur_env ()) (Some t) in
  let getType uv: Tac _ = tc (cur_env ()) uv in
  unshelve uv;
  guard (eq_term (getType uv) t);
  exact (quote wit);
  assert_ps_is ["Prims.squash Prims.l_True"];
  assert_term_is (getType uv) "wit: 'a{ref wit}"
)

// Here however, the proof that [wit] respects the refinement [ref] is given by [proof]
// We can observe that [uv] is retyped with type [a], while [ref wit] is added as a new goal
let f2 (ref: 'a -> Type0) (wit: 'a) (proof: ref wit)
  = assert True by (
  let t = quote (x:'a {ref x}) in
  let uv = uvar_env (cur_env ()) (Some t) in
  let getType uv: Tac _ = tc (cur_env ()) uv in
  unshelve uv;
  guard (eq_term (getType uv) t);
  assert_ps_is ["x: 'a{ref x}"; "Prims.squash Prims.l_True"];
  exact (quote wit);
  assert_ps_is ["Prims.squash (ref wit)"; "Prims.squash Prims.l_True"];
  assert_term_is (getType uv) "'a"
)

Thus, following this observation, the module from @TWal can be rewrote as:

assume val predicate: int -> Type0
// If we add the SMTPat, then `test` succeed
assume val predicate_is_true_lemma: x:int -> squash (predicate x) //[SMTPat (predicate x)]

val prove_predicate: unit -> Tac unit
let prove_predicate () =
  dump "goal";
  exact (quote (predicate_is_true_lemma 42));
  // apply_lemma (`predicate_is_true_lemma);
  dump "goal solved"

assume val test_function1: x:int -> squash (predicate x) -> int

// Subtyping check failed; expected type squash (predicate 42); got type unit;
let test: int = (_ by (
  let proof = uvar_env (top_env ()) (Some (`(squash (predicate 42)))) in
  unshelve proof;
  focus (fun () ->
    prove_predicate ()
  );
  exact (mk_e_app (`test_function1) [(`42); proof])
))

Though it's not very intuitive. But maybe just using something like tcut is better here, i.e.:

assume val predicate: int -> Type0
assume val predicate_is_true_lemma: x:int -> Lemma (predicate x)
assume val test_function1: x:int -> squash (predicate x) -> int
let test: int = (_ by (
  let proof = tcut (`(squash (predicate 42))) in
  flip (); apply_lemma (`predicate_is_true_lemma);
  exact (mk_e_app (`test_function1) [`42; binder_to_term proof])
))