Why does a Turing-complete type system make type checking undecidable?

All type systems have false positives by their nature. The trick is...humans have to be able to reason about their type errors so they can fix them. If the type system is too expressive, reasoning about type errors can be incredibly difficult.

When I worked for coverity, a lot of time and resources were spent on consulting to help customers understand the errors they were getting, and to identify and lower false positives. Usability is key, or no one can/will use your stuff.

You can bound your loops and say you don't know. I thought that's what the parent meant by "don't know."

if loopcount > limit then Left Dunno else Right ...

Except you can bound it, and you can escape it that way. IE "not gotten anywhere after 30 iterations, so don't know".

Otherwise, you couldn't, for example, ever compute the tripcount for a loop without risking running forever.

" Compilers happily cheat on optimizations, register layout, etc."

They don't cheat. They just make the problem easier at a cost of optimality. Or, they discover they didn't need to solve the problem they thought they did.

A great example is register allocation. NP-complete to do graph coloring.

NP-complete to decide if a given graph admits a k-coloring for a given k except for the cases k ∈ {0,1,2}.

NP-hard to compute the chromatic number (ie just figuring out the minimum number of colors for a graph)

This was the state, right up until a number of people proved that, if you do it on SSA form (a linear time transformation), you can optimally color it in linear time. A small difference.

So, often, these upper bounds that seem "futile", maybe are not as futile as one thinks.

All type checkers for sophisticated dependent type theories (e.g. MLTT) will resist any bound on time or memory you try to place, let alone a quadratic or exponential one. Somehow nobody seems to complain about how long they take to type-check. Both decidability and worst case time bounds are red herrings when it comes to a good type system (even for proof assistants).

That's the difference between theory and real world. In theory something may not be perfect, but it's still good enough for practical use.

For instance, planetary motion is not really well described without solving N-body problems and taking relativity into account, and yet Newtonian dynamics and slide rules were enough to land us on the Moon.

Well there's two problems there: you can easily "reduce" a P problem to an NP-complete one; it's when you do it the other way around (reduce graph coloring to an instance of problem X) that you even have anything to worry about. But yes, worst time bounds for many problems are devilishly hard to achieve even when you're trying.

You have it the opposite way, if you can reduce an instance of an NP-complete problem to your problem, then your problem is NP-complete. Is that what you meant by a fallacy?

In fact literally the same problem! Seeing the connection explained[1] was probably the most enlightening thing I've ever seen for both results.

[1]: http://www.scottaaronson.com/blog/?p=710