Static typing means that the types cannot change. Dynamic languages can still declare types. It's just that they are allowed to morph. A good analyzer can track those changes and know when types are equivalent (TypeScript does this).
Furthermore, typing is one mechanism to express contracts within your code- such as 'this method takes argument X which is of the form Y and will return something which looks like Z'.
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.
I am all about code contracts and enforcement of those contracts. But this is not necessarily tied to a static language.
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) -> ...
This is the type of the contract you specified.
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.