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.85k stars 182 forks source link

Recursive Solver fails to solve recursive associated type with GAT #815

Open ShoyuVanilla opened 4 months ago

ShoyuVanilla commented 4 months ago

This seems quite obvious, but fails;

#[test]
fn recursive_assoc_with_gat() {
    test! {
        program {
            #[non_enumerable]
            trait Foo {
                type Assoc;
                type Gat<T>: Foo<Assoc = T>;
            }
        }

        goal {
            forall<T> {
                if (
                    T: Foo
                ) {
                    exists<U> {
                        <T as Foo>::Assoc = U
                    }
                }
            }
        } yields {
            expect![[r#"Unique; substitution [?0 := (Foo::Assoc)<!1_0>]"#]]
        }
    }
}
expected:
Ambiguous; no inference guidance
actual:
Unique; substitution [?0 := (Foo::Assoc)<!1_0>]
thread 'test::projection::foobar' panicked at tests/test_util.rs:52:9:
assertion failed: `(left == right)`

Diff < left / right > :
<Ambiguous;noinferenceguidance
>Unique;substitution[?0:=(Foo:

This causes rust-lang/rust-analyzer#17725 but next-gen trait solver compiles the code in this issue with no error. I guess that this is because while next-gen solver has a branch that returns Err(NoSolution) for some flounderings; https://github.com/rust-lang/rust/blob/7e3a971870f23c94f7aceb53b490fb37333150ff/compiler/rustc_next_trait_solver/src/solve/mod.rs#L248-L262 but the chalk returns Ok(Solution::Ambig(Guidance::Unknown)) for every Flounder; https://github.com/rust-lang/chalk/blob/5bcd6117c8209960bb05ee05bfea68e8bc567dea/chalk-recursive/src/solve.rs#L129-L151 like the relevant case for the above test case; https://github.com/rust-lang/chalk/blob/5bcd6117c8209960bb05ee05bfea68e8bc567dea/chalk-solve/src/clauses.rs#L595-L627 and this taints all the other Unique solutions along the way