Ambiguity problems with associated types

[flodiebold]

While handling associated types in rust-analyzer, I ran into two problems that I want to ask about. These are probably not related, so I can split this up if necessary, but I wanted to discuss them a bit first :slightly_smiling_face:

Number 1: (moved to #235)

Number 2:

#[test]
fn projection_equality() {
    test! {
        program {
            trait Trait1 {
                type Type;
            }
            trait Trait2<T> { }
            impl<T, U> Trait2<T> for U where U: Trait1<Type = T> {}

            struct u32 {}
            struct S {}
            impl Trait1 for S {
                type Type = u32;
            }
        }

        goal {
            exists<U> {
                S: Trait2<U>
            }
        } yields {
            "Unique"
        }
    }
}

I'd expect this to pass, but it yields ambiguity, I think because the ProjectionEq is ambiguous between u32 and Trait1::Type<S>. But those are really the same type. I found #74, but it's not clear to me how this kind of thing is supposed to work with ProjectionEq. #111 is maybe related?

[nikomatsakis]

Hmm so digging into number 1, something does indeed seem a bit wrong.

We wind up with these two program clauses:

for<type> Normalize(<Vec<^0> as IntoIterator>::Item -> ^0) :- 
    Implemented(Vec<^0>: IntoIterator)

for<type> Normalize(<^0 as IntoIterator>::Item -> <^0 as Iterator>::Item) :- 
    Implemented(^0: IntoIterator)

I think what I'd expect is something like

for<type> Normalize(<Vec<^0> as IntoIterator>::Item -> ^0)

for<type> Normalize(<^0 as IntoIterator>::Item -> <^0 as Iterator>::Item) :- 
    Implemented(^0: Iterator)

In particular, inlining the where-clauses and conditions of the impl into the rule. @scalexm -- do you recall why we set things up the way we did?

[nikomatsakis]

OK, looking at number 2, I see the problem you are highlighting. It does seem to be a shortcoming in the current "projection-eq" vs "normalization" scheme. Basically the problem here, as you said, is that we produce two answers:

U = u32

and

U = S::Item

The latter of which does (indeed) normalize to u32.

The thought I think initially was that getting back ambiguity here was ok, and that normally you'd get forced down path or the other from the top-level, but it'd be nice to avoid that.

Before we had the current path, I think, we tried a different path that had a notion of "fallback" (rather like how rustc handles things, actually), but iirc it led to a number of complications. I'd prefer not to go down that path again, but I suspect we will need further experimentation here.

[flodiebold]

The thought I think initially was that getting back ambiguity here was ok, and that normally you'd get forced down path or the other from the top-level, but it'd be nice to avoid that.

Hmm, but how would we get forced down one path or the other? IIRC we don't get any further information back from Chalk about this, so I don't see how we'd make progress. So is it a matter of the Solution / Guidance not being detailed enough?

[nikomatsakis]

Giving some more thought to number 2, it seems like we could pursue a different strategy. The idea would be something like this. First, perhaps we remove the idea of a "placeholder projection type". Then we only have projection types.

Now, if we find ourselves in a position where we have a projection type on exactly one side of a unification:

<P0 as Trait<P1..Pn>>::Foo<Pn...Pm> = T // or
T = <P0 as Trait<P1..Pn>>::Foo<Pn...Pm>

we can just convert that to a normalization rule, because there is no other possibility:

Normalize(<P0 as Trait<P1..Pn>>::Foo<Pn...Pm> -> T)

Similarly, if we find ourselves with two projections, but of different items:

<P0 as Trait<P1..Pn>>::Foo<Pn...Pm> =
<Q0 as Trait<Q...>>::Bar<...>

then we can just normalize one to the other:

Normalize(<P0 as Trait<P1..Pn>>::Foo<Pn...Pm> -> <Q0 as Trait<...>::Bar<..>)

If however we find ourselves with two projects but of the SAME item, then we have to add the extra possibility that forall<i> Pi = Qi.

[nikomatsakis]

OK, I see the next challenge though =) In this case, we have an unresolved inference variable, so we can't decide which of these paths we need (of course).

UPDATE 1: Maybe, in such cases, it'd be ok to just unify the type variable with the projection type. Basically just push the problem down the line. I think that should be fine.

UPDATE 2: Well, sort of fine. It seems plausible that you could wind up with two different answers to a given query, where one is S: Foo<u32> and one is S: Foo<S::Item>, and those are equivalent but are not syntactically equal. Not sure if that's a problem, but it could certainly confuse the logic that looks for unique answers.

[nikomatsakis]

@flodiebold

Hmm, but how would we get forced down one path or the other? IIRC we don't get any further information back from Chalk about this, so I don't see how we'd make progress.

Yeah, that's kind of the flaw in the thinking. =)

[scalexm]

@nikomatsakis I don’t think there’s any good reason why the where clauses are not inlined.

I probably thought it was equivalent because there would be a « perfect match » with the impl, but of course two impls can have a non-empty intersection with respect to their receiver type.

[nikomatsakis]

@scalexm that's kind of what I thought.

@flodiebold so indeed I think we should split the issues. I think that issue 1 is relatively easy to resolve. Issue 2 requires a bit more thought. At the moment, I've gone off and started doing some background reading I probably should have done a long time ago (e.g., reading Type Checking with Open Type Functions, which seems pretty directly relevant), but I'm not 100% sure where that will lead yet. It might be a good idea to do some experimentation too.

[flodiebold]

Ok, I moved the first one to a separate issue.

[nikomatsakis]

So I've been thinking about this problem. I wanted to leave some notes.

The current modeling I think is basically correct in some sense. That is, it creates rules that are provable in the cases we want them to be provable. In particular, when proving that a projection type equals another type, there is ultimately a kind of choice involved -- you can prove it using the "placeholder" route or you can prove it by showing that they normalize to the same thing (via an impl).

However, the rules are not optimal in a few respects:

• They generate too many solutions, which then confuses the uniqueness checker later on (the issue most directly reported here).
• This is probably also inefficient.

I think there are a few approaches worth thinking about. I'm ranking them a bit here in terms of "easy to hard" and maybe also in order of increasing desirability.

Improve the uniqueness checker.

The immediate problem is that we generate two solutions, one with U = u32 and one with U = S::Item. There is already code that tries to "generalize" multiple types. It would certainly be plausible for that code to check whether S::Item normalizes to u32 and, if so, ignore the S::Item answer. Note that this code lives outside the core SLG engine, which would be unaffected -- it would be generated multiple answers as ever, but we wouldn't consider them to overlap.

There are some subtle points here. For example, imagine that you have a solution like <Vec<?A> as Foo>::Bar and u32. Here the projection type has unresolved inference variables, and we have to be a bit careful. We are looking ultimately for a boolean result here, so we can't have free existentials (which could give back multiple results). I think we would want to prove that forall<T> { Normalize(<Vec<T> as Foo>::Bar -> u32) }. In other words, we would want to prove that no matter what those variables wind up to be, the equality stands. This will work fine in most common cases, of course.

The upside of this approach is that it might be minimally invasive, and it keeps the "SLG" core simple (though I've not deeply investigated what it will take). The downside of this approach is that it is relatively inefficient. Now we are not only generating more answers, we're also normalizing them rather late.

Don't search all the options.

Just because we can prove projection-equality using either a placeholder or a normalized type doesn't mean we should always try both. You could imagine adding some kind of || operator; this would be a logical or, but rather a kind of "guided search". To a first approximation (we'll see the problems with this later), if you had P || Q it would mean "try to prove P and, if you are able to, don't bother proving Q". In prolog, you could do things like this with a cut. The idea here would basically be to say "prove projection equality with normalizing if you can, and don't try to prove with placeholders unless you must". So in that case ProjectionEq(S::Item = ?X) would wind up with only one answer, X = u32. Having fewer answers already makes me a bit nervous, but I don't see any immediate problems with it.

Implementing this || operator is a bit interesting and reveals that it is indeed a kind of core modification to the logic/solver. At first, I thought maybe you could "desugar" P :- A || B into P :- A and P :- not { A }, B but that's not right. I was thinking of not as if it were "negation as failure", i.e., try to solve A and succeed if you fail, but we're actually smarter than that. We implement real logical negation. That turns out not to be what we want. For example I tried modifying the placeholder rule to be something like this:

forall<S> {
  ProjectionEq(<S as Trait>::Foo = (Trait::Foo)<S>) :-
    not { exists<A> { Normalize(<S as Trait>::Foo -> ?X) } }
}

but when S is itself some placeholder type (i.e., in a generic context), this doesn't work. This is because we don't know what S is there, and we can't prove that there isn't (or won't be) some type that can normalize. (This is similar to how we can't prove forall<T> { not { T = u32 } } even though we also can't prove forall<T> { T = u32 }.)

So I think you'd have to add some other kind of negation-like operator, or else add some custom sort of table or custom sort of strand, to implement this. And anyway what exactly do we want it to do? It should basically try to normalize and, if that succeeds, ignore the placeholder option -- but what about if it conditionally succeeds?

As before, imagine that we have a goal like ProjectionEq(<S as Trait1<?A>>::Item = ?B). Now imagine that we normalize with [?a = u32, ?B = u32]. That isn't a "complete" normalization, it's only a solution for the case where ?A = u32. There may be other cases (perhaps ones we don't know about locally). So we might want to preserve the placeholder option there.

So we need something that's like "convert this goal into closed form, with open inference variables replaced with forall variables, and try to prove that" (sort of like we saw in the previous section) or perhaps "prove without affecting the inference state" or some other such thing. This is all seeming quite unfortunate at this point. (Another option would just be to refuse to decide the result until those inference variables get resolved.)

Ultimately though this approach seems like it would be vaguely similar to what rustc is trying to do, though I'd have to put some thought into how comparable the two are. But rustc certainly has an approach of saying "I prefer to normalize to impls where I can, and fallback to placeholders if I can't". I'm sure rustc also makes some arbitrary choices now and again as well.

Using a different approach to normalizing.

Coming back to the core intution, though, I think we do ultimately want some kind of normalization routine where we normalize the left and right sides independently and then compare for equality, somewhat in contrast to the current projection-eq approach. This might require extending the "core logic" with some kind of "normalization" operator, but that operator would be (hopefully) easier to reason about than the direction I was describing in the previous section.

There is definitely applicable work elsewhere. I cited the paper Type Checking with Open Type Functions earlier, for example. Having read it, it's clearly aiming at solving basically the same problem. It may be that the normalization algorithm they describe there, which has a series of steps and so forth, can be applied in our context. I'll be honest and say that while the "overall shape" of their algorithm makes sense to me, I have to work through the paper a few more dozen times to really get it I suspect, and in particular the section on interactions with inference variables (which seems important) will require some careful examination.

Immediate steps?

It seems like we might experiment with the first approach (pruning out duplicate answers) with relative ease.

[nikomatsakis]

I put some more time thinking about lazy normalization.

First off, I spent some more time reading related work, but I've not really figured out how to map it to a Rust context yet.

On of the things I've been looking at separately is how to improve chalk's API so that when it requests sets of impls, it can generally avoid asking for "all impls".

In particular, it'd be nice if we could be sure that always know something about some input type -- or, perhaps even more narrowly, about the self type. This is related to questions of when to flounder.

Rustc today flounders whenever the self type is unknown, though, so let's take that as a starting point. In that case, you could almost be sure that you will know what the "self type" is when you are requesting impls, though it might of course be some placeholder type.

However, the current approach for lazy normalization introduces a complication. An "unnormalized" like T::Foo is essentially an inference variable.

This got me to thinking about an idea that I've kicked around from time to time. The existing approach to handling projection types is actually a kind of interpreter over a more basic logic, one in which equality means syntactic equality. Maybe it would be helpful to eliminate "unnormalized" projection types entirely and instead "desugar" them into explicit goals when lowering. I'd have to think about the best place/way to do this. But let me explain the idea first:

Basically, imagine that we have today a goal like:

forall<T> {
  Implemented(<T as Iterator>::Item: Trait<T>) :-
    T: Iterator
}

What happens today is that when we unify that rule with (say) Implemented[Trait](u32, Foo), then unification "outputs" a goal ProjectionEq(<Foo as Iterator>::Item = u32) that gets added to the goal list. What I have thought about instead is "lowering" the above rule to:

forall<T, U> {
  Implemented(U: Trait<T>) :-
    T: Iterator,
    ProjectionEq(<T as Iterator>::Item = U)
}

The effect of such a transformation is that we would never need "unnormalized" types at all. The only types we would have are placeholder types and ordinary, normalized types.

[flodiebold]

I'm not sure I understand the notation Implemented[Trait](<T as Iterator>::Item, T)... is that Implemented(<T as Iterator>::Item: Trait)? :thinking:

[nikomatsakis]

@flodiebold er, yes, sorry, my bad. Let me edit the notation, but it would mean

Implemented(<T as Iterator>::Item: Trait<T>)

[nikomatsakis]

The problem with that notion (Implemented(P0: Trait<P1...Pn>)) is that it doesn't make clear which things can be variables (notably, the parameters) and which cannot (the trait name, at least not yet). But anyway.

[nikomatsakis]

We talked about this in our design meeting today and decided to do a dedicated meeting on this topic next week (calendar event). We've created a hackmd for collecting notes leading up the meeting.

[p-avital]

Hello, Any updates on this? Sorry for being pushy, but most of rust-analyser's issues with type resolution point to this issue, I'd just like to see if there's any progress :)

[jackh726]

We discussed this some more today in the design meeting (link). Unfortunately it's a really difficult problem with some fundamental design questions. We still don't have a "clear" path forward, but there's a couple things to do/think about:

1. Niko's recursive solver could fix this. But we'll have to decide if that's the right approach.
2. We might be able to track normalization, in-type (my previous testing branches) or out-of-type (congruence edges). This isn't super clear, only brainstorming.

We'll definitely keep this on our radar, but as I said, there's not a clear path forward right now.