As I mentioned with my caveat, I'm an amateur type theorist, so I'm still digging into a lot of things. Do you have some relevant literature for me about this being impossible?
My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.
That certainly tells us that there is no single type system that can describe every correct program, which seems to be the stronger version of Steve's thesis that he was supporting in the immediate parent.
A weaker version of his thesis, which could still support his original phrasing in the GGP, would be "for any correct program, there exists a type system in which it can be typed [though we might not be able to find it]." That doesn't seem to be ruled out, and sounds plausible, though I don't know of any specific results on it.
My claim may have been too strong: I meant more that "it hasn't been disproven that type systems are inherently disjoint." Similar to how physicists believe there's a Grand Unified Theory of physics, but that doesn't mean we actually know it yet.