diff --git a/toolchain/check/impl_lookup.cpp b/toolchain/check/impl_lookup.cpp index 2fbaa85cfdd4..0405ec6942f2 100644 --- a/toolchain/check/impl_lookup.cpp +++ b/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( + 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(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(result_witness_id)) { + CARBON_CHECK( + !context.insts().Is(result_witness_id)); + if (IsFinalWitness(context, result_witness_id)) { // Found a final witness, use it. - CARBON_CHECK( - !context.insts().Is(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(witness_inst_id)) { + if (IsFinalWitness(context, witness_inst_id)) { return context.constant_values().Get(witness_inst_id); } } diff --git a/toolchain/check/testdata/facet/period_self.carbon b/toolchain/check/testdata/facet/period_self.carbon index e54243a43a31..b59e40f8b0f5 100644 --- a/toolchain/check/testdata/facet/period_self.carbon +++ b/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]]";