In static typing context, "types" is a lexical construct of subexpressions. In this context, dynamically typed languages are "untyped" or "unityped" (one type for all expressions).
In dynamic typing context, "types" are the runtime tags of data with rules about dispatch and what kinds of tags are allowed with what operations.
I think for the benefit of communication, we should refer to the static, compile-time annotation on sub-expressions as "types", and the entity dynamic languages calls "types" as "tags".
> More complex analysis requires more and more annotations to specify the contracts of the methods. An example is a C function which takes a char* and an int. You want to annotate that the int indicates the length of the char* buffer, and have a static analyzer enforce that
This is of course certainly compatible with types. Something like:
func : (n : Int) -> Ptr (Array n Char) -> ...
Static types and static analysis are basically variants on the same idea. However, static types is part of the ordinary workflow, and static analysis is often treated as an "after-the-fact" feature. This will not work as well, since much of the power of types relates to techniques to structure our programs so that types cover as much as possible.