d(p) - Static dependency of a program p, measured as the number of tangled packages.
q(p) - Quality metric of a program p (there are almost no restriction about it. Can be number of defects, cost per feature, etc. Can be calculated analytically or measured empirically).
"Equivalent programs" - Two programs that produce the same output for the same input.
[A1] Given two equivalent programs, x and y, then if x's code provides more type information that y's the following holds: q(x) > q(y)
[A2] q(p) and d(p) are inversely correlated
 Given a statically typed program, p1, compute q(p1), d(p1).
 Obtain a program p2 that upholds the following conditions: p2 is equivalent to p1; p2 has no tangled packages; p2 has less type information that p1. The transformation rules described here ensure the existence of a program p2. However, any p2 that satisfies these conditions is suitable.
 p2 has less type information than p1 (see ). Based on [A1] we have that q(p1) > q(p2)
 p2 has no tangled packages (see ) so necessarily d(p1) >= d(p2). Based on [A2] we have that q(p1) <= q(p2)
The conclusions of  and  form a contradiction: q(p1) > q(p2), q(p1) <= q(p2). Therefore we have that one of our assumptions, either [A1] or [A2] is wrong.
I am tempted to put a Q.E.D here, but that is not the point. I do not think that either static type checking (that is: [A1]) or that static analysis ([A2]) is completely useless. However, this little proof shows that applying them indiscriminately is logically flawed. Universal statements such as "a tangle was formed hence quality eroded" are ill formed without additional reasoning and explanations.
Update 1: Changed the phrasing of  to explicitly express the requirements from p2.
Update 2: Removed an unnecessary step.