Clarify ambiguity during unification; overhaul normalization fallback

[aturon]

This PR makes a few important changes:

• It clarifies ambiguity during unification so that we understand a query like !0 = i32 or !0 = !1 as asking the question for all possible substitutions, meaning that we can neither prove nor refute it, and hence return an ambiguous result.

• Furthermore, we treat program clauses as comprising a closed world (as intended) that cannot be extended further through environmental assumptions. That means, in particular, that we can simply ignore environmental assumptions that would require ambiguous unification to employ.

• Rather than using negation for normalization fallback, we introduce an explicit notion of "fallback program clauses" which are employed only when it is clear that no other forward progress on the goal is possible.

[nikomatsakis]

Some thoughts:

0. The concept of fallback program clauses seems good and I agree we should have something like that. I also agree that the if the "normalization fallback" is a kind of poor man's congruence closure.

1. It seems to me that Ambiguous(Guidance::Unknown) is being given "extra" significance here -- in a way, it plays the role I was suggesting we call CannotProve. For example, we opt to take the "fallback" in that situation. Your comment says we take fallback "only when it is clear that no other forward progress on the goal is possible", but (to me) it's not clear that "ambiguous, no guidance" means that no forward progress on the goal is possible (maybe we just don't have a clear route to suggest).

2. I don't quite understand the way that fallback interacts with guidance. In particular, it seems like the existence of a fallback rule can cause guidance to change from "definite" to "suggested" -- I guess this is just an approximation (i.e., if the "fallback rule" definite is Unique(S) and the guidance were Definite(S) for the same substitution S, then this is weaker than necessary, right?)

3. I am not yet fully comfortable with the idea of "privileging" program clauses over clauses that are "hypothesized" in the environment. Maybe I don't quite get your reasoning.

At first, I thought the idea was that the "ground truth" derives from the set of impls -- and I guess it might be fruitful for us to try to specify what a "correct" result means for our logic in some way that takes this into account. But just because clauses are in the program doesn't necessarily make them fit this definition. For example, in #12, we are talking about adding program clauses to handle "supertrait implications" (e.g. that T: Ord => T: PartialOrd). Those don't seem so radically different from where clauses on a function to me.

I guess at the end of the day it just feels sort of inconsistent to say that we can ignore i32: Foo<T> when searching for T: Foo<U> because it would require that we prove T = U (which we can never do), but we will yield ambiguous if asked to prove T = U itself. I think that the reason this seems "ok" does come back to those program clauses -- for any given instantiation, either this implication is false, or else there should be some impl that would let us "re-derive it"?

I am wondering how the "closed world" notion that we are using here would interact with (e.g.) coherence checking. Do we need different assumptions there? In that case, we (sometimes) have to assume that there might be more impls/types we don't know about, right? (e.g., in this case, it's very possible)

[aturon]

@nikomatsakis Thanks for the thoughtful comments!

It seems to me that Ambiguous(Guidance::Unknown) is being given "extra" significance here -- in a way, it plays the role I was suggesting we call CannotProve. For example, we opt to take the "fallback" in that situation. Your comment says we take fallback "only when it is clear that no other forward progress on the goal is possible", but (to me) it's not clear that "ambiguous, no guidance" means that no forward progress on the goal is possible (maybe we just don't have a clear route to suggest).

Yes, I agree with all of this. What I meant by "no forward progress on the goal is possible" is just that, in terms of what we're yielding up, there's no action that can be taken to "unblock" us. But of course our goal might be in the context of another Fulfill, in which case working toward other goals may indeed unblock us.

Thinking more about CannotProve -- yesterday, I was having a hard time distinguishing that in my head from "refuted", given a closed-world assumption. But now I think the point is it says: I can neither prove nor refute this, and no change to the ambient inference state will ever change that. Maybe Unknowable or something is better (since we want to equally weight proving and refuting here).

I don't quite understand the way that fallback interacts with guidance. In particular, it seems like the existence of a fallback rule can cause guidance to change from "definite" to "suggested"

I think this is just a bug. If we go this route, I'll re-work it.

I think that the reason this seems "ok" does come back to those program clauses -- for any given instantiation, either this implication is false, or else there should be some impl that would let us "re-derive it"?

Yes, exactly; this is what I had been thinking, but failed to articulate.

Note that things work fine even if we remove this special-casing; it just changes some inference heuristics.

Here's a good case to keep in mind:

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.

I am wondering how the "closed world" notion that we are using here would interact with (e.g.) coherence checking. Do we need different assumptions there?

Yes, this is precisely what the compat modality is about -- literally changing the statement from being about the current world (which we can assume is fixed) to all compatible ones.

[nikomatsakis]

OK, since @aturon is on PTO for this week, and I want to unblock stuff, I'm going to land this PR and open an issue to discuss follow-up changes.