Add `WithData` to generalise over `WithName` and `WithFC`

[andrevidela]

Description

This is the first step towards #3570 it adds three modules:

• Libraries.Data.Record a generic labelled record with runtime nat-indexing for performance
• Libraries.Data.WithData A datastructure to attach metadata to a type by means of a record
• Core.WithData A series of helpers for existing known metadata that the compiler already uses

This design addresses the goals set out by #3570 by allowing us to refactor a number of existing records into either Record or WithData. This refactoring, in turn, allows us to make changes to the metadata without changing the fundamental structure of the surrounding program, since most tree operations are metadata agnostic.

Once we add the Reify and Reflect instances for those types, they will also remove the need to write bespoke versions for types that use them in their definitions.

Finally, it allows some data that is currently spread out to be appropriately related, removing the uncertainty about what a piece of data does, and self-documenting the code.

[gallais]

refactor a number of existing records into either Record or WithData.

Built-in records have constant time access to their fields but for Record it's linear in the index. Isn't that problematic?

[andrevidela]

yes this is worse, i'll benchmark my huge PR that refactors the trees using this and come back with a concrete number to measure the difference.

I didn't notice anything in particular while working on it so my hope is that because most the records are 1 or 2 elements long the overhead is negligible.

Do you know of a way to replace the heterogenous list by an IOArray? This should get us back O(1) indexing

[andrevidela]

Here are the benchmark results

Methodology

• bootstrap the compiler, the output binary has been compiled with the bootstrap compiler
• compile the compiler with the bootstrapped compiler, the new compiler binary is now compiled with itself
• install the libraries for this version of the compiler because of some TTC differences
• measure how long this compiler takes to typecheck idris2.ipkg on main
• repeat 5 times

essentially:

make clean
make bootstrap
make all
make install-libs
time ./build/exec/idris2 --typecheck idris2.ipkg

For benchmarking the branch with the refactored tree, I made sure to move back to main so that the program compiled is the same for both runs. I also double checked that the compiler version used was indeed the one being tested

Compiling the compiler currently:

Idris 2, version 0.7.0-562ef55a3
./build/exec/idris2 --typecheck idris2.ipkg  102.30s user 2.64s system 97% cpu 1:47.12 total
./build/exec/idris2 --typecheck idris2.ipkg  102.79s user 2.21s system 99% cpu 1:45.94 total
./build/exec/idris2 --typecheck idris2.ipkg  103.64s user 2.21s system 99% cpu 1:46.75 total
./build/exec/idris2 --typecheck idris2.ipkg  108.79s user 2.42s system 98% cpu 1:52.49 total
./build/exec/idris2 --typecheck idris2.ipkg  109.23s user 2.92s system 96% cpu 1:56.33 total

average: 105.35, median: 103.64

Compiling the compiler with some of the tree refactored to use WIthData

Idris 2, version 0.7.0-3e48e3e44
./build/exec/idris2 --typecheck idris2.ipkg  99.51s user 1.86s system 99% cpu 1:42.12 total
./build/exec/idris2 --typecheck idris2.ipkg  101.64s user 1.94s system 99% cpu 1:44.16 total
./build/exec/idris2 --typecheck idris2.ipkg  103.58s user 2.16s system 99% cpu 1:46.61 total
./build/exec/idris2 --typecheck idris2.ipkg  104.92s user 2.33s system 99% cpu 1:48.24 total
./build/exec/idris2 --typecheck idris2.ipkg  105.79s user 2.37s system 99% cpu 1:49.22 total

average: 103.09 median: 103.58

In conclusion, while the access time of the records and WithData is O(n) it does not seem to impact performance outside of run-to-run differences

(All tests run on MacOS 15.5 (24F74) with an M4 cpu and 16GB of ram)

[andrevidela]

If nobody else objects in the meantime, I'll merge it in 2 days