Avoid symbolic witnesses for .Self in an impl decl (#7564)

Point symbolic witnesses into `.Self` written inside an impl decl at the
impl that is being declared. This is tricky because the impl does not
yet exist. So we use a new instruction `ImplSelfWitness` which _will_ be
replaced by the `ImplWitness` once it becomes available. The
`ImplSelfWitness` acts like a symbolic witness, except it does not
perform lookup, since we know which impl we will get a witness from.

This prevents us from finding other impls when performing lookups into
`.Self` in an impl decl, which produces incorrect/incoherent results.
This commit is contained in:
Dana Jansens
2026-07-29 16:25:23 +00:00
committed by GitHub
parent 2ac425e591
commit f51c075f8b
94 changed files with 3221 additions and 2797 deletions
@@ -83,10 +83,10 @@ interface C {
// CHECK:STDOUT: %J2.type: type = facet_type <@J2> [concrete]
// CHECK:STDOUT: %Self.c1f: %J2.type = symbolic_binding Self, 0 [symbolic]
// CHECK:STDOUT: %Self.as_type: type = facet_access_type %Self.c1f [symbolic]
// CHECK:STDOUT: %I2.lookup_impl_witness.b5c: <witness> = lookup_impl_witness %Self.c1f, @I2 [symbolic]
// CHECK:STDOUT: %.be9: require_specific_def_type = require_specific_def @V.as_type.as.I2.impl(%Self.c1f) [symbolic]
// CHECK:STDOUT: %I2.facet.39b: %I2.type = facet_value %Self.as_type, (%I2.lookup_impl_witness.b5c) [symbolic]
// CHECK:STDOUT: %impl.elem0.422: type = impl_witness_access %I2.lookup_impl_witness.b5c, element0 [symbolic]
// CHECK:STDOUT: %I2.lookup_impl_witness: <witness> = lookup_impl_witness %Self.c1f, @I2 [symbolic]
// CHECK:STDOUT: %.a84: require_specific_def_type = require_specific_def @V.as_type.as.I2.impl(%Self.c1f) [symbolic]
// CHECK:STDOUT: %I2.facet.39b: %I2.type = facet_value %Self.as_type, (%I2.lookup_impl_witness) [symbolic]
// CHECK:STDOUT: %impl.elem0.422: type = impl_witness_access %I2.lookup_impl_witness, element0 [symbolic]
// CHECK:STDOUT: %.932: Core.Form = init_form %impl.elem0.422 [symbolic]
// CHECK:STDOUT: %pattern_type.ff8: type = pattern_type %impl.elem0.422 [symbolic]
// CHECK:STDOUT: %return.param_patt: %pattern_type.ff8 = out_param_pattern [symbolic]
@@ -114,9 +114,9 @@ interface C {
// CHECK:STDOUT: %return.patt.loc14_11.1: @J2.WithSelf.F2.%pattern_type (%pattern_type.ff8) = return_slot_pattern %return.param_patt.loc14_14.1, %U2.ref [symbolic = %return.patt.loc14_11.2 (constants.%return.patt)]
// CHECK:STDOUT: } {
// CHECK:STDOUT: %Self.as_type.loc14_14.2: type = facet_access_type @J2.%Self [symbolic = %Self.as_type.loc14_14.1 (constants.%Self.as_type)]
// CHECK:STDOUT: %I2.facet.loc14_14.2: %I2.type = facet_value %Self.as_type.loc14_14.2, (constants.%I2.lookup_impl_witness.b5c) [symbolic = %I2.facet.loc14_14.1 (constants.%I2.facet.39b)]
// CHECK:STDOUT: %I2.facet.loc14_14.2: %I2.type = facet_value %Self.as_type.loc14_14.2, (constants.%I2.lookup_impl_witness) [symbolic = %I2.facet.loc14_14.1 (constants.%I2.facet.39b)]
// CHECK:STDOUT: %.loc14_14.3: %I2.type = converted @J2.%Self, %I2.facet.loc14_14.2 [symbolic = %I2.facet.loc14_14.1 (constants.%I2.facet.39b)]
// CHECK:STDOUT: %impl.elem0.loc14_14.2: type = impl_witness_access constants.%I2.lookup_impl_witness.b5c, element0 [symbolic = %impl.elem0.loc14_14.1 (constants.%impl.elem0.422)]
// CHECK:STDOUT: %impl.elem0.loc14_14.2: type = impl_witness_access constants.%I2.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc14_14.1 (constants.%impl.elem0.422)]
// CHECK:STDOUT: %U2.ref: type = name_ref U2, %impl.elem0.loc14_14.2 [symbolic = %impl.elem0.loc14_14.1 (constants.%impl.elem0.422)]
// CHECK:STDOUT: %.loc14_14.4: Core.Form = init_form %U2.ref [symbolic = %.loc14_14.2 (constants.%.932)]
// CHECK:STDOUT: %return.param: ref @J2.WithSelf.F2.%impl.elem0.loc14_14.1 (%impl.elem0.422) = out_param call_param0
@@ -138,8 +138,8 @@ interface C {
// CHECK:STDOUT: generic fn @J2.WithSelf.F2(@J2.%Self: %J2.type) {
// CHECK:STDOUT: %Self: %J2.type = symbolic_binding Self, 0 [symbolic = %Self (constants.%Self.c1f)]
// CHECK:STDOUT: %Self.as_type.loc14_14.1: type = facet_access_type %Self [symbolic = %Self.as_type.loc14_14.1 (constants.%Self.as_type)]
// CHECK:STDOUT: %.loc14_14.1: require_specific_def_type = require_specific_def @V.as_type.as.I2.impl(%Self) [symbolic = %.loc14_14.1 (constants.%.be9)]
// CHECK:STDOUT: %I2.lookup_impl_witness: <witness> = lookup_impl_witness %Self, @I2 [symbolic = %I2.lookup_impl_witness (constants.%I2.lookup_impl_witness.b5c)]
// CHECK:STDOUT: %.loc14_14.1: require_specific_def_type = require_specific_def @V.as_type.as.I2.impl(%Self) [symbolic = %.loc14_14.1 (constants.%.a84)]
// CHECK:STDOUT: %I2.lookup_impl_witness: <witness> = lookup_impl_witness %Self, @I2 [symbolic = %I2.lookup_impl_witness (constants.%I2.lookup_impl_witness)]
// CHECK:STDOUT: %I2.facet.loc14_14.1: %I2.type = facet_value %Self.as_type.loc14_14.1, (%I2.lookup_impl_witness) [symbolic = %I2.facet.loc14_14.1 (constants.%I2.facet.39b)]
// CHECK:STDOUT: %impl.elem0.loc14_14.1: type = impl_witness_access %I2.lookup_impl_witness, element0 [symbolic = %impl.elem0.loc14_14.1 (constants.%impl.elem0.422)]
// CHECK:STDOUT: %.loc14_14.2: Core.Form = init_form %impl.elem0.loc14_14.1 [symbolic = %.loc14_14.2 (constants.%.932)]
@@ -155,8 +155,8 @@ interface C {
// CHECK:STDOUT: specific @J2.WithSelf.F2(constants.%Self.c1f) {
// CHECK:STDOUT: %Self => constants.%Self.c1f
// CHECK:STDOUT: %Self.as_type.loc14_14.1 => constants.%Self.as_type
// CHECK:STDOUT: %.loc14_14.1 => constants.%.be9
// CHECK:STDOUT: %I2.lookup_impl_witness => constants.%I2.lookup_impl_witness.b5c
// CHECK:STDOUT: %.loc14_14.1 => constants.%.a84
// CHECK:STDOUT: %I2.lookup_impl_witness => constants.%I2.lookup_impl_witness
// CHECK:STDOUT: %I2.facet.loc14_14.1 => constants.%I2.facet.39b
// CHECK:STDOUT: %impl.elem0.loc14_14.1 => constants.%impl.elem0.422
// CHECK:STDOUT: %.loc14_14.2 => constants.%.932
+6 -6
View File
@@ -151,11 +151,11 @@ interface A(T: type) {
// CHECK:STDOUT: %empty_struct: %empty_struct_type = struct_value () [concrete]
// CHECK:STDOUT: %.Self.frozen: %I.type = symbolic_binding .Self [symbolic_self]
// CHECK:STDOUT: %.Self.frozen.as_type: type = facet_access_type %.Self.frozen [symbolic_self]
// CHECK:STDOUT: %I.lookup_impl_witness.ced: <witness> = lookup_impl_witness %.Self.frozen, @I [symbolic_self]
// CHECK:STDOUT: %impl.elem0.aef: %C = impl_witness_access %I.lookup_impl_witness.ced, element0 [symbolic_self]
// CHECK:STDOUT: %.f01: <witness> = impl_self_witness %.Self.frozen, @I [symbolic_self]
// CHECK:STDOUT: %impl.elem0.419: %C = impl_witness_access %.f01, element0 [symbolic_self]
// CHECK:STDOUT: %.Self: %I.type = symbolic_binding .Self [symbolic_self]
// CHECK:STDOUT: %I.lookup_impl_witness.78b: <witness> = lookup_impl_witness %.Self, @I [symbolic_self]
// CHECK:STDOUT: %impl.elem0.cc9: %C = impl_witness_access %I.lookup_impl_witness.78b, element0 [symbolic_self]
// CHECK:STDOUT: %.00f: <witness> = impl_self_witness %.Self, @I [symbolic_self]
// CHECK:STDOUT: %impl.elem0.adf: %C = impl_witness_access %.00f, element0 [symbolic_self]
// CHECK:STDOUT: }
// CHECK:STDOUT:
// CHECK:STDOUT: file {
@@ -175,11 +175,11 @@ interface A(T: type) {
// CHECK:STDOUT: %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.frozen.as_type]
// CHECK:STDOUT: %.loc16_20: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.frozen.as_type]
// CHECK:STDOUT: %T.ref: %I.assoc_type = name_ref T, @T.%assoc0 [concrete = constants.%assoc0]
// CHECK:STDOUT: %impl.elem0.loc16_20.1: %C = impl_witness_access constants.%I.lookup_impl_witness.ced, element0 [symbolic_self = constants.%impl.elem0.aef]
// CHECK:STDOUT: %impl.elem0.loc16_20.1: %C = impl_witness_access constants.%.f01, element0 [symbolic_self = constants.%impl.elem0.419]
// CHECK:STDOUT: %.loc16_27: %empty_struct_type = struct_literal () [concrete = constants.%empty_struct]
// CHECK:STDOUT: %C.ref: type = name_ref C, file.%C.decl [concrete = constants.%C]
// CHECK:STDOUT: %rewrite.loc16_23.1 = requirement_rewrite %impl.elem0.loc16_20.1, <error> [concrete]
// CHECK:STDOUT: %impl.elem0.loc16_20.2: %C = impl_witness_access constants.%I.lookup_impl_witness.78b, element0 [symbolic_self = constants.%impl.elem0.cc9]
// CHECK:STDOUT: %impl.elem0.loc16_20.2: %C = impl_witness_access constants.%.00f, element0 [symbolic_self = constants.%impl.elem0.adf]
// CHECK:STDOUT: %rewrite.loc16_23.2 = requirement_rewrite %impl.elem0.loc16_20.2, <error> [concrete]
// CHECK:STDOUT: %.loc16_14: type = where_expr [concrete = <error>] {
// CHECK:STDOUT: %base_facet_type = requirement_base_facet_type %I.ref [concrete]