Skip to content

Fails to solve some existential clause #816

Open
@ShoyuVanilla

Description

@ShoyuVanilla
#[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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions