FStar fails to autocast a function with return type refinement to pure func with the same or weaker post-condition

[hacklex]

As @aseemr asked, I'm creating this issue with the following minimal example code:

assume val f : unit -> Pure int (requires True) (ensures fun x -> x >= 0)
assume val g (f:unit -> nat) : unit
let test () : unit = g f

The final line is not accepted by F*; last tested on version 2021.09.25.