From f0bae9637363bba24c3a5d1c8a072fbb53fd5168 Mon Sep 17 00:00:00 2001 From: Dana Jansens Date: Wed, 14 Oct 2026 16:44:37 +0000 Subject: [PATCH] Verify non-extend require constraints are satisfied at `impl as` definition (#7937) Rewrites in `extend requires` are used to set the witness table values of the impl. Rewrites in non-extend `requires` are treated as same-type constraints and must be true at the point of the impl definition. --- toolchain/check/facet_type.cpp | 22 +++++ toolchain/check/facet_type.h | 4 + toolchain/check/impl.cpp | 40 ++++++--- toolchain/check/testdata/for/actual.carbon | 6 +- ...uire_satisified_in_named_constraint.carbon | 81 +++++++++++++++++++ toolchain/check/type_completion.cpp | 17 +++- toolchain/diagnostics/kind.def | 1 + toolchain/sem_ir/identified_facet_type.cpp | 21 ++++- toolchain/sem_ir/identified_facet_type.h | 19 ++++- toolchain/sem_ir/stringify.cpp | 22 +++++ 10 files changed, 214 insertions(+), 19 deletions(-) diff --git a/toolchain/check/facet_type.cpp b/toolchain/check/facet_type.cpp index 241af7bd48ef..9122bd907326 100644 --- a/toolchain/check/facet_type.cpp +++ b/toolchain/check/facet_type.cpp @@ -705,6 +705,28 @@ auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, .specific_id = specific_id}}; } +auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, + SemIR::IdentifiedFacetType::Equivalent equiv, + SubstIdentifiedWitnessesCallbacks& callbacks) + -> SemIR::IdentifiedFacetType::Equivalent { + // SubstIdentifiedWitnesses allows the caller to cleverly replace witnesses + // coming from identify with their own. If we do this in the middle of + // identify, it means there is another caller waiting for identify and they + // may also want to do their own replacements. This would be problematic! But + // since during identify we only create specifics, and resolving them through + // eval should not end up here, we make note of that. + CARBON_CHECK(!context.eval_impl_lookup_to_identified_witness(), + "SubstIdentifiedWitnesses called during identify"); + + EvaluateSubstCallbacks subst_callbacks(&context, loc_id, &callbacks); + auto lhs_inst_id = SubstInst( + context, context.constant_values().GetInstId(equiv.lhs), subst_callbacks); + auto rhs_inst_id = SubstInst( + context, context.constant_values().GetInstId(equiv.rhs), subst_callbacks); + return {context.constant_values().Get(lhs_inst_id), + context.constant_values().Get(rhs_inst_id)}; +} + auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, SemIR::ConstantId const_id, SubstIdentifiedWitnessesCallbacks& callbacks) diff --git a/toolchain/check/facet_type.h b/toolchain/check/facet_type.h index 212b55df1c53..fb62bf29e880 100644 --- a/toolchain/check/facet_type.h +++ b/toolchain/check/facet_type.h @@ -118,6 +118,10 @@ auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, SemIR::IdentifiedFacetType::RequiredImpl req, SubstIdentifiedWitnessesCallbacks& callbacks) -> SemIR::IdentifiedFacetType::RequiredImpl; +auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, + SemIR::IdentifiedFacetType::Equivalent equiv, + SubstIdentifiedWitnessesCallbacks& callbacks) + -> SemIR::IdentifiedFacetType::Equivalent; auto SubstIdentifiedWitnesses(Context& context, SemIR::LocId loc_id, SemIR::ConstantId const_id, SubstIdentifiedWitnessesCallbacks& callbacks) diff --git a/toolchain/check/impl.cpp b/toolchain/check/impl.cpp index c616cc229640..8bef1e8620ab 100644 --- a/toolchain/check/impl.cpp +++ b/toolchain/check/impl.cpp @@ -883,12 +883,6 @@ auto CheckRequireDeclsSatisfied(Context& context, SemIR::LocId loc_id, return; } - // TODO: Check other kinds of constraints too: rewrites into targets other - // than `Self.(TargetInterface.__)` and same-type constraints. Consider maybe - // building a facet type that just excludes anything about the impl-as target - // interface, and then just perform lookup of Self as that facet type, so we - // don't have to re-implement all of the validation of impl lookup? - // The IdentifiedFacetType canonicalizes the self facets, so we do the same // for comparing with it. auto self_const_id = @@ -919,13 +913,11 @@ auto CheckRequireDeclsSatisfied(Context& context, SemIR::LocId loc_id, "implements `{2}`", SemIR::DeclaredFacetTypeId, InstIdAsConstant, SemIR::SpecificInterface); + auto facet_type = context.insts().GetAs( + context.constant_values().GetConstantInstId(full_constraint_id)); context.emitter().Emit( loc_id, IdentifiedRequireImplsNotImplemented, - context.insts() - .GetAs( - context.constant_values().GetConstantInstId( - full_constraint_id)) - .declared_facet_type_id, + facet_type.declared_facet_type_id, context.constant_values().GetInstId(req.self_facet_value), req.specific_interface); } @@ -935,6 +927,32 @@ auto CheckRequireDeclsSatisfied(Context& context, SemIR::LocId loc_id, } } + for (auto equiv : identified.equivalents()) { + // This replaces both IdentifiedWitness and ImplSelfWitness referring to + // this impl with the impl's ImplWitness. That causes any access through the + // witness to resolve to the value from the impl's witness table. + SubstWithImplWitness callbacks(&context, &impl); + auto subst_equiv = + SubstIdentifiedWitnesses(context, loc_id, equiv, callbacks); + + if (subst_equiv.lhs != subst_equiv.rhs) { + CARBON_DIAGNOSTIC(IdentifiedRequireImplsNotEquivalent, Error, + "constraint {0} being implemented requires that {1} " + "equals {2}; found {3} and {4}", + SemIR::DeclaredFacetTypeId, InstIdAsConstant, + InstIdAsConstant, InstIdAsConstant, InstIdAsConstant); + auto facet_type = context.insts().GetAs( + context.constant_values().GetConstantInstId(full_constraint_id)); + context.emitter().Emit( + loc_id, IdentifiedRequireImplsNotEquivalent, + facet_type.declared_facet_type_id, + context.constant_values().GetInstId(equiv.lhs), + context.constant_values().GetInstId(equiv.rhs), + context.constant_values().GetInstId(subst_equiv.lhs), + context.constant_values().GetInstId(subst_equiv.rhs)); + } + } + const auto& interface = context.interfaces().Get(impl.interface.interface_id); auto require_ids = diff --git a/toolchain/check/testdata/for/actual.carbon b/toolchain/check/testdata/for/actual.carbon index debc7757baca..45e0b43a6316 100644 --- a/toolchain/check/testdata/for/actual.carbon +++ b/toolchain/check/testdata/for/actual.carbon @@ -388,10 +388,10 @@ fn Read(generic y: Core.IntLiteral) { // CHECK:STDOUT: %return.param: ref @IntRange.as.Iterate.impl.Next.%Optional.loc11_72.1 (%Optional.b5c) = out_param call_param2 // CHECK:STDOUT: %return: ref @IntRange.as.Iterate.impl.Next.%Optional.loc11_72.1 (%Optional.b5c) = return_slot %return.param // CHECK:STDOUT: } -// CHECK:STDOUT: %Iterate.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant.loc9_87.2, %impl_witness_assoc_constant.loc9_87.1, %IntRange.as.Iterate.impl.NewCursor.decl, %IntRange.as.Iterate.impl.Next.decl), @IntRange.as.Iterate.impl [concrete] +// CHECK:STDOUT: %Iterate.impl_witness_table = impl_witness_table (%impl_witness_assoc_constant.loc9_87.1, %impl_witness_assoc_constant.loc9_87.2, %IntRange.as.Iterate.impl.NewCursor.decl, %IntRange.as.Iterate.impl.Next.decl), @IntRange.as.Iterate.impl [concrete] // CHECK:STDOUT: %Iterate.impl_witness.loc9_87.1: = impl_witness %Iterate.impl_witness_table, @IntRange.as.Iterate.impl(constants.%N) [symbolic = %Iterate.impl_witness.loc9_87.2 (constants.%Iterate.impl_witness)] -// CHECK:STDOUT: %impl_witness_assoc_constant.loc9_87.1: %Destroy.type = impl_witness_assoc_constant constants.%Destroy.facet.e3e [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.e3e)] -// CHECK:STDOUT: %impl_witness_assoc_constant.loc9_87.2: %facet_type.f48 = impl_witness_assoc_constant constants.%facet_value [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)] +// CHECK:STDOUT: %impl_witness_assoc_constant.loc9_87.1: %facet_type.f48 = impl_witness_assoc_constant constants.%facet_value [symbolic = %facet_value.loc9_85.1 (constants.%facet_value)] +// CHECK:STDOUT: %impl_witness_assoc_constant.loc9_87.2: %Destroy.type = impl_witness_assoc_constant constants.%Destroy.facet.e3e [symbolic = %Destroy.facet.loc9_54.1 (constants.%Destroy.facet.e3e)] // CHECK:STDOUT: // CHECK:STDOUT: !members: // CHECK:STDOUT: .N = diff --git a/toolchain/check/testdata/impl/require_satisified_in_named_constraint.carbon b/toolchain/check/testdata/impl/require_satisified_in_named_constraint.carbon index ef864c0c24d5..8dd2d9450b79 100644 --- a/toolchain/check/testdata/impl/require_satisified_in_named_constraint.carbon +++ b/toolchain/check/testdata/impl/require_satisified_in_named_constraint.carbon @@ -134,3 +134,84 @@ impl () as Z(B); impl () as N(A) {} impl () as Z(B) {} + +// --- require_non_extended_rewrite.carbon +library "[[@TEST_NAME]]"; + +interface Y {} +interface Z { let Z1: type; } + +constraint N { + extend require impls Y; + require impls Z where .Z1 = (); +} + +impl () as N; + +// Match the requirement. +impl () as Z where .Z1 = (); + +impl () as N {} + +impl () as Z where .Z1 = () {} + +// --- fail_require_non_extended_rewrite_wrong_type.carbon +library "[[@TEST_NAME]]"; + +interface Y {} +interface Z { let Z1: type; } + +constraint N { + extend require impls Y; + require impls Z where .Z1 = (); +} + +impl () as N; + +// Wrong type for the requirement. +impl () as Z where .Z1 = {}; + +// CHECK:STDERR: fail_require_non_extended_rewrite_wrong_type.carbon:[[@LINE+8]]:1: error: constraint `N` being implemented requires that `().(Z.Z1)` equals `()`; found `{}` and `()` [IdentifiedRequireImplsNotEquivalent] +// CHECK:STDERR: impl () as N {} +// CHECK:STDERR: ^~~~~~~~~~~~~~ +// CHECK:STDERR: +// CHECK:STDERR: fail_require_non_extended_rewrite_wrong_type.carbon:[[@LINE-6]]:1: error: impl declared but not defined [ImplMissingDefinition] +// CHECK:STDERR: impl () as Z where .Z1 = {}; +// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~ +// CHECK:STDERR: +impl () as N {} + +impl () as Z where .Z1 = () {} + +// --- require_non_extended_rewrite_same_interface.carbon +library "[[@TEST_NAME]]"; + +interface Z { let Z1: type; } + +constraint N { + // Extend Z without a rewrite. + extend require impls Z; + // But require `.Z1` is () anyway. + require impls Z where .Z1 = (); +} + +impl () as N where .Z1 = () {} + +// --- fail_require_non_extended_rewrite_same_interface_wrong_type.carbon +library "[[@TEST_NAME]]"; + +interface Z { let Z1: type; } + +constraint N { + // Extend Z without a rewrite. + extend require impls Z; + // But require .Z1 is () anyway. + require impls Z where .Z1 = (); +} + +// Wrong type for `.Z1`. +// CHECK:STDERR: fail_require_non_extended_rewrite_same_interface_wrong_type.carbon:[[@LINE+4]]:1: error: constraint `N where .(Z.Z1) = {}` being implemented requires that `().(Z.Z1)` equals `()`; found `{}` and `()` [IdentifiedRequireImplsNotEquivalent] +// CHECK:STDERR: impl () as N where .Z1 = {} {} +// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +// CHECK:STDERR: +impl () as N where .Z1 = {} {} diff --git a/toolchain/check/type_completion.cpp b/toolchain/check/type_completion.cpp index aba096d9ce7f..cd3a6e439873 100644 --- a/toolchain/check/type_completion.cpp +++ b/toolchain/check/type_completion.cpp @@ -1030,6 +1030,7 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id, llvm::SmallVector extends; llvm::SmallVector impls; llvm::SmallVector rewrites; + llvm::SmallVector equivalents; while (!work.empty()) { SelfImplsFacetType next_impls = work.pop_back_val(); @@ -1076,8 +1077,19 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id, rewrites, llvm::map_range(declared_facet_type.rewrite_constraints, rewrite_as_constants)); } else { - // TODO: Store the rewrites as equality constraints. + auto rewrite_as_constants = + [&](auto rewrite) -> SemIR::IdentifiedFacetType::Equivalent { + return {context.constant_values().Get( + GetImplWitnessAccessWithoutSubstitution(context, + rewrite.lhs_id)), + context.constant_values().Get(rewrite.rhs_id)}; + }; + llvm::append_range( + equivalents, llvm::map_range(declared_facet_type.rewrite_constraints, + rewrite_as_constants)); } + // TODO: Store equivalent constraints from the `declared_facet_type` once + // they exist. if (declared_facet_type.extend_named_constraints.empty() && declared_facet_type.self_impls_named_constraints.empty() && @@ -1265,9 +1277,8 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id, } } - // TODO: Process other kinds of requirements. return context.identified_facet_types().Add( - {key, partially_identified, extends, impls, rewrites}); + {key, partially_identified, extends, impls, rewrites, equivalents}); } auto TryToIdentifyFacetType(Context& context, SemIR::LocId loc_id, diff --git a/toolchain/diagnostics/kind.def b/toolchain/diagnostics/kind.def index 936fa93ced8c..cb24c664ea87 100644 --- a/toolchain/diagnostics/kind.def +++ b/toolchain/diagnostics/kind.def @@ -427,6 +427,7 @@ CARBON_DIAGNOSTIC_KIND(RequireImplsMissingSelfEmptyFacetType) CARBON_DIAGNOSTIC_KIND(RequireImplsIncompleteFacetType) CARBON_DIAGNOSTIC_KIND(RequireImplsReferenceCycle) CARBON_DIAGNOSTIC_KIND(RequireImplsUnidentifiedFacetType) +CARBON_DIAGNOSTIC_KIND(IdentifiedRequireImplsNotEquivalent) CARBON_DIAGNOSTIC_KIND(IdentifiedRequireImplsNotImplemented) CARBON_DIAGNOSTIC_KIND(InterfaceRequireImplsNotImplemented) CARBON_DIAGNOSTIC_KIND(RequireInWrongScope) diff --git a/toolchain/sem_ir/identified_facet_type.cpp b/toolchain/sem_ir/identified_facet_type.cpp index 3a3ccdf6a94a..42b6a6358f98 100644 --- a/toolchain/sem_ir/identified_facet_type.cpp +++ b/toolchain/sem_ir/identified_facet_type.cpp @@ -41,10 +41,25 @@ static auto RequiredLess(const IdentifiedFacetType::RequiredImpl& lhs, rhs.specific_interface.specific_id.index); } +// Canonically ordered by the numerical ids. +static auto RewriteLess(const IdentifiedFacetType::Rewrite& lhs, + const IdentifiedFacetType::Rewrite& rhs) -> bool { + return std::tie(lhs.lhs.index, lhs.rhs.index) < + std::tie(rhs.lhs.index, rhs.rhs.index); +} + +// Canonically ordered by the numerical ids. +static auto EquivalentLess(const IdentifiedFacetType::Equivalent& lhs, + const IdentifiedFacetType::Equivalent& rhs) -> bool { + return std::tie(lhs.lhs.index, lhs.rhs.index) < + std::tie(rhs.lhs.index, rhs.rhs.index); +} + IdentifiedFacetType::IdentifiedFacetType( IdentifiedFacetTypeKey key, bool partially_identified, llvm::ArrayRef extends, - llvm::ArrayRef self_impls, llvm::ArrayRef rewrites) + llvm::ArrayRef self_impls, llvm::ArrayRef rewrites, + llvm::ArrayRef equivalents) : key_(key) { required_impls_.reserve(extends.size() + self_impls.size()); llvm::append_range(required_impls_, extends); @@ -62,6 +77,7 @@ IdentifiedFacetType::IdentifiedFacetType( llvm::append_range(required_impls_, self_impls); SortAndDeduplicate(required_impls_, RequiredLess); + SortAndDeduplicate(required_impls_, RequiredLess); if (partially_identified) { // This marks the IdentifiedFacetType as being partially identified, and @@ -72,6 +88,9 @@ IdentifiedFacetType::IdentifiedFacetType( } rewrites_.assign(rewrites); + SortAndDeduplicate(rewrites_, RewriteLess); + equivalents_.assign(equivalents); + SortAndDeduplicate(equivalents_, EquivalentLess); } auto AddCanonicalWitnessesBlock(File& sem_ir, diff --git a/toolchain/sem_ir/identified_facet_type.h b/toolchain/sem_ir/identified_facet_type.h index d942ce4af525..7f739053807d 100644 --- a/toolchain/sem_ir/identified_facet_type.h +++ b/toolchain/sem_ir/identified_facet_type.h @@ -49,11 +49,19 @@ struct IdentifiedFacetType { friend auto operator==(const Rewrite& lhs, const Rewrite& rhs) -> bool = default; }; + struct Equivalent { + ConstantId lhs; + ConstantId rhs; + + friend auto operator==(const Equivalent& lhs, const Equivalent& rhs) + -> bool = default; + }; IdentifiedFacetType(IdentifiedFacetTypeKey key, bool partially_identified, llvm::ArrayRef extends, llvm::ArrayRef self_impls, - llvm::ArrayRef rewrites); + llvm::ArrayRef rewrites, + llvm::ArrayRef equivalents); // The order here defines the order of impl witnesses for this facet type. auto required_impls() const -> llvm::ArrayRef { @@ -61,6 +69,9 @@ struct IdentifiedFacetType { } auto rewrites() const -> llvm::ArrayRef { return rewrites_; } + auto equivalents() const -> llvm::ArrayRef { + return equivalents_; + } // Can this be used to the right of an `as` in an `impl` declaration? auto is_valid_impl_as_target() const -> bool { @@ -105,6 +116,12 @@ struct IdentifiedFacetType { // non-extended require decl are treated as same-type requirements. llvm::SmallVector rewrites_; + // Same-type requirements from a facet type and any named constraints that it + // references, flattened to a single list. This includes rewrite requirements + // from non-extended require decls, which are treated as being same-type + // requirements. + llvm::SmallVector equivalents_; + // The single interface from `required_impls` to implement if this is // the facet type to the right of an `impl`...`as`, or `None` if no such // single interface. diff --git a/toolchain/sem_ir/stringify.cpp b/toolchain/sem_ir/stringify.cpp index a7ff85c1f49b..fb2e066eeb62 100644 --- a/toolchain/sem_ir/stringify.cpp +++ b/toolchain/sem_ir/stringify.cpp @@ -761,6 +761,10 @@ class Stringifier { sem_ir_->insts().TryGetAs(witness_inst_id)) { specific_interface = sem_ir_->specific_interfaces().Get( self_witness->specific_interface_id); + } else if (auto id_witness = sem_ir_->insts().TryGetAs( + witness_inst_id)) { + specific_interface = sem_ir_->specific_interfaces().Get( + id_witness->query_specific_interface_id); } else { auto lookup = sem_ir_->insts().GetAs(witness_inst_id); specific_interface = sem_ir_->specific_interfaces().Get( @@ -818,6 +822,18 @@ class Stringifier { if (!is_period_self) { step_stack_->PushInstId(self_witness->period_self); } + } else if (auto lookup = sem_ir_->insts().TryGetAs( + witness_inst_id)) { + bool is_period_self = false; + if (auto sym_name = sem_ir_->insts().TryGetAs( + lookup->query_self_inst_id)) { + auto name_id = + sem_ir_->entity_names().Get(sym_name->entity_name_id).name_id; + is_period_self = (name_id == NameId::PeriodSelf); + } + if (!is_period_self) { + step_stack_->PushInstId(lookup->query_self_inst_id); + } } else if (auto lookup = sem_ir_->insts().TryGetAs( witness_inst_id)) { bool is_period_self = false; @@ -861,6 +877,12 @@ class Stringifier { sem_ir_->ints().Get(inst.int_id).print(*out_, /*isSigned=*/true); } + auto StringifyInst(InstId /*inst_id*/, IdentifiedWitness inst) -> void { + step_stack_->Push( + inst.query_self_inst_id, " as ", + sem_ir_->specific_interfaces().Get(inst.query_specific_interface_id)); + } + auto StringifyInst(InstId /*inst_id*/, LookupImplWitness inst) -> void { step_stack_->Push( inst.query_self_inst_id, " as ",