Trouble with SMT fallback and tactic left uninstantiated variable

[nikswamy]

Here's an example that works

module IncrPair
open Steel.Memory
open Steel.Effect
open Steel.Reference
open Steel.FractionalPermission
open Steel.Effect.Atomic
open FStar.Ghost
assume
val pts_to (#a:Type u#0)
           (r:ref a)
           ([@@@ smt_fallback] v:a)
  : slprop u#1

assume
val read (#a:Type) (#v:Ghost.erased a) (r:ref a)
  : Steel a (pts_to r v) (fun x -> pts_to r x)
            (requires fun _ -> True)
            (ensures fun _ x _ -> x == Ghost.reveal v)

assume
val write (#a:Type0) (#v:Ghost.erased a) (r:ref a) (x:a)
  : SteelT unit (pts_to r v)
                (fun _ -> pts_to r x)

let incr (#v:Ghost.erased int) (r:ref int) ()
  : SteelT unit (pts_to r v)
                (fun _ -> pts_to r (v + 1))
  = let x = read r in
    write #_ #(hide x) r (x + 1);
    change_slprop (pts_to r (x + 1)) (pts_to r (v + 1)) (fun _ -> ())

But, this one fails, with a tactic trying to solve a non-trivial (but provable goal) with true_p

let incr (#v:Ghost.erased int) (r:ref int) ()
  : SteelT unit (pts_to r v)
                (fun _ -> pts_to r (v + 1))
  = let x = read r in
      write r (x + 1)

And this one fails too, with a tactic left uninstantiated variable message

let incr (#v:Ghost.erased int) (r:ref int) ()
  : SteelT unit (pts_to r v)
                (fun _ -> pts_to r (v + 1))
  = let x = read r in
    write #_ #_ r (x + 1);
    change_slprop (pts_to r (x + 1)) (pts_to r (v + 1)) (fun _ -> ())

[R1kM]

The first one is due to a limitation where there is no smt fallback in can_be_split_post.
I'm currently not sure how we could add it, encoding an abstract smt fallback prop that would depend on both the intermediate and final value is a bit hairy.

A workaround to avoid running smt fallback in can_be_split_post is to let-bind the return value (or in this case, add a trailing unit). This currently lead ot the same uninstantiated uvar as above, debugging further.

[R1kM]

The second one is a bit more complex. The problem occurs when the smt fallback path operates on a term containing unresolved implicit(s).
In your example, unification is attempted between the postcondition of read, pts_to r x, and the precondition of write, pts_to r (reveal (?u206 x)), where ?u206 corresponds to the v:Ghost.erased a argument of write.
Because head symbols do not match, standard unification fails, and we fall back on SMT. But since the SMT equality generation does not solve any uvar, ?u206 remains and causes problems.

One solution would be to prevent SMT fallback when uvars are present, and force annotations then, but it might be a bit frustrating. What do you think?