Recursive solver reports ambiguity

[iDawer]

In https://github.com/rust-analyzer/rust-analyzer/issues/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: https://github.com/rust-lang/chalk/blob/10ba203d660ac1ee80f19b5d162ae6e62f6b9ee1/chalk-solve/src/solve.rs#L64-L89 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? :thinking:

[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:

https://github.com/rust-lang/chalk/blob/f470f2f493203f58d493c7221863bca2ce1a6dad/chalk-recursive/src/solve.rs#L157-L160

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:

https://github.com/rust-lang/chalk/blob/f470f2f493203f58d493c7221863bca2ce1a6dad/chalk-solve/src/solve.rs#L44-L64

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