[satvikpendem]

Soundness is not decidability. The reason TS is unsound is not directly because it's undecidable, as any Turing complete system is undecidable, and the TS type system is Turing complete.