really-small-backpack-example VS nodedemo

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.

for particular types a, c, b, and d. The issue that I'm essentially running into is that I'm not sure how I can get my hands on the copies/instances of the 'Node' type used by the library that implements 'bimapNode'. A more detailed/precise description of the problem, a minimum "working" example, and my attempts so far are at https://github.com/noinia/nodedemo .Does ideas on how to proceed with this kind of thing?