Yeah if you’re writing a standard library or a parser or maybe a database query optimizer, but if you aren’t writing code about code, then it’s probably not the way to go.
It also has a very nice quality of not mucking up your runtime performance with doing all the constraint checking on-demand and in very branchy ways.
As a simple example of how useful the approach can be, here's a thing we did awhile ago for making safe abstractions to low-level hardware resources: https://blog.auxon.io/2019/10/25/type-level-registers/ .
With that approach we could build a pipeline to consume hundreds of pages of SoC datasheet, generate the appropriate type specs from the register definitions, and end up with an API to the hardware that would fail to compile if a program was written to consume the hardware interface in a way that violated the spec in the datasheet.
In particular, this property of the described system makes it trivial for the unknowing or uncaring to subvert it: > It provides a string-management kernel that lets you create “safe strings” by certifying a regular string as representing either text or a fragment of a known language.
From what I understood, the certification is an unchecked assertion made by the program. One of the comments gives a great example of how this will go wrong in practice. The other aspect of this that is glossed over is that many data schemas represent all these things as "text". It is again an exercise for the program to get this right at the io boundaries.
i agree that it's not foolproof, but it's better than treating everything as an undifferentiated string.