> A simple compiler that sometimes requires a type annotation.
It is easy to show that that will not solve the problem. If your language is Turing-complete, then you can embed (say) a Lisp interpreter and arbitrary Lisp code within it. The only way your compiler can be complete and correct for your language is for it to be complete and correct for this embedded Lisp. This is a fundamental result. There is no way around it.
> Those are your only options. Reasonable people can disagree over which is preferable.
Ah ok. Being right seems to be more important to you than having a honest discussion.
Have fun, I'm out.