StackInline not inlined at extraction

[sonmarcho]

If I hide a StackInline function's implementation behind an interface and don't declare it inline_for_extraction, Kremlin generates code where the function is not inlined, while I would have expected it to fail (and I couldn't see any related warning).

Module 1:

(*** .fsti *)
module ExtractStackInline2

open FStar.HyperStack
open FStar.HyperStack.ST
open LowStar.Buffer

#set-options "--z3rlimit 25 --ifuel 0 --fuel 0"

val alloca_buf : unit -> StackInline (buffer bool)
  (requires (fun _ -> True))
  (ensures (fun h0 b h1 ->
    modifies loc_none h0 h1 /\
    fresh_loc (loc_buffer b) h0 h1 /\
    loc_includes (loc_region_only true (get_tip h1)) (loc_buffer b)))

(*** .fst *)
module ExtractStackInline2

open FStar.HyperStack
open FStar.HyperStack.ST
open LowStar.Buffer

#set-options "--z3rlimit 25 --ifuel 0 --fuel 0"

let alloca_buf () =
  alloca true 10ul

Module 2:

module ExtractStackInline

open FStar.HyperStack
open FStar.HyperStack.ST
open LowStar.Buffer

#set-options "--z3rlimit 25 --ifuel 0 --fuel 0"

open ExtractStackInline2

let f () : Stack unit (fun _ -> True) (fun _ _ _ -> True) =
  push_frame ();
  let b = alloca_buf () in
  pop_frame ();
  ()

Generated code:

void ExtractStackInline_f()
{
  bool *b = ExtractStackInline2_alloca_buf();
}