Add storage for `<type> impls <facettype>` in the FacetTypeInfo (#7005)

We don't yet actually add any in check, but this adds the storage for
them, and capabilities to import them, evaluate them, substitute into
them with specifics, name them, format them, and stringify them.

---------

Co-authored-by: Chandler Carruth <chandlerc@gmail.com>

toolchain/check/eval.cpp

@@ -718,6 +718,7 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
 
   info.extend_constraints.reserve(orig.extend_constraints.size());
   for (const auto& extend : orig.extend_constraints) {
+    // TODO: Add GetConstantValue for SpecificInterface.
     info.extend_constraints.push_back(
         {.interface_id = extend.interface_id,
          .specific_id =
@@ -726,6 +727,7 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
 
   info.self_impls_constraints.reserve(orig.self_impls_constraints.size());
   for (const auto& self_impls : orig.self_impls_constraints) {
+    // TODO: Add GetConstantValue for SpecificInterface.
     info.self_impls_constraints.push_back(
         {.interface_id = self_impls.interface_id,
          .specific_id =
@@ -734,6 +736,7 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
 
   info.extend_named_constraints.reserve(orig.extend_named_constraints.size());
   for (const auto& extend : orig.extend_named_constraints) {
+    // TODO: Add GetConstantValue for SpecificNamedConstraint.
     info.extend_named_constraints.push_back(
         {.named_constraint_id = extend.named_constraint_id,
          .specific_id =
@@ -743,12 +746,41 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
   info.self_impls_named_constraints.reserve(
       orig.self_impls_named_constraints.size());
   for (const auto& self_impls : orig.self_impls_named_constraints) {
+    // TODO: Add GetConstantValue for SpecificNamedConstraint.
     info.self_impls_named_constraints.push_back(
         {.named_constraint_id = self_impls.named_constraint_id,
          .specific_id =
              GetConstantValue(eval_context, self_impls.specific_id, phase)});
   }
 
+  info.type_impls_interfaces.reserve(orig.type_impls_interfaces.size());
+  for (const auto& type_impls : orig.type_impls_interfaces) {
+    info.type_impls_interfaces.push_back(
+        {.self_type =
+             GetConstantValue(eval_context, type_impls.self_type, phase),
+         // TODO: Add GetConstantValue for SpecificInterface.
+         .specific_interface = {
+             .interface_id = type_impls.specific_interface.interface_id,
+             .specific_id = GetConstantValue(
+                 eval_context, type_impls.specific_interface.specific_id,
+                 phase)}});
+  }
+
+  info.type_impls_named_constraints.reserve(
+      orig.type_impls_named_constraints.size());
+  for (const auto& type_impls : orig.type_impls_named_constraints) {
+    info.type_impls_named_constraints.push_back(
+        {.self_type =
+             GetConstantValue(eval_context, type_impls.self_type, phase),
+         // TODO: Add GetConstantValue for SpecificNamedConstraint.
+         .specific_named_constraint = {
+             .named_constraint_id =
+                 type_impls.specific_named_constraint.named_constraint_id,
+             .specific_id = GetConstantValue(
+                 eval_context, type_impls.specific_named_constraint.specific_id,
+                 phase)}});
+  }
+
   // Rewrite constraints are resolved first before replacing them with their
   // canonical instruction, so that in a `WhereExpr` we can work with the
   // `ImplWitnessAccess` references to `.Self` on the LHS of the constraints
@@ -972,6 +1004,14 @@ static auto ResolveSpecificDeclForInst(EvalContext& eval_context,
           ResolveSpecificDeclForSpecificId(eval_context,
                                            constraint.specific_id);
         }
+        for (const auto& type_impls : info.type_impls_interfaces) {
+          ResolveSpecificDeclForSpecificId(
+              eval_context, type_impls.specific_interface.specific_id);
+        }
+        for (const auto& type_impls : info.type_impls_named_constraints) {
+          ResolveSpecificDeclForSpecificId(
+              eval_context, type_impls.specific_named_constraint.specific_id);
+        }
         break;
       }
       case CARBON_KIND(SemIR::SpecificId specific_id): {
@@ -2542,6 +2582,9 @@ auto TryEvalTypedInst<SemIR::WhereExpr>(EvalContext& eval_context,
               eval_context.facet_types().Get(base_facet_type->facet_type_id);
           info.extend_constraints.append(base_info.extend_constraints);
           info.self_impls_constraints.append(base_info.self_impls_constraints);
+          info.type_impls_interfaces.append(base_info.type_impls_interfaces);
+          info.type_impls_named_constraints.append(
+              base_info.type_impls_named_constraints);
           info.rewrite_constraints.append(base_info.rewrite_constraints);
           info.other_requirements |= base_info.other_requirements;
         }
@@ -2582,6 +2625,12 @@ auto TryEvalTypedInst<SemIR::WhereExpr>(EvalContext& eval_context,
                                more_info.extend_named_constraints);
             llvm::append_range(info.self_impls_named_constraints,
                                more_info.self_impls_named_constraints);
+            // If `.Self impls Z` and Z implies `C impls Y`, then the facet type
+            // of `.Self` also knows `C impls Y`.
+            llvm::append_range(info.type_impls_interfaces,
+                               more_info.type_impls_interfaces);
+            llvm::append_range(info.type_impls_named_constraints,
+                               more_info.type_impls_named_constraints);
             // Other requirements are copied in.
             llvm::append_range(info.rewrite_constraints,
                                more_info.rewrite_constraints);

toolchain/check/handle_require.cpp

@@ -222,9 +222,13 @@ static auto ValidateRequire(Context& context, SemIR::LocId loc_id,
                    "facet type has constraints that we don't handle yet");
       return std::nullopt;
     }
+    auto named_constraints_from_type_impls = llvm::map_range(
+        constraint_facet_type_info.type_impls_named_constraints,
+        [](auto impls) { return impls.specific_named_constraint; });
     auto named_constraints = llvm::concat<const SemIR::SpecificNamedConstraint>(
         constraint_facet_type_info.extend_named_constraints,
-        constraint_facet_type_info.self_impls_named_constraints);
+        constraint_facet_type_info.self_impls_named_constraints,
+        named_constraints_from_type_impls);
     for (auto c : named_constraints) {
       if (c.named_constraint_id == named_constraint->named_constraint_id) {
         const auto& named_constraint =

toolchain/check/import_ref.cpp

@@ -3417,6 +3417,38 @@ static auto ResolveFacetTypeInfo(
     }
   }
 
+  if (local_facet_type_info) {
+    local_facet_type_info->type_impls_interfaces.reserve(
+        import_facet_type_info.type_impls_interfaces.size());
+  }
+  for (const auto& type_impls : import_facet_type_info.type_impls_interfaces) {
+    auto self_type = GetLocalConstantInstId(resolver, type_impls.self_type);
+    auto data =
+        GetLocalSpecificInterfaceData(resolver, type_impls.specific_interface);
+    if (local_facet_type_info) {
+      local_facet_type_info->type_impls_interfaces.push_back(
+          {self_type, GetLocalSpecificInterface(
+                          resolver, type_impls.specific_interface, data)});
+    }
+  }
+
+  if (local_facet_type_info) {
+    local_facet_type_info->type_impls_named_constraints.reserve(
+        import_facet_type_info.type_impls_named_constraints.size());
+  }
+  for (const auto& type_impls :
+       import_facet_type_info.type_impls_named_constraints) {
+    auto self_type = GetLocalConstantInstId(resolver, type_impls.self_type);
+    auto data = GetLocalSpecificNamedConstraintData(
+        resolver, type_impls.specific_named_constraint);
+    if (local_facet_type_info) {
+      local_facet_type_info->type_impls_named_constraints.push_back(
+          {self_type,
+           GetLocalSpecificNamedConstraint(
+               resolver, type_impls.specific_named_constraint, data)});
+    }
+  }
+
   if (local_facet_type_info) {
     local_facet_type_info->rewrite_constraints.reserve(
         import_facet_type_info.rewrite_constraints.size());

toolchain/check/subst.cpp

@@ -11,6 +11,7 @@
 #include "toolchain/sem_ir/copy_on_write_block.h"
 #include "toolchain/sem_ir/ids.h"
 #include "toolchain/sem_ir/inst.h"
+#include "toolchain/sem_ir/specific_named_constraint.h"
 #include "toolchain/sem_ir/typed_insts.h"
 
 namespace Carbon::Check {
@@ -134,17 +135,26 @@ static auto PushOperand(Context& context, Worklist& worklist,
     }
     case CARBON_KIND(SemIR::FacetTypeId facet_type_id): {
       const auto& facet_type_info = context.facet_types().Get(facet_type_id);
-      for (auto interface : facet_type_info.extend_constraints) {
-        push_specific(interface.specific_id);
+      for (auto extends : facet_type_info.extend_constraints) {
+        push_specific(extends.specific_id);
       }
-      for (auto interface : facet_type_info.self_impls_constraints) {
-        push_specific(interface.specific_id);
+      for (auto impls : facet_type_info.self_impls_constraints) {
+        push_specific(impls.specific_id);
       }
-      for (auto interface : facet_type_info.extend_named_constraints) {
-        push_specific(interface.specific_id);
+      for (auto extends : facet_type_info.extend_named_constraints) {
+        push_specific(extends.specific_id);
       }
-      for (auto interface : facet_type_info.self_impls_named_constraints) {
-        push_specific(interface.specific_id);
+      for (auto impls : facet_type_info.self_impls_named_constraints) {
+        push_specific(impls.specific_id);
+      }
+      for (const auto& type_impls : facet_type_info.type_impls_interfaces) {
+        worklist.Push(type_impls.self_type);
+        push_specific(type_impls.specific_interface.specific_id);
+      }
+      for (const auto& type_impls :
+           facet_type_info.type_impls_named_constraints) {
+        worklist.Push(type_impls.self_type);
+        push_specific(type_impls.specific_named_constraint.specific_id);
       }
       for (auto rewrite : facet_type_info.rewrite_constraints) {
         worklist.Push(rewrite.lhs_id);
@@ -248,6 +258,36 @@ static auto PopOperand(Context& context, Worklist& worklist,
         auto lhs_id = worklist.Pop();
         new_constraint = {.lhs_id = lhs_id, .rhs_id = rhs_id};
       }
+      new_facet_type_info.type_impls_named_constraints.resize(
+          old_facet_type_info.type_impls_named_constraints.size(),
+          {SemIR::InstId::None, SemIR::SpecificNamedConstraint::None});
+      for (auto [old_type_impls, new_type_impls] :
+           llvm::reverse(llvm::zip_equal(
+               old_facet_type_info.type_impls_named_constraints,
+               new_facet_type_info.type_impls_named_constraints))) {
+        auto specific_id =
+            pop_specific(old_type_impls.specific_named_constraint.specific_id);
+        auto self_type = worklist.Pop();
+        new_type_impls = {
+            .self_type = self_type,
+            .specific_named_constraint = {
+                old_type_impls.specific_named_constraint.named_constraint_id,
+                specific_id}};
+      }
+      new_facet_type_info.type_impls_interfaces.resize(
+          old_facet_type_info.type_impls_interfaces.size(),
+          {SemIR::InstId::None, SemIR::SpecificInterface::None});
+      for (auto [old_type_impls, new_type_impls] : llvm::reverse(
+               llvm::zip_equal(old_facet_type_info.type_impls_interfaces,
+                               new_facet_type_info.type_impls_interfaces))) {
+        auto specific_id =
+            pop_specific(old_type_impls.specific_interface.specific_id);
+        auto self_type = worklist.Pop();
+        new_type_impls = {
+            .self_type = self_type,
+            .specific_interface = {
+                old_type_impls.specific_interface.interface_id, specific_id}};
+      }
       new_facet_type_info.self_impls_named_constraints.resize(
           old_facet_type_info.self_impls_named_constraints.size(),
           SemIR::SpecificNamedConstraint::None);

toolchain/check/type_completion.cpp

@@ -903,6 +903,12 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
         -> SemIR::IdentifiedFacetType::RequiredImpl {
       return {self_const_id, interface};
     };
+    auto type_and_interface =
+        [&](const SemIR::FacetTypeInfo::TypeImplsInterface& impls)
+        -> SemIR::IdentifiedFacetType::RequiredImpl {
+      return {context.constant_values().Get(impls.self_type),
+              impls.specific_interface};
+    };
 
     if (facet_type_extends) {
       llvm::append_range(extends,
@@ -916,9 +922,13 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
     llvm::append_range(impls,
                        llvm::map_range(facet_type_info.self_impls_constraints,
                                        self_and_interface));
+    llvm::append_range(impls,
+                       llvm::map_range(facet_type_info.type_impls_interfaces,
+                                       type_and_interface));
 
     if (facet_type_info.extend_named_constraints.empty() &&
-        facet_type_info.self_impls_named_constraints.empty()) {
+        facet_type_info.self_impls_named_constraints.empty() &&
+        facet_type_info.type_impls_named_constraints.empty()) {
       continue;
     }
 
@@ -1040,6 +1050,67 @@ static auto IdentifyFacetType(Context& context, SemIR::LocId loc_id,
         work.push_back({false, require_self, facet_type_id});
       }
     }
+
+    for (const auto& type_impls :
+         facet_type_info.type_impls_named_constraints) {
+      auto [self_type_inst_id, impls] = type_impls;
+      const auto& constraint =
+          context.named_constraints().Get(impls.named_constraint_id);
+
+      llvm::ArrayRef<SemIR::RequireImplsId> require_impls_ids;
+      if (constraint.is_complete()) {
+        require_impls_ids = context.require_impls_blocks().Get(
+            constraint.require_impls_block_id);
+      } else if (allow_partially_identified) {
+        partially_identified = true;
+        if (constraint.is_being_defined()) {
+          require_impls_ids = context.require_impls_stack().PeekForScope(
+              impls.named_constraint_id);
+        } else {
+          continue;
+        }
+      } else {
+        if (diagnose) {
+          DiagnoseIncompleteNamedConstraint(context, impls.named_constraint_id);
+        }
+        return SemIR::IdentifiedFacetTypeId::None;
+      }
+
+      auto self_type_facet = GetSelfFacetValue(
+          context, context.constant_values().Get(self_type_inst_id));
+
+      auto constraint_with_self_specific_id = MakeSpecificWithInnerSelf(
+          context, loc_id, constraint.generic_id,
+          constraint.generic_with_self_id, impls.specific_id, self_type_facet);
+      if (SpecificHasError(context, constraint_with_self_specific_id)) {
+        return SemIR::IdentifiedFacetTypeId::None;
+      }
+
+      for (auto require_impls_id : llvm::reverse(require_impls_ids)) {
+        const auto& require = context.require_impls().Get(require_impls_id);
+
+        // Each require is in its own generic, with no additional bindings and
+        // no definition, so that they can have their specifics independently
+        // instantiated.
+        auto require_specific_id = CopySpecificToGeneric(
+            context, SemIR::LocId(require.decl_id),
+            constraint_with_self_specific_id, require.generic_id);
+        auto require_self = GetConstantValueInSpecific(
+            context.sem_ir(), require_specific_id, require.self_id);
+        auto require_facet_type = GetConstantValueInSpecific(
+            context.sem_ir(), require_specific_id, require.facet_type_inst_id);
+        if (require_self == SemIR::ErrorInst::ConstantId ||
+            require_facet_type == SemIR::ErrorInst::ConstantId) {
+          return SemIR::IdentifiedFacetTypeId::None;
+        }
+
+        auto facet_type_id =
+            context.constant_values()
+                .GetInstAs<SemIR::FacetType>(require_facet_type)
+                .facet_type_id;
+        work.push_back({false, require_self, facet_type_id});
+      }
+    }
   }
 
   // TODO: Process other kinds of requirements.

toolchain/sem_ir/facet_type_info.cpp

@@ -25,8 +25,8 @@ static auto SortAndDeduplicate(VecT& vec,
 }
 
 // Canonically ordered by the numerical ids.
-static auto ImplsLess(const FacetTypeInfo::ImplsConstraint& lhs,
-                      const FacetTypeInfo::ImplsConstraint& rhs) -> bool {
+static auto InterfaceLess(const SpecificInterface& lhs,
+                          const SpecificInterface& rhs) -> bool {
   return std::tie(lhs.interface_id.index, lhs.specific_id.index) <
          std::tie(rhs.interface_id.index, rhs.specific_id.index);
 }
@@ -39,12 +39,36 @@ static auto RewriteLess(const FacetTypeInfo::RewriteConstraint& lhs,
 }
 
 // Canonically ordered by the numerical ids.
-static auto NamedConstraintsLess(const SpecificNamedConstraint& lhs,
-                                 const SpecificNamedConstraint& rhs) -> bool {
+static auto NamedConstraintLess(const SpecificNamedConstraint& lhs,
+                                const SpecificNamedConstraint& rhs) -> bool {
   return std::tie(lhs.named_constraint_id.index, lhs.specific_id.index) <
          std::tie(rhs.named_constraint_id.index, rhs.specific_id.index);
 }
 
+// Canonically ordered by the numerical ids.
+static auto TypeImplsInterfaceLess(const FacetTypeInfo::TypeImplsInterface& lhs,
+                                   const FacetTypeInfo::TypeImplsInterface& rhs)
+    -> bool {
+  return std::tie(lhs.self_type.index,
+                  lhs.specific_interface.interface_id.index,
+                  lhs.specific_interface.specific_id.index) <
+         std::tie(rhs.self_type.index,
+                  rhs.specific_interface.interface_id.index,
+                  rhs.specific_interface.specific_id.index);
+}
+
+// Canonically ordered by the numerical ids.
+static auto TypeImplsNamedConstraintLess(
+    const FacetTypeInfo::TypeImplsNamedConstraint& lhs,
+    const FacetTypeInfo::TypeImplsNamedConstraint& rhs) -> bool {
+  return std::tie(lhs.self_type.index,
+                  lhs.specific_named_constraint.named_constraint_id.index,
+                  lhs.specific_named_constraint.specific_id.index) <
+         std::tie(rhs.self_type.index,
+                  rhs.specific_named_constraint.named_constraint_id.index,
+                  rhs.specific_named_constraint.specific_id.index);
+}
+
 // Canonically ordered by the numerical ids.
 static auto RequiredLess(const IdentifiedFacetType::RequiredImpl& lhs,
                          const IdentifiedFacetType::RequiredImpl& rhs) -> bool {
@@ -131,6 +155,11 @@ auto FacetTypeInfo::Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
   CombineVectors(info.self_impls_named_constraints,
                  lhs.self_impls_named_constraints,
                  rhs.self_impls_named_constraints);
+  CombineVectors(info.type_impls_interfaces, lhs.type_impls_interfaces,
+                 rhs.type_impls_interfaces);
+  CombineVectors(info.type_impls_named_constraints,
+                 lhs.type_impls_named_constraints,
+                 rhs.type_impls_named_constraints);
   CombineVectors(info.rewrite_constraints, lhs.rewrite_constraints,
                  rhs.rewrite_constraints);
   info.other_requirements = lhs.other_requirements || rhs.other_requirements;
@@ -138,13 +167,16 @@ auto FacetTypeInfo::Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
 }
 
 auto FacetTypeInfo::Canonicalize() -> void {
-  SortAndDeduplicate(extend_constraints, ImplsLess);
-  SortAndDeduplicate(self_impls_constraints, ImplsLess);
-  SubtractSorted(self_impls_constraints, extend_constraints, ImplsLess);
-  SortAndDeduplicate(extend_named_constraints, NamedConstraintsLess);
-  SortAndDeduplicate(self_impls_named_constraints, NamedConstraintsLess);
+  SortAndDeduplicate(extend_constraints, InterfaceLess);
+  SortAndDeduplicate(self_impls_constraints, InterfaceLess);
+  SubtractSorted(self_impls_constraints, extend_constraints, InterfaceLess);
+  SortAndDeduplicate(extend_named_constraints, NamedConstraintLess);
+  SortAndDeduplicate(self_impls_named_constraints, NamedConstraintLess);
   SubtractSorted(self_impls_named_constraints, extend_named_constraints,
-                 NamedConstraintsLess);
+                 NamedConstraintLess);
+  SortAndDeduplicate(type_impls_interfaces, TypeImplsInterfaceLess);
+  SortAndDeduplicate(type_impls_named_constraints,
+                     TypeImplsNamedConstraintLess);
   SortAndDeduplicate(rewrite_constraints, RewriteLess);
 }
 
@@ -155,7 +187,7 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
   if (!extend_constraints.empty()) {
     out << outer_sep << "extends interface: ";
     llvm::ListSeparator sep;
-    for (ImplsConstraint req : extend_constraints) {
+    for (auto req : extend_constraints) {
       out << sep << req.interface_id;
       if (req.specific_id.has_value()) {
         out << "(" << req.specific_id << ")";
@@ -166,7 +198,7 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
   if (!self_impls_constraints.empty()) {
     out << outer_sep << "self impls interface: ";
     llvm::ListSeparator sep;
-    for (ImplsConstraint req : self_impls_constraints) {
+    for (auto req : self_impls_constraints) {
       out << sep << req.interface_id;
       if (req.specific_id.has_value()) {
         out << "(" << req.specific_id << ")";
@@ -174,14 +206,6 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
     }
   }
 
-  if (!rewrite_constraints.empty()) {
-    out << outer_sep << "rewrites: ";
-    llvm::ListSeparator sep;
-    for (RewriteConstraint req : rewrite_constraints) {
-      out << sep << req.lhs_id << "=" << req.rhs_id;
-    }
-  }
-
   if (!extend_named_constraints.empty()) {
     out << outer_sep << "extends named constraint: ";
     llvm::ListSeparator sep;
@@ -204,6 +228,39 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
     }
   }
 
+  if (!type_impls_interfaces.empty()) {
+    out << outer_sep << "type impls interface: ";
+    llvm::ListSeparator sep;
+    for (const auto& type_impls : type_impls_interfaces) {
+      out << sep << type_impls.self_type;
+      out << " impls " << type_impls.specific_interface.interface_id;
+      if (type_impls.specific_interface.specific_id.has_value()) {
+        out << "(" << type_impls.specific_interface.specific_id << ")";
+      }
+    }
+  }
+
+  if (!type_impls_named_constraints.empty()) {
+    out << outer_sep << "type impls interface: ";
+    llvm::ListSeparator sep;
+    for (const auto& type_impls : type_impls_named_constraints) {
+      out << sep << type_impls.self_type;
+      out << " impls "
+          << type_impls.specific_named_constraint.named_constraint_id;
+      if (type_impls.specific_named_constraint.specific_id.has_value()) {
+        out << "(" << type_impls.specific_named_constraint.specific_id << ")";
+      }
+    }
+  }
+
+  if (!rewrite_constraints.empty()) {
+    out << outer_sep << "rewrites: ";
+    llvm::ListSeparator sep;
+    for (auto req : rewrite_constraints) {
+      out << sep << req.lhs_id << "=" << req.rhs_id;
+    }
+  }
+
   if (other_requirements) {
     out << outer_sep << "+ TODO requirements";
   }
@@ -285,7 +342,7 @@ auto AddCanonicalWitnessesBlock(File& sem_ir,
   // canonical order in which the witnesses must appear for a given facet type
   // so that ImplWitnessAccess can find the appropriate witness.
   llvm::sort(sortable, [](auto& lhs, auto& rhs) {
-    return ImplsLess(lhs.first, rhs.first);
+    return InterfaceLess(lhs.first, rhs.first);
   });
 
   // Update the original list with the new order (reusing to avoid an

toolchain/sem_ir/facet_type_info.h

@@ -22,6 +22,20 @@ class File;
 using SingleExtendFacetType =
     std::variant<SpecificInterface, SpecificNamedConstraint>;
 
+// The canonical description of a FacetType. Contains the interfaces, named
+// constraints, and any constraints on types that are part of the facet type.
+// All values within are canonical in order for comparison to be used for
+// type equality.
+//
+// The structure keeps separate dependencies on interfaces and named
+// constraints, even though named constraints ultimately just name interfaces,
+// as it provides a canonical but otherwise unprocessed representation of the
+// facet type.
+//
+// The flattening of the named constraints into interfaces is done by forming
+// the IdentifiedFacetType for a specific Self type.
+//
+// TODO: Rename to DeclaredFacetType.
 struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // Returns a FacetTypeInfo that combines `lhs` and `rhs`. It is not
   // canonicalized, so that it can be further modified by the caller if desired.
@@ -35,14 +49,10 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // TODO: Replace these vectors with an array allocated in an
   // `llvm::BumpPtrAllocator`.
 
-  // `ImplsConstraint` holds the interfaces this facet type requires.
-  // TODO: extend this so it can represent named constraint requirements
-  // and requirements on members, not just `.Self`.
-  using ImplsConstraint = SpecificInterface;
   // These are the required interfaces that are lookup contexts.
-  llvm::SmallVector<ImplsConstraint> extend_constraints;
+  llvm::SmallVector<SpecificInterface> extend_constraints;
   // These are the required interfaces that are not lookup contexts.
-  llvm::SmallVector<ImplsConstraint> self_impls_constraints;
+  llvm::SmallVector<SpecificInterface> self_impls_constraints;
 
   // These name constraints add interfaces as lookup contexts, if they are
   // extended in the named constraint.
@@ -50,6 +60,29 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // These name constraints don't add interfaces as lookup contexts.
   llvm::SmallVector<SpecificNamedConstraint> self_impls_named_constraints;
 
+  // Requirements on types other than the generic self.
+  struct TypeImplsInterface {
+    // A facet or type value, which is required to implement the interface.
+    // Must be a canonical instruction to ensure comparison works correctly.
+    InstId self_type;
+    SpecificInterface specific_interface;
+
+    friend auto operator==(const TypeImplsInterface& lhs,
+                           const TypeImplsInterface& rhs) -> bool = default;
+  };
+  struct TypeImplsNamedConstraint {
+    // A facet or type value, which is required to implement the constraint.
+    // Must be a canonical instruction to ensure comparison works correctly.
+    InstId self_type;
+    SpecificNamedConstraint specific_named_constraint;
+
+    friend auto operator==(const TypeImplsNamedConstraint& lhs,
+                           const TypeImplsNamedConstraint& rhs)
+        -> bool = default;
+  };
+  llvm::SmallVector<TypeImplsInterface> type_impls_interfaces;
+  llvm::SmallVector<TypeImplsNamedConstraint> type_impls_named_constraints;
+
   // Rewrite constraints of the form `.T = U`.
   //
   // The InstIds here must be canonical instructions (which come from the
@@ -84,7 +117,9 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // has any other requirements.
   auto TryAsSingleExtend() const -> std::optional<SingleExtendFacetType> {
     if (!self_impls_constraints.empty() ||
-        !self_impls_named_constraints.empty() || !rewrite_constraints.empty() ||
+        !self_impls_named_constraints.empty() ||
+        !type_impls_interfaces.empty() ||
+        !type_impls_named_constraints.empty() || !rewrite_constraints.empty() ||
         other_requirements) {
       return std::nullopt;
     }
@@ -103,6 +138,8 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
     return extend_constraints.empty() && extend_named_constraints.empty() &&
            self_impls_constraints.empty() &&
            self_impls_named_constraints.empty() &&
+           type_impls_interfaces.empty() &&
+           type_impls_named_constraints.empty() &&
            rewrite_constraints.empty() && !other_requirements;
   }
 
@@ -113,6 +150,9 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
            lhs.extend_named_constraints == rhs.extend_named_constraints &&
            lhs.self_impls_named_constraints ==
                rhs.self_impls_named_constraints &&
+           lhs.type_impls_interfaces == rhs.type_impls_interfaces &&
+           lhs.type_impls_named_constraints ==
+               rhs.type_impls_named_constraints &&
            lhs.rewrite_constraints == rhs.rewrite_constraints &&
            lhs.other_requirements == rhs.other_requirements;
   }
@@ -138,6 +178,11 @@ struct IdentifiedFacetTypeKey {
                          const IdentifiedFacetTypeKey& rhs) -> bool = default;
 };
 
+// The IdentifiedFacetType represents all of the interfaces required by a facet
+// type against a given Self type, and any other types it constrains. The order
+// of the interfaces is fixed for a given facet type, and can thus be used as a
+// key for storing and finding witnesses or other data associated with a facet
+// type.
 struct IdentifiedFacetType {
   // A requirement that `self_facet_value` implements the `specific_interface`.
   struct RequiredImpl {

toolchain/sem_ir/formatter.cpp

@@ -1452,6 +1452,13 @@ auto Formatter::FormatArg(FacetTypeId id) -> void {
   // used as the argument to a `facet_type` instruction.
   out() << "<";
 
+  auto format_specific = [&](SemIR::SpecificId specific_id) {
+    if (specific_id.has_value()) {
+      out() << ", ";
+      FormatName(specific_id);
+    }
+  };
+
   llvm::ListSeparator sep(" & ");
   if (info.extend_constraints.empty() &&
       info.extend_named_constraints.empty()) {
@@ -1460,45 +1467,56 @@ auto Formatter::FormatArg(FacetTypeId id) -> void {
     for (auto extend : info.extend_constraints) {
       out() << sep;
       FormatName(extend.interface_id);
-      if (extend.specific_id.has_value()) {
-        out() << ", ";
-        FormatName(extend.specific_id);
-      }
+      format_specific(extend.specific_id);
     }
     for (auto extend : info.extend_named_constraints) {
       out() << sep;
       FormatName(extend.named_constraint_id);
-      if (extend.specific_id.has_value()) {
-        out() << ", ";
-        FormatName(extend.specific_id);
-      }
+      format_specific(extend.specific_id);
     }
   }
 
   if (info.other_requirements || !info.self_impls_constraints.empty() ||
+      !info.type_impls_interfaces.empty() ||
+      !info.type_impls_named_constraints.empty() ||
       !info.rewrite_constraints.empty()) {
     out() << " where ";
     llvm::ListSeparator and_sep(" and ");
-    if (!info.self_impls_constraints.empty() ||
-        !info.self_impls_named_constraints.empty()) {
+    int num_self_impls = info.self_impls_constraints.size() +
+                         info.self_impls_named_constraints.size();
+    if (num_self_impls > 0) {
       out() << and_sep << ".Self impls ";
       llvm::ListSeparator amp_sep(" & ");
+      if (num_self_impls > 1) {
+        out() << "(";
+      }
       for (auto self_impls : info.self_impls_constraints) {
         out() << amp_sep;
         FormatName(self_impls.interface_id);
-        if (self_impls.specific_id.has_value()) {
-          out() << ", ";
-          FormatName(self_impls.specific_id);
-        }
+        format_specific(self_impls.specific_id);
       }
       for (auto self_impls : info.self_impls_named_constraints) {
         out() << amp_sep;
         FormatName(self_impls.named_constraint_id);
-        if (self_impls.specific_id.has_value()) {
-          out() << ", ";
-          FormatName(self_impls.specific_id);
-        }
+        format_specific(self_impls.specific_id);
       }
+      if (num_self_impls > 1) {
+        out() << ")";
+      }
+    }
+    for (const auto& type_impls : info.type_impls_interfaces) {
+      out() << and_sep;
+      FormatName(type_impls.self_type);
+      out() << " impls ";
+      FormatName(type_impls.specific_interface.interface_id);
+      format_specific(type_impls.specific_interface.specific_id);
+    }
+    for (const auto& type_impls : info.type_impls_named_constraints) {
+      out() << and_sep;
+      FormatName(type_impls.self_type);
+      out() << " impls ";
+      FormatName(type_impls.specific_named_constraint.named_constraint_id);
+      format_specific(type_impls.specific_named_constraint.specific_id);
     }
     for (auto rewrite : info.rewrite_constraints) {
       out() << and_sep;

toolchain/sem_ir/inst_namer.cpp

@@ -1050,6 +1050,8 @@ auto InstNamer::NamingContext::NameInst() -> void {
       bool has_where = facet_type_info.other_requirements ||
                        !facet_type_info.self_impls_constraints.empty() ||
                        !facet_type_info.self_impls_named_constraints.empty() ||
+                       !facet_type_info.type_impls_interfaces.empty() ||
+                       !facet_type_info.type_impls_named_constraints.empty() ||
                        !facet_type_info.rewrite_constraints.empty();
       if (facet_type_info.extend_constraints.size() == 1 &&
           facet_type_info.extend_named_constraints.empty()) {

toolchain/sem_ir/stringify.cpp

@@ -744,7 +744,24 @@ class Stringifier {
       step_stack_->PushString(" .Self impls ");
       some_where = true;
     }
-    // TODO: Other restrictions from facet_type_info.
+    for (const auto& type_impls :
+         llvm::reverse(facet_type_info.type_impls_interfaces)) {
+      if (some_where) {
+        step_stack_->PushString(" and");
+      }
+      step_stack_->Push(type_impls.self_type, " impls ",
+                        type_impls.specific_interface);
+      some_where = true;
+    }
+    for (const auto& type_impls :
+         llvm::reverse(facet_type_info.type_impls_named_constraints)) {
+      if (some_where) {
+        step_stack_->PushString(" and");
+      }
+      step_stack_->Push(type_impls.self_type, " impls ",
+                        type_impls.specific_named_constraint);
+      some_where = true;
+    }
     if (some_where) {
       step_stack_->PushString(" where");
     }