Specifically, one interesting case is when we are working with a language that already performs runtime type checks. Not just runtime checks, but runtime type checks. As an instance, Python raises TypeError when the type of things do not match.
For those languages, a natural question then is that can we reuse these already-present checks for gradual typing? This idea is called Safe Erasure Gradual Typing: although the elaboration is merely erasing type annotations, a well-typed term still either 1) diverges, 2) reduces to a so-typed value, or 3) triggers an error at a runtime check already present in the dynamic language.
But what does safe erasure mean, after all? From the intuition, we can understand safe erasure as: the guarantees provided by the types are still sound because of existing runtime checks.
For a function, the inferred function parameters must be over-approximations of their uses in the function body, because otherwise the type would include less values than what would be accepted, which in turn implies more checks than actual, so it would be unsafe to erase.
On the other hand, the inferred function return types are also over-approximations of what would actually be returned, otherwise it would be also unsafe to erase that type because there are no real checks for return types.
What about annotated types? One caveat is that types are not strict anymore. By not being strict I mean that, for example, the return value of a function with type A -> B might not be B. Only strong functions have such property; ordinary functions, when passed a value with the unknown type, only returns an unknown.
This landscape deliberately leaves the other direction open, i.e. under-approximation of function parameter type and under-approximation or function return type.