Comment by refulgentis

This is the elegant solution.

Where does it break down?

This isn't the same thing as "magically" changing the type.

What does the syntax technically mean?

What refinement is undone?

I think you're a bit too wedded to the idea that there's a type conversion going on or some dark magic or something behind the scenes that's "done" then "undone" like a mechanism. There isn't. It's just static analysis. Same as:

    let x: Animal;
    x = Dog()
    if (x is Dog) { 
      x.bark()
    }

The Zen koan you want to ponder on your end is, why do you want to A) eliminate polymorphism from OOP B) remove the safety of a compiler error if the code is changed to x = Cat()?