> Most other languages I know of only have a single type for a variable
This may be pedantic, but with subtyping many OO languages can give many different distinct types for a variable. In Java you can assign any non-primitive typed expression to a variable of type Object. So almost any expression in Java can be typed as Object.
What you are describing as novel is rather the phenomenon of type refinement in a pattern match or conditional expression. When an expression undergoes pattern matching, its type becomes increasingly refined. This is a useful feature in intermediate-to-advanced Haskell (known as GADT) as well as dependently typed languages.
This may be pedantic, but with subtyping many OO languages can give many different distinct types for a variable. In Java you can assign any non-primitive typed expression to a variable of type Object. So almost any expression in Java can be typed as Object.
What you are describing as novel is rather the phenomenon of type refinement in a pattern match or conditional expression. When an expression undergoes pattern matching, its type becomes increasingly refined. This is a useful feature in intermediate-to-advanced Haskell (known as GADT) as well as dependently typed languages.