This seems to me like it’d require dependent types for all but trivial things. For example, imagine the condition `x > 0`. The compiler must know how all function that act on `x` behave. It must know that, when acting on a positive, multiplying by a negative always flips the sign, subtracting a positive sometimes flips the sign, and adding a positive never flips the sign. The compiler must be taught rules about each each and every operation. It’s infeasible for the Swift compiler to infer these rules automatically with the current type system.
I’d definitely find it exciting if Swift ventured into dependent typing territory, but it’d be a significant complication of the type system.
— Jaden Geller