really-small-backpack-example VS cargo-crate-api

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.

As for detecting this, the cargo team has been maintaining documentation on crate semver compatibility (which is similar but not exactly the same as the stdlib) and we've been finding we want to switch to automating this instead. We are looking at adopting my proof of concept. I've been meaning to get it setup for a bigger request-for-contributors but haven't gotten to it yet.

cargo-crate-api

cargo-crate-api checks out a ref to an arbitrary directory. It chooses the latest tag if one wasn't specified