That's certainly not true in general (at least, if you want your compiler to provably halt) and it's really easy to point at counterexamples... for instance, Coq is capable of fully representing Peano arithmetic, and is dependently typed, so it follows that synthesizing its proof terms can require supplying proofs of arbitrary statements in PA, which is undecidable. But typechecking Coq proof terms is very much decidable, or at least if it isn't it's not because it includes PA.

That being said, even if your standard for synthesis is "works in practice" rather than some halting-related criterion, it's still really easy to find type systems that don't qualify. There are also sometimes practical concerns around separate compilation--if you're relying on introspection and not just interfaces for typechecking, and someone just tells you what interface will be satisfied at runtime, you won't be able to repeat this kind of analysis; the same sorts of problems occur when you perform reflection.

I don’t follow that argument. I know that checking a proof almost always is a lot simpler than creating it (and certainly never harder), but when a programmer annotates a function, they don’t provide a proof that the property holds, they just make an assertion that the it holds, and the compiler has to check it.

If the compiler can do such a check, and the number of possible annotations is finite, it can check each of them, thus computing the set of annotations that the function adheres to.

Well, the problem is that the number of annotations is not finite, and often there are many valid signatures that would work for a function. Determining which ones make the whole program typecheck is not a decidable problem for most type systems, and even for those for which it is, this often requires sufficient amounts of global knowledge to make the problem totally intractable in practice.

This is a problem you run into very quickly--for example, Hindley-Milner is only decidable because it will only infer "forall a" in prenex form (so its "most general" annotation is only most-general in that context). Type inference if you allow non-prenex quantification--even very mild non-prenex quantification--is undecidable, despite these being just as easy to typecheck as the prenex versions!

Now, in practice programs are made up finite numbers of terms, so for some of these type systems you could certainly come up with some sort of semidecision procedure by iterating through every possible sequence of type annotations. But as this kind of brute force algorithm will not terminate if it can't find the right set of annotations, and in practice will not terminate within human lifespans even in most cases where the right set of annotations exist, I don't think people would be very happy with such a system.

This is especially true if the only reason to find the annotations was to perform program optimizations, and not to enforce correctness. People are already wholly unwilling to give compilers unlimited amounts of time to do interprocedural analysis, which is mostly done in LLVM and such by just inlining everything. If having effect annotations were actually critical for being able to apply the optimizations from the paper (which, like I said earlier, I don't know that they are), this would pretty much be another instance of a global program rewrite too expensive for an optimizing compiler to perform in practice.

BTW, since I just realized I was insufficiently clear about the Coq example, I should clarify--in a dependently typed language, synthesizing the right type can actually require synthesizing a well-typed term (this is where the dependency comes in, after all), so it's not generally easier to synthesize types than terms in such a language. You need a sufficiently complex dependently-typed program for this to start separating itself from "ordinary" difficulties with type inference in practice, but when you start playing around with indexed vectors you run into situations like this a lot--cases where you struggle to even be able to write down the thing you're trying to prove, because the type is only well-formed in a particular context and you need to essentially prove to the compiler that you are in such a context for type inference to remain decidable.

For example, to write down (not prove!) an equality between two vectors indexed by their length, at least in Coq (and other type theories without extensional equality, which is in general undecidable), you have to first show that they have the same length--otherwise the expressions are not well-typed. The length can be any well-typed term of type nat, and like I said before Coq is far more than powerful enough to express Peano arithmetic, so you can see already that synthesizing an equality type between two vectors is just as difficult as proving an equality between two natural numbers, so it is very much undecidable in general. In fact, it is quite difficult to write down in practice even in some surprisingly simple cases! The actual proof term, however, is usually something like a pattern match on some other equality followed by the creation of a function that pattern matches on another equality, etc. down the line, until it returns the unhelpful constructor `eq_refl` (which basically just says `x = x`). So all of the interesting work in such cases has transferred to the type system, with the proof term basically just there to perform type casts and coercions.