Compiler enforced static typing rejects many correct programs, which is a disadvantage.
Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway.
On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".
Is that true? Is there a difference between the things which can be proven true in the sense used in mathematics and the set of things which are computable? The limits of proof (e.g., Goedel's incompleteness theorems) and computability (e.g., the halting problem) are at least deeply related, and I'm not at all convinced that your premise here is true.
In practice, however, it is only a theoretical disadvantage. The kind of "correct" programs that get rejected are not very useful.
Do you have any examples of programs that would be actually useful? I don't necessarily doubt that they exist, but it's not an interesting point if the argument is basically "they exist, but I don't know of anyone in particular".
In the first category, one example is programs requiring higher-rank polymorphism. They are always allowed in untyped languages but in Haskell this feature is hidden behind a language pragma to keep type inference simpler by default.
On the second category, an example I like is parametric polymorphism vs subtyping. The type system gets really tricky if you try to use both at the same time so most static languages either limit the polymorphism or don't allow subtyping. ON the other hand, in a dynamic language you can use both styles if you want, although you have to do so at your own risk.
