CheckNoUVars Failure in Steel

[R1kM]

The following code snippet

val test (#a:Type0) (p:t a)
  : SteelSel (t a * t a) (llist p) (fun res -> llist (snd res))
                (requires fun _ -> True)
                (ensures fun _ _ _ -> True)

let test #a p =
  noop ();
  (p, p)

fails in Steel with the error below

(Error) ASSERTION FAILURE: (<dummy>(0,0-0,0)) CheckNoUvars: Unexpected unification variable remains: (*?u2895*) _

The core of the issue is likely that pairs and their projectors are normalized in Steel. Replacing the pair result by a similar datatype, but without the normalization, does not raise an error.

The small repro is available on the _afromher_debug branch: https://github.com/FStarLang/FStar/blob/_afromher_debug/examples/steel/Selectors.Debug.fst

[nikswamy]

Here's another repro without selectors

assume
val p : int -> slprop u#1

assume
val f0 : unit -> SteelT (int * int) emp (fun v -> p (fst v) `star` p (snd v))

assume
val f1 : x:int -> y:int -> SteelT unit (p x `star` p y) (fun _ -> emp)

assume
val f2 : x:int -> SteelT unit (p x) (fun _ -> emp)

let test () 
  : SteelT unit emp (fun _ -> emp)
  = let x = f0 () in
    f1 (fst x) (snd x)

let test2 () 
  : SteelT unit emp (fun _ -> emp)
  = let x = f0 () in
    f2 (fst x);
    f2 (snd x)

[R1kM]

This has been tracked by @nikswamy to an issue in the interactive mode, these files verify from the command line.

We need to debug further and fix the issue. In the meantime, when facing this problem in Steel, adding the option --ide_id_info_off is sufficient.

[R1kM]

Part of the issue seems to be related to an aggressive normalization of fst/snd in the Steel tactic. Using a custom fst/snd inside the tactic so that all fst/snd are not normalized might also help with this issue