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

Implied bounds on nested references + variance = soundness hole #25860

Open
aturon opened this Issue May 28, 2015 · 22 comments

Comments

Projects
None yet
9 participants
@aturon
Member

aturon commented May 28, 2015

The combination of variance and implied bounds for nested references opens a hole in the current type system:

static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'a, T>(x: &'a T) -> &'static T {
    let f: fn(&'static &'a (), &'a T) -> &'static T = foo;
    f(UNIT, x)
}

This can likely be resolved by checking well-formedness of the instantiated fn type.


Update from @pnkfelix :

While the test as written above is rejected by Rust today (with the error message for line 6 saying "in type &'static &'a (), reference has a longer lifetime than the data it references"), that is just an artifact of the original source code (with its explicit type signature) running up against one new WF-check.

The fundamental issue persists, since one can today write instead:

static UNIT: &'static &'static () = &&();

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T { v }

fn bad<'a, T>(x: &'a T) -> &'static T {
    let f: fn(_, &'a T) -> &'static T = foo;
    f(UNIT, x)
}

(and this way, still get the bad behaving fn bad, by just side-stepping one of the explicit type declarations.)

@aturon

This comment has been minimized.

Show comment
Hide comment
@aturon

aturon May 28, 2015

Member

What's going on here is that foo gets to assume that 'b: 'a, but this isn't actually checked when producing f.

This assumption was thought to be valid because any nested reference type &'a &'b T has to guarantee it for well-formedness. But variance currently allows you to switch around the lifetimes before actually passing in the witnessing argument.

Member

aturon commented May 28, 2015

What's going on here is that foo gets to assume that 'b: 'a, but this isn't actually checked when producing f.

This assumption was thought to be valid because any nested reference type &'a &'b T has to guarantee it for well-formedness. But variance currently allows you to switch around the lifetimes before actually passing in the witnessing argument.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis May 28, 2015

Contributor

One solution is to be more aggressive about checking WFedness, but there are other options to consider.

Contributor

nikomatsakis commented May 28, 2015

One solution is to be more aggressive about checking WFedness, but there are other options to consider.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jun 2, 2015

Contributor

triage: P-high T-lang

Contributor

nikomatsakis commented Jun 2, 2015

triage: P-high T-lang

@rust-highfive rust-highfive added P-high and removed I-nominated labels Jun 2, 2015

@nikomatsakis nikomatsakis self-assigned this Jun 2, 2015

@nikomatsakis nikomatsakis added the T-lang label Jun 2, 2015

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jun 2, 2015

Contributor

I've been working on some proposal(s) that address this bug (among others), so assigning to me.

Contributor

nikomatsakis commented Jun 2, 2015

I've been working on some proposal(s) that address this bug (among others), so assigning to me.

nikomatsakis added a commit to nikomatsakis/rust that referenced this issue Jun 5, 2015

Check that fn arguments are WF when calling the fn. In combination with
invariance, this restores soundness to implied bounds (I think). :)

Fixes rust-lang#25860.

nikomatsakis added a commit to nikomatsakis/rust that referenced this issue Jun 8, 2015

Check that fn arguments are WF when calling the fn. In combination with
invariance, this restores soundness to implied bounds (I think). :)

Fixes rust-lang#25860.

nikomatsakis added a commit to nikomatsakis/rust that referenced this issue Jun 9, 2015

Check that fn arguments are WF when calling the fn. In combination with
invariance, this restores soundness to implied bounds (I think). :)

Fixes rust-lang#25860.
@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jun 15, 2015

Contributor

There is a related problem that doesn't require variance on argument types. The current codebase doesn't check that the expected argument type is well-formed, only the provided one, which is a subtype of the expected one. This is insufficient (but easily rectified).

Contributor

nikomatsakis commented Jun 15, 2015

There is a related problem that doesn't require variance on argument types. The current codebase doesn't check that the expected argument type is well-formed, only the provided one, which is a subtype of the expected one. This is insufficient (but easily rectified).

nikomatsakis added a commit to nikomatsakis/rust that referenced this issue Jul 6, 2015

Check that fn arguments are WF when calling the fn. In combination with
invariance, this restores soundness to implied bounds (I think). :)

Fixes rust-lang#25860.
@Stebalien

This comment has been minimized.

Show comment
Hide comment
@Stebalien

Stebalien Sep 30, 2015

Contributor

@nikomatsakis I believe you meant to close this.

Contributor

Stebalien commented Sep 30, 2015

@nikomatsakis I believe you meant to close this.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Sep 30, 2015

Contributor

The work needed to close this has not yet landed. It's in the queue though, once we finish up rust-lang/rfcs#1214.

Contributor

nikomatsakis commented Sep 30, 2015

The work needed to close this has not yet landed. It's in the queue though, once we finish up rust-lang/rfcs#1214.

@Stebalien

This comment has been minimized.

Show comment
Hide comment
@Stebalien

Stebalien Sep 30, 2015

Contributor

Sorry, I saw the commit but didn't notice that it hadn't been merged.

Contributor

Stebalien commented Sep 30, 2015

Sorry, I saw the commit but didn't notice that it hadn't been merged.

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jan 21, 2016

Member

One interesting thing to note, in light of the new WF checks that have landed with the preliminary implementation of rust-lang/rfcs#1214, is that if we change the definition of fn foo like this (where we rewrite the implied lifetime bounds to be explicitly stated in a where-clause :

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T where 'b: 'a { v }

then it seems like the code is rejected properly.

I am currently trying to puzzle through whether this kind of "switch from implicit to explicit", assuming it were done as a kind of desugaring by the compiler, if that would be effectively the same as "remove support for contravariance" from the language, or if it represents some other path...

Member

pnkfelix commented Jan 21, 2016

One interesting thing to note, in light of the new WF checks that have landed with the preliminary implementation of rust-lang/rfcs#1214, is that if we change the definition of fn foo like this (where we rewrite the implied lifetime bounds to be explicitly stated in a where-clause :

fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) -> &'a T where 'b: 'a { v }

then it seems like the code is rejected properly.

I am currently trying to puzzle through whether this kind of "switch from implicit to explicit", assuming it were done as a kind of desugaring by the compiler, if that would be effectively the same as "remove support for contravariance" from the language, or if it represents some other path...

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jan 22, 2016

Member

Here's a variation on the original example that retains explicit types (rather than resorting to _ as a type like I did in the description):

fn foo<'a, 'b, T>(_false_witness: Option<&'a &'b ()>, v: &'b T) -> &'a T { v }

fn bad<'c, 'd, T>(x: &'c T) -> &'d T {
    // below is using contravariance to assign `foo` to `f`,
    // side-stepping the obligation to prove `'c: 'd`
    // implicit in the original `fn foo`.
    let f: fn(Option<&'d &'d ()>, &'c T) -> &'d T = foo;
    f(None, x)
}

fn main() {
    fn inner() -> &'static String {
        bad(&format!("hello"))
    }

    let x = inner();
    println!("x: {}", x);
}
Member

pnkfelix commented Jan 22, 2016

Here's a variation on the original example that retains explicit types (rather than resorting to _ as a type like I did in the description):

fn foo<'a, 'b, T>(_false_witness: Option<&'a &'b ()>, v: &'b T) -> &'a T { v }

fn bad<'c, 'd, T>(x: &'c T) -> &'d T {
    // below is using contravariance to assign `foo` to `f`,
    // side-stepping the obligation to prove `'c: 'd`
    // implicit in the original `fn foo`.
    let f: fn(Option<&'d &'d ()>, &'c T) -> &'d T = foo;
    f(None, x)
}

fn main() {
    fn inner() -> &'static String {
        bad(&format!("hello"))
    }

    let x = inner();
    println!("x: {}", x);
}
@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jan 22, 2016

Member

I am currently trying to puzzle through whether this kind of "switch from implicit to explicit", assuming it were done as a kind of desugaring by the compiler, if that would be effectively the same as "remove support for contravariance" from the language

After some reflection, I think this does represent a (perhaps appropriately) weakened variation on "remove contravariance from the language"

In particular, if we did the desugaring right (where implied lifetime bounds from a fn-signature would get transformed into where clauses on the fn), then we could still have useful contravariance for fn's that have no such implied bounds.

Member

pnkfelix commented Jan 22, 2016

I am currently trying to puzzle through whether this kind of "switch from implicit to explicit", assuming it were done as a kind of desugaring by the compiler, if that would be effectively the same as "remove support for contravariance" from the language

After some reflection, I think this does represent a (perhaps appropriately) weakened variation on "remove contravariance from the language"

In particular, if we did the desugaring right (where implied lifetime bounds from a fn-signature would get transformed into where clauses on the fn), then we could still have useful contravariance for fn's that have no such implied bounds.

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jan 22, 2016

Member

as an aside, part of me does think that it would be better if we also added some way to write the proposed implied where-clauses explicitly as part of the fn-type. I.e. if you consider the following example:

fn bad<'a, 'b>(g: fn (&'a &'b i32) -> i32) {
    let _f: fn(x: &'b &'b i32) -> i32 = g;
}

under my imagined new system, the above assignment of g to _f would be illegal, due to the implied bounds attached to g (that are not part of the type of _f).

But it might be nice if we could actually write:

fn explicit_types<'a, 'b>(callback: fn (&'a i32, &'b i32) -> i32 where 'a: 'b) {
    ...
}

(note that the where clause there is part of the type of callback)

Member

pnkfelix commented Jan 22, 2016

as an aside, part of me does think that it would be better if we also added some way to write the proposed implied where-clauses explicitly as part of the fn-type. I.e. if you consider the following example:

fn bad<'a, 'b>(g: fn (&'a &'b i32) -> i32) {
    let _f: fn(x: &'b &'b i32) -> i32 = g;
}

under my imagined new system, the above assignment of g to _f would be illegal, due to the implied bounds attached to g (that are not part of the type of _f).

But it might be nice if we could actually write:

fn explicit_types<'a, 'b>(callback: fn (&'a i32, &'b i32) -> i32 where 'a: 'b) {
    ...
}

(note that the where clause there is part of the type of callback)

@RalfJung

This comment has been minimized.

Show comment
Hide comment
@RalfJung

RalfJung Jan 22, 2016

Member

I take it from your comments that removing or restricting the variance is actually considered as a solution to this?

That's surprising me. I cannot see variance at fault here. The observation underlying the issue is that implicit bounds are not properly preserved under variance. The most obvious solution (for me, anyways) would be to make the implicit bounds explicit: If "fn foo<'a, 'b, T>(&'a &'b (), &'b T) -> &'a T" would be considered mere syntactic sugar for "fn foo<'a, 'b, T>(&'a &'b (), &'b T) -> &'a T where 'b: 'a, 'a: 'fn, T: 'b" (using 'fn for the lifetime of the function), and from then on the checks are preserved and adapted appropriately when applying variance or specializing lifetimes, wouldn't that also catch the trouble? (Making implied bounds explicit was also discussed in rust-lang/rfcs#1327, since implied bounds are also a trouble for drop safety.)

Member

RalfJung commented Jan 22, 2016

I take it from your comments that removing or restricting the variance is actually considered as a solution to this?

That's surprising me. I cannot see variance at fault here. The observation underlying the issue is that implicit bounds are not properly preserved under variance. The most obvious solution (for me, anyways) would be to make the implicit bounds explicit: If "fn foo<'a, 'b, T>(&'a &'b (), &'b T) -> &'a T" would be considered mere syntactic sugar for "fn foo<'a, 'b, T>(&'a &'b (), &'b T) -> &'a T where 'b: 'a, 'a: 'fn, T: 'b" (using 'fn for the lifetime of the function), and from then on the checks are preserved and adapted appropriately when applying variance or specializing lifetimes, wouldn't that also catch the trouble? (Making implied bounds explicit was also discussed in rust-lang/rfcs#1327, since implied bounds are also a trouble for drop safety.)

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jan 22, 2016

Member

@RalfJung

I cannot see variance at fault here.

I've been saying the similar things to @nikomatsakis

But the first step for me was to encode the test case in a way that made made it apparent (at least to me) that contravariance is (part of) why we are seeing this happen.

I think that #25860 (comment) is very much the same as what you are describing: 1. Ensure the implicit bounds are actually part of the fn-type itself (even if most users will not write the associated where clause explicitly) and are checked before allowing any calls to a value of a given fn-type, and then 2. fix the subtyping relation between fn-types to ensure that such where-clauses are preserved.

Member

pnkfelix commented Jan 22, 2016

@RalfJung

I cannot see variance at fault here.

I've been saying the similar things to @nikomatsakis

But the first step for me was to encode the test case in a way that made made it apparent (at least to me) that contravariance is (part of) why we are seeing this happen.

I think that #25860 (comment) is very much the same as what you are describing: 1. Ensure the implicit bounds are actually part of the fn-type itself (even if most users will not write the associated where clause explicitly) and are checked before allowing any calls to a value of a given fn-type, and then 2. fix the subtyping relation between fn-types to ensure that such where-clauses are preserved.

@RalfJung

This comment has been minimized.

Show comment
Hide comment
@RalfJung

RalfJung Jan 22, 2016

Member

I think that #25860 (comment) is very much the same as what you are describing: 1. Ensure the implicit bounds are actually part of the fn-type itself (even if most users will not write the associated where clause explicitly) and are checked before allowing any calls to a value of a given fn-type, and then 2. fix the subtyping relation between fn-types to ensure that such wshere-clauses are preserved.

Yes, that sounds like we're talking about the same idea.

Member

RalfJung commented Jan 22, 2016

I think that #25860 (comment) is very much the same as what you are describing: 1. Ensure the implicit bounds are actually part of the fn-type itself (even if most users will not write the associated where clause explicitly) and are checked before allowing any calls to a value of a given fn-type, and then 2. fix the subtyping relation between fn-types to ensure that such wshere-clauses are preserved.

Yes, that sounds like we're talking about the same idea.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jan 22, 2016

Contributor

I do not consider the problem to be fundamentally about contravariance -- but I do consider removing contravariance from fn arguments to be a pragmatic way to solve the problem, at least in the short term. In one of the drafts for RFC rust-lang/rfcs#1214, I wrote the section pasted below, which I think is a good explanation of the problem as I understand it:

Appendix: for/where, an alternative view

The natural generalization of our current fn types is adding the ability to attach arbitrary where clauses to higher-ranked types. That is, a type like for<'a,'b> fn(&'a &'b T) might be written out more explicitly by adding the implied bounds as explicit where-clauses attached to the for:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T)

These where-clauses must be discharged before the fn can be called. They can also be discharged through subtyping, if no higher-ranked regions are involved: that is, there might be a typing rule that allows a where clause to be dropped from the type so long as it can be proven in the current environment (similarly, having fewer where clauses would be a subtype of having more.)

You can view the current notion of implied bounds as being a more limited form of this formalism where the where clauses are exactly the implied bounds of the argument types. However, making the where clauses explicit has some advantages, because it means that one can vary the types of the arguments (via contravariance) while leaving the where clauses intact.

For example, if you had a function:

fn foo<'a,'b,T>(&'a &'b T) { ... }

Under this RFC, the type of this function is:

for<'a,'b> fn(&'a &'b T)

Under the for/where scheme, the full type would be:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T)

Now, if we upcast this type to only accept static data as argument, the where clauses are unaffected:

for<'a,'b> where<'b:'a, T:'b> fn(&'static &'static T)

Viewed this way, we can see why the current fn types (in which one cannot write where clauses explicitly) are invariant: changing the argument types is fine, but it also changes the where clauses, and the new where clauses are not a superset of the old ones, so the subtyping relation does not hold. That is, if we write out the implicit where clauses that result implicitly, we can see why variance on fns causes problems:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T, &'b T) -> &'a T 
<:
for<'a,'b> fn(&'static &'static T, &'b T) -> &'a T
? (today yes, under this RFC no)

Clearly, this subtype relationship should not hold, because the where clauses in the subtype are not implied by the supertype.

Contributor

nikomatsakis commented Jan 22, 2016

I do not consider the problem to be fundamentally about contravariance -- but I do consider removing contravariance from fn arguments to be a pragmatic way to solve the problem, at least in the short term. In one of the drafts for RFC rust-lang/rfcs#1214, I wrote the section pasted below, which I think is a good explanation of the problem as I understand it:

Appendix: for/where, an alternative view

The natural generalization of our current fn types is adding the ability to attach arbitrary where clauses to higher-ranked types. That is, a type like for<'a,'b> fn(&'a &'b T) might be written out more explicitly by adding the implied bounds as explicit where-clauses attached to the for:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T)

These where-clauses must be discharged before the fn can be called. They can also be discharged through subtyping, if no higher-ranked regions are involved: that is, there might be a typing rule that allows a where clause to be dropped from the type so long as it can be proven in the current environment (similarly, having fewer where clauses would be a subtype of having more.)

You can view the current notion of implied bounds as being a more limited form of this formalism where the where clauses are exactly the implied bounds of the argument types. However, making the where clauses explicit has some advantages, because it means that one can vary the types of the arguments (via contravariance) while leaving the where clauses intact.

For example, if you had a function:

fn foo<'a,'b,T>(&'a &'b T) { ... }

Under this RFC, the type of this function is:

for<'a,'b> fn(&'a &'b T)

Under the for/where scheme, the full type would be:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T)

Now, if we upcast this type to only accept static data as argument, the where clauses are unaffected:

for<'a,'b> where<'b:'a, T:'b> fn(&'static &'static T)

Viewed this way, we can see why the current fn types (in which one cannot write where clauses explicitly) are invariant: changing the argument types is fine, but it also changes the where clauses, and the new where clauses are not a superset of the old ones, so the subtyping relation does not hold. That is, if we write out the implicit where clauses that result implicitly, we can see why variance on fns causes problems:

for<'a,'b> where<'b:'a, T:'b> fn(&'a &'b T, &'b T) -> &'a T 
<:
for<'a,'b> fn(&'static &'static T, &'b T) -> &'a T
? (today yes, under this RFC no)

Clearly, this subtype relationship should not hold, because the where clauses in the subtype are not implied by the supertype.

@arielb1

This comment has been minimized.

Show comment
Hide comment
@arielb1

arielb1 Jan 22, 2016

Contributor

To make the point clearer, the principal part of the issue involves higher-ranked types. The rank 0 issue should not be that hard to solve (by requiring WF when instantiating a function - I am a bit surprised we don't do so already).

An example of the problem path (I am intentionally making the problem binder separate from the problem where-clause-container):

fn foo<'a, 'b, T>() -> fn(Option<&'a &'b ()>, &'b T) -> &'a T {
    fn foo_inner<'a, 'b, T>(_witness: Option<&'a &'b ()>, v: &'b T) -> &'a T {
        v
    }
    foo_inner
}

fn bad<'c, 'd, T>(x: &'c T) -> &'d T {
    // instantiate `foo`
    let foo1: for<'a, 'b> fn() -> fn(Option<&'a &'b ()>, &'b T) -> &'a T = foo;
    // subtyping: instantiate `'b <- 'c`
    let foo2: for<'a> fn() -> fn(Option<&'a &'c ()>, &'c T) -> &'a T = foo1;
    // subtyping: contravariantly 'c becomes 'static
    let foo3: for<'a> fn() -> fn(Option<&'a &'static ()>, &'c T) -> &'a T = foo2;
    // subtyping: instantiate `'a <- 'd`
    let foo4: fn() -> fn(Option<&'d &'static ()>, &'c T) -> &'d T = foo3;
    // boom!
    foo4()(None, x)
}

fn main() {
    fn inner() -> &'static String {
        bad(&format!("hello"))
    }

    let x = inner();
    println!("x: {}", x);
}
Contributor

arielb1 commented Jan 22, 2016

To make the point clearer, the principal part of the issue involves higher-ranked types. The rank 0 issue should not be that hard to solve (by requiring WF when instantiating a function - I am a bit surprised we don't do so already).

An example of the problem path (I am intentionally making the problem binder separate from the problem where-clause-container):

fn foo<'a, 'b, T>() -> fn(Option<&'a &'b ()>, &'b T) -> &'a T {
    fn foo_inner<'a, 'b, T>(_witness: Option<&'a &'b ()>, v: &'b T) -> &'a T {
        v
    }
    foo_inner
}

fn bad<'c, 'd, T>(x: &'c T) -> &'d T {
    // instantiate `foo`
    let foo1: for<'a, 'b> fn() -> fn(Option<&'a &'b ()>, &'b T) -> &'a T = foo;
    // subtyping: instantiate `'b <- 'c`
    let foo2: for<'a> fn() -> fn(Option<&'a &'c ()>, &'c T) -> &'a T = foo1;
    // subtyping: contravariantly 'c becomes 'static
    let foo3: for<'a> fn() -> fn(Option<&'a &'static ()>, &'c T) -> &'a T = foo2;
    // subtyping: instantiate `'a <- 'd`
    let foo4: fn() -> fn(Option<&'d &'static ()>, &'c T) -> &'d T = foo3;
    // boom!
    foo4()(None, x)
}

fn main() {
    fn inner() -> &'static String {
        bad(&format!("hello"))
    }

    let x = inner();
    println!("x: {}", x);
}
@brson

This comment has been minimized.

Show comment
Hide comment
@brson

brson Jun 23, 2016

Contributor

@rust-lang/lang no activity in a while. Still P-high? Anybody working on it or can we lower it?

Contributor

brson commented Jun 23, 2016

@rust-lang/lang no activity in a while. Still P-high? Anybody working on it or can we lower it?

@brson brson added the I-nominated label Jun 23, 2016

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jun 23, 2016

Member

(this issue really wants input from @nikomatsakis )

Member

pnkfelix commented Jun 23, 2016

(this issue really wants input from @nikomatsakis )

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 1, 2016

Contributor

I think we need to make progress on this issue, but I've been saying that for a year and we haven't. I would put this on the list of "important soundness issues" to address but I'm not sure how to prioritize that work in general relative to other tasks.

As far as the range of possible fixes I think nothing has changed from this previous comment:

  • We can ban contravariance, at least for fn arguments.
  • We can make for carry a notion of bounds, at least internally.

From a purely theoretical point-of-view, I would prefer the latter but I am wary of trying to implement it. It seems obvious that it will be hard to do in a complete way if we are talking about arbitrary sets of bounds. On the other hand, it may be that if we are just talking about implied bounds, we can implement the checks in a pretty simple way, since the bounds in question will have particular forms. I've been meaning to take some time and think about this more -- I think that some of the work being done for lazy normalization may help here -- but I've not really done so.

As far as the user-visible language changes that would result, removing contravariance for fn args is a nice simplification, but it is almost certainly more backwards incompatible than something based on making for carry a notion of bounds. When I first checked, the impact was small, but we have tarried quite some time and I don't know if that is still true.

Contributor

nikomatsakis commented Jul 1, 2016

I think we need to make progress on this issue, but I've been saying that for a year and we haven't. I would put this on the list of "important soundness issues" to address but I'm not sure how to prioritize that work in general relative to other tasks.

As far as the range of possible fixes I think nothing has changed from this previous comment:

  • We can ban contravariance, at least for fn arguments.
  • We can make for carry a notion of bounds, at least internally.

From a purely theoretical point-of-view, I would prefer the latter but I am wary of trying to implement it. It seems obvious that it will be hard to do in a complete way if we are talking about arbitrary sets of bounds. On the other hand, it may be that if we are just talking about implied bounds, we can implement the checks in a pretty simple way, since the bounds in question will have particular forms. I've been meaning to take some time and think about this more -- I think that some of the work being done for lazy normalization may help here -- but I've not really done so.

As far as the user-visible language changes that would result, removing contravariance for fn args is a nice simplification, but it is almost certainly more backwards incompatible than something based on making for carry a notion of bounds. When I first checked, the impact was small, but we have tarried quite some time and I don't know if that is still true.

@aturon aturon added P-medium and removed I-nominated P-high labels Jul 7, 2016

@aturon

This comment has been minimized.

Show comment
Hide comment
@aturon

aturon Jul 7, 2016

Member

The lang team met and determined that we should move to P-medium; no one is going to close this in the near future, but we want to keep it on the radar.

Member

aturon commented Jul 7, 2016

The lang team met and determined that we should move to P-medium; no one is going to close this in the near future, but we want to keep it on the radar.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Mar 3, 2017

Contributor

After some further thought -- and in particular working more on chalk -- I have started to have some hope that we would be able to close this using the more principled approach described here. Basically the idea would be that for<'a> fn(...) has "implied bounds" that are sufficient to make the fn well-formed, and that when we upcast we have to prove an "entailment" for the type that we are casting to. I used to be afraid of this entailment but I am... less afraid now. =) More investigation needed, of course.

Contributor

nikomatsakis commented Mar 3, 2017

After some further thought -- and in particular working more on chalk -- I have started to have some hope that we would be able to close this using the more principled approach described here. Basically the idea would be that for<'a> fn(...) has "implied bounds" that are sufficient to make the fn well-formed, and that when we upcast we have to prove an "entailment" for the type that we are casting to. I used to be afraid of this entailment but I am... less afraid now. =) More investigation needed, of course.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment