Typing error raised by steel's tactics when using smt_fallback

[857b]

trafficstars

On a steel example similar to the one given for PR#2534, fstar still fails to rewrite a vprop with an smt_fallback and raises a typing error:

module Mem = Steel.Memory
open Steel.Effect
open Steel.Effect.Atomic

assume
val int_sl (n : int) : Mem.slprop u#1

type int_sel_t (n : int) : Type
  = m : int { m <= n }

assume
val int_sel (n : int)
  : selector (int_sel_t n) (int_sl n)

[@@__steel_reduce__]
let vint' ([@@@smt_fallback] n : int) : vprop' =
  {
    hp  = int_sl    n;
    t   = int_sel_t n;
    sel = int_sel   n
  }

unfold let vint ([@@@smt_fallback] n : int) : vprop =
  VUnit (vint' n)

let test0 (n:int)
  : SteelT unit (vint n) (fun _ -> vint (n+1-1))
  = change_equal_slprop (vint n) (vint (n+1-1)) // OK

let test1 (n:int)
  : SteelT unit (vint n) (fun _ -> vint (n+1-1))
  = noop () // Error

The error displayed is the following: (Error 228) user tactic failed: `tc: tcc: Cannot type m <= n in context ((n: Prims.int), (_: (*?u597*) _), (m: Prims.int), (x: Prims.unit)). Error = (Violation of locally nameless convention: m)` It seems to be linked to the dependency of the selector int_sel_t on the argument n of the vprop. There is no error if one replaces m <= n with m <= 0.