Recursive Solver fails to solve recursive associated type with GAT

This seems quite obvious, but fails;

```rust
#[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

	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));
	}
	}

	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);
	}

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

ShoyuVanilla
openedon Jul 30, 2024

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

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

Description

ShoyuVanillaopenedon Jul 30, 2024

Metadata