Extraction to KReMLin: preorder arguments not erased

[tahina-pro]

Consider the following example:

module Te

module B = LowStar.Monotonic.Buffer
module U32 = FStar.UInt32
module HST = FStar.HyperStack.ST

inline_for_extraction
type t =
  (#rrel : B.srel U32.t) ->
  (#rel: B.srel U32.t) ->
  (b: B.mbuffer U32.t rrel rel) ->
  HST.ST unit (fun _ -> True) (fun _ _ _ -> True)

let f : t = fun #rrel #rel b -> ()

let h : t = f

When trying to extract with fstar.exe --extract_module Te --codegen Kremlin Te.fst, I get the following error message:

Te.fst(16,12-16,13): (Error 216) Variable Te.f has a polymorphic type (forall 'Arrel, 'Arel. (FStar_UInt32.t, 'Arrel, 'Arel) LowStar_Monotonic_Buffer.mbuffer  ->  unit); expected it to be fully instantiated, but got Te.f
1 error was reported (see above)

If I remove the definition of h, then extraction goes through, but actually, f is not extracted at all, presumably because F* thinks that f is polymorphic.

I was expecting F* to actually erase the #rrel #rel arguments of f instead of considering them as a source of polymorphism.

[nikswamy]

Trying to fix this. A minimal repro fstar --codegen OCaml Bug1694.fst

module Bug1694
type t = #a:Type -> a -> Tot a
let f : t = fun #a x -> x
let h : t = f

[nikswamy]

FYI, this is high on my priority list since we are working around it by explicitly erasing preorder arguments in LowParse, which is making other code in miTLS clumsy to work with.