Skip to content

Commit 0c761a9

Browse files
authored
Find the builtin TypeCanAggregateDestroy in the FacetType for facet values (carbon-language#6119)
When doing impl lookup with a constraint facet type including the builtin `TypeCanAggregateDestroy`, we look at the type to see if it satisfies it. However if the type is a facet value, we need to look at the FacetType to see if the eventual concrete type is going to satisfy it. Note that we can do this check up front in the `LookupImplWitness()` function without creating a symbolic instruction to be modified by future specifics with a more precise type for the facet value, because the result of `TypeCanAggregateDestroy` does not actually provide a witness, so we don't need the final specific type. This was noticed by removing the "shortcut" in convert for converting a `FacetAccessType(<symbolic binding>)` to `typeof(<symbolic binding>)`. By removing the shortcut, we go into impl lookup when checking `impl` decls containing `TypeCanAggregateDestroy` via deduce.
1 parent 57c0fde commit 0c761a9

File tree

4 files changed

+34
-13
lines changed

4 files changed

+34
-13
lines changed

toolchain/check/convert.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1225,9 +1225,6 @@ static auto PerformBuiltinConversion(
12251225
// form. We can skip past the whole impl lookup step then and do that
12261226
// here.
12271227
//
1228-
// See also test:
1229-
// facet_access_type_converts_back_to_original_facet_value.carbon
1230-
//
12311228
// TODO: This instruction is going to become a `SymbolicBindingType`, so
12321229
// we'll need to handle that instead.
12331230
auto const_type_inst_id =

toolchain/check/eval_inst.cpp

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -210,14 +210,12 @@ auto EvalConstantInst(Context& context, SemIR::FacetValue inst)
210210
if (auto access =
211211
context.insts().TryGetAs<SemIR::FacetAccessType>(inst.type_inst_id)) {
212212
auto bind_id = access->facet_value_inst_id;
213-
auto bind = context.insts().Get(bind_id);
214-
if (bind.Is<SemIR::BindSymbolicName>()) {
215-
// If the FacetTypes are the same, then the FacetValue didn't add/remove
216-
// any witnesses.
217-
if (bind.type_id() == inst.type_id) {
218-
return ConstantEvalResult::Existing(
219-
context.constant_values().Get(bind_id));
220-
}
213+
auto bind = context.insts().TryGetAs<SemIR::BindSymbolicName>(bind_id);
214+
// If the FacetTypes are the same, then the FacetValue didn't add/remove
215+
// any witnesses.
216+
if (bind.has_value() && bind->type_id == inst.type_id) {
217+
return ConstantEvalResult::Existing(
218+
context.constant_values().Get(bind_id));
221219
}
222220
}
223221

toolchain/check/impl_lookup.cpp

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -545,8 +545,19 @@ static auto GetOrAddLookupImplWitness(Context& context, SemIR::LocId loc_id,
545545
// Returns true if the `Self` should impl `Destroy`.
546546
static auto TypeCanDestroy(Context& context,
547547
SemIR::ConstantId query_self_const_id) -> bool {
548-
auto inst = context.insts().Get(
549-
context.constant_values().GetInstId(query_self_const_id));
548+
auto inst = context.insts().Get(context.constant_values().GetInstId(
549+
GetCanonicalizedFacetOrTypeValue(context, query_self_const_id)));
550+
551+
// For facet values, look if the FacetType provides the same.
552+
if (auto facet_type =
553+
context.types().TryGetAs<SemIR::FacetType>(inst.type_id())) {
554+
const auto& info = context.facet_types().Get(facet_type->facet_type_id);
555+
if (info.builtin_constraint_mask.HasAnyOf(
556+
SemIR::BuiltinConstraintMask::TypeCanDestroy)) {
557+
return true;
558+
}
559+
}
560+
550561
CARBON_KIND_SWITCH(inst) {
551562
case CARBON_KIND(SemIR::ClassType class_type): {
552563
auto class_info = context.classes().Get(class_type.class_id);

toolchain/check/testdata/builtins/type/can_destroy.carbon

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,21 @@ fn G() {
3838
//@dump-sem-ir-end
3939
}
4040

41+
// --- symbolic.carbon
42+
library "[[@TEST_NAME]]";
43+
44+
interface Z {}
45+
46+
fn CanDestroy() -> type = "type.can_destroy";
47+
48+
fn G(U:! CanDestroy()) {}
49+
50+
fn F(T:! Z & CanDestroy()) {
51+
// Requires a conversion (and thus impl lookup into `T`) since `T` and `U`
52+
// have different (but compatible) facet types.
53+
G(T);
54+
}
55+
4156
// --- fail_incomplete.carbon
4257
library "[[@TEST_NAME]]";
4358

0 commit comments

Comments
 (0)