Unit elimination in function pointers passed to extern functions
nikswamy opened this issue · 0 comments
nikswamy commented
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
?