Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
ShoyuVanilla opened this issue Jul 30, 2024 · 0 comments
Open

Comments

@ShoyuVanilla
Copy link
Member

ShoyuVanilla commented Jul 30, 2024

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;

fn solve_from_clauses(
&mut self,
canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
minimums: &mut Minimums,
should_continue: impl std::ops::Fn() -> bool + Clone,
) -> Fallible<Solution<I>> {
let mut clauses = vec![];
let db = self.db();
let could_match = |c: &ProgramClause<I>| {
c.could_match(
db.interner(),
db.unification_database(),
&canonical_goal.canonical.value.goal,
)
};
clauses.extend(db.custom_clauses().into_iter().filter(could_match));
match program_clauses_that_could_match(db, canonical_goal) {
Ok(goal_clauses) => clauses.extend(goal_clauses.into_iter().filter(could_match)),
Err(Floundered) => {
return Ok(Solution::Ambig(Guidance::Unknown));
}
}

like the relevant case for the above test case;
DomainGoal::Normalize(Normalize { alias, ty: _ }) => match alias {
AliasTy::Projection(proj) => {
// Normalize goals derive from `AssociatedTyValue` datums,
// which are found in impls. That is, if we are
// normalizing (e.g.) `<T as Iterator>::Item>`, then
// search for impls of iterator and, within those impls,
// for associated type values:
//
// ```ignore
// impl Iterator for Foo {
// type Item = Bar; // <-- associated type value
// }
// ```
let associated_ty_datum = db.associated_ty_data(proj.associated_ty_id);
let trait_id = associated_ty_datum.trait_id;
let trait_ref = db.trait_ref_from_projection(proj);
let trait_parameters = trait_ref.substitution.as_parameters(interner);
let trait_datum = db.trait_datum(trait_id);
let self_ty = trait_ref.self_type_parameter(interner);
if let TyKind::InferenceVar(_, _) = self_ty.kind(interner) {
panic!("Inference vars not allowed when getting program clauses");
}
// Flounder if the self-type is unknown and the trait is non-enumerable.
//
// e.g., Normalize(<?X as Iterator>::Item = u32)
if (self_ty.is_general_var(interner, binders))
&& trait_datum.is_non_enumerable_trait()
{
return Err(Floundered);
}

and this taints all the other Unique solutions along the way

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant