UInt* structure codegen

Stream: lean4

[Mac]

Currently, wrapping a primitive type like UInt32 in a structure makes it boxed:

structure AddressSpace where
  index : UInt32

@[extern "foo"]
constant foo (addrSpace : AddressSpace) : IO PUnit
-- passes address space as an `lean_object*`

@[extern "bar"]
constant bar (addrSpace : UInt32) : IO PUnit
-- passes address space as an `uint32`

This poses a problem for examples like the above where, for type safety reasons, wrapping a primitive type in a singleton structure is desirable.

Would it be feasible for such wrappers to also be special-cased by the code generator?

[Sebastian Ullrich]

Oh... this is already the case, but, what I can only assume is an oversight, only in the case of parameterized structures

[Mac]

lol! Well then, should I submit an issue about it?

[Sebastian Ullrich]

https://github.com/leanprover/lean4/pull/556

[Mac]

I discovered another place where unbox-ness is not preserved. Though, this may be intended:

constant Address : Type := USize
-- Address is a `lean_object*` instead of a `usize`

Would it be feasible for such opaque definitions to also preserve unbox-ness?