I feel like the real question here is what will the semantics of a programming language with dependent types look like without enforcing of GADTs all the way, and whether it will work. That is, thanks to GADTs functional languages with dependent types -- in a sense -- make traditional runtime look like static since the type is non-constant while the checking is static (meaning, dependent operations over a variable returns a variable with redefined type, not possible now in Rust). This seems to be the main difference for now, as Rust the type is constant. Yet, this might very well be enough for practical usefulness -- with GADTs all the way you can reason about nice properties such as termination (sometimes) and certain mathematical interest such as generalisations of programming, but this is likely uninteresting for most. Rust might very well apply the same kind of golden middle road to dependent types as it did for linearity via affine types. Will be interesting how this evolves further!