I'm uncomfortable with programs that rely on complicated compile-time evaluation within the type system. For complicated runtime behavior, we have various tools for stepping through the evaluations as they unfold. E.g., debuggers, print statements, etc. But I haven't come across anything similar for these type-based evaluations. Usually the best I get is a compiler warning or error, or even worse, an unexpected succe…
I think that behind this sentiment is an assumption that software development is mostly applications and CRUD services.
If the target system is a space rocket, medical systems, etc. One really want to have guarantees.