"Statically-typed" and "type-safe" don't mean the same thing.

"Type-safe" means that the type of a value is always correct. For example, if I have a function of type Int -> String, a type-safe language will not let me pass it a Float argument, no matter what I do. A type-unsafe language might let me, if I can "cast" the value to a new type without changing its representation (ie. it's still a Float, but the type-checker now thinks it's an Int).

Type-safe languages are preferred over type-unsafe languages, since they avoid all kinds of problems like undefined behaviour.

"Statically-typed" means that every variable, function argument, return value, etc. is associated with (usually one, "principle") type. These may be written explicitly, inferred, etc.

"Dynamically-typed" means that all values use the same static type. This type is usually a recursive sum of lots of useful types, for example (in pseudo-Haskell):

type UniType = I Int | L [UniType] | F (UniType -> UniType) | O (Object UniType) | E Error | ....

Dynamically-typed languages are type-safe, but in a trivial way: there's no way for a value to have the wrong type, since there's only 1 type!

Many users of dynamically typed languages don't realise that static types are being used "behind the scenes", because:

* All of their code has the same type, so there's no need for any annotations, inference, type-checking or compilation. Many believe it's because there are no types, rather than the fact these have been made trivial.

* Sum types and recursive types aren't widely known, especially to those using dynamic languages who don't need to care about types at all. Hence, many make the assumption that "I don't know how to type this code" implies "this code is untypeable" and refer to such things as 'dynamic behaviour'.

* Many dynamic languages are implemented in languages with unsafe, anemic type systems, like C. Since 'dynamic behaviour' can't be represented safely in these languages, it's implemented unsafely, reinforcing the assumption that dynamic languages aren't type-safe.

* Other dynamic languages are implemented in themselves, which hides the UniType underlying it all.

* A few dynamic languages are implemented in languages with strong, safe type-systems, where the UniType is explicit and obvious, but most users stick to the dynamic language and never look at the implementation.

* Many languages confuse terminology by using the word "type" to refer to tags (the "I", "L", "F", "O", "E", ... in my UniType above); for example "if (get_type(x) === "int") {...}" instead of "if (get_tag(x) === I) {...}", but this doesn't make sense: types don't exist at runtime and even if they did the "get_type" function would always return the same thing (the UniType). The fact that many languages represent tags as strings doesn't help either!

* Dynamic languages allow any variable to contain any value, but most of the time only a small part of this domain is expected. This causes most functions to be partial, but whenever this partiality is encountered, one of two things happens: a) the program fails with a "runtime type error", which is incorrect and doesn't make sense, b) the language supplies an error value in response, and is regarded as doing something "unsafe" or "untyped", when in fact error values are perfectly valid (I've tagged them with "E" above) and it's the programmer's fault for not handling all of the possible cases they (implicitly, via UniType) asked for.

The work you've linked to is about selectively weakening the types in a program, so rather than having the whole thing be unityped or the whole thing use distinct types, instead we can write code both ways, then automatically strengthen/weaken the types and lower/lift the functions, so that they interoperate. The types are always safe, but the unityped part will have many more partial functions than total functions.

In contrast, we can't (yet) make a type system "gradually safe", since a single unsafe cast can break anything else ("ex falso quodlibet"). It would require some kind of para-consistent logic, which I've never seen in type theory. The difference is that 'gradual types' let us say "Any" instead of "Int", whereas unsafe types let us say "X" instead of "Int", for any "X".