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

Fails to solve some existential clause #816

Open ShoyuVanilla opened 3 months ago

ShoyuVanilla commented 3 months ago
#[test]
fn trait_parameter() {
    test! {
        program {
            #[non_enumerable]
            trait Trait<T> {
                type Assoc;
            }

            struct Foo {}
            struct Bar {}

            impl Trait<()> for Foo {
                type Assoc = Bar;
            }
        }

        goal {
            exists<T, U> {
                <Foo as Trait<T>>::Assoc = U
            }
        } yields {
            expect![[r#"Unique; substitution [?0 := 0<[]>, ?1 := Bar<[]>]"#]]
        }
    }
}

fails with

program {
    #[non_enumerable] trait Trait<T> { type Assoc; } struct Foo {} struct Bar
    {} impl Trait<()> for Foo { type Assoc = Bar; }
}
----------------------------------------------------------------------
goal { exists<T, U> { <Foo as Trait<T>>::Assoc = U } }
using solver: SLG { max_size: 10, expected_answers: None }
----------------------------------------------------------------------
goal { exists<T, U> { <Foo as Trait<T>>::Assoc = U } }
using solver: Recursive { overflow_depth: 100, caching_enabled: true, max_size: 30 }

comparing solvers:
        expected: SLG { max_size: 10, expected_answers: None }
        actual: Recursive { overflow_depth: 100, caching_enabled: true, max_size: 30 }

expected:
Ambiguous; no inference guidance
actual:
Ambiguous; no inference guidance
jackh726 commented 3 months ago

You could have a downstream crate with struct Local; impl Trait<Local> for Foo { .. }.

Then, () and Local don't unify and its ambiguous.

This should give guidance, though.

ShoyuVanilla commented 3 months ago

Oh, I see. Thanks for the answer. I'll try investigating in that way