Flow-sensitive typing

In programming language theory, flow-sensitive typing (also called flow typing or occurrence typing) is a type system where the type of an expression depends on its position in the control flow.
In statically typed languages, a type of an expression is determined by the types of the sub-expressions that compose it. However, in flow-sensitive typing, an expression's type may be updated to a more specific type if it follows a statement that validates its type. The type is determined by using type inference and type information is carried using algebraic data types.
Example.
Ceylon.
See the following example in Ceylon which illustrates the concept:
// Object? means the variable "name" is of type Object or else null
void hello(Object? name) {
 if (is String name) {
 // "name" now has type String in this block
 print("Hello, ``name``!");
 // and it is possible to call String methods on the variable
 print(" String.size is ``name.size``");
 else if (exists name) {
 // "name" now has type Object in this block
 print("Hello, object ``name``!");
 else {
 print("Hello, world!");
hello(null);
hello(1);
hello("John Doe");
Which outputs:
 Hello, world!
Hello, object 1!
Hello, John Doe!
 String.size is 8
Kotlin.
See this example in Kotlin:
fun hello(obj: Any) {
 // A type cast fails if `obj` is not a String
 obj as String
 // Since the type cast did not fail, `obj` must be a String!
 val l = obj.length
 println("'$obj' is a string of length $l")
 
hello("Mooooo")
Benefits.
This technique coupled with type inference reduces the need for writing type annotations for all variables or to do type casting, like is seen with dynamic languages that use duck typing. It reduces verbosity and makes up for terser code, easier to read and modify.
It can also help language implementers provide implementations that execute dynamic languages faster by predicting the type of objects statically.
Finally, it increases type safety and can prevent problems due to null pointers, labeled by C.A.R. Hoare—the null reference inventor—as "the billion dollar mistake"
Implementations.
Typed Scheme, a type system for Scheme, was the first type system with this feature. Shortly thereafter, David J. Pearce independently reinvented it in Whiley, the first language to have this feature built-in.
The successor to Typed Scheme, Typed Racket (a dialect of Racket), still makes extensive use of occurrence typing. It has since appeared in Ceylon, TypeScript and Facebook Flow.
There are also a few languages that don't have union types but do have nullable types, that have a limited form of this feature that only applies to nullable types, such as C#, Kotlin, and Lobster.