Unit buffer elimination breaks type unification when combined with buffer built-ins
landonf opened this issue · 0 comments
landonf commented
Given the following test case:
module Example
module B = LowStar.Buffer
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
noeq
type foo = {
ptr:B.pointer_or_null unit
}
let test (): ST.St (option foo) =
let b = B.malloc HS.root () (1ul) in
if B.is_null b then None else Some ({ ptr = b })
Kremlin rewrites b
to EUnit
in DataTypes.remove_unit_buffers
, but this produces a subtype mismatch with LowStar.Monotonic.Buffer.is_null
(which itself is typed TArrow (TBuf (TAny, false), TBool
):
> fstar --odir . --codegen Kremlin Example.fst && krml -skip-compilation -warn-error @4 out.krml
✔ [Monomorphization] ⏱️ 11ms
Cannot re-check Example.test as valid Low* and will not extract it. If Example.test is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.
Warning 4: in the arguments to LowStar.Monotonic.Buffer.is_null, after the definition of b, in top-level declaration Example.test, in file Example: Malformed input:
subtype mismatch, () (a.k.a. ()) vs any* (a.k.a. any*)
Warning 4 is fatal, exiting.
I'm required to state: Not a Contribution.