rust-lang / chalk

An implementation and definition of the Rust trait system using a PROLOG-like logic solver
https://rust-lang.github.io/chalk/book/
Other
1.84k stars 182 forks source link

Ambiguity through unrelated env clauses because of implied bounds #750

Open flodiebold opened 2 years ago

flodiebold commented 2 years ago

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:

  1. we're trying to solve <A as IntoIterator>::Item = ?0
  2. 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)
  3. for that, we need to prove A: Iterator; we don't have that in the environment, but from implied bounds we have FromEnv(<^0.0 as IntoIterator>::IntoIter: Iterator) :- FromEnv(^0.0: IntoIterator), i.e. if there was some type T that implements IntoIterator whose IntoIter is A, that would prove that A: Iterator. This does make logical sense, but basically dooms us to fail, because:
  4. to use this, we need to find some ?1 where FromEnv(?1: IntoIterator) and <?1 as IntoIterator>::IntoIter = A. There are two options in the environment for the first part, A and B. So the first goal is ambiguous.
  5. the second goal <?1 as IntoIterator>::IntoIter = A flounders because IntoIterator is non-enumerable.
  6. 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:

flodiebold commented 2 years ago

Looking into https://github.com/rust-lang/chalk/issues/727, it does at least seem to be caused by the same implied env rule.