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.81k stars 179 forks source link

Unable to deduce projection types of dyn types from supertrait bounds #777

Closed lowr closed 1 year ago

lowr commented 2 years ago

Context: https://github.com/rust-lang/rust-analyzer/issues/13169

It seems chalk is unable to deduce projection type of trait object types when it's not specified in dyn notation but the trait has supertrait with its projection type specified.

I expect the following tests to succeed but all three fail. This is because according to the rules described in #203, chalk yields AliasEq(<dyn Trait as Base>::Output = usize) as a subgoal but there's no "fact" clause for that to prove it. Shouldn't the AliasEq clause be also produced as a fact under these circumstances, or should we explicitly pass the AliasEq clause?

test! {
    program {
        trait Base { type Output; }
        trait Trait where Self: Base<Output = usize> {}
    }

    goal {
        forall<'s> {
            dyn Trait + 's: Trait
        }
    } yields[SolverChoice::recursive_default()] {
        expect![[r#"Unique"#]] // fails: "No possible solution"
    }

    goal {
        forall<'s> {
            dyn Trait + 's: Base<Output = usize>
        }
    } yields[SolverChoice::recursive_default()] {
        expect![[r#"Unique"#]] // fails: "No possible solution"
    }

    goal {
        forall<'s> {
            exists<T> {
                dyn Trait + 's: Base<Output = T>
            }
        }
    } yields[SolverChoice::recursive_default()] {
        // fails: "Unique; substitution [?0 := (Base::Output)<dyn for<type> [for<> Implemented(^1.0: Trait)] + '!1_0>]"
        expect![[r#"Unique; substitution [?0 := Uint(Usize)]"#]]
    }
}