The annotations have fairly well defined semantics, the behavior of typecheckers in the absence of annotations, where types are ambiguous (a common case being when the type is a generic collection type but the defining position is assignment to an empty collection so that the correct specialization of the generic type is ambiguous) is less defined.

What should a type checker say about this code?

  x = []
  x.append(1)
  x[0] = "new"
  x[0] + "oops"

They don't. They're just documentation.