Skip to content
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

Treatment of regions in trait matching is perhaps too simplistic #21974

Open
nikomatsakis opened this issue Feb 5, 2015 · 10 comments

Comments

Projects
None yet
6 participants
@nikomatsakis
Copy link
Contributor

commented Feb 5, 2015

Not sure why I didn't see this coming. Until now, the treatment of regions in trait matching has intentionally ignored lifetimes (in the sense of, it did not consider lifetime constraints when deciding what impl to apply -- once an impl is selected, the constraints that appear on it naturally are enforced). The reason for this is that lifetime inference is a second pass that uses a much more flexible constraint-graph solving algorithm, in contrast to the bulk of type inference which uses something much closer to unification. A side-effect of this is that you cannot easily get a "yes or no" answer to the question "does 'x : 'y hold?" One must see wait until all the constraints have been gathered to know.

However, this leads to problems when you have multiple predicates in the environment that reference lifetimes. This is easy to see in the following example, but one does not need where clauses to get into this situation:

trait Foo {
    fn foo(self);
}

fn foo<'a,'b,T>(x: &'a T, y: &'b T)
    where &'a T : Foo,
          &'b T : Foo
{
    x.foo(); 
    y.foo();
}

fn main() { }

this winds up failing to compile because it can't really distinguish the two predicates here, since they are identical but for the specific lifetimes involved. This doesn't arise much in practice because it's unusual to have two requirements like that, usually you either have a more universal requirement (e.g., for<'a> &'a T : Foo), or just one particular lifetime you are interested in. I observed this problem however when experimenting with implied bounds, because it is common for multiple indistinguishable bounds of this kind to be generated as part of that proposal.

I'm not really sure how best to solve this at the moment.

@nikomatsakis nikomatsakis self-assigned this Feb 5, 2015

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

commented Feb 5, 2015

Note that this problem only really arises with where-clauses, since in the case of impls all lifetimes (other than 'static) are variables bound in the impl itself.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

commented Feb 5, 2015

After some discussion with @aturon I feel a bit better here. It's true that the current code is not handling this scenario correctly, in a couple of ways, but there is a plausible way forward (described below). Moreover, for the short short term, I think I can make progress in my implied bounds experiments by filtering the predicates we add to the environment a bit.

The obvious way forward is to overhaul region inference so that rather than simply infallibly collecting constraints as it goes, it actually evaluates the constraints that it has at hand to decide whether adding a new constraint will create an insolvable graph or not. I have to do some investigation into the best algorithms here but this kind of "live updated" dataflow graph seems like something that has certainly been explored over time, so I'm sure there's a really nifty algorithmic solution that will be tons of fun to implement.

The other change that is needed is to modify the trait checker, which currently has a rule that says "If I see two matches from where clauses, drop one of them". This rule can probably be dropped completely given #21968, but if not, it can at least be made more sensitive. This would imply that the calls above would yield ambiguous results until the inference graph is complete enough to select just one of the where clauses.

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

commented Feb 5, 2015

Note that this is not obviously 100% backwards compat, but I think it probably falls under the realm of "bug fix".

@nikomatsakis

This comment has been minimized.

Copy link
Contributor Author

commented Feb 5, 2015

In particular, if we do it right, we're just detecting (earlier) guaranteed errors that will occur later. But we should probably modify the trait checker so that the example above at least yields ambiguity now. I will experiment with that.

@bluss

This comment has been minimized.

Copy link
Contributor

commented May 3, 2015

Here are some weird things I've noticed.

This doesn't compile, the compiler is too picky:

use std::ops::Add;

fn plus<T>(a: &T, b: &T) -> T where
    for <'a> &'a T: Add<&'a T, Output=T>,
{
    a + b // error: cannot infer an appropriate lifetime for automatic coercion due to conflicting requirements
}
fn main() {}

Solution: Either annotate a and b params with the same lifetime, or do the following

fn plus<T>(a: &T, b: &T) -> T where
    for <'a, 'b> &'a T: Add<&'b T, Output=T>,
{
    a + b
}

But we can add nonsense bounds to existential clauses too

fn plus<'c, T>(a: &'c T, b: &'c T) -> T where
    for <'a: 'c> &'a T: Add<&'a T, Output=T>,
{
    let s = a + b;
    &s + &s
}

Only Add for lifetimes longer than 'c. Wait, our local variable s can't live up to that?

@arielb1

This comment has been minimized.

Copy link
Contributor

commented May 7, 2015

@bluss

The problem with your first program is that trait matching does not do subtyping - it does work if you reborrow:

use std::ops::Add;

fn plus<T>(a: &T, b: &T) -> T where
    for <'a> &'a T: Add<&'a T, Output=T>,
{
    &*a + &*b
}
fn main() {
    println!("1+1={}", plus(&1,&1));
}

You last program works as you wrote it – http://is.gd/SUyb2X.

@arielb1

This comment has been minimized.

Copy link
Contributor

commented May 7, 2015

Neither of these examples are relevant to this issue anyway.

@bluss

This comment has been minimized.

Copy link
Contributor

commented May 7, 2015

@arielb1 Thanks for the clarification!

The last program had the for <'a: 'c> requirement on 'a which I think is probably not used by rustc. If it would use it, the program shouldn't be legal.

@steveklabnik

This comment has been minimized.

Copy link
Member

commented Nov 29, 2016

Triage: this issue is kind of vague, and has a lot going on. Given this comment and that the original example still does not compile, it seems like this is something that might be doable, but it's not clear that we will/should.

@Zoxc

This comment has been minimized.

Copy link
Contributor

commented Sep 25, 2017

Apparently this causes problems when adding new implicit type parameter bounds and implicit trait supertraits (like Move and DynSized). In particular the following code reduced from the spectral crate will fail to compile:

use std::fmt::Debug;

trait DescriptiveSpec<'r> {}

impl<'r, T> DescriptiveSpec<'r> for &'r T {}

fn from_spec<'r, T: DescriptiveSpec<'r>>(spec: &'r T)  {}

fn matching_contains<'s, T: 's, I>(a: &mut &'s I) where &'s I: Debug {
    from_spec(a);
}

fn main() {}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.