Recursive solver reports ambiguity

[iDawer]

In rust-lang/rust-analyzer#9990 we've found this failing test:

test!(
    program {
        #[upstream] #[non_enumerable] #[lang(sized)]
        trait Sized {}

        #[non_enumerable] #[object_safe]
        trait Database {}

        #[non_enumerable]
        trait QueryGroup
        where
            Self: Sized,
        {
            type DynDb: Database + HasQueryGroup<Self>;
        }

        #[non_enumerable] #[object_safe]
        trait HasQueryGroup<G>
        where
            Self: Database,
            G: QueryGroup,
            G: Sized,
        { }

        #[non_enumerable] #[object_safe]
        trait HelloWorld
        where
            Self: HasQueryGroup<HelloWorldStorage>,
        { }

        struct HelloWorldStorage {}

        impl QueryGroup for HelloWorldStorage {
            type DynDb = dyn HelloWorld + 'static;
        }
        impl<DB> HelloWorld for DB
        where
            DB: Database,
            DB: HasQueryGroup<HelloWorldStorage>,
            DB: Sized,
        { }
    }

    goal {
        forall<T> {
            if (FromEnv(T: Database); FromEnv(T: HasQueryGroup<HelloWorldStorage>); FromEnv(T: Sized)) {
                T: HelloWorld
            }
        }
    } yields[SolverChoice::slg_default()] { // ok
        "Unique"
    } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
        "Unique"
    }
);

Removing DB: Database bound and FromEnv(T: Database) makes the test pass.

[matthewjasper]

This seems to be a general issue with how chalk handles elaborating environment clauses. The second test case here shows this best, there are two different FromEnv traits that are both elaborated to give the same thing. The recursive solver considers this ambiguous.

Other test cases

#[test]
fn impl_that_should_work() {
    test!(
        program {
            #[non_enumerable] #[object_safe]
            trait Database {}

            #[non_enumerable]
            trait QueryGroup
            {
                type DynDb: Database + HasQueryGroup<Self>;
            }

            #[non_enumerable] #[object_safe]
            trait HasQueryGroup<G>
            where
                Self: Database,
                G: QueryGroup,
            { }

            struct HelloWorldStorage {}

            impl QueryGroup for HelloWorldStorage {
                type DynDb = dyn HasQueryGroup<HelloWorldStorage> + 'static;
            }
        }

        goal {
            forall<T> {
                if (FromEnv(T: HasQueryGroup<HelloWorldStorage>)) {
                    T: Database
                }
            }
        } yields[SolverChoice::slg_default()] {
            "Unique"
        } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
            "Unique"
        }
    );
}

#[test]
fn impl_that_should_work2() {
    test!(
        program {
            #[non_enumerable]
            trait Database {}

            #[non_enumerable]
            trait HasQueryGroup<G>
            where
                Self: Database,
            { }

            struct HelloWorldStorage {}

            impl Database for HelloWorldStorage { }
        }

        goal {
            forall<T, S> {
                if (FromEnv(HelloWorldStorage: HasQueryGroup<T>); FromEnv(HelloWorldStorage: HasQueryGroup<S>)) {
                    HelloWorldStorage: Database
                }
            }
        } yields[SolverChoice::slg_default()] {
            "Unique"
        } yields[SolverChoice::recursive_default()] { // fails: "Ambiguous; no inference guidance"
            "Unique"
        }
    );
}

[flodiebold]

Yeah. It's actually surprising that this doesn't work though, since solutions do get combined using combine:

chalk/chalk-solve/src/solve.rs

Lines 64 to 89 in 10ba203

	pub fn combine(self, other: Solution<I>, interner: &I) -> Solution<I> {
	use self::Guidance::*;
	if self == other {
	return self;
	}
	debug!(
	"combine {} with {}",
	self.display(interner),
	other.display(interner)
	);
	// Otherwise, always downgrade to Ambig:
	let guidance = match (self.into_guidance(), other.into_guidance()) {
	(Definite(ref subst1), Definite(ref subst2)) if subst1 == subst2 => {
	Definite(subst1.clone())
	}
	(Suggested(ref subst1), Suggested(ref subst2)) if subst1 == subst2 => {
	Suggested(subst1.clone())
	}
	_ => Unknown,
	};
	Solution::Ambig(guidance)
	}

and if the solution doesn't have variables and is unique, the self == other condition should trigger, right? Is the problem that there's somehow an intermediate solution where there's a variable involved? 🤔

[iDawer]

I've also noticed that removing DynDb associated type makes the test pass

[flodiebold]

I think the original case is actually the same problem as I investigated in #750.

@matthewjasper's impl_that_should_work2 is also interesting in that it's also a case where the recursive solver can't deal with the implied env though.

(To elaborate on impl_that_should_work2:)

1. We try to prove FromEnv(HelloWorldStorage: Database) from the general implied env rule FromEnv(^0.0: Database) :- FromEnv(^0.0: HasQueryGroup<^0.1>). This requires solving FromEnv(HelloWorldStorage: HasQueryGroup<?0>).
2. There are two solutions for FromEnv(HelloWorldStorage: HasQueryGroup<?0>, ?0 = T and ?0 = S. These are different solutions that can't be merged, so the whole thing is ambiguous in the recursive solver. The SLG solver would be able to yield both solutions.

Contrary to the original case and #750, there are no associated types and no floundering involved here.

[nikomatsakis]

So I have a simple fix that addresses the case from the OP and impl_that_should_work2, but which does not fix impl_that_should_work. That case is a bit trickier.

The code that "combines" results in the recursive solver is actually a bit overconservative. In particular, this logic:

chalk/chalk-recursive/src/solve.rs

Lines 157 to 160 in f470f2f

	// If we have a completely ambiguous answer, it's not going to get better, so stop
	if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
	return Ok(Solution::Ambig(Guidance::Unknown));
	}

is incorrect. That would be reasonable if all of the clauses had to be true, but in fact any of the clauses can be true and they are all equally valid. So the fact that one clause was ambiguous isn't a problem if other clauses are not.

To make the tests pass, you also have to adjust the combine routine:

chalk/chalk-solve/src/solve.rs

Lines 44 to 64 in f470f2f

	/// There are multiple candidate solutions, which may or may not agree on
	/// the values for existential variables; attempt to combine them. This
	/// operation does not depend on the order of its arguments.
	//
	// This actually isn't as precise as it could be, in two ways:
	//
	// a. It might be that while there are multiple distinct candidates, they
	// all agree about *some things*. To be maximally precise, we would
	// compute the intersection of what they agree on. It's not clear though
	// that this is actually what we want Rust's inference to do, and it's
	// certainly not what it does today.
	//
	// b. There might also be an ambiguous candidate and a successful candidate,
	// both with the same refined-goal. In that case, we could probably claim
	// success, since if the conditions of the ambiguous candidate were met,
	// we know the success would apply. Example: `?0: Clone` yields ambiguous
	// candidate `Option<?0>: Clone` and successful candidate `Option<?0>:
	// Clone`.
	//
	// But you get the idea.
	pub fn combine(self, other: Solution<I>, interner: I) -> Solution<I> {

As the comment notes, it is not particularly precise. I added a really simple fix to start that just checks whether self or other corresponds to a Unique result with an empty substitution and no region constraints, which is the most accepting thing you can have. If so, I just return that. To do this properly, we would also handle other interesting cases: e.g., if one of them works then ?T = u32 but the other solution requires ?T = u32, ?U = u32, we can accept the first one (more generally, if one solution entails the other).

Unfortunately, this isn't enough to fix that impl_that_should_work test -- I'll explain why in next comment. (I'll also push a branch with these changes.)

[nikomatsakis]

So why doesn't impl_that_should_work work? Well, the problem has do with handling of associated types and the lack of an explicit impl.

We wind up concluding that T: Database may be true because Database is a supertrait of T: HasQueryGroup<HelloWorldStorage>. That works fine.

But then, clever us, we also notice this:

trait QueryGroup
{
    type DynDb: Database + HasQueryGroup<Self>;
}

and so run off trying to prove whether there exists a ?X such that <?X as QueryGroup>::DynDb = T. Naturally we can't resolve that, it would require some epic leaps of inference, and anyway QueryGroup is non-enumerable, so we call it ambiguous.

I'm not sure the best way to fix this just now, it's tied in with some other stuff that I'm in the midst of reconsidering (how we handle assoc type normalization; how best to talk about the WF conditions and implied bounds), but it certainly doesn't seem fatal. The key insight is, that for an implied bound, we're really only interested in normalizations that result from where-clauses, because any normalization that we can derive from an impl means the impl where clause are satisfied and we could as well derive the conclusion from first principles.

[nikomatsakis]

opened #754