[mraleph]

The reason why languages promote variable types based on control flow is because developers en masse actually expect that to happen, e.g. facing the code like

    Dog? maybeDog;
    if (maybeDog != null) {
      maybeDog.bark();
    }

If compiler says "sorry, maybeDog might be null", developer (rightfully so) usually responds "but I have just checked and I know it is not, why do you bother me?". So languages chose to accommodate this.

> What if I want to set the value back to nil if it is not-nil?

You can. The type of the variable does not actually change. You could say that the information about more precise type is simply propagated to the uses which are guarded by the control flow. The following will compile just fine:

    Dog? maybeDog;
    if (maybeDog != null) {
      maybeDog.bark();
      maybeDog = null;
    }

> Why should I have to wrap things back in an optional if I want to pass it along as such?

You don't, with a few exceptions. There is a subtype relationship between T and T?: T <: T?, so the following is just fine:

    void foo(Dog? maybeDog);

    Dog? maybeDog;
    if (maybeDog != null) {
      maybeDog.bark();
      foo(maybeDog);  // Dog can be used where Dog? is expected
    }
 

You might need to account for it in places where type inference infers type which is too precise, e.g.

    Dog? maybeDog;
    if (maybeDog != null) {
      // This will be List<Dog> rather than List<Dog?>. 
      final listOfDogs = [maybeDog];
    }

Though I don't think it is that bad of a problem in practice.

[saagarjha]

See, I don't think languages should accommodate this, because I see it as an ugly solution. It's nice that it works in a few cases but then it very quickly breaks down: a developer finds that their null check is enough to strip an optional, but a test against zero doesn't convert their signed integer to unsigned. Checking that a collection has elements in it doesn't magically turn it into a "NonEmptyCollection" with guaranteed first and last elements. I'm all for compilers getting smarter to help do what programmers expect, but when they can't do a very good job I don't find the tradeoff to be very appealing. Basically, I think pattern matching is a much better solution this problem, rather than repurposing syntax that technically means something else (even though 90% of the time people who reach for it mean to do the other thing).

Also, fwiw, I was mostly talking about things like the last example you gave. I guess it would be possible that in circumstances where T is invalid but T? would be valid, the language actually silently undos the refinement to make that code work. However, I am not sure this is actually a positive, and it doesn't help with the ambiguous cases anyways.

[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()?

[troupo]

The ugly solution is Swift's if let x = x which is literally the same check, but in a more verbose manner.

Yes, compilers should be able to help in this and many other cases, and not just give up and force the programmer to do all the unnecessary manual work