really-small-backpack-example VS agda2hs

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.

My concrete long term strategy is to learn Agda well enough that I can write all logic exclusively in Agda and then extract Haskell through agda2hs.

Have you seen agda2hs?

The tool itself can be found here: https://github.com/agda/agda2hs