Validate that rewrite constraints match the requirements

[danakj]

When doing impl lookup from a concrete value, or converting between facet values (which is implemented as impl lookup), ensure that the rewrite constraints known about the source value cover all of the requirements from the target facet type, and do not contradict any requirements.

To do this, we need additional information returned from the second stage of LookupImplWitness() (the stage on the other side of eval), to know the FacetType from which a symbolic LookupImplWitness finds its answer. The instruction itself erases that information, since it will continuing looking for a concrete answer on further (more specific) evaluations, but LookupImplWitness() needs the facet type to combine the rewrite constraints across all found witnesses and verify that they satisfy the query's constraints.

[danakj]

The changes to eval are kind of terrible, but this is a starting point that works and shows what is needed, from which we can discuss what to actually do.

[danakj]

I have gone ahead and cleaned up the impl lookup code now since it is not immediately obvious that this is not how we need to/should solve this problem. I resolved a TODO to share more code between impl lookup and eval by doing the canonicalization of the self in EvalLookupSingleImplWitness and having it return that. And I added a bunch more comments, and improved some of the flow around both called to EvalLookupSingleImplWitness.

[danakj]

I have added AddInstWithoutEval which uses AddImportedInst to avoid running eval for the instruction being added, and used that for the LookupImplWitness. Open to renaming or adjusting anything of course, but wasn't sure what to rename AddImportedInst to so I left it for the moment.

This will benefit from https://github.com/carbon-language/carbon-lang/pull/5517 but it's not dependent on it.

This removes the eval.cpp specialization for LookupImplWitness.

[danakj]

I have rebased this onto trunk to make it easier to review, and get tests to run again, so it now already includes #5517.

[danakj]

I think this is doing the right thing for simple cases, but I'm concerned that this approach won't scale up to more complicated examples. For example, if we have T:! I where .X = C(.Y), and the impl witness for type Z tells us that .Y = i32 and .X = C(i32), the comparison we perform will fail.

In order to get this right in general, we could do something along these lines:

• Substitute .Self for the type T in the requirements.
• Resolve the facet type by performing rewrites into the rewrites. (Either before or after the previous step, I suppose.)
• Check that the resulting LHS and RHS are equal after substitution.

Eg, for T:! I where .X = C(.Y), substituting in Z for .Self gives I where Z.(I.X) = C(Z.(I.Y)), which evaluates to I where C(i32) = C(i32), so the check should succeed.

In order for that kind of approach to work, we'd first need to use rewrite constraints as part of constant-evaluation of ImplWitnessAccess instructions. Perhaps we should be looking into that before we go too deep into checking that rewrite constraints are satisfied, so that we can reuse that work as part of the checking process?

I think I get what you're saying here, yeah. I will look into this first (but I have addressed the small stuff in this PR in the meantime and added tests that we'll want to have pass either way).

[danakj]

In order for that kind of approach to work, we'd first need to use rewrite constraints as part of constant-evaluation of ImplWitnessAccess instructions. Perhaps we should be looking into that before we go too deep into checking that rewrite constraints are satisfied, so that we can reuse that work as part of the checking process?

Given this simple example:

interface I { let X:! type; }

fn F(T:! I where .X = ()) {}

fn G(V:! I where .X = ()) {
  F(V);
}

I think you're saying that when we construct the specific for F(V), we want to evaluate the .X ImplWitnessAccess in the signature of F.

What we do is we evaluate the BindSymbolicName for T, which replaces it with the BindSymbolicName for V. We don't do anything with the ImplWitnessAccess in the type of T and it's never evaluated at a point where the witness is concrete (an ImplWitness).

So then I think what you're saying is that when evaluating BindSymbolicName for T once we have a CompileTimeBindValue for it, we want to construct basically a new witness table by re-evaluating the instructions in the witness table of the FacetType of the BindSymbolicName for T by calling ReplaceTypeWithConstantValue . Then comparing the table for each element that is an associated constant with the witness table of the type of the original BindSymbolicName for T.

Does that sound like what you're thinking?

[zygoloid]

Given this simple example:

interface I { let X:! type; }

fn F(T:! I where .X = ()) {}

fn G(V:! I where .X = ()) {
  F(V);
}

I think you're saying that when we construct the specific for F(V), we want to evaluate the .X ImplWitnessAccess in the signature of F.

I think it probably makes sense to do this check as part of the conversion of V to the type I where .X = (). (In this case, that's a no-op conversion so maybe we can skip this logic, but of course it wouldn't be in general.)

The left-hand side of the constraint here is .Self.X and the right-hand side is (). Substituting .Self = V into both produces an LHS of V.X and an RHS of (). The LHS is an ImplWitnessAccess naming X in V, and the type of V has a rewrite .X = (), so constant evaluation of that ImplWitnessAccess should result in () (even though the witness is still symbolic) -- that's the new step that we don't have yet, that ImplWitnessAccess evaluation should take into account rewrite rules in the type of the left-hand side to directly produce a result even when the impl witness itself is symbolic. That rewrite results in the LHS and RHS evaluating to the same constant, in this case (), so the check passes and we can allow the conversion of V to type I where .X = ().

[danakj]

Given this simple example:

interface I { let X:! type; }

fn F(T:! I where .X = ()) {}

fn G(V:! I where .X = ()) {
  F(V);
}

I think you're saying that when we construct the specific for F(V), we want to evaluate the .X ImplWitnessAccess in the signature of F.

I think it probably makes sense to do this check as part of the conversion of V to the type I where .X = (). (In this case, that's a no-op conversion so maybe we can skip this logic, but of course it wouldn't be in general.)

The left-hand side of the constraint here is .Self.X and the right-hand side is (). Substituting .Self = V into both produces an LHS of V.X and an RHS of (). The LHS is an ImplWitnessAccess naming X in V, and the type of V has a rewrite .X = (), so constant evaluation of that ImplWitnessAccess should result in () (even though the witness is still symbolic) -- that's the new step that we don't have yet, that ImplWitnessAccess evaluation should take into account rewrite rules in the type of the left-hand side to directly produce a result even when the impl witness itself is symbolic. That rewrite results in the LHS and RHS evaluating to the same constant, in this case (), so the check passes and we can allow the conversion of V to type I where .X = ().

When you say to substitute the query self type here for .Self, we can literally do this with Subst, I guess. Like we did in deduce?

But over there we said that was not ideal, and that we'd like to apply a specific instead. I am trying to wrap my head around how to construct a specific for the target facet type so that when we get constant values we would replace .Self with the query self type. But the FacetType in the query constraint is concrete in this example, even though there's a symbolic value in the rewrite. This is seemingly intentional, introduced in 33110d096cb0c089995dfbf5c1986d4d5c178dad. So we can't replace the .Self in the FacetType through eval. We will have to use Subst I guess.

But is this good?

[danakj]

https://github.com/carbon-language/carbon-lang/pull/5617 and its successors will be superceding this PR