From f4f3d501dea926786bfaa0034e2f28f057f31bb1 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 00:15:26 +0100 Subject: [PATCH 1/8] RFC 803: Change where type ascribed expressions can be coerced --- text/0803-type-ascription.md | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/text/0803-type-ascription.md b/text/0803-type-ascription.md index e5e62c37ad2..edea3319224 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 ` is a type ascription -expression): - -``` -&[mut] -let ref [mut] x = -match { .. ref [mut] x .. => { .. } .. } -.foo() // due to autoref - = ...; -``` +`e` is an lvalue, and an rvalue otherwise. +In order to prevent the unsoundness problem, 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. +This way, it's easy to see that: + +* Coercions can only occur where they're already possible without type ascription, so no new unsoundness is introduced. +* The increase of language complexity due to coercions is minimal. +* Type ascription is 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. + +With that rule in place, the above example doesn't compile since using `foo` of +type `S` in a context where a supertype of `S` is required is considered to be +a coercion and `&mut e` is not a coercion site. # Drawbacks From ca4bbedad146370ec3eec09e5fe252f6171b477c Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 03:22:48 +0100 Subject: [PATCH 2/8] RFC 2623: Add dedicated paper --- text/2623-type-ascribed-coercions.md | 144 +++++++++++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 text/2623-type-ascribed-coercions.md diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md new file mode 100644 index 00000000000..0c5fc249e1e --- /dev/null +++ b/text/2623-type-ascribed-coercions.md @@ -0,0 +1,144 @@ +- Feature Name: Type Ascribed Coercions +- Start Date: 2019-01-06 +- RFC PR: [rust-lang/rfcs#2623](https://github.com/rust-lang/rfcs/pull/2623) +- Rust Issue: _ + +[RFC 803]: https://github.com/rust-lang/rfcs/blob/master/text/0803-type-ascription.md +[RCF 2522]: https://github.com/rust-lang/rfcs/pull/2522 + +# Summary +[summary]: #summary + +The +[Rust reference defines *coercion sites*](https://doc.rust-lang.org/reference/type-coercions.html#coercion-sites) +which are contexts in which a coercion can occur. +For consistency, we change the specification as of [RFC 803] such that a type +ascribed expression that needs to be coerced can only occur at these coercion +sites. +# Motivation +[motivation]: #motivation + +The +[subsection "Type ascription and temporaries"](https://github.com/rust-lang/rfcs/blob/master/text/0803-type-ascription.md#type-ascription-and-temporaries) +of the merged [RFC 803] defines certain contexts (so-called *reference +contexts*) in which a type ascription that needs coercion **can not occur**. +Meanwhile and in contrast, the +[Rust reference defines *coercion sites*](https://doc.rust-lang.org/reference/type-coercions.html#coercion-sites) +which are contexts in which a coercion **can occur**. + +By applying the same rule to type ascribed expressions, we aim to reduce language complexity and increase consistency. + +This change shouldn't in any way conflict with [RCF 2522] + +# Guide-level explanation +[guide-level-explanation]: #guide-level-explanation + +Coercions are implicit type conversions and they already in the language. +You can read more about them +[here](https://doc.rust-lang.org/nomicon/coercions.html). + +The already merged (but not yet stabilized) [RFC 803] added type ascription for +expressions. +You should read it first. +It proposed that a type ascribed lvalue is still an lvalue and a type ascribed +rvalue is still an rvalue. +[An lvalues is a value that lives in a memory location.](https://stackoverflow.com/a/42313956/7350842) +The author of [RFC 803] correctly identified a problem that could arise with +the following code: + +``` +let mut foo: S = ...; +{ + 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 possibly code that would compile with [RFC 803] and that doesn't +compile with this change. +Such code would however rely on a coercion in a context that wasn't supposed to +introduce coercions. + +# 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. + +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 break the invariant that those +two lines are interchangable: + +```rust +let _ : T = e; +let _ = e : T: +``` From 4ec8e466a9ffa7578b58ebc50358068a65419a3d Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 03:25:12 +0100 Subject: [PATCH 3/8] RFC 803: Revert semantical change The change is now covered by the paper of RFC 2623 --- text/0803-type-ascription.md | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/text/0803-type-ascription.md b/text/0803-type-ascription.md index edea3319224..0b9e9e6bb8f 100644 --- a/text/0803-type-ascription.md +++ b/text/0803-type-ascription.md @@ -174,22 +174,19 @@ reference to a temporary copy of `x`. The proposed solution is that type ascription expressions inherit their 'lvalue-ness' from their underlying expressions. I.e., `e: T` is an lvalue if -`e` is an lvalue, and an rvalue otherwise. -In order to prevent the unsoundness problem, 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. -This way, it's easy to see that: - -* Coercions can only occur where they're already possible without type ascription, so no new unsoundness is introduced. -* The increase of language complexity due to coercions is minimal. -* Type ascription is 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. - -With that rule in place, the above example doesn't compile since using `foo` of -type `S` in a context where a supertype of `S` is required is considered to be -a coercion and `&mut e` is not a coercion site. +`e` is an lvalue, and an rvalue otherwise. 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. These +reference contexts are as follows (where `` is a type ascription +expression): + +``` +&[mut] +let ref [mut] x = +match { .. ref [mut] x .. => { .. } .. } +.foo() // due to autoref + = ...; +``` # Drawbacks From 0d3418f97213d813f3d8aae7961a158be0eb3534 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 03:46:19 +0100 Subject: [PATCH 4/8] RFC 2623: In Rationale, add implementation argument --- text/2623-type-ascribed-coercions.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md index 0c5fc249e1e..01658d302ce 100644 --- a/text/2623-type-ascribed-coercions.md +++ b/text/2623-type-ascribed-coercions.md @@ -15,6 +15,7 @@ which are contexts in which a coercion can occur. For consistency, we change the specification as of [RFC 803] such that a type ascribed expression that needs to be coerced can only occur at these coercion sites. + # Motivation [motivation]: #motivation @@ -132,6 +133,10 @@ 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. From a86743bb80b88c05f51982fefe492fb4ec602836 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 04:06:27 +0100 Subject: [PATCH 5/8] RFC 2623: Add link to the relevant page of the nomicon --- text/2623-type-ascribed-coercions.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md index 01658d302ce..5fd5b2253d6 100644 --- a/text/2623-type-ascribed-coercions.md +++ b/text/2623-type-ascribed-coercions.md @@ -76,6 +76,12 @@ There are several solutions to this problem: would be possible anyway. The above example wouldn't compile, because `&mut e` is not a coercion site. +More examples of what's a coercion site (i. e. a context in which an expression +can be subject to coercion) can be found on +[the corresponding page of the nomicon](https://doc.rust-lang.org/nomicon/coercions.html). +The same examples will still compile if the resulting type of the coercion is +ascribed. + # Reference-level explanation [reference-level-explanation]: #reference-level-explanation From d572d8a40a50b5c04505b00717d7b4ad295361b3 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 17:39:20 +0100 Subject: [PATCH 6/8] RFC 2623: Add note regarding expressions with infered type --- text/2623-type-ascribed-coercions.md | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md index 5fd5b2253d6..baa50ba6c2d 100644 --- a/text/2623-type-ascribed-coercions.md +++ b/text/2623-type-ascribed-coercions.md @@ -16,6 +16,10 @@ For consistency, we change the specification as of [RFC 803] such that a type ascribed expression that needs to be coerced can only occur at these coercion sites. +Note: +Type ascribed expressions that need only type inference undergo no changes, so +they can still occur everywhere. + # Motivation [motivation]: #motivation @@ -82,6 +86,9 @@ can be subject to coercion) can be found on The same examples will still compile if the resulting type of the coercion is ascribed. +Type ascribed expressions that need only type inference can still occur +everywhere, like it was the case with [RFC 803]. + # Reference-level explanation [reference-level-explanation]: #reference-level-explanation From e2519b222bb0dfcb8fde7134b90cb706a11db593 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 17:54:55 +0100 Subject: [PATCH 7/8] RFC 2623: Correct argumentation against no coercion --- text/2623-type-ascribed-coercions.md | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md index baa50ba6c2d..bdd7e4508b6 100644 --- a/text/2623-type-ascribed-coercions.md +++ b/text/2623-type-ascribed-coercions.md @@ -153,10 +153,5 @@ 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 break the invariant that those -two lines are interchangable: - -```rust -let _ : T = e; -let _ = e : T: -``` +This would however possibly be cumbersome and the consensus in [RFC 803] was +that we want some coercions in type ascribed expressions. From fa15db360e9ed39a4ec3c4a9fad59f2fa06013b4 Mon Sep 17 00:00:00 2001 From: haslersn Date: Sun, 6 Jan 2019 17:59:57 +0100 Subject: [PATCH 8/8] RFC 2623: Further elaboration of practical differences --- text/2623-type-ascribed-coercions.md | 37 +++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 4 deletions(-) diff --git a/text/2623-type-ascribed-coercions.md b/text/2623-type-ascribed-coercions.md index bdd7e4508b6..acfc1e06cf5 100644 --- a/text/2623-type-ascribed-coercions.md +++ b/text/2623-type-ascribed-coercions.md @@ -4,7 +4,7 @@ - Rust Issue: _ [RFC 803]: https://github.com/rust-lang/rfcs/blob/master/text/0803-type-ascription.md -[RCF 2522]: https://github.com/rust-lang/rfcs/pull/2522 +[RFC 2522]: https://github.com/rust-lang/rfcs/pull/2522 # Summary [summary]: #summary @@ -33,7 +33,7 @@ which are contexts in which a coercion **can occur**. By applying the same rule to type ascribed expressions, we aim to reduce language complexity and increase consistency. -This change shouldn't in any way conflict with [RCF 2522] +This change shouldn't in any way conflict with [RFC 2522] # Guide-level explanation [guide-level-explanation]: #guide-level-explanation @@ -125,10 +125,32 @@ This change doesn't introduce any new semantics since *coercion sites* and # Drawbacks [drawbacks]: #drawbacks -There's possibly code that would compile with [RFC 803] and that doesn't +There's code that would compile with [RFC 803] and that doesn't compile with this change. -Such code would however rely on a coercion in a context that wasn't supposed to +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 @@ -155,3 +177,10 @@ 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?