normalization and the meaning of unique

[nikomatsakis]

We are still wrestling to some extent with the meaning of "unique" and how to handle negative reasoning. In #38, @aturon made a number of changes, but I have some reservations about some of the details of that PR. There are also some scenarions that are still not handled very well in that PR that we may want to consider.

When @aturon and I last spoke, we had decided to shift the approach of the PR in two ways -- at least, if I remember correctly. First, to introduce a CannotProve variant, which is used to mean that the system cannot prove a particular goal, and never will be able to, but that the goal may hold for some instantiations of the universally quantified variables in scope (but it also may not hold for some instantiations). In particular, this would be returned when you attempt to unify (e.g.) !1 and !2 or !1 and Vec<T>. Currently, those unification attempts "succeed" with the "ambiguous" flag set to true, and hence forall<T,U> { T = U } yields an ambiguous result. Under this proposal it would yield CannotProve.

The meaning of the various return values for proving goal G is thus:

• Unique: There is a unique MGU of the existentials for which G is provable (and here is the corresponding MGU).
• Ambiguous: The goal may be provable in multiple ways, given a suitable instantiation of the existentials. Here is a suggestion that can lead you to one of those ways.
  • Definite: If this goal is to ever work, the existentials must take the given values. (edited)
  • Suggested: This is an opinionated suggestion. This is what we think the user meant ,but there are other things they could have typed.
  • Unknown: No advice, you're on your own buddy.
• CannotProve: There is no instantiation of the existentials for which we could prove this goal to be true. Nonetheless, the goal may yet be true for some instantiations of the universals. In other words, this goal is neither true nor false.
• Error: This goal is provably false.

In general, the modality controls whether we consider the set of impls/environmental clauses/etc to be a closed world.

Just adding CannotProve alone doesn't quite give us enough resolution to always negate the way we might want to. In particular, not { G } where G yields CannotProve also yields CannotProve, and hence not { forall<T,U> { T = U } } is also going to yield up "cannot prove" (as would forall<T,U> { not { T = U } }). It is plausible that we could instead say that not { forall } is Unique and forall { not } is Error; but to handle it, we would have to track the "sense" of a goal more deeply (right now, the fulfillment context cannot distinguish between a not inside or outside the forall binder).

If we add CannotProve, we ought to be able to remove the "special treatment" that we give to the environment right now (which makes me uncomfortable in any case, at least in its current form). In particular, we have some logic that makes an ambiguous unification in the environment become a "hard error", which implies that forall<T,U> if (T: Foo) { U: Foo } will reject using T: Foo, even though T = U yields "ambiguous". Once we have CannotProve, then T = U can yield CannotProve, and we are universally justified in ignoring proof routes that yield CannotProve.

Test cases

Some interesting benchmarks and examples to use to evaluate possible solutions:

Example 1: Maybe implements.

trait Foo {}
struct i32 {}
impl Foo for i32 {}

forall<T> { T: Foo }
forall<T> { not { T: Foo } }

It's vital here that we treat T as possibly implementing Foo due to the impls. So that's at least the minimum bar.

Example 2: negation and binders.

not { forall<T, U> { T = U } } // provably true
// vs
forall<T, U> { not { T = U } } // neither true nor false

Example 3: Normalization.

struct i32 { }
trait Iterator { type Item; }
impl Iterator for i32 { type Item = i32; }

Given the query forall<T> { if (T: Iterator<Item = i32>) { T: Iterator } }, current code can fail with ambiguity. The environment supplies T: Iterator<Item = i32> but the program clauses supply i32: Iterator<Item = i32>.

[nikomatsakis]

Evaluating the "cannot prove" rule on the various examples shows that it works well, modulo the imprecision around not and forall binders I mentioned:

Example 1. In the first case (forall<T> { T: Foo }), trying to unify T: Foo against the impl would yield CannotProve, which would lead to an overall CannotProve result. Negating CannotProve again yields CannotProve. This successfully indicates that the goal may be provable for some instantiations (but not all).

Example 2. Negation and binders. We would yield CannotProve for both; to do better requires a different fulfillment context desugaring.

Example 3. Unifying the T: Iterator<Item = i32> goal with the impl would yield CannotProve, and hence we would drop that rule in favor of T: Iterator<Item = i32> from the environment.

[nikomatsakis]

After #45, this might be basically done -- the only thing left might be changing how we handle negative reasoning, if we decide we want more precise results. That could also be a separate bug.

[aturon]

Definite: The goal will definitely work. (Does this mean something closer to Unique?)

That's not quite right. The reading is rather: if this goal is to ever work, the existentials must take the given values.

[nikomatsakis]

@aturon updated

[nikomatsakis]

So I resolved this in #60. The first key observation is that free universally quantified variables (i.e., ForAll) cannot be considered ground and require some special treatment (this is why for<A, B> { not { A = B } } was giving us such trouble). The second is that the behavior of existentials in that case is exactly what we want. So essentially was #60 does is to say that, to solve a query like not { !1 = !2 }, we will check whether ?1 = ?2 has any answers. In other words, convert the universally quantified variables into existential ones. This allows us to drop "cannot prove" entirely.

Revisiting my examples:

Example 1.

trait Foo {}
struct i32 {}
impl Foo for i32 {}

forall<T> { T: Foo } // false
forall<T> { not { T: Foo } } // false -- ?T: Foo has an answer

Example 2.

not { forall<T, U> { T = U } } // true
forall<T, U> { not { T = U } } // false, ?T = ?U has an answer

Example 3.

T: Iterator<Item = i32> from environment is the only choice.