Open iDawer opened 2 years ago
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.
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:
I've also noticed that removing DynDb
associated type makes the test pass
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
:)
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>)
.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.
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:
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:
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.)
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.
opened #754
In https://github.com/rust-analyzer/rust-analyzer/issues/9990 we've found this failing test:
Removing
DB: Database
bound andFromEnv(T: Database)
makes the test pass.