[ proposal ] fixed size C arrays a-la Struct

[ear7h]

Description

We have a blessed Struct type for passing around c structs using FFI, but I could not hack fixed size arrays. Idris seems to be okay with basic newtypes, but it complains for dependent types like:

data CArray : Nat -> Type -> Type where

I think what's happening is that the index types (the thing left of : right?) are being subject to the FFI restrictions of being basic types. I think a more radical fix here would be to drop the restrictions on types and only enforce them on constructors.

---

Some notes:

• the blessed type is called CArray in idris code to avoid clashing with the common Array type
• I'm using the 99 tag as placeholder

Self-check

• This is my first time contributing, I've carefully read CONTRIBUTING.md
  and I've updated CONTRIBUTORS with my name.
• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG_NEXT.md
• I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

[ear7h]

This is actually a fix to an existing compilation bug, I should break it into a different PR.

cftySpec outputs the scheme form of the type within a struct, and cftySpecArg outputs the scheme form of the type within function arguments.

Relevant documentation:

(* ftype-name): This type allows a pointer to a foreign type (ftype) to be passed. The argument must be an ftype pointer of the type identified by ftype-name, and the actual argument is the address encapsulated in the ftype pointer.
...
(& ftype-name): This type allows a foreign type (ftype) to be passed as a value, but represented on the Scheme side as a pointer to the foreign-type data. That is, a (& ftype-name) argument is represented on the Scheme side the same as a (* ftype-name) argument, but a (& ftype-name) argument is passed to the foreign procedure as the content at the foreign pointer's address instead of as the address.

https://cisco.github.io/ChezScheme/csug/foreign.html