diff --git a/text/0803-type-ascription.md b/text/0803-type-ascription.md index e5e62c37ad2..0b9e9e6bb8f 100644 --- a/text/0803-type-ascription.md +++ b/text/0803-type-ascription.md @@ -161,7 +161,7 @@ as an lvalue (i.e., no new temporary), then there is potential for unsoundness: ``` let mut foo: S = ...; { - let bar = &mut (foo: T); // S <: T, no coercion required + let bar = &mut (foo: T); // S <: T, coercion from S to T *bar = ... : T; } // Whoops, foo has type T, but the compiler thinks it has type S, where potentially T If the type ascription expression is +in reference context, then we require the ascribed type to exactly match the +type of the expression, i.e., neither subtyping nor coercion is allowed. + +Instead, we use the +[Rust reference's definition of a *coercion site*](https://doc.rust-lang.org/reference/type-coercions.html#coercion-sites) and extend it by the new rule: +A type ascription expression `e : T` is a coercion site if and only if it +occurs at a coercion site itself. + +If `e` is of type `S` and the expression `e : T` occurs at a coercion site that +expects the type `U`, then it shall be required that `S` is coercible to `T` +and `T` is coercible to `U`. +In that case, the semantics are that of coercing `S` to `U`, which is possible +because of the transitivity. + +Remarks: + + * `e` in `e : T` can of course only be subject to coercion if `e : T` is a coercion site by that rule. + * With `S <: T`, coercing `S` to `T` is also + [considered a coercion](https://doc.rust-lang.org/reference/type-coercions.html#coercion-types). + +With that rule, type ascription is still idempotent since applying the same +type ascription twice doesn't only preserve the type but also whether the +ascribed expression is considered to occur at a coercion site. + +This change doesn't introduce any new semantics since *coercion sites* and +[RFC 803]'s *reference contexts* are disjoint. + +# Drawbacks +[drawbacks]: #drawbacks + +There's code that would compile with [RFC 803] and that doesn't +compile with this change. +For example, the following code doesn't compile if `e` isn't of type `T`, even +if it's coercible to `T`: + +```rust +let _ = e : T; // ERROR, not a coercion site +``` + +The reason is that `let _ = ;` is not a coercion site, because it +relies on type inference. + +Such code does however rely on a coercion in a context that wasn't supposed to +introduce coercions. +There's also no need to support this, since you can still type ascribe the +identifier whose type is to be infered: + +```rust +let _ : T = e; +``` + +This alternative is what the above mentioned compile error should suggest. +It should work in all cases as soon as [RFC 2522] gets merged. + +This drawback **might actually be an advantage** in the sense that there should be +one and only one obvious way to do something. + +# Rationale and alternatives +[rationale-and-alternatives]: #rationale-and-alternatives + +Type ascription wasn't intended to introduce sites for conversions, but to help +the compiler infer the correct type. +Therefore type ascription isn't the correct feature in case a user wants a +conversion that wouldn't already happen without type ascription. + +With this design, coercions can only occur where they're already possible +without type ascription, which has the additional benefit that it's easy to see +that no new unsoundness is introduced. + +Having coercion consistent across language features also minimizes the increase +of language complexity, which is good for both, the implementors and the users. +For example, there's no need to define *reference contexts* anymore. + +Coercion in type ascribed expressions is +[not yet implemented](https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=825110d9744d502cf30544e3c86ed37c). +This change should make its implementation easier. + +The only alternative that I currently see is to disallow coercions in all type +ascribed expressions, such that the ascribed type always has to match the type +of the expression exactly. +This would however possibly be cumbersome and the consensus in [RFC 803] was +that we want some coercions in type ascribed expressions. + +# Unresolved questions + +* In [drawbacks] we've seen an example that doesn't compile but has an + existing alternative. + Are there any examples that don't compile and don't have an obvious + alternative?