Unit buffer elimination breaks type unification when combined with buffer built-ins

[landonf]

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.