I think the potential issues you've raised (and that @John_McCall emphasised) are valid concerns. They're just not conclusive - it's not self-evident that sufficiently "global" analysis can't be done performantly (nor that it can, of course).
Re. developer understanding, I agree with the implicit premise - that code needs to be readable, meaning self-explanatory - but I'm just not sure if that'd prove to be a problem in this case. At least in simple examples, e.g.:
var callCount = 0
@MainActor
func doThings() {
…
callCount += 1
}
…it's quite apparent to a reader what the intention is, and if the reader knows the compiler will catch if callCount is used elsewhere in an unsafe way, then they're satisfied; they don't need to actually see @MainActor on callCount.
This is actually similar to how @MainActor propagates implicitly already, e.g. if you declare a protocol member method as @MainActor you don't need to explicitly declare that on any actual implementations of that method (nor do you need to explicitly mark them as async, even though they are!). Though relevantly this does seem to be an occasional source of confusion, e.g. Method marked with globalActor modifying property in class.
In more complicated examples (where the behaviour might not be as obvious), or in any case at the author's discretion, they can always choose to add explicit annotations. Again, type inference is the exemplar here - one can argue that implicitly-typed variables are confusing (or make compilation too slow), but one doesn't have to use them, which lets type inference exist for those that people don't find it confusing (nor too slow).
But in any case, I think what matters more is the question of whether developers want to care. They just want code that works. They want the compiler to get in their way only if the compiler can point out a genuine reason their code doesn't work [reliably]. And of course they want the compiler to be very good at determining if their code does or does not work. And the less they have to do to help it, the better.
That's the principle, of course. That's all I was alluding to in my post. Pragmatically the compiler might need some help, whether for compilation performance or implementation difficulty or whatever. I was just expressing a preference; I'd just like to see a little more elaboration on why the author has to do more to help the compiler, if that turns out to be the case.