A type such as U8#[5] is intended to be the unboxed array type, i.e., values are sequences of 5 bytes.
Normally such types are translated to C array types, such as u8[5U] and
values of the type are treated as sharable and discardible by the type checker.
However, if used as a function argument or result, such as in
f: U8#[5] -> U8#[5]
f x = x
Cogent translates f to a C function
static inline u8 *f(u8 [5U]);
where the result type is a pointer type and the argument type is adjusted by C to the pointer type u8*.
This does not correspond to the Cogent semantics of U8#[5], it could cause pointers to be shared or discarded.
Moreover, the C implementation of f allocates the result as local variable on the stack and then returns a pointer to it!
Of course this is a C problem because C does not allow arrays as function results and adjusts them to pointers if used as argument.
However, for Cogent this means to either forbid using unboxed array types as function argument and result types, or
translate them by wrapping them in a single-field struct, such as {u8 arr[5];}.
A type such as
U8#[5]is intended to be the unboxed array type, i.e., values are sequences of 5 bytes. Normally such types are translated to C array types, such asu8[5U]and values of the type are treated as sharable and discardible by the type checker. However, if used as a function argument or result, such as inCogent translates f to a C function
where the result type is a pointer type and the argument type is adjusted by C to the pointer type
u8*. This does not correspond to the Cogent semantics ofU8#[5], it could cause pointers to be shared or discarded. Moreover, the C implementation of f allocates the result as local variable on the stack and then returns a pointer to it! Of course this is a C problem because C does not allow arrays as function results and adjusts them to pointers if used as argument. However, for Cogent this means to either forbid using unboxed array types as function argument and result types, or translate them by wrapping them in a single-field struct, such as{u8 arr[5];}.