Freeze the .Self type and make non-extend constraints available after where (#7501)

The type of `.Self` introduced by `where` may contain a `.Self` inside
it. Freeze the type so that we have a consistent view of `.Self` inside
the facet type, where they are all frozen.

The type of `.Self` only has extend constraints from the LHS of the
`where`. So we need to copy any non-extend constraints into the
`where_stack` so they are available as early-impls and can be used for
impl lookups on the RHS of the where. We need to freeze any `.Self`
references in these just as we do for rewrite constraints.

toolchain/check/handle_where.cpp

@@ -34,7 +34,10 @@ static auto GetPeriodSelfType(Context& context,
     -> SemIR::TypeId {
   if (auto facet_type =
           context.types().TryGetAs<SemIR::FacetType>(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<SemIR::FacetType>(
           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;

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;
       }
     }

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]]";
 

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);
 }