Ghost.erased not working as expected?

[jaybosamiya]

Consider the following Test.fst:

module Test

module G = FStar.Ghost
module I32 = FStar.Int32

noeq
type foo = {
  x: I32.t;
  y: G.erased int;
}

Running krml Test.fst produces this in Test.h:

typedef struct Test_foo_s
{
  int32_t x;
  void *y;
}
Test_foo;

Expected output:

typedef struct Test_foo_s
{
  int32_t x;
}
Test_foo;

---

Alternative example (with functions and pairs) instead:

Consider Test2.fst:

let bar (x:I32.t) : (y:(I32.t * G.erased int)) =
  x, G.hide (I32.v x)

Produced output in Test2.c:

K___int32_t___ Test2_bar(int32_t x)
{
  return ((K___int32_t___){ .fst = x, .snd = (void *)(uint8_t)0U });
}

Expected output:

int32_t Test2_bar(int32_t x)
{
  return x;
}

---

I'm not sure if the above is expected behavior. I would expect erased stuff to be completely removed, and not even leave in a void* being assigned to NULL.

[jaybosamiya]

Awesome! Thanks @msprotz :smile: