FStarLang/karamel

Unit elimination in function pointers passed to extern functions

nikswamy opened this issue · 0 comments

Consider this:

module FunPtr
open FStar.Ghost

inline_for_extraction
let f_type = x:erased bool -> bool -> bool
let f : f_type = fun _ b -> b

let g (f:f_type) = f (hide false) true
let test () = g f

assume
val extern_test (f:f_type) : bool
let test2 () = extern_test f

At the call to extern_test f, krml complains with a

Cannot re-check FunPtr.test2 as valid Low* and will not extract it.  If FunPtr.t
est2 is not meant to be extracted, consider marking it as Ghost, noextract, or u
sing a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in the arguments to FunPtr.extern_test, in top-level declaration FunP
tr.test2, in file FunPtr: Malformed input:
subtype mismatch, (() -> bool -> bool) -> bool (a.k.a. (() -> bool -> bool) -> bool) vs (bool -> bool) -> bool (a.k.a. (bool -> bool) -> bool)

Notice that it has not eliminated the unit argument in the function pointer argument in the signature of extern_test.
However, it has done this elimination in the signature of g.
Is there a reason for this? Is it possible to treat the the signature of extern_test in the same way as g?