This is an extremely well-written and readable post. Nice and to the point. The use<T>, use<>, 'static trick is really fascinating and made me understand the issue at hand better. E.g. in the last example since the type of "the length of the slice" is irrelevant to "the type of slice" we ideally want to be able to express that in the type system. As an Agda developer, and a proponent of formal methods, it's very pleasurable to see these kind of novel PLT ideas being used in a mainstream language.

The implications of this on async seem tremendous. I'm a believer of async, even though it did do quite a bit of damage to the ecosystem, in the long term I bet on it being the correct abstraction (and Rust's implementation being close to the correct implementation). I think this change will make async more convenient and less restrictive to use.