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.
Sure, but if you do this in Java you must use different variable names for the reference of type Animal and the reference of type Object.
I think algebraic data types and type refinement are great, but I’m not a fan of automagically changing the types of variables in different scopes if it can’t be applied consistently.
I'm still kinda new to the idea of using conditional branches to inform static type checkers but it sounds like it's an idea that has been thought about in some depth [1][2][3] (i.e. doesn't sound like it was jimmy-rigged to match common JS patterns).
I personally love type refinement. Hacklang's type refinement was the first time it clicked that statically typed languages could _actually help_ you write code instead of get in the way.
[0] https://docs.hhvm.com/hack/types/type-refinement
[1] https://sites.cs.ucsb.edu/~benh/research/papers/kashyap13typ...
[2] Type refinements (page 23) https://drops.dagstuhl.de/opus/volltexte/2018/9219/pdf/LIPIc...
[3] Occurrence Typing (section 8.5) http://soft.vub.ac.be/Publications/2019/vub-soft-phd-19-02.p...
FWIW, Go also changes the variable's type in type-switch cases: https://tour.golang.org/methods/16
Personally it doesn't feel complicated to use/understand (at least the kind of thing that these languages do)
That being said, I still think TypeScript's solution to handling them of using "type guards" where the type of a variable changes in different scopes is definitely designed to match common JS patterns at the cost of added complexity. Most other languages I know of only have a single type for a variable (and if you want to pattern match you must give each case a new variable name).