Skip to content

Settle desired semantics of divergence for purposes of coercion #40800

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
nikomatsakis opened this issue Mar 24, 2017 · 9 comments
Closed

Settle desired semantics of divergence for purposes of coercion #40800

nikomatsakis opened this issue Mar 24, 2017 · 9 comments
Labels
A-type-system Area: Type system C-bug Category: This is a bug. I-needs-decision Issue: In need of a decision. T-lang Relevant to the language team, which will review and decide on the PR/issue.

Comments

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Mar 24, 2017

In #40224, I adopted the rule that one can coerce into the type ! if your expression is considered to diverge (in short, returns, breaks, or must evaluate some expression of type !).

However, the code doens't quite implement that rule. As described in this comment, it actually uses the self.diverges flag of the FnCtxt, which today tracks a property that is different in a subtle way. The property we are checking is: if the coercion of the expression E happens in the context of an expression F, it is permitted to coerce to ! if the expression F has diverged by the time that E finishes evaluating.

So in particular, under the rules I originally envisioned, this would not be allowed (see src/test/compile-fail/coerce-to-bang.rs for more examples):

fn foo(x: usize, y: !) { }
foo(return, 22); // the expression `22` does not diverge

But under the rules as implemented, it is allowed. It's not clear which rules we would prefer. I think I lean towards my original rules: they mean that whether an expression E can be coerced to a type T is purely a function of E (modulo free variables of course). But implementing that will require refactoring the compiler.

In my diverging-types-and-reachability branch, I changed how things work so that divergence is propagated upward, and "reachability" is passed downward. Divergence is thus a property purely of the expression at hand, whereas reachability is computed based on context. We use the combination of the two to drive unreachable warnings -- in particular, when you have reachable code which evaluates a diverging expression, the next thing to be evaluated triggered a warning. The precise setup I had in that branch doesn't work, sadly, because it only computed divergence after all types were known. Some refactoring needed.

Moreover, there are some other places I cut corners in the existing code, and I'm using this same FIXME to track them: in particular, in cast expressions, I am ignoring whether they diverge for the purposes of this check. That's just laziness.

@nikomatsakis
Copy link
Contributor Author

cc @rust-lang/lang @canndrew @arielb1

@nikomatsakis nikomatsakis added A-type-system Area: Type system T-lang Relevant to the language team, which will review and decide on the PR/issue. labels Mar 24, 2017
@dhardy
Copy link
Contributor

dhardy commented May 5, 2017

It sounds to me like your original rules are more intuitive and less likely to lead to weird behaviour (e.g. under the current rules, foo(return, 22) is allowed, but bar(22, return) for fn bar(y: !, x: usize) is not allowed). So surely the only question is whether changing the rules now breaks much existing code?

@nikomatsakis
Copy link
Contributor Author

@dhardy yes. I suspect the impact is quite minimal, but hard to know until we put in the implementation effort. I should probably write up some mentoring instructions; I know I don't have time to pursue it myself.

@dhardy
Copy link
Contributor

dhardy commented May 5, 2017

Ah, I see. One of these days I should put in the effort of learning the Rust codebase.

@Mark-Simulacrum Mark-Simulacrum added C-bug Category: This is a bug. I-needs-decision Issue: In need of a decision. labels Jul 27, 2017
@shepmaster shepmaster changed the title settle desires semantics of divergence for purposes of coercion Settle desired semantics of divergence for purposes of coercion Aug 3, 2017
@canndrew
Copy link
Contributor

@nikomatsakis What's the status of this at the moment? Has any more work been done towards it or do you have any solid ideas about what needs to be done?

@nikomatsakis
Copy link
Contributor Author

@arielb1 and I were talking and I've been kind of failing to find the time to write up our conclusions. In the case of this question, we were wondering if would be possible to remove the "coerce into !" semantics entirely -- it's not clear why it's ever useful. There are some examples in run-pass of things that used to do it in the while, but they are very much corner cases. We'd be interested in removing this coercion and doing a crater run to measure the effects. @canndrew -- think you'd be interested in preparing that PR? Wouldn't be too hard (for the purposes of a crater run, just adding an if false in the right place would suffice, I suppose...)

@canndrew
Copy link
Contributor

canndrew commented Nov 9, 2017

I'm happy to do whatever needs to be done to get ! stable. I'm about to camping for the next two weeks though, so I won't be able to start until after that...

@canndrew
Copy link
Contributor

just adding an if false in the right place would suffice, I suppose...

Whereabouts might this "right place" be? I had a look but couldn't see where this coercion happens :/

@nikomatsakis
Copy link
Contributor Author

I believe @arielb1 implemented this in #45880, now merged. Closing.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-type-system Area: Type system C-bug Category: This is a bug. I-needs-decision Issue: In need of a decision. T-lang Relevant to the language team, which will review and decide on the PR/issue.
Projects
None yet
Development

No branches or pull requests

4 participants