I think your comment was unfairly downvoted without objective reasons. This is a real issue with advanced type systems and the current solutions are not very good (although they can be practical in some cases) - you can either automatically decorate constructors with assertion code (slow) or trust external input (unsafe, something like __builtin_unreachable in C).
And after you're done with that, good luck getting a deterministic and fast type checker which can verify proofs (which you have to write yourself) about arbitrary theorems in your program. Yes, I'm aware there exist languages that can do this to a degree but there is a good reason why they aren't used in mainstream software.
I genuinely wonder how one would write a proof in something like Agda, that
I wish this was the first such case. But, what I see happen way too often is this:
Some dude comes up with another data definition language (DDL) that uses ML-style types. Everyone jumps from their seats in standing ovation. And in the end we get another useless configuration language that cannot come anywhere close to the needs of application developers, and so they pedal away on their squared-wheel bicycles of hand-rolled very custom data validation procedures.
This is even more disheartening because we already have created tools that made some very good progress into systematic input validation. And they were with us since the down of programming (well, almost, we had SQL since early 70's, then we also had Prolog, then we had various XML schema languages, and finally TLA+). It's amazing how people keep ignoring solutions that achieved so much compared to ensuring that a list isn't empty... and yet present it as the way forward...
I genuinely wonder how one would write a proof in something like Agda, that
always succeeds