really-small-backpack-example VS cute-c2-hs

Isn’t this what Haskell’s backpack does? https://github.com/danidiaz/really-small-backpack-example

Also worth mention how module identity works in Backapck: two modules instantiated separately but with the same ingredients are "equal" and have compatible types.

Anyway, an alternative to RULES that I've explored is to put the proofs behind a module signature and compile to versions of the program, one with "real" proofs and another with unsafeCoerced ones. This avoids the danger of the RULEs silently ceasing to apply because of name changes (don't know how common is that danger in practice though).

Here's an example of how to use Backpack (instead of rewrite rules) to alternate between "normal" proofs and the ones which use usafeCoerce.

Perhaps Backpack could enable something similar to that?

While being nowhere near programmability, Cabal's common stanzas can be very useful to reduce duplication. An example.

The games are built on a custom "engine" made with SDL2 and some other C libraries I wrote bindings for: sdl-gpu, cute_c2, and cute_sound. I use apecs and cleff for the general architecture. And for animations, I use a combination of animate and ease.