Mismatch in the post slprop type in the case of weakening

[aseemr]

This code fails with an SMT failure:

module Test

open Steel.Memory
open Steel.Effect

assume val elim_pure (p:prop)
  : SteelT (_:unit{p}) (pure p) (λ _ → emp)

assume val my_prop1 : prop
assume val my_prop2 : prop

let sl1 : slprop u#1 = pure my_prop1
let sl2 : slprop u#1 = pure my_prop2

assume val change_slprop (_:unit) : SteelT unit sl1 (λ _ → sl2)

let test ()
  : Steel unit
      sl1
      (λ _ → emp)
      (λ _ → ⊤)
      (λ _ _ _ → my_prop2)
  = change_slprop ();
    elim_pure my_prop2

@R1kM and I debugged it together and suspect that it happens because for the elim_pure my_prop2 expression, we compute its type to be _:unit{myprop2}, introduce a post slprop uvar at type _:unit{myprop2} -> slprop, weaken its type to unit, introduce another slprop uvar at type unit -> slprop, and then these two uvars are then equated from the tactic with use_eq flag. This sends a query to the solver to prove myprop2 without any assumption in the context, and that query fails.

It is quite rough and needs more investigation but just recording here. If we move the refinement from the type of elim_pure to ensures, then this works fine.

[R1kM]

Another observation was that if we manually add a trailing (), in theory mimicking the insertion of a return by the typechecker for the weakening, this also works fine.