normalization and the meaning of unique about chalk

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