Blog post: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies

@RalfJ this seems like a problem one can just throw machine resources and tooling at to keep going for quite a while. For example, we got nearly 30x proving speedup over many commits in a large project by doing both selection + fine-grained parallelization, and with Dune and other tricks things could go even faster. So is there really a “hard” limit to the unbundled approach?