IdentifiedWitness is not a final witness (#7985)

If we perform impl lookup during identify by resolving a specific, we
can run into IdentifiedWitnesses in a FacetValue. If the witness is the
only one in the FacetValue we may use it as a final witness, which is
not correct. IdentifiedWitness is not a final witness.

To test this, we add a test that places an IdentifiedWitness into a
FacetValue and then uses that facet value to get an associated constant.
If treated as a final witness, we try to do a lookup where the query
self contains the IdentifiedWitness and we crash coming across it in the
TypeIterator. We should never come across an IdentifiedWitness in an
impl lookup query.

The test also shows a case that should work but does not because of
`impl_lookup_no_symbolic_final_lookups`. We set
`impl_lookup_no_symbolic_final_lookups` while collecting witnesses to
avoid cycles in impl lookup. This test fails because of that. It
prevents us from forming a correct specific for the class `C` by
creating a specific where `C.C1` is a symbolic value. Later we try to
form the specific again, where we would see a concrete value for `C.C1`,
but the specific already exists, so we can't get to the concrete value.

toolchain/check/impl_lookup.cpp

@@ -37,6 +37,12 @@
 
 namespace Carbon::Check {
 
+static auto IsFinalWitness(Context& context, SemIR::InstId inst_id) -> bool {
+  return !context.insts()
+              .IsOneOf<SemIR::LookupImplWitness, SemIR::IdentifiedWitness>(
+                  inst_id);
+}
+
 // Returns IRs which are allowed to define an `impl` involving the arguments.
 // This is limited by the orphan rule.
 static auto FindAssociatedImportIRs(
@@ -375,12 +381,15 @@ static auto CollectFacetWitnessSources(
       //
       // TODO: This prevents some legitimate code from working, as we can't find
       // some witnesses that involve concrete associated constants from a
-      // symbolic facet. We could consider another approach: When we identify
-      // and replace `.Self` with `facet_const_id` in each constraint in its
-      // facet type, remove that constraint from the type of `facet_const_id`.
-      // Then each cycle back through to `facet_const_id` will have a smaller
-      // type until it runs out of constraints. See for example the
-      // fail_todo_concrete_access_witness_m_in_impls_constraint.carbon test.
+      // symbolic facet, and this can cause us to form incorrect specifics. See
+      // for example the test:
+      // fail_todo_specific_resolves_final_impl_while_collecting_witnesses.carbon.
+      //
+      // We could consider another approach: When we identify and replace
+      // `.Self` with `facet_const_id` in each constraint in its facet type,
+      // remove that constraint from the type of `facet_const_id`. Then each
+      // cycle back through to `facet_const_id` will have a smaller type until
+      // it runs out of constraints.
       {
         IncrementScope inc(context.impl_lookup_no_symbolic_final_lookups());
         req = EvaluateIdentifiedWitnesses(context, loc_id, req);
@@ -394,7 +403,7 @@ static auto CollectFacetWitnessSources(
             context.inst_blocks().Get(facet_value->witnesses_block_id)[index];
         // Using a non-final witness here would preclude finding a final witness
         // from other places.
-        if (!context.insts().Is<SemIR::LookupImplWitness>(witness_id)) {
+        if (IsFinalWitness(context, witness_id)) {
           final_witness_id = witness_id;
         }
       }
@@ -989,10 +998,10 @@ auto LookupImplWitness(Context& context, SemIR::LocId loc_id,
          .query_specific_interface_id =
              context.specific_interfaces().Add(req_impl.specific_interface)});
     result_witness_id = context.constant_values().GetInstId(witness_const_id);
-    if (!context.insts().Is<SemIR::LookupImplWitness>(result_witness_id)) {
+    CARBON_CHECK(
+        !context.insts().Is<SemIR::IdentifiedWitness>(result_witness_id));
+    if (IsFinalWitness(context, result_witness_id)) {
       // Found a final witness, use it.
-      CARBON_CHECK(
-          !context.insts().Is<SemIR::IdentifiedWitness>(result_witness_id));
       result_witness_ids.push_back(result_witness_id);
       continue;
     }
@@ -1213,7 +1222,7 @@ auto EvalLookupSingleFinalWitness(Context& context, SemIR::LocId loc_id,
       CARBON_CHECK(witnesses.size() == 1);
       auto witness_inst_id = witnesses.front();
       // Only use the witness in monomoprhization if it's a final witness.
-      if (!context.insts().Is<SemIR::LookupImplWitness>(witness_inst_id)) {
+      if (IsFinalWitness(context, witness_inst_id)) {
         return context.constant_values().Get(witness_inst_id);
       }
     }

toolchain/check/testdata/facet/period_self.carbon

@@ -399,6 +399,45 @@ interface Z(T: Y) {}
 // converting it to `Y`.
 fn F(generic T: L where .W impls Y and .Self impls Z(.W) and .Self impls M, a: T.W) -> () { return a; }
 
+// --- fail_todo_specific_resolves_final_impl_while_collecting_witnesses.carbon
+library "[[@TEST_NAME]]";
+
+interface L { let L1: type; }
+
+interface M {}
+final impl forall [T: M] T as L where .L1 = () {}
+
+interface Y { let Y1: L; }
+class C(U: Y, v: U.Y1.L1) {
+  // The type `U.Y1.L1` remains symbolic here, since we don't know that `U.Y1`
+  // impls `M` and can't use the `final impl` above. So `C1` is a symbolic type
+  // in the self specific.
+  alias C1 = U.Y1.L1;
+}
+
+// When we form the specific `C(T, ())` for the return type, we replace `U`
+// with `T` which knows that `.Y1 impls M`. This means `T.Y1.L1 = ()` so
+// `C(T, ()).C1 = ()`.
+//
+// However while forming that specific we must convert `T` to `Y` which does
+// the lookup `T as Y`. This identifies the type of `T` to collect witnesses
+// (like `.Y1 impls M`). But we also collect the witness
+// `C(.Self, ()) impls M` which forms the specific `C(T, ())`.
+//
+// During the collection of witnesses, we prevent cycles by preventing witnesses
+// that are substituted to replace `.Self` from evaluating. That means the
+// specific `C(T, ())` is formed without being able to use the `final impl` to
+// resolve the access of `C(T, ()).C1` which would remain symbolic.
+//
+// This creates a bug in the toolchain since the specific is now wrong and we're
+// unable to get the concrete value of `C(T, ()).C1`.
+fn F(generic T: Y where .Y1 impls M and C(.Self, ()) impls M) -> C(T, ()).C1 {
+  // CHECK:STDERR: fail_todo_specific_resolves_final_impl_while_collecting_witnesses.carbon:[[@LINE+3]]:3-12: error: cannot implicitly convert expression of type `()` to `T.(Y.Y1).(L.L1)` [ConversionFailure]
+  // CHECK:STDERR: fail_todo_specific_resolves_final_impl_while_collecting_witnesses.carbon:[[@LINE+2]]:3-12: note: type `()` does not implement interface `Core.ImplicitAs(T.(Y.Y1).(L.L1))` [MissingImplInMemberAccessInContext]
+  // CHECK:STDERR:
+  return ();
+}
+
 // --- concrete_access_witness_m_in_extend_constraint.carbon
 library "[[@TEST_NAME]]";