chalk
chalk copied to clipboard
Ambiguity through unrelated env clauses because of implied bounds
This comes from https://github.com/rust-analyzer/rust-analyzer/issues/10653, basically the example is this:
fn foo<A, B>()
where
A: IntoIterator<Item = u32>,
B: IntoIterator<Item = usize>,
{
let _x: <A as IntoIterator>::Item;
}
We'd expect _x
to have type u32
here of course, but actually we can't solve the projection. Removing the second where clause (about B
) makes it work. This might be related to #727, but it seems it's probably something separate.
Here's the same problem in Chalk test form:
fn rust_analyzer_into_iterator() {
test! {
disable_coherence; // just to remove distractions
program {
#[non_enumerable]
trait Iterator {
type Item;
}
#[non_enumerable]
trait IntoIterator {
type Item;
type IntoIter: Iterator<Item = <Self as IntoIterator>::Item>;
}
impl<I> IntoIterator for I where I: Iterator {
type Item = <I as Iterator>::Item;
type IntoIter = I;
}
}
goal {
forall<A, B> {
if (A: IntoIterator<Item = u32>; B: IntoIterator<Item = usize>) {
exists<T> {
<A as IntoIterator>::Item = T
}
}
}
} /*yields[SolverChoice::slg_default()] {
// this is wrong, chalk#234
expect![["Ambiguous; no inference guidance"]]
}*/ yields[SolverChoice::recursive_default()] {
expect![["Unique; substitution [?0 := Uint(U32)]"]]
}
}
}
What happens is basically this:
- we're trying to solve
<A as IntoIterator>::Item = ?0
- because of the
impl IntoIterator for I where I: Iterator
, we consider whether we can solve<A as Iterator>::Item = ?0
(this makes sense, but it's a wrong path that should ultimately give no solution here) - for that, we need to prove
A: Iterator
; we don't have that in the environment, but from implied bounds we haveFromEnv(<^0.0 as IntoIterator>::IntoIter: Iterator) :- FromEnv(^0.0: IntoIterator)
, i.e. if there was some type T that implements IntoIterator whoseIntoIter
isA
, that would prove thatA: Iterator
. This does make logical sense, but basically dooms us to fail, because: - to use this, we need to find some
?1
whereFromEnv(?1: IntoIterator)
and<?1 as IntoIterator>::IntoIter = A
. There are two options in the environment for the first part,A
andB
. So the first goal is ambiguous. - the second goal
<?1 as IntoIterator>::IntoIter = A
flounders becauseIntoIterator
is non-enumerable. - hence the whole thing is ambiguous, and we fail.
I'm not sure how to fix this. Using the implied env rule in step 4 in this way is basically impossible for the recursive solver, because it has to intersect solutions for two separate goals that very likely have multiple solutions, but the SLG solver could theoretically do it. I guess theoretically we could have a where clause like B: IntoIterator<Item = u32, IntoIter = A>
and then this path would actually give us the solution. Though current rustc does not reason this way as far as I can tell, so maybe it would be possible to optionally skip this rule for now to make rust-analyzer work in actual situations :thinking:
Looking into https://github.com/rust-lang/chalk/issues/727, it does at least seem to be caused by the same implied env rule.