Out of curiosity — has there ever been a type system that was discovered to be Turing-complete and then actually have caused a bug for a real application that was caused by the fact that it allowed an invalid program through?
I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.
I suspect the opposite situation is what you run into: it is possible to write programs that are valid and out to be accepted by the type system, but get rejected because you blew the stack of the type checker. Had the type checker been allocated more memory / time, it could have accepted the program, but it crashed before that.
You can craft font files that perform arbitrary calculations… if you give the font shaping engine a (practically) unlimited stack, where it usually limits recursion to 6 levels. If you do so, you can make a font that does math (or whatever you want) as part of computing ligatures.
But in practice, you hardly ever hit those kinds of limits unless you're trying to do something silly on purpose. Sure you cannot port Doom to font substitution lookup tables, despite them being Turing complete. But that doesn't make your font shaping engine useless, or even broken.
I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.