Better guidance for projections

[flodiebold]

I think the following test, or something similar, should pass:

#[test]
fn projection_guidance() {
    test! {
        program {
            trait Iterator { type Item; }
            #[non_enumerable]
            trait Step {}

            struct Range<T> {}

            impl<T> Iterator for Range<T> where T: Step {
                type Item = T;
            }
        }

        goal {
            exists<T> {
                exists<U> {
                    <Range<T> as Iterator>::Item = U
                }
            }
        } yields[SolverChoice::recursive()] {
            "Ambiguous; definite substitution { [?0 := ?0.0, ?1 = ?0.0] }"
        }
    }
}

I.e. the recursive solver should be able to tell that there is only one impl that could possibly apply, so we know the Item type. This is derived from the following real-world case (from rust-lang/rust-analyzer#4072:

enum Option<T> {}
trait Iterator {
    type Item;

    fn next(&mut self) -> Option<Self::Item>;
}

trait Step { }
impl Step for i32 {}
impl Step for u32 {}

struct Range<T>(T, T);

impl<A: Step> Iterator for Range<A> {
    type Item = A;
}

fn main() {
    let x = Range(0, 10).next();
}

which rustc manages to figure out. (This isn't related to integer type variables / fallback, it's just an easy way to get a type variable.)

The SLG solver gives Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := (Iterator::Item)<Range<^0.0>>] }, which is also not very helpful, but that's related to other problems, I think.

I haven't really looked into why this doesn't work in the recursive solver or how to fix it; I think it may be that the solver just gives up too early when one subgoal flounders (in this case the ?0: Step goal). It could be a good first issue for getting into the recursive solver. It may be more complicated though.

This issue has been assigned to @Mcat12 via this comment.

[AzureMarker]

I've started looking into this and I think I've found why the solver fails, though I may need some guidance on how to properly fix it.

@rustbot claim

The gist is that the recursive solver gets to to the point where it has to prove Implemented(^0.0: Step), but it does not receive any clauses which it can use. I think it just needs Implemented(^0.0: Step) :- FromEnv(^0.0: Step) and FromEnv(^0.0: Step), but they are not made available.

Snippet from debug output

| solve_goal(UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Implemented(^0.0: Step) }, binders: [U0 with kind type] }, universes: 1 }) {
: | solve_new_subgoal(canonical_goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([]), goal: Implemented(^0.0: Step) }, binders: [U0 with kind type] }, universes: 1 }, depth=StackDepth { depth: 3 }, dfn=DepthFirstNumber { index: 3 }) {
: : | prog_clauses {
: : : | program_clauses_for_goal(goal=Implemented(^0.0: Step), environment=Env([])) {
: : : : | program_clauses_that_could_match(goal=Implemented(^0.0: Step)) {
: : : : | }
: : : | }
: : | }
: : | prog_solution=Ok(Ambig(Unknown))
: : | solve_new_subgoal: loop iteration result = Ok(Ambig(Unknown)) with minimums Minimums { positive: DepthFirstNumber { index: 18446744073709551615 } }
: | }

I've modified program_clauses_that_could_match to generate the trait datum clauses before doing the non-enumerable check (adding the implemented -: from_env rule). I was originally going to try and avoid the Err(Floundered) by checking the environment for FromEnv(^0.0: Step), but the environment is completely empty. I'm also not sure if this is the right approach, since I don't really have any background in the recursive solver. Let me know if there's a more "idiomatic" way to solve this, and in the meantime I'll keep plugging away at it.

[flodiebold]

Returning Ambig(Unknown) for Implemented(^0.0: Step) is correct, I think. When the solver gets a goal like Implemented(^0.0: Step), it cannot enumerate all types that implement Step, so even if it did have some other program clauses for this goal, and those program clauses did give solutions, it still doesn't know whether there are other solutions. I think the actual problem is in the layer above that, where it's trying to apply the Normalize rule and getting Ambig for the subgoal.

Also #433 might be related to this, I'm not sure.

[AzureMarker]

I was a little confused by why Normalize required Implemented rules, as the types should still be equivalent regardless of if the trait is implemented or well-formed. Perhaps the Implemented rules should be moved to another clause?

[AzureMarker]

Reading the debug output, a solution is found but the ambiguous solution from Implemented(^0.0: Step) is used instead because it has a higher priority:

preferring solution: Ambig(Unknown) over Unique(Canonical { value: ConstrainedSubst { subst: [?0 := ^0.0, ?1 := (Iterator::Item)<Range<^0.0>>], constraints: [] }, binders: [U0 with kind type] }) because of higher prio

Edit: the following is probably irrelevant, as both the SLG solver and recursive solver get the same answer, but the recursive solver disregards the trivial solution because it has a lower priority. I will look into #443 to see if the ideas can be adapted for the recursive solver.

There is a similar test in #433 (no associated types though) while seems to work as expected:

chalk/tests/test/impls.rs

Lines 643 to 660 in c8135bb

	#[test]
	fn unify_types_in_ambiguous_impl() {
	test! {
	program {
	#[non_enumerable]
	trait Constraint {}
	trait Trait<T> {}
	struct A<T> {}
	impl<T> Trait<T> for A<T> where T: Constraint {}
	}
	goal {
	exists<T,U> { A<T>: Trait<U> }
	} yields {
	"Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }"
	}
	}
	}

However, the PR is mainly for the SLG solver.

[flodiebold]

I was a little confused by why Normalize required Implemented rules, as the types should still be equivalent regardless of if the trait is implemented or well-formed. Perhaps the Implemented rules should be moved to another clause?

This is why: #235
The Normalize rule needs to check the where clauses of the impl.

Reading the debug output, a solution is found but the ambiguous solution from Implemented(^0.0: Step) is used instead because it has a higher priority

That's also correct, the low-priority solution isn't really helpful here either, it's just a placeholder for the associated type in case we find no other solution.

However, the PR is mainly for the SLG solver.

The PR also contains a fix for the recursive solver, it's just much smaller apparently 😉

[AzureMarker]

So I took another look at the Type equality and unification logic to figure out what path the logic is expected to take in order to arrive at the Ambiguous; definite substitution { [?0 := ?0.0, ?1 = ?0.0] } solution. Once we reach the goal Normalize(<Range<T> as Iterator>::Item -> T) we produce the following clause:

forall<T> {
    Normalize(<Range<T> as Iterator>::Item -> T) :-
        Implemented(T: Step)
}

The documentation proposes an additional condition, Implemented(Range<T>: Iterator), but it seems fine for the implementation to elude it since it is always true given Implemented(T: Step).

Intuitively, we know T implements Step because it is a condition of the impl. That is, there should be a FromEnv(T: Step) in the environment once we enter the impl. I think this is where the problem occurs, because the implementation does not do this and then trips up because Step is non-enumerable. @flodiebold this is where I'd like tap your knowledge, because I'm not sure where/when the recursive solver is expected to add facts to the environment. Is it just a bug that it doesn't happen once we enter the impl, or is that expected? Looking through the places where the environment is given facts/clauses, maybe we should be pushing a GoalData::Implies to our Fulfill instance when entering the impl?

Edit: if this is the cause, then this issue generalizes to both solvers and the fix should fix both.

[flodiebold]

The documentation proposes an additional condition, Implemented(Range: Iterator), but it seems fine for the implementation to elude it since it is always true given Implemented(T: Step).

That's the documentation being outdated; the condition for the Normalize rule used to be just that the corresponding trait is implemented, but that was wrong because of #235. And yeah, the current conditions imply that condition (but not the other direction).

Intuitively, we know T implements Step because it is a condition of the impl. That is, there should be a FromEnv(T: Step) in the environment once we enter the impl.

I'm not sure what exactly you see as "entering the impl" here. We try to apply the Normalize rule, and that requires us to prove Implemented(?0: Step), we can't just assume it. We would be able to assume it if we were trying to prove an implication like T: Step => Normalize(<Range<T> as Iterator>::Item -> T), but that's not the situation we're in here.

[AzureMarker]

I mean "entering the impl" as the for loop over all the impls of Iterator (maybe it should be further down the logical chain, like when we try to prove Implemented(T: Step)?):

chalk/chalk-solve/src/clauses.rs

Lines 328 to 341 in 01690cf

	for impl_id in builder.db.impls_for_trait(trait_id, trait_parameters) {
	let impl_datum = builder.db.impl_datum(impl_id);
	if !impl_datum.is_positive() {
	continue;
	}
	debug!("impl_id = {:?}", impl_id);
	for &atv_id in &impl_datum.associated_ty_value_ids {
	let atv = builder.db.associated_ty_value(atv_id);
	debug!("atv_id = {:?} atv = {:#?}", atv_id, atv);
	atv.to_program_clauses(builder);
	}
	}

We are given that T: Step in the impl parameters, therefore we should know FromEnv(T: Step) while we are checking if the normalization is valid (I'm not directly assuming Implemented(T: Step)). If this isn't true, then how else would we show [?0 := ?0.0, ?1 = ?0.0]?

[flodiebold]

we should know FromEnv(T: Step) while we are checking if the normalization is valid

We don't know that; otherwise the result would be that the normalization is always valid, which it isn't.

But yes, the reasoning here is basically "if this were true, then the substitution would be [?0 := ?0.0, ?1 = ?0.0]. So I guess it could be possible to detect the situation, solve the goal assuming the condition, and then see what the substitution would be. I just think this is probably too complicated of a solution, and there should be a simpler fix for this; because we already have the substitution when we're trying to prove the Normalize rule, we just need to return it when we get an ambiguous result. There may be additional conditions necessary though.

[AzureMarker]

Ok, now I feel a little silly, but at least I understand the solver code a little better. #443 fixes this issue for the recursive solver (a simple 6-line change). However, it regresses the SLG solver to return Ambiguous; no inference guidance instead of Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := (Iterator::Item)<Range<^0.0>>] }.

Edit: The solution is slightly different. It has a for binder: Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }. Is this expected?

[flodiebold]

Actually, I think that's the correct way to write what I meant 🙂

However, it regresses the SLG solver to return Ambiguous; no inference guidance instead of Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := (Iterator::Item)<Range<^0.0>>] }.

Hm, well, the previous answer from the SLG solver is wrong anyway, and the SLG solver has problems with projections anyway (#234), so this doesn't seem that worrying to me, but I also don't know enough about the SLG solver to know whether there's a problem in the PR.