Treatment of regions in trait matching is perhaps too simplistic

[nikomatsakis]

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]

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]

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]

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

[nikomatsakis]

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]

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]

@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.