Partial application for erased types, type parameters and implicits should be permitted when lowering to C

[shravanrn]

In general partial application is not permitted in Low* to C extraction. However, for certain parameters, this can be reasonably allowed - namely

• Parameters of erased types
• Statically specified type parameters
• Statically specified or automatically deduced Implicit parameters

Reason why above should be possible

• Parameters of an erased type such as (HS.rid) are used primarily to check for correctness and are erased into unit as part of the lowering. Thus partial application would effectively translate to a no-op once lowered to C
• Type parameters are monomorphized before lowering to C, so as long as the type parameters are specified statically, the appropriate monomorphizations can be generated and called during the lowering stage
• Implicit parameters - similar reason as parameters of erased types

Some of these cases are partially supported and may partially work with some of the listed workarounds below, but still run into issues. Here are examples for the first 2 cases that cause some issues

Example of erased type partial application failure

module ErasedTypeFailure

module I32 = FStar.Int32
module B = LowStar.Buffer
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack

type t_F (a:Type) = B.pointer a -> HST.St (unit)

let bar (#a:Type) (p:t_F a) : HST.St (unit) = ()

type t_D (r:HS.rid) = 
| D_Cons :
    rCopy : (v:HS.rid{ v = r}) ->
    len : (I32.t) ->
    t_D r

val foo (#r: HS.rid) : t_F (t_D r)
let foo #r p = ()

let main() : HST.St I32.t 
=
let r = HST.new_region HS.root in
let f = foo #(r) in
let x = bar f in
0l

This fails with the following error

Warning 16: : Cannot enforce arity at call-site for ErasedTypeFailure.foo (Invalid_argument split -- is this a partial application?)
Warning 16 is fatal, exiting.

Marking foo with unfold or inline_with_extraction lets it go further but it now fails with

Warning 11: in top-level declaration main: this expression is not Low*; the enclosing function cannot be translated into C*: fun (p(0, ): t_D*) :() { () }
Warning 11 is fatal, exiting.

Example of type parameters partial application failure

module TypeParameterFailure

module I32 = FStar.Int32
module B = LowStar.Buffer
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack

type t_F (a:Type) = B.pointer a -> HST.St (unit)

let bar (#a:Type) (p:t_F a) : HST.St (unit) = ()

type t_D (r:HS.rid) = 
| D_Cons :
    rCopy : (v:HS.rid{ v = r}) ->
    len : (I32.t) ->
    t_D r

val foo (a:Type) : t_F (a)
let foo a p = ()

let main() : HST.St I32.t 
=
let r = HST.new_region HS.root in
let f = foo (t_D r) in
let x = bar f in
0l

This creates the following error

Warning 4: in top-level declaration TypeParameterFailure.foo__TypeParameterFailure_t_D, in file TypeParameterFailure: Malformed input:
subtype mismatch, () (a.k.a. ()) vs TypeParameterFailure_t_D* -> () (a.k.a. TypeParameterFailure_t_D* -> ())

Workaround - However, the workaround of marking t_F as inline_for_extraction allows this example to work, but there are likely other examples, where this would not suffice.

[msprotz]

Both of these examples can be fixed by marking t_F (and not foo itself) as inline_for_extraction.

inline_for_extraction
type t_F (a:Type) = B.pointer a -> HST.St unit

However, I would still consider this is a usability issue, at the very least. The fundamental reason for this is, in Low*, int -> int -> int is not the same thing as int -> (int -> int). A C function with two arguments is not the same as a C function with a single argument returning a function pointer.

However, we have no way through the syntax of types to figure out which one of these two a user intended to express. This means that the user will have a very hard time even writing higher-order function types since there's not even syntax for it. So, by default, int -> int -> int is always the type of a function with two arguments.

What KreMLin does to recover from this limitation is look at the number of arguments on a function definition. At definition-time, we can do second-order, and "chop" the function type according to the number of arguments. So if you do:

val f: int -> int -> int
let f x = g

KreMLin will know that f is a function that only takes a single argument and will re-parenthesize every call-site accordingly. But if you do:

val f: (int -> (int -> int)) -> unit
let f _ = ()

the first argument of f will still be a function that takes two arguments (no third-order).

Now about this specific bug report. What happens is, when matching a function definition against its type, and trying to "chop up" the function type to match the number of arguments, due to the type abbreviation, there are now less arrows than the number of arguments, which gets the extraction confused.

This is an F* warning and looks as follows:

Not extracting HigherOrder6.foo to KreMLin (function type annotation has less arrows than the number of arguments; please mark the return type abbreviation as inline_for_extraction)

confusingly, the function is (right now) extracted nonetheless because making this a hard fail caused a regression in other parts of Everest.

My goal is to at least make this a fatal warning, so that KreMLin doesn't receive invalid information. Then, F* should be able to do the inlining automatically so that the user doesn't have to write inline_for_extraction on the type definition.

Hope this helps,

Jonathan

[shravanrn]

Thank you for the detailed explanation. I will try the suggested workaround for example 1

• Warning 16 not fatal
• inline only on t_F

and report if anything else comes up