Comment by captaincrowbar

This feels like a restatement of the trivially obvious observation that, if your type system is Turing complete, you're going to run into the halting problem.