The annotation does need to be propagated backwards to callers and declarers - and there needs to be a way to "annotate" an existing pointer in the scopes where

The annotation does need to be propagated backwards to callers and declarers - and there needs to be a way to "annotate" an existing pointer in the scopes where you've proven that it's not null - but that's better than having no annotation at all. (Although this is something I'd 100% want C++ to do, and not with an annotation but with a very short operator or reserved word.)