This reminds me strongly of Absal[0]. Could somebody familiar with both give a comparison?

This looks like a really cool idea, and I'd love to see a GHC backend for it.

It might also be nice to have a brief explanation if an interaction between without just linking to a big theory paper.

[0] https://github.com/VictorTaelin/abstract-algorithm

eta: I only now notice that Victor Taelin is the author of both packages.