diff --git a/toolchain/check/handle_where.cpp b/toolchain/check/handle_where.cpp index 8019cbad4627..f28fa87afdeb 100644 --- a/toolchain/check/handle_where.cpp +++ b/toolchain/check/handle_where.cpp @@ -34,7 +34,10 @@ static auto GetPeriodSelfType(Context& context, -> SemIR::TypeId { if (auto facet_type = context.types().TryGetAs(facet_type_type_id)) { - return GetExtendedOnlyFacetType(context, *facet_type); + auto extended_id = GetExtendedOnlyFacetType(context, *facet_type); + auto frozen_const_id = + FreezePeriodSelf(context, extended_id.AsConstantId()); + return context.types().GetTypeIdForTypeConstantId(frozen_const_id); } else if (facet_type_type_id == SemIR::TypeType::TypeId) { // The self may be `TypeType` in `type where X impls Y`, so we use an empty // facet type. @@ -82,7 +85,8 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool { context.scope_stack().PushForSameRegion(); // Introduce `.Self` as a symbolic binding. Its type is the value of the // expression to the left of `where`, so `MyInterface` in the example above. - MakePeriodSelfFacetValue(context, node_id, period_self_type_id); + auto period_self = + MakePeriodSelfFacetValue(context, node_id, period_self_type_id); // Going to put each requirement on `args_type_info_stack`, so we can have an // inst block with the varying number of requirements but keeping other @@ -100,16 +104,16 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool { // later constraints to read from them eagerly. context.where_stack().push_back({.loc_id = node_id}); - // Make rewrite constraints from the self facet type available immediately to - // expressions in rewrite constraints for this `where` expression. - // - // Note that the where_stack rewrites need to be frozen. The rewrites in - // the base facet type will be thawed since their `WhereExpr` would have - // already been handled, so we need to freeze them again here. if (auto self_facet_type = context.types().TryGetAs( self_with_constraints_type_id)) { const auto& base_facet_type_info = context.facet_types().Get(self_facet_type->facet_type_id); + // Make rewrite constraints from the self facet type available immediately + // to expressions in rewrite constraints for this `where` expression. + // + // Note that the where_stack rewrites need to be frozen. The rewrites in + // the base facet type will be thawed since their `WhereExpr` would have + // already been handled, so we need to freeze them again here. for (const auto& rewrite : base_facet_type_info.rewrite_constraints) { if (rewrite.lhs_id != SemIR::ErrorInst::InstId) { auto const_id = context.constant_values().Get( @@ -119,6 +123,63 @@ auto HandleParseNode(Context& context, Parse::WhereOperandId node_id) -> bool { rewrite.rhs_id); } } + + // Make impls (non-extend) constraints from the self facet type available + // immediately for this `where` expression, since only extend constraints + // are preserved in the facet type of `.Self`. + // + // Note that the where_stack rewrites need to be frozen. The rewrites in the + // base facet type will be thawed since their `WhereExpr` would have already + // been handled, so we need to freeze them again here. Note that + // `period_self` is already frozen since it is created in that state. + for (const auto& impls : base_facet_type_info.self_impls_constraints) { + auto self_frozen_const_id = context.constant_values().Get(period_self); + auto type_const_id = + GetInterfaceType(context, impls.interface_id, impls.specific_id) + .AsConstantId(); + auto type_frozen_const_id = FreezePeriodSelf(context, type_const_id); + context.where_stack().back().impls.push_back( + {.self_const_id = self_frozen_const_id, + .facet_type_const_id = type_frozen_const_id}); + } + for (const auto& impls : + base_facet_type_info.self_impls_named_constraints) { + auto self_frozen_const_id = context.constant_values().Get(period_self); + auto type_const_id = + GetNamedConstraintType(context, impls.named_constraint_id, + impls.specific_id) + .AsConstantId(); + auto type_frozen_const_id = FreezePeriodSelf(context, type_const_id); + context.where_stack().back().impls.push_back( + {.self_const_id = self_frozen_const_id, + .facet_type_const_id = type_frozen_const_id}); + } + for (const auto& type_impls : base_facet_type_info.type_impls_interfaces) { + auto self_const_id = context.constant_values().Get(type_impls.self_type); + auto self_frozen_const_id = FreezePeriodSelf(context, self_const_id); + auto type_const_id = + GetInterfaceType(context, type_impls.specific_interface.interface_id, + type_impls.specific_interface.specific_id) + .AsConstantId(); + auto type_frozen_const_id = FreezePeriodSelf(context, type_const_id); + context.where_stack().back().impls.push_back( + {.self_const_id = self_frozen_const_id, + .facet_type_const_id = type_frozen_const_id}); + } + for (const auto& type_impls : + base_facet_type_info.type_impls_named_constraints) { + auto self_const_id = context.constant_values().Get(type_impls.self_type); + auto self_frozen_const_id = FreezePeriodSelf(context, self_const_id); + auto type_const_id = + GetNamedConstraintType( + context, type_impls.specific_named_constraint.named_constraint_id, + type_impls.specific_named_constraint.specific_id) + .AsConstantId(); + auto type_frozen_const_id = FreezePeriodSelf(context, type_const_id); + context.where_stack().back().impls.push_back( + {.self_const_id = self_frozen_const_id, + .facet_type_const_id = type_frozen_const_id}); + } } return true; diff --git a/toolchain/check/period_self.cpp b/toolchain/check/period_self.cpp index 0f03f1b49809..b058151ca56a 100644 --- a/toolchain/check/period_self.cpp +++ b/toolchain/check/period_self.cpp @@ -425,6 +425,11 @@ class FreezeAndThawCallbacks : public SubstInstCallbacks { auto subst_id = Rebuild(inst_id, bind); cache_.Insert(inst_id, subst_id); inst_id = subst_id; + // The type of `.Self` may contain another `.Self` as in `Z(.Self) where + // .Self ...` so we would need to SubstOperands still to get to them. + // But we just leave them as frozen. When identifying a facet type and + // substituting in, we will replace the `.Self` value here, which means + // its frozen type is never used. return FullySubstituted; } } diff --git a/toolchain/check/testdata/facet/nested_facet_types.carbon b/toolchain/check/testdata/facet/nested_facet_types.carbon index cc120885f196..2d7d47e87a45 100644 --- a/toolchain/check/testdata/facet/nested_facet_types.carbon +++ b/toolchain/check/testdata/facet/nested_facet_types.carbon @@ -92,6 +92,36 @@ interface Z { // CHECK:STDERR: fn F(unused generic FF: (Z where .T = .U) where .T = {}) {} +// --- fail_nested_facet_types_different_with_impls_interface.carbon +library "[[@TEST_NAME]]"; + +interface Z { + let T: type; + let U: type; +} +interface Y {} + +// CHECK:STDERR: fail_nested_facet_types_different_with_impls_interface.carbon:[[@LINE+4]]:25: error: associated constant `.(Z.T)` given two different values `()` and `{}` [AssociatedConstantWithDifferentValues] +// CHECK:STDERR: fn F(unused generic FF: (Z where .Self impls Y and .T = ()) where .T = {}) {} +// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +// CHECK:STDERR: +fn F(unused generic FF: (Z where .Self impls Y and .T = ()) where .T = {}) {} + +// --- fail_nested_facet_types_different_with_impls_constraint.carbon +library "[[@TEST_NAME]]"; + +interface Z { + let T: type; + let U: type; +} +constraint Y {} + +// CHECK:STDERR: fail_nested_facet_types_different_with_impls_constraint.carbon:[[@LINE+4]]:25: error: associated constant `.(Z.T)` given two different values `()` and `{}` [AssociatedConstantWithDifferentValues] +// CHECK:STDERR: fn F(unused generic FF: (Z where .Self impls Y and .T = ()) where .T = {}) {} +// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +// CHECK:STDERR: +fn F(unused generic FF: (Z where .Self impls Y and .T = ()) where .T = {}) {} + // --- fail_nested_facet_types_different_with_associated_in_generic_parameter.carbon library "[[@TEST_NAME]]"; diff --git a/toolchain/check/testdata/facet/period_self.carbon b/toolchain/check/testdata/facet/period_self.carbon index da722a3c94ff..20604855a5b6 100644 --- a/toolchain/check/testdata/facet/period_self.carbon +++ b/toolchain/check/testdata/facet/period_self.carbon @@ -442,7 +442,7 @@ fn I(generic T: (L & M) where C(.W) impls Z(.Self)) { C(()) as Z(T); } -// --- fail_todo_concrete_access_witness_m_in_impls_constraint.carbon +// --- concrete_access_witness_m_in_extend_constraint_compound_access.carbon library "[[@TEST_NAME]]"; interface L { let W: type; } @@ -454,37 +454,283 @@ interface Z(Z1: type) {} class C(C1: type); +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn I(generic T: (L & M) where C(.Self.(L.W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_m_in_impls_interface.carbon +library "[[@TEST_NAME]]"; + +interface L { let W: type; } + +interface M {} +final impl forall [T: M] T as L where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn H(generic T: (L where .Self impls M) where C(.W) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_m_in_impls_constraint.carbon +library "[[@TEST_NAME]]"; + +interface L { let W: type; } + +interface M {} +constraint GivesM { require impls M; } +final impl forall [T: M] T as L where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn H(generic T: (L where .Self impls GivesM) where C(.W) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_m_in_type_impls_interface.carbon +library "[[@TEST_NAME]]"; + +interface L { let W: type; } + +interface M {} +final impl forall [T: M] T as L where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); +class D(D1: type); + +// Should pass. `.(L.W)` can resolve to `()` immediately through the type of +// `D(.Self)` (since we know `D(.Self)` impls `M`) and the `final impl` as `L`. +// So we can get a witness for `C(())` from `T`. +fn H(generic T: (type where D(.Self) impls M) where C(D(.Self).(L.W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_m_in_type_impls_constraint.carbon +library "[[@TEST_NAME]]"; + +interface L { let W: type; } + +interface M {} +constraint GivesM { require impls M; } +final impl forall [T: M] T as L where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); +class D(D1: type); + +// Should pass. `.(L.W)` can resolve to `()` immediately through the type of +// `D(.Self)` (since we know `D(.Self)` impls `M`) and the `final impl` as `L`. +// So we can get a witness for `C(())` from `T`. +fn H(generic T: (type where D(.Self) impls GivesM) where C(D(.Self).(L.W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_m_in_earlier_requirement.carbon +library "[[@TEST_NAME]]"; + +interface L { let W: type; } + +interface M {} +final impl forall [T: M] T as L where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn G(generic T: L where .Self impls M and C(.W) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_generic_m_in_extend_constraint.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn H(generic T: (L(.Self) & M(.Self)) where C(.W) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- fail_todo_concrete_access_witness_generic_m_in_extend_constraint_compound_access.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + // Should pass. `.W` can resolve to `()` immediately through the type of `.Self` // (since the type of `.Self` contains `M`) and the `final impl`. So we can get // a witness for `C(())` from `T`. // -// TODO: How come we don't get `.W` evaluating to `()` when `M` comes from a -// non-extend constraint? -fn H(generic T: (L where .Self impls M) where C(.W) impls Z(.Self)) { - // CHECK:STDERR: fail_todo_concrete_access_witness_m_in_impls_constraint.carbon:[[@LINE+4]]:3: error: cannot convert type `C(())` into type implementing `Z(T)` [ConversionFailureTypeToFacet] +// TODO: We have a witness for `L(.Self: type)` but we need a witness for +// `L(.Self: (L(.Self: type) & M(.Self: type)))`, so this fails to convert. +// CHECK:STDERR: fail_todo_concrete_access_witness_generic_m_in_extend_constraint_compound_access.carbon:[[@LINE+4]]:47: error: cannot convert type `.Self` that implements `L(.Self) & M(.Self)` into type implementing `L(.Self)` [ConversionFailureFacetToFacet] +// CHECK:STDERR: fn H(generic T: (L(.Self) & M(.Self)) where C(.Self.(L(.Self).W)) impls Z(.Self)) { +// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~ +// CHECK:STDERR: +fn H(generic T: (L(.Self) & M(.Self)) where C(.Self.(L(.Self).W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- fail_todo_concrete_access_witness_generic_m_in_impls_interface.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +// +// TODO: The `.W` contains `.Self: L(.Self: type)`. Notably the `.Self` in the +// specific of `L` has type `type`. When we find the `final impl` we deduce `U` +// as `.Self: type` and need a witness for `M(.Self: type)`. But we have a +// witness for `M(.Self: L(.Self: type))` instead, so we don't use the impl. +// The test passes if we write `.W` as `.Self.(L(.Self).W)` instead. +fn H(generic T: (L(.Self) where .Self impls M(.Self)) where C(.W) impls Z(.Self)) { + // CHECK:STDERR: fail_todo_concrete_access_witness_generic_m_in_impls_interface.carbon:[[@LINE+4]]:3: error: cannot convert type `C(())` into type implementing `Z(T)` [ConversionFailureTypeToFacet] // CHECK:STDERR: C(()) as Z(T); // CHECK:STDERR: ^~~~~~~~~~~~~ // CHECK:STDERR: C(()) as Z(T); } -// --- concrete_access_witness_m_in_earlier_constraint.carbon +// --- fail_todo_concrete_access_witness_generic_m_in_impls_constraint.carbon library "[[@TEST_NAME]]"; -interface L { let W: type; } +interface L(L1: type) { let W: type; } -interface M {} -final impl forall [T: M] T as L where .W = () {} +interface M(M1: type) {} +constraint GivesM(M1: type) { require impls M(M1); } +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} interface Z(Z1: type) {} class C(C1: type); +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +// +// TODO: The `.W` contains `.Self: L(.Self: type)`. Notably the `.Self` in the +// specific of `L` has type `type`. When we find the `final impl` we deduce `U` +// as `.Self: type` and need a witness for `M(.Self: type)`. But we have a +// witness for `M(.Self: L(.Self: type))` instead, so we don't use the impl. +// The test passes if we write `.W` as `.Self.(L(.Self).W)` instead. +fn H(generic T: (L(.Self) where .Self impls GivesM(.Self)) where C(.W) impls Z(.Self)) { + // CHECK:STDERR: fail_todo_concrete_access_witness_generic_m_in_impls_constraint.carbon:[[@LINE+4]]:3: error: cannot convert type `C(())` into type implementing `Z(T)` [ConversionFailureTypeToFacet] + // CHECK:STDERR: C(()) as Z(T); + // CHECK:STDERR: ^~~~~~~~~~~~~ + // CHECK:STDERR: + C(()) as Z(T); +} + +// --- concrete_access_witness_generic_m_in_type_impls_interface.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); +class D(D1: type); // Should pass. `.W` can resolve to `()` immediately through the type of `.Self` // (since the type of `.Self` contains `M`) and the `final impl`. So we can get // a witness for `C(())` from `T`. -fn G(generic T: L where .Self impls M and C(.W) impls Z(.Self)) { +fn H(generic T: (L(.Self) where D(.Self) impls M(.Self)) where C(D(.Self).(L(.Self).W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- concrete_access_witness_generic_m_in_type_impls_constraint.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +constraint GivesM(M1: type) { require impls M(M1); } +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); +class D(D1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +fn H(generic T: (L(.Self) where D(.Self) impls GivesM(.Self)) where C(D(.Self).(L(.Self).W)) impls Z(.Self)) { + C(()) as Z(T); +} + +// --- fail_todo_concrete_access_witness_generic_m_in_earlier_requirement.carbon +library "[[@TEST_NAME]]"; + +interface L(L1: type) { let W: type; } + +interface M(M1: type) {} +final impl forall [U: type, T: M(U)] T as L(U) where .W = () {} + +interface Z(Z1: type) {} + +class C(C1: type); + +// Should pass. `.W` can resolve to `()` immediately through the type of `.Self` +// (since the type of `.Self` contains `M`) and the `final impl`. So we can get +// a witness for `C(())` from `T`. +// +// TODO: The `.W` contains `.Self: L(.Self: type)`. Notably the `.Self` in the +// specific of `L` has type `type`. When we find the `final impl` we deduce `U` +// as `.Self: type` and need a witness for `M(.Self: type)`. But we have a +// witness for `M(.Self: L(.Self: type))` instead, so we don't use the impl. +// The test passes if we write `.W` as `.Self.(L(.Self).W)` instead. +fn H(generic T: L(.Self) where .Self impls M(.Self) and C(.W) impls Z(.Self)) { + // CHECK:STDERR: fail_todo_concrete_access_witness_generic_m_in_earlier_requirement.carbon:[[@LINE+4]]:3: error: cannot convert type `C(())` into type implementing `Z(T)` [ConversionFailureTypeToFacet] + // CHECK:STDERR: C(()) as Z(T); + // CHECK:STDERR: ^~~~~~~~~~~~~ + // CHECK:STDERR: C(()) as Z(T); }