@neauoire Now combine this with egraphs (https://egraphs-good.github.io/) for the ultimate metalanguage.

I've had a half-formed idea for an egraphs-and-datalog dependent type system brewing for years now.