Implement ...`where .Self impls`... (#5238)

* Also remove facet type deduction, since we decided against it on
[2025-04-02](https://docs.google.com/document/d/1Iut5f2TQBrtBNIduF4vJYOKfw7MbS8xH_J01_Q4e6Rk/edit?pli=1&resourcekey=0-mc_vh5UzrzXfU4kO-3tOjA&tab=t.0#heading=h.95phmuvxog9n).

---------

Co-authored-by: Josh L <josh11b@users.noreply.github.com>
Co-authored-by: Dana Jansens <danakj@orodu.net>

toolchain/check/deduce.cpp

@@ -119,24 +119,6 @@ class DeductionWorklist {
            context_->type_blocks().Get(args), needs_substitution);
   }
 
-  auto AddAll(SemIR::FacetTypeId params, SemIR::FacetTypeId args,
-              bool needs_substitution) -> void {
-    const auto& param_impls =
-        context_->facet_types().Get(params).impls_constraints;
-    const auto& arg_impls = context_->facet_types().Get(args).impls_constraints;
-    // TODO: Decide whether to error on these or just treat the parameter list
-    // as non-deduced. For now we treat it as non-deduced.
-    if (param_impls.size() != 1 || arg_impls.size() != 1) {
-      return;
-    }
-    auto param = param_impls.front();
-    auto arg = arg_impls.front();
-    if (param.interface_id != arg.interface_id) {
-      return;
-    }
-    Add(param.specific_id, arg.specific_id, needs_substitution);
-  }
-
   // Adds a (param, arg) pair for an instruction argument, given its kind.
   auto AddInstArg(SemIR::Inst::ArgAndKind param, int32_t arg,
                   bool needs_substitution) -> void {
@@ -144,6 +126,11 @@ class DeductionWorklist {
       case SemIR::IdKind::None:
       case SemIR::IdKind::For<SemIR::ClassId>:
       case SemIR::IdKind::For<SemIR::IntKind>:
+      // Decided on 2025-04-02 not to do deduction through facet types, because
+      // types can implement a generic interface multiple times with different
+      // arguments. See:
+      // https://docs.google.com/document/d/1Iut5f2TQBrtBNIduF4vJYOKfw7MbS8xH_J01_Q4e6Rk/edit?pli=1&resourcekey=0-mc_vh5UzrzXfU4kO-3tOjA&tab=t.0#heading=h.95phmuvxog9n
+      case SemIR::IdKind::For<SemIR::FacetTypeId>:
         break;
       case CARBON_KIND(SemIR::InstId inst_id): {
         Add(inst_id, SemIR::InstId(arg), needs_substitution);
@@ -169,10 +156,6 @@ class DeductionWorklist {
         Add(specific_id, SemIR::SpecificId(arg), needs_substitution);
         break;
       }
-      case CARBON_KIND(SemIR::FacetTypeId facet_type_id): {
-        AddAll(facet_type_id, SemIR::FacetTypeId(arg), needs_substitution);
-        break;
-      }
       default:
         CARBON_FATAL("unexpected argument kind");
     }

toolchain/check/eval.cpp

@@ -592,9 +592,16 @@ static auto GetConstantFacetTypeInfo(EvalContext& eval_context,
                                      Phase* phase) -> SemIR::FacetTypeInfo {
   const auto& orig = eval_context.facet_types().Get(facet_type_id);
   SemIR::FacetTypeInfo info;
-  info.impls_constraints.reserve(orig.impls_constraints.size());
-  for (const auto& interface : orig.impls_constraints) {
-    info.impls_constraints.push_back(
+  info.extend_constraints.reserve(orig.extend_constraints.size());
+  for (const auto& interface : orig.extend_constraints) {
+    info.extend_constraints.push_back(
+        {.interface_id = interface.interface_id,
+         .specific_id =
+             GetConstantValue(eval_context, interface.specific_id, phase)});
+  }
+  info.self_impls_constraints.reserve(orig.self_impls_constraints.size());
+  for (const auto& interface : orig.self_impls_constraints) {
+    info.self_impls_constraints.push_back(
         {.interface_id = interface.interface_id,
          .specific_id =
              GetConstantValue(eval_context, interface.specific_id, phase)});
@@ -1816,6 +1823,34 @@ auto TryEvalTypedInst<SemIR::BindSymbolicName>(EvalContext& eval_context,
   return MakeConstantResult(eval_context.context(), bind, phase);
 }
 
+static auto IsPeriodSelf(EvalContext& eval_context, SemIR::ConstantId const_id)
+    -> bool {
+  // This also rejects the singleton Error value as it's concrete.
+  if (!const_id.is_symbolic()) {
+    return false;
+  }
+  const auto& symbolic =
+      eval_context.constant_values().GetSymbolicConstant(const_id);
+  // Fast early reject before doing more expensive operations.
+  if (symbolic.dependence != SemIR::ConstantDependence::PeriodSelf) {
+    return false;
+  }
+  auto inst_id = symbolic.inst_id;
+  // Unwrap the `FacetAccessType` instruction, which we get when the `.Self` is
+  // converted to `type`.
+  if (auto facet_access_type =
+          eval_context.insts().TryGetAs<SemIR::FacetAccessType>(inst_id)) {
+    inst_id = facet_access_type->facet_value_inst_id;
+  }
+  if (auto bind_symbolic_name =
+          eval_context.insts().TryGetAs<SemIR::BindSymbolicName>(inst_id)) {
+    const auto& bind_name =
+        eval_context.entity_names().Get(bind_symbolic_name->entity_name_id);
+    return bind_name.name_id == SemIR::NameId::PeriodSelf;
+  }
+  return false;
+}
+
 // TODO: Convert this to an EvalConstantInst instruction. This will require
 // providing a `GetConstantValue` overload for a requirement block.
 template <>
@@ -1856,6 +1891,37 @@ auto TryEvalTypedInst<SemIR::WhereExpr>(EvalContext& eval_context,
         UpdatePhaseIgnorePeriodSelf(eval_context, rhs, &phase);
         info.rewrite_constraints.push_back(
             {.lhs_const_id = lhs, .rhs_const_id = rhs});
+      } else if (auto impls =
+                     eval_context.insts().TryGetAs<SemIR::RequirementImpls>(
+                         inst_id)) {
+        SemIR::ConstantId lhs = eval_context.GetConstantValue(impls->lhs_id);
+        SemIR::ConstantId rhs = eval_context.GetConstantValue(impls->rhs_id);
+        if (rhs != SemIR::ErrorInst::SingletonConstantId &&
+            IsPeriodSelf(eval_context, lhs)) {
+          auto rhs_inst_id = eval_context.constant_values().GetInstId(rhs);
+          if (rhs_inst_id == SemIR::TypeType::SingletonInstId) {
+            // `.Self impls type` -> nothing to do.
+          } else {
+            auto facet_type =
+                eval_context.insts().GetAs<SemIR::FacetType>(rhs_inst_id);
+            SemIR::FacetTypeInfo more_info = GetConstantFacetTypeInfo(
+                eval_context, facet_type.facet_type_id, &phase);
+            // The way to prevent lookup into the interface requirements of a
+            // facet type is to put it to the right of a `.Self impls`, which we
+            // accomplish by putting them into `self_impls_constraints`.
+            llvm::append_range(info.self_impls_constraints,
+                               more_info.extend_constraints);
+            llvm::append_range(info.self_impls_constraints,
+                               more_info.self_impls_constraints);
+            // Other requirements are copied in.
+            llvm::append_range(info.rewrite_constraints,
+                               more_info.rewrite_constraints);
+            info.other_requirements |= more_info.other_requirements;
+          }
+        } else {
+          // TODO: Handle `impls` constraints beyond `.Self impls`.
+          info.other_requirements = true;
+        }
       } else {
         // TODO: Handle other requirements
         info.other_requirements = true;

toolchain/check/facet_type.cpp

@@ -16,7 +16,7 @@ namespace Carbon::Check {
 auto FacetTypeFromInterface(Context& context, SemIR::InterfaceId interface_id,
                             SemIR::SpecificId specific_id) -> SemIR::FacetType {
   SemIR::FacetTypeId facet_type_id = context.facet_types().Add(
-      SemIR::FacetTypeInfo{.impls_constraints = {{interface_id, specific_id}},
+      SemIR::FacetTypeInfo{.extend_constraints = {{interface_id, specific_id}},
                            .other_requirements = false});
   return {.type_id = SemIR::TypeType::SingletonTypeId,
           .facet_type_id = facet_type_id};
@@ -30,26 +30,30 @@ static auto WitnessAccessMatchesInterface(
   auto access = context.insts().GetAs<SemIR::FacetAccessWitness>(witness_id);
   auto type_id = context.insts().Get(access.facet_value_inst_id).type_id();
   auto facet_type = context.types().GetAs<SemIR::FacetType>(type_id);
-  const auto& facet_info = context.facet_types().Get(facet_type.facet_type_id);
-  if (auto impls = facet_info.TryAsSingleInterface()) {
-    return impls->interface_id == interface.interface_id &&
-           impls->specific_id == interface.specific_id;
-  }
-  return false;
+  // The order of witnesses is from the identified facet type.
+  auto identified_id = RequireIdentifiedFacetType(context, facet_type);
+  const auto& identified = context.identified_facet_types().Get(identified_id);
+  const auto& impls = identified.required_interfaces()[access.index.index];
+  return impls == interface;
 }
 
 static auto IncompleteFacetTypeDiagnosticBuilder(
     Context& context, SemIRLoc loc, SemIR::InstId facet_type_inst_id,
     bool is_definition) -> DiagnosticBuilder {
-  // The other case is "impl as incomplete facet type with rewrites", but
-  // currently all incomplete facet types with rewrites trigger errors before
-  // this.
-  CARBON_CHECK(is_definition);
-  CARBON_DIAGNOSTIC(ImplAsIncompleteFacetTypeDefinition, Error,
-                    "definition of impl as incomplete facet type {0}",
-                    InstIdAsType);
-  return context.emitter().Build(loc, ImplAsIncompleteFacetTypeDefinition,
-                                 facet_type_inst_id);
+  if (is_definition) {
+    CARBON_DIAGNOSTIC(ImplAsIncompleteFacetTypeDefinition, Error,
+                      "definition of impl as incomplete facet type {0}",
+                      InstIdAsType);
+    return context.emitter().Build(loc, ImplAsIncompleteFacetTypeDefinition,
+                                   facet_type_inst_id);
+  } else {
+    CARBON_DIAGNOSTIC(
+        ImplAsIncompleteFacetTypeRewrites, Error,
+        "declaration of impl as incomplete facet type {0} with rewrites",
+        InstIdAsType);
+    return context.emitter().Build(loc, ImplAsIncompleteFacetTypeRewrites,
+                                   facet_type_inst_id);
+  }
 }
 
 auto InitialFacetTypeImplWitness(

toolchain/check/impl_lookup.cpp

@@ -94,7 +94,11 @@ static auto FindAssociatedImportIRs(Context& context,
         case CARBON_KIND(SemIR::FacetTypeId facet_type_id): {
           const auto& facet_type_info =
               context.facet_types().Get(facet_type_id);
-          for (const auto& impl : facet_type_info.impls_constraints) {
+          for (const auto& impl : facet_type_info.extend_constraints) {
+            add_entity(context.interfaces().Get(impl.interface_id));
+            push_args(impl.specific_id);
+          }
+          for (const auto& impl : facet_type_info.self_impls_constraints) {
             add_entity(context.interfaces().Get(impl.interface_id));
             push_args(impl.specific_id);
           }
@@ -195,9 +199,12 @@ static auto GetInterfacesFromConstantId(
   const auto& facet_type_info =
       context.facet_types().Get(facet_type_inst.facet_type_id);
   has_other_requirements = facet_type_info.other_requirements;
-  // TODO: This needs to match the order of witnesses for the facet type, which
-  // will need to be maintained once we add support for named constraints.
-  return facet_type_info.impls_constraints;
+  auto identified_id = RequireIdentifiedFacetType(context, facet_type_inst);
+  auto interfaces_array_ref =
+      context.identified_facet_types().Get(identified_id).required_interfaces();
+  // Returns a copy to avoid use-after-free when the identified_facet_types
+  // store resizes.
+  return {interfaces_array_ref.begin(), interfaces_array_ref.end()};
 }
 
 static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
@@ -259,7 +266,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
           .facet_type_id;
   const auto& deduced_constraint_facet_type_info =
       context.facet_types().Get(deduced_constraint_facet_type_id);
-  CARBON_CHECK(deduced_constraint_facet_type_info.impls_constraints.size() ==
+  CARBON_CHECK(deduced_constraint_facet_type_info.extend_constraints.size() ==
                1);
 
   if (deduced_constraint_facet_type_info.other_requirements) {
@@ -270,7 +277,7 @@ static auto GetWitnessIdForImpl(Context& context, SemIR::LocId loc_id,
   // The specifics in the queried interface must match the deduced specifics in
   // the impl's constraint facet type.
   auto impl_interface_specific_id =
-      deduced_constraint_facet_type_info.impls_constraints[0].specific_id;
+      deduced_constraint_facet_type_info.extend_constraints[0].specific_id;
   auto query_interface_specific_id = interface.specific_id;
   if (impl_interface_specific_id != query_interface_specific_id) {
     return EvalImplLookupResult::MakeNone();
@@ -307,14 +314,11 @@ static auto FindWitnessInFacet(
   SemIR::TypeId facet_type_id = context.insts().Get(facet_inst_id).type_id();
   if (auto facet_type_inst =
           context.types().TryGetAs<SemIR::FacetType>(facet_type_id)) {
-    const auto& facet_type_info =
-        context.facet_types().Get(facet_type_inst->facet_type_id);
-    // TODO: This depends on the index into `impls_constraints` matching
-    // the index into the facet type witness. This will have to be maintained
-    // even for facet types that include named constraints, once that is
-    // supported.
+    auto identified_id = RequireIdentifiedFacetType(context, *facet_type_inst);
+    const auto& identified =
+        context.identified_facet_types().Get(identified_id);
     for (auto [index, interface] :
-         llvm::enumerate(facet_type_info.impls_constraints)) {
+         llvm::enumerate(identified.required_interfaces())) {
       if (interface == specific_interface) {
         auto witness_id =
             GetOrAddInst(context, loc_id,

toolchain/check/import_ref.cpp

@@ -991,7 +991,7 @@ static auto GetLocalSpecificInterface(
   if (auto facet_type = interface_const_inst.TryAs<SemIR::FacetType>()) {
     const SemIR::FacetTypeInfo& new_facet_type_info =
         context.local_facet_types().Get(facet_type->facet_type_id);
-    return new_facet_type_info.impls_constraints.front();
+    return *new_facet_type_info.TryAsSingleInterface();
   } else {
     auto generic_interface_type =
         context.local_types().GetAs<SemIR::GenericInterfaceType>(
@@ -2450,14 +2450,19 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
                                 SemIR::FacetType inst) -> ResolveResult {
   CARBON_CHECK(inst.type_id == SemIR::TypeType::SingletonTypeId);
 
-  const SemIR::FacetTypeInfo& facet_type_info =
+  const SemIR::FacetTypeInfo& import_facet_type_info =
       resolver.import_facet_types().Get(inst.facet_type_id);
-  for (auto interface : facet_type_info.impls_constraints) {
+  for (auto interface : import_facet_type_info.extend_constraints) {
     // We discard this here and recompute it below instead of saving it to avoid
     // allocations.
     GetLocalSpecificInterfaceData(resolver, interface);
   }
-  for (auto rewrite : facet_type_info.rewrite_constraints) {
+  for (auto interface : import_facet_type_info.self_impls_constraints) {
+    // We discard this here and recompute it below instead of saving it to avoid
+    // allocations.
+    GetLocalSpecificInterfaceData(resolver, interface);
+  }
+  for (auto rewrite : import_facet_type_info.rewrite_constraints) {
     GetLocalConstantId(resolver, rewrite.lhs_const_id);
     GetLocalConstantId(resolver, rewrite.rhs_const_id);
   }
@@ -2465,25 +2470,32 @@ static auto TryResolveTypedInst(ImportRefResolver& resolver,
     return ResolveResult::Retry();
   }
 
-  llvm::SmallVector<SemIR::FacetTypeInfo::ImplsConstraint> impls_constraints;
-  for (auto interface : facet_type_info.impls_constraints) {
+  SemIR::FacetTypeInfo local_facet_type_info = {
+      .other_requirements = import_facet_type_info.other_requirements};
+  local_facet_type_info.extend_constraints.reserve(
+      import_facet_type_info.extend_constraints.size());
+  for (auto interface : import_facet_type_info.extend_constraints) {
+    auto data = GetLocalSpecificInterfaceData(resolver, interface);
+    local_facet_type_info.extend_constraints.push_back(
+        GetLocalSpecificInterface(resolver, interface, data));
+  }
+  local_facet_type_info.self_impls_constraints.reserve(
+      import_facet_type_info.self_impls_constraints.size());
+  for (auto interface : import_facet_type_info.self_impls_constraints) {
     auto data = GetLocalSpecificInterfaceData(resolver, interface);
-    impls_constraints.push_back(
+    local_facet_type_info.self_impls_constraints.push_back(
         GetLocalSpecificInterface(resolver, interface, data));
   }
-  llvm::SmallVector<SemIR::FacetTypeInfo::RewriteConstraint>
-      rewrite_constraints;
-  for (auto rewrite : facet_type_info.rewrite_constraints) {
-    rewrite_constraints.push_back(
+  local_facet_type_info.rewrite_constraints.reserve(
+      import_facet_type_info.rewrite_constraints.size());
+  for (auto rewrite : import_facet_type_info.rewrite_constraints) {
+    local_facet_type_info.rewrite_constraints.push_back(
         {.lhs_const_id = GetLocalConstantId(resolver, rewrite.lhs_const_id),
          .rhs_const_id = GetLocalConstantId(resolver, rewrite.rhs_const_id)});
   }
   // TODO: Also process the other requirements.
   SemIR::FacetTypeId facet_type_id =
-      resolver.local_facet_types().Add(SemIR::FacetTypeInfo{
-          .impls_constraints = impls_constraints,
-          .rewrite_constraints = rewrite_constraints,
-          .other_requirements = facet_type_info.other_requirements});
+      resolver.local_facet_types().Add(std::move(local_facet_type_info));
   return ResolveAs<SemIR::FacetType>(
       resolver, {.type_id = SemIR::TypeType::SingletonTypeId,
                  .facet_type_id = facet_type_id});

toolchain/check/member_access.cpp

@@ -306,19 +306,13 @@ static auto LookupMemberNameInScope(Context& context, SemIR::LocId loc_id,
         // First look for `assoc_interface` in the type of the base. If it is
         // found, get the witness that the interface is implemented from
         // `base_id`.
-        const auto& facet_type_info =
-            context.facet_types().Get(facet_type->facet_type_id);
+        auto identified_id = RequireIdentifiedFacetType(context, *facet_type);
+        const auto& identified =
+            context.identified_facet_types().Get(identified_id);
         // Witness that `T` implements the `assoc_interface`.
         SemIR::InstId witness_inst_id = SemIR::InstId::None;
-        // TODO: This assumes `impls_constraints` are in the same order as
-        // `CompleteFacetType::required_interfaces`, and come first in the list.
-        // Once we add support for named constraints there may be more
-        // interfaces in the `CompleteFacetType`, and we will require those
-        // additional interfaces in the `CompleteFacetType` to come after the
-        // ones we see in `impls_constraints` in order to not invalidate the
-        // index computed here.
         for (auto [index, base_interface] :
-             llvm::enumerate(facet_type_info.impls_constraints)) {
+             llvm::enumerate(identified.required_interfaces())) {
           // Get the witness that `T` implements `base_type_id`.
           if (base_interface == assoc_interface) {
             witness_inst_id = GetOrAddInst(

toolchain/check/name_lookup.cpp

@@ -319,12 +319,11 @@ auto AppendLookupScopesForConstant(Context& context, SemIR::LocId loc_id,
               return context.emitter().Build(
                   loc_id, QualifiedExprInIncompleteFacetTypeScope, base_id);
             })) {
-      auto identified_id =
-          RequireIdentifiedFacetType(context, *base_as_facet_type);
-      CARBON_CHECK(identified_id.has_value());
-      const auto& identified =
-          context.identified_facet_types().Get(identified_id);
-      for (const auto& interface : identified.required_interfaces()) {
+      auto facet_type_info =
+          context.facet_types().Get(base_as_facet_type->facet_type_id);
+      // Name lookup into "extend" constraints but not "self impls" constraints.
+      // TODO: Include named constraints, once they are supported.
+      for (const auto& interface : facet_type_info.extend_constraints) {
         auto& interface_info = context.interfaces().Get(interface.interface_id);
         scopes->push_back({.name_scope_id = interface_info.scope_id,
                            .specific_id = interface.specific_id});

toolchain/check/subst.cpp

@@ -121,7 +121,10 @@ 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.impls_constraints) {
+      for (auto interface : facet_type_info.extend_constraints) {
+        push_specific(interface.specific_id);
+      }
+      for (auto interface : facet_type_info.self_impls_constraints) {
         push_specific(interface.specific_id);
       }
       for (auto rewrite : facet_type_info.rewrite_constraints) {
@@ -242,12 +245,22 @@ static auto PopOperand(Context& context, Worklist& worklist,
         auto lhs_id = context.constant_values().Get(worklist.Pop());
         new_constraint = {.lhs_const_id = lhs_id, .rhs_const_id = rhs_id};
       }
-      new_facet_type_info.impls_constraints.resize(
-          old_facet_type_info.impls_constraints.size(),
+      new_facet_type_info.self_impls_constraints.resize(
+          old_facet_type_info.self_impls_constraints.size(),
+          SemIR::SpecificInterface::None);
+      for (auto [old_constraint, new_constraint] : llvm::reverse(
+               llvm::zip(old_facet_type_info.self_impls_constraints,
+                         new_facet_type_info.self_impls_constraints))) {
+        new_constraint = {
+            .interface_id = old_constraint.interface_id,
+            .specific_id = pop_specific(old_constraint.specific_id)};
+      }
+      new_facet_type_info.extend_constraints.resize(
+          old_facet_type_info.extend_constraints.size(),
           SemIR::SpecificInterface::None);
       for (auto [old_constraint, new_constraint] :
-           llvm::reverse(llvm::zip(old_facet_type_info.impls_constraints,
-                                   new_facet_type_info.impls_constraints))) {
+           llvm::reverse(llvm::zip(old_facet_type_info.extend_constraints,
+                                   new_facet_type_info.extend_constraints))) {
         new_constraint = {
             .interface_id = old_constraint.interface_id,
             .specific_id = pop_specific(old_constraint.specific_id)};

toolchain/check/testdata/facet/min_prelude/combine.carbon

@@ -130,3 +130,104 @@ fn G[T:! Iface & GenericIface(GenericClass(ImplIface))](t: T) {}
 fn F() {
   G({} as C);
 }
+
+// --- compare_equal.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn AssertSame[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I;
+interface J;
+interface K(T:! type);
+
+fn TestIncomplete() {
+  AssertSame(Type(I), Type(I & I));
+  AssertSame(Type(I), Type(I & I & I));
+  AssertSame(Type(I & J), Type(J & I));
+  AssertSame(Type(I & J), Type(I & I & J));
+  AssertSame(Type(I & J), Type(I & J & I));
+  AssertSame(Type(I & J), Type(J & I & I));
+  AssertSame(Type(I & K({})), Type(K({}) & I));
+  AssertSame(Type(I & K({}) & K(())), Type(K(()) & K({}) & I));
+}
+
+interface I {}
+interface J {}
+interface K(T:! type) {}
+
+fn TestComplete() {
+  AssertSame(Type(I), Type(I & I));
+  AssertSame(Type(I), Type(I & I & I));
+  AssertSame(Type(I & J), Type(J & I));
+  AssertSame(Type(I & J), Type(I & I & J));
+  AssertSame(Type(I & J), Type(I & J & I));
+  AssertSame(Type(I & J), Type(J & I & I));
+  AssertSame(Type(I & K({})), Type(K({}) & I));
+  AssertSame(Type(I & K({}) & K(())), Type(K(()) & K({}) & I));
+}
+
+// --- fail_compare_not_equal.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I {}
+interface J {}
+interface K {}
+
+fn Test() {
+  // CHECK:STDERR: fail_compare_not_equal.carbon:[[@LINE+7]]:3: error: inconsistent deductions for value of generic parameter `T` [DeductionInconsistent]
+  // CHECK:STDERR:   Same(Type(I & J), Type(K & I & J));
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_compare_not_equal.carbon:[[@LINE-11]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  Same(Type(I & J), Type(K & I & J));
+}
+
+// --- fail_compare_not_equal_parameterized.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I {}
+interface J(T:! type) {}
+
+fn Test() {
+  // CHECK:STDERR: fail_compare_not_equal_parameterized.carbon:[[@LINE+7]]:3: error: inconsistent deductions for value of generic parameter `T` [DeductionInconsistent]
+  // CHECK:STDERR:   Same(Type(I & J(())), Type(J({}) & I));
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_compare_not_equal_parameterized.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  Same(Type(I & J(())), Type(J({}) & I));
+}
+
+// --- fail_compare_not_equal_parameterized_extra.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I {}
+interface J(T:! type) {}
+
+fn Test() {
+  // CHECK:STDERR: fail_compare_not_equal_parameterized_extra.carbon:[[@LINE+7]]:3: error: inconsistent deductions for value of generic parameter `T` [DeductionInconsistent]
+  // CHECK:STDERR:   Same(Type(I & J(())), Type(J(()) & J({}) & I));
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_compare_not_equal_parameterized_extra.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  Same(Type(I & J(())), Type(J(()) & J({}) & I));
+}

toolchain/check/testdata/facet/min_prelude/convert_facet_value_to_narrowed_facet_type.carbon

@@ -75,30 +75,16 @@ fn CallsWithExtraWhereExplicit(U:! type where .Self impls type) {
   TakesTypeExplicit(U);
 }
 
-// --- fail_todo_no_interfaces.carbon
+// --- no_interfaces.carbon
 library "[[@TEST_NAME]]";
 
 fn TakesExtraWhereDeduced[T:! type where .Self impls type](x: T) {}
 fn CallsWithType[U:! type](y: U) {
-  // CHECK:STDERR: fail_todo_no_interfaces.carbon:[[@LINE+7]]:3: error: cannot convert type `U` into type implementing `type where...` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   TakesExtraWhereDeduced(y);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR: fail_todo_no_interfaces.carbon:[[@LINE-5]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
-  // CHECK:STDERR: fn TakesExtraWhereDeduced[T:! type where .Self impls type](x: T) {}
-  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR:
   TakesExtraWhereDeduced(y);
 }
 
 fn TakesExtraWhereExplicit(T:! type where .Self impls type) {}
 fn CallsWithTypeExplicit(U:! type) {
-  // CHECK:STDERR: fail_todo_no_interfaces.carbon:[[@LINE+7]]:3: error: cannot convert type `U` into type implementing `type where...` [ConversionFailureTypeToFacet]
-  // CHECK:STDERR:   TakesExtraWhereExplicit(U);
-  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~
-  // CHECK:STDERR: fail_todo_no_interfaces.carbon:[[@LINE-5]]:28: note: initializing generic parameter `T` declared here [InitializingGenericParam]
-  // CHECK:STDERR: fn TakesExtraWhereExplicit(T:! type where .Self impls type) {}
-  // CHECK:STDERR:                            ^
-  // CHECK:STDERR:
   TakesExtraWhereExplicit(U);
 }
 
@@ -1052,19 +1038,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %TakesA.type: type = fn_type @TakesA [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %TakesA: %TakesA.type = struct_value () [concrete]
-// CHECK:STDOUT:   %require_complete.cf4: <witness> = require_complete_type %T.as_type [symbolic]
+// CHECK:STDOUT:   %require_complete.cf45b7.1: <witness> = require_complete_type %T.as_type [symbolic]
 // CHECK:STDOUT:   %.Self: %A.type = bind_symbolic_name .Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
-// CHECK:STDOUT:   %A_where.type: type = facet_type <@A where TODO> [concrete]
-// CHECK:STDOUT:   %U: %A_where.type = bind_symbolic_name U, 0 [symbolic]
-// CHECK:STDOUT:   %U.patt: %A_where.type = symbolic_binding_pattern U, 0 [symbolic]
+// CHECK:STDOUT:   %U: %A.type = bind_symbolic_name U, 0 [symbolic]
+// CHECK:STDOUT:   %U.patt: %A.type = symbolic_binding_pattern U, 0 [symbolic]
 // CHECK:STDOUT:   %U.as_type: type = facet_access_type %U [symbolic]
 // CHECK:STDOUT:   %WithExtraWhere.type: type = fn_type @WithExtraWhere [concrete]
 // CHECK:STDOUT:   %WithExtraWhere: %WithExtraWhere.type = struct_value () [concrete]
-// CHECK:STDOUT:   %require_complete.732: <witness> = require_complete_type %U.as_type [symbolic]
-// CHECK:STDOUT:   %U.as_wit.iface0: <witness> = facet_access_witness %U, element0 [symbolic]
-// CHECK:STDOUT:   %A.facet: %A.type = facet_value %U.as_type, (%U.as_wit.iface0) [symbolic]
-// CHECK:STDOUT:   %TakesA.specific_fn: <specific function> = specific_function %TakesA, @TakesA(%A.facet) [symbolic]
+// CHECK:STDOUT:   %require_complete.cf45b7.2: <witness> = require_complete_type %U.as_type [symbolic]
+// CHECK:STDOUT:   %TakesA.specific_fn: <specific function> = specific_function %TakesA, @TakesA(%U) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1098,24 +1081,24 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %x: @TakesA.%T.as_type.loc7_21.2 (%T.as_type) = bind_name x, %x.param
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %WithExtraWhere.decl: %WithExtraWhere.type = fn_decl @WithExtraWhere [concrete = constants.%WithExtraWhere] {
-// CHECK:STDOUT:     %U.patt.loc9_19.1: %A_where.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_19.2 (constants.%U.patt)]
+// CHECK:STDOUT:     %U.patt.loc9_19.1: %A.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_19.2 (constants.%U.patt)]
 // CHECK:STDOUT:     %y.patt: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) = binding_pattern y
 // CHECK:STDOUT:     %y.param_patt: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) = value_param_pattern %y.patt, call_param0
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc9_25.1: type = splice_block %.loc9_25.2 [concrete = constants.%A_where.type] {
+// CHECK:STDOUT:     %.loc9_25.1: type = splice_block %.loc9_25.2 [concrete = constants.%A.type] {
 // CHECK:STDOUT:       %A.ref: type = name_ref A, file.%A.decl [concrete = constants.%A.type]
 // CHECK:STDOUT:       %.Self: %A.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: %A.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
 // CHECK:STDOUT:       %.loc9_31: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
-// CHECK:STDOUT:       %.loc9_25.2: type = where_expr %.Self [concrete = constants.%A_where.type] {
+// CHECK:STDOUT:       %.loc9_25.2: type = where_expr %.Self [concrete = constants.%A.type] {
 // CHECK:STDOUT:         requirement_impls %.loc9_31, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %U.loc9_19.1: %A_where.type = bind_symbolic_name U, 0 [symbolic = %U.loc9_19.2 (constants.%U)]
+// CHECK:STDOUT:     %U.loc9_19.1: %A.type = bind_symbolic_name U, 0 [symbolic = %U.loc9_19.2 (constants.%U)]
 // CHECK:STDOUT:     %y.param: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) = value_param call_param0
 // CHECK:STDOUT:     %.loc9_52.1: type = splice_block %.loc9_52.2 [symbolic = %U.as_type.loc9_52.2 (constants.%U.as_type)] {
-// CHECK:STDOUT:       %U.ref: %A_where.type = name_ref U, %U.loc9_19.1 [symbolic = %U.loc9_19.2 (constants.%U)]
+// CHECK:STDOUT:       %U.ref: %A.type = name_ref U, %U.loc9_19.1 [symbolic = %U.loc9_19.2 (constants.%U)]
 // CHECK:STDOUT:       %U.as_type.loc9_52.1: type = facet_access_type %U.ref [symbolic = %U.as_type.loc9_52.2 (constants.%U.as_type)]
 // CHECK:STDOUT:       %.loc9_52.2: type = converted %U.ref, %U.as_type.loc9_52.1 [symbolic = %U.as_type.loc9_52.2 (constants.%U.as_type)]
 // CHECK:STDOUT:     }
@@ -1137,7 +1120,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %T.as_type.loc7_21.2: type = facet_access_type %T.loc7_11.2 [symbolic = %T.as_type.loc7_21.2 (constants.%T.as_type)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @TakesA.%T.as_type.loc7_21.2 (%T.as_type) [symbolic = %require_complete (constants.%require_complete.cf4)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @TakesA.%T.as_type.loc7_21.2 (%T.as_type) [symbolic = %require_complete (constants.%require_complete.cf45b7.1)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%T.patt.loc7_11.1: %A.type](%x.param_patt: @TakesA.%T.as_type.loc7_21.2 (%T.as_type)) {
 // CHECK:STDOUT:   !entry:
@@ -1145,28 +1128,22 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @WithExtraWhere(%U.loc9_19.1: %A_where.type) {
-// CHECK:STDOUT:   %U.loc9_19.2: %A_where.type = bind_symbolic_name U, 0 [symbolic = %U.loc9_19.2 (constants.%U)]
-// CHECK:STDOUT:   %U.patt.loc9_19.2: %A_where.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_19.2 (constants.%U.patt)]
+// CHECK:STDOUT: generic fn @WithExtraWhere(%U.loc9_19.1: %A.type) {
+// CHECK:STDOUT:   %U.loc9_19.2: %A.type = bind_symbolic_name U, 0 [symbolic = %U.loc9_19.2 (constants.%U)]
+// CHECK:STDOUT:   %U.patt.loc9_19.2: %A.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_19.2 (constants.%U.patt)]
 // CHECK:STDOUT:   %U.as_type.loc9_52.2: type = facet_access_type %U.loc9_19.2 [symbolic = %U.as_type.loc9_52.2 (constants.%U.as_type)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) [symbolic = %require_complete (constants.%require_complete.732)]
-// CHECK:STDOUT:   %U.as_wit.iface0.loc10_11.3: <witness> = facet_access_witness %U.loc9_19.2, element0 [symbolic = %U.as_wit.iface0.loc10_11.3 (constants.%U.as_wit.iface0)]
-// CHECK:STDOUT:   %A.facet.loc10_11.3: %A.type = facet_value %U.as_type.loc9_52.2, (%U.as_wit.iface0.loc10_11.3) [symbolic = %A.facet.loc10_11.3 (constants.%A.facet)]
-// CHECK:STDOUT:   %TakesA.specific_fn.loc10_3.2: <specific function> = specific_function constants.%TakesA, @TakesA(%A.facet.loc10_11.3) [symbolic = %TakesA.specific_fn.loc10_3.2 (constants.%TakesA.specific_fn)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) [symbolic = %require_complete (constants.%require_complete.cf45b7.2)]
+// CHECK:STDOUT:   %TakesA.specific_fn.loc10_3.2: <specific function> = specific_function constants.%TakesA, @TakesA(%U.loc9_19.2) [symbolic = %TakesA.specific_fn.loc10_3.2 (constants.%TakesA.specific_fn)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn[%U.patt.loc9_19.1: %A_where.type](%y.param_patt: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type)) {
+// CHECK:STDOUT:   fn[%U.patt.loc9_19.1: %A.type](%y.param_patt: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type)) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %TakesA.ref: %TakesA.type = name_ref TakesA, file.%TakesA.decl [concrete = constants.%TakesA]
 // CHECK:STDOUT:     %y.ref: @WithExtraWhere.%U.as_type.loc9_52.2 (%U.as_type) = name_ref y, %y
-// CHECK:STDOUT:     %U.as_wit.iface0.loc10_11.1: <witness> = facet_access_witness constants.%U, element0 [symbolic = %U.as_wit.iface0.loc10_11.3 (constants.%U.as_wit.iface0)]
-// CHECK:STDOUT:     %A.facet.loc10_11.1: %A.type = facet_value constants.%U.as_type, (%U.as_wit.iface0.loc10_11.1) [symbolic = %A.facet.loc10_11.3 (constants.%A.facet)]
-// CHECK:STDOUT:     %.loc10_11.1: %A.type = converted constants.%U.as_type, %A.facet.loc10_11.1 [symbolic = %A.facet.loc10_11.3 (constants.%A.facet)]
-// CHECK:STDOUT:     %U.as_wit.iface0.loc10_11.2: <witness> = facet_access_witness constants.%U, element0 [symbolic = %U.as_wit.iface0.loc10_11.3 (constants.%U.as_wit.iface0)]
-// CHECK:STDOUT:     %A.facet.loc10_11.2: %A.type = facet_value constants.%U.as_type, (%U.as_wit.iface0.loc10_11.2) [symbolic = %A.facet.loc10_11.3 (constants.%A.facet)]
-// CHECK:STDOUT:     %.loc10_11.2: %A.type = converted constants.%U.as_type, %A.facet.loc10_11.2 [symbolic = %A.facet.loc10_11.3 (constants.%A.facet)]
-// CHECK:STDOUT:     %TakesA.specific_fn.loc10_3.1: <specific function> = specific_function %TakesA.ref, @TakesA(constants.%A.facet) [symbolic = %TakesA.specific_fn.loc10_3.2 (constants.%TakesA.specific_fn)]
+// CHECK:STDOUT:     %.loc10_11.1: %A.type = converted constants.%U.as_type, constants.%U [symbolic = %U.loc9_19.2 (constants.%U)]
+// CHECK:STDOUT:     %.loc10_11.2: %A.type = converted constants.%U.as_type, constants.%U [symbolic = %U.loc9_19.2 (constants.%U)]
+// CHECK:STDOUT:     %TakesA.specific_fn.loc10_3.1: <specific function> = specific_function %TakesA.ref, @TakesA(constants.%U) [symbolic = %TakesA.specific_fn.loc10_3.2 (constants.%TakesA.specific_fn)]
 // CHECK:STDOUT:     %TakesA.call: init %empty_tuple.type = call %TakesA.specific_fn.loc10_3.1(%y.ref)
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -1184,16 +1161,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %U.as_type.loc9_52.2 => constants.%U.as_type
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @TakesA(constants.%A.facet) {
-// CHECK:STDOUT:   %T.loc7_11.2 => constants.%A.facet
+// CHECK:STDOUT: specific @TakesA(constants.%U) {
+// CHECK:STDOUT:   %T.loc7_11.2 => constants.%U
 // CHECK:STDOUT:   %T.patt.loc7_11.2 => constants.%T.patt
 // CHECK:STDOUT:   %T.as_type.loc7_21.2 => constants.%U.as_type
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.732
+// CHECK:STDOUT:   %require_complete => constants.%require_complete.cf45b7.2
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @TakesA(@WithExtraWhere.%A.facet.loc10_11.3) {}
+// CHECK:STDOUT: specific @TakesA(@WithExtraWhere.%U.loc9_19.2) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- no_interfaces_success.carbon
 // CHECK:STDOUT:
@@ -1205,13 +1182,13 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %TakesTypeDeduced: %TakesTypeDeduced.type = struct_value () [concrete]
 // CHECK:STDOUT:   %require_complete.4ae: <witness> = require_complete_type %T [symbolic]
 // CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
-// CHECK:STDOUT:   %U: %type_where = bind_symbolic_name U, 0 [symbolic]
-// CHECK:STDOUT:   %U.patt: %type_where = symbolic_binding_pattern U, 0 [symbolic]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %U: %type = bind_symbolic_name U, 0 [symbolic]
+// CHECK:STDOUT:   %U.patt: %type = symbolic_binding_pattern U, 0 [symbolic]
 // CHECK:STDOUT:   %U.as_type: type = facet_access_type %U [symbolic]
 // CHECK:STDOUT:   %CallsWithExtraWhere.type: type = fn_type @CallsWithExtraWhere [concrete]
 // CHECK:STDOUT:   %CallsWithExtraWhere: %CallsWithExtraWhere.type = struct_value () [concrete]
-// CHECK:STDOUT:   %require_complete.220: <witness> = require_complete_type %U.as_type [symbolic]
+// CHECK:STDOUT:   %require_complete.5eb: <witness> = require_complete_type %U.as_type [symbolic]
 // CHECK:STDOUT:   %TakesTypeDeduced.specific_fn: <specific function> = specific_function %TakesTypeDeduced, @TakesTypeDeduced(%U.as_type) [symbolic]
 // CHECK:STDOUT:   %TakesTypeExplicit.type: type = fn_type @TakesTypeExplicit [concrete]
 // CHECK:STDOUT:   %TakesTypeExplicit: %TakesTypeExplicit.type = struct_value () [concrete]
@@ -1246,21 +1223,21 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %x: @TakesTypeDeduced.%T.loc3_21.2 (%T) = bind_name x, %x.param
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %CallsWithExtraWhere.decl: %CallsWithExtraWhere.type = fn_decl @CallsWithExtraWhere [concrete = constants.%CallsWithExtraWhere] {
-// CHECK:STDOUT:     %U.patt.loc4_24.1: %type_where = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc4_24.2 (constants.%U.patt)]
+// CHECK:STDOUT:     %U.patt.loc4_24.1: %type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc4_24.2 (constants.%U.patt)]
 // CHECK:STDOUT:     %y.patt: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) = binding_pattern y
 // CHECK:STDOUT:     %y.param_patt: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) = value_param_pattern %y.patt, call_param0
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc4_33.1: type = splice_block %.loc4_33.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc4_33.1: type = splice_block %.loc4_33.2 [concrete = constants.%type] {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.loc4_33.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       %.loc4_33.2: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %U.loc4_24.1: %type_where = bind_symbolic_name U, 0 [symbolic = %U.loc4_24.2 (constants.%U)]
+// CHECK:STDOUT:     %U.loc4_24.1: %type = bind_symbolic_name U, 0 [symbolic = %U.loc4_24.2 (constants.%U)]
 // CHECK:STDOUT:     %y.param: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) = value_param call_param0
 // CHECK:STDOUT:     %.loc4_60.1: type = splice_block %.loc4_60.2 [symbolic = %U.as_type.loc4_60.2 (constants.%U.as_type)] {
-// CHECK:STDOUT:       %U.ref: %type_where = name_ref U, %U.loc4_24.1 [symbolic = %U.loc4_24.2 (constants.%U)]
+// CHECK:STDOUT:       %U.ref: %type = name_ref U, %U.loc4_24.1 [symbolic = %U.loc4_24.2 (constants.%U)]
 // CHECK:STDOUT:       %U.as_type.loc4_60.1: type = facet_access_type %U.ref [symbolic = %U.as_type.loc4_60.2 (constants.%U.as_type)]
 // CHECK:STDOUT:       %.loc4_60.2: type = converted %U.ref, %U.as_type.loc4_60.1 [symbolic = %U.as_type.loc4_60.2 (constants.%U.as_type)]
 // CHECK:STDOUT:     }
@@ -1272,16 +1249,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %T.loc8_22.1: type = bind_symbolic_name T, 0 [symbolic = %T.loc8_22.2 (constants.%T)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %CallsWithExtraWhereExplicit.decl: %CallsWithExtraWhereExplicit.type = fn_decl @CallsWithExtraWhereExplicit [concrete = constants.%CallsWithExtraWhereExplicit] {
-// CHECK:STDOUT:     %U.patt.loc9_32.1: %type_where = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_32.2 (constants.%U.patt)]
+// CHECK:STDOUT:     %U.patt.loc9_32.1: %type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_32.2 (constants.%U.patt)]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc9_41.1: type = splice_block %.loc9_41.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc9_41.1: type = splice_block %.loc9_41.2 [concrete = constants.%type] {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.loc9_41.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       %.loc9_41.2: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %U.loc9_32.1: %type_where = bind_symbolic_name U, 0 [symbolic = %U.loc9_32.2 (constants.%U)]
+// CHECK:STDOUT:     %U.loc9_32.1: %type = bind_symbolic_name U, 0 [symbolic = %U.loc9_32.2 (constants.%U)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -1298,16 +1275,16 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @CallsWithExtraWhere(%U.loc4_24.1: %type_where) {
-// CHECK:STDOUT:   %U.loc4_24.2: %type_where = bind_symbolic_name U, 0 [symbolic = %U.loc4_24.2 (constants.%U)]
-// CHECK:STDOUT:   %U.patt.loc4_24.2: %type_where = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc4_24.2 (constants.%U.patt)]
+// CHECK:STDOUT: generic fn @CallsWithExtraWhere(%U.loc4_24.1: %type) {
+// CHECK:STDOUT:   %U.loc4_24.2: %type = bind_symbolic_name U, 0 [symbolic = %U.loc4_24.2 (constants.%U)]
+// CHECK:STDOUT:   %U.patt.loc4_24.2: %type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc4_24.2 (constants.%U.patt)]
 // CHECK:STDOUT:   %U.as_type.loc4_60.2: type = facet_access_type %U.loc4_24.2 [symbolic = %U.as_type.loc4_60.2 (constants.%U.as_type)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) [symbolic = %require_complete (constants.%require_complete.220)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) [symbolic = %require_complete (constants.%require_complete.5eb)]
 // CHECK:STDOUT:   %TakesTypeDeduced.specific_fn.loc5_3.2: <specific function> = specific_function constants.%TakesTypeDeduced, @TakesTypeDeduced(%U.as_type.loc4_60.2) [symbolic = %TakesTypeDeduced.specific_fn.loc5_3.2 (constants.%TakesTypeDeduced.specific_fn)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn[%U.patt.loc4_24.1: %type_where](%y.param_patt: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type)) {
+// CHECK:STDOUT:   fn[%U.patt.loc4_24.1: %type](%y.param_patt: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type)) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %TakesTypeDeduced.ref: %TakesTypeDeduced.type = name_ref TakesTypeDeduced, file.%TakesTypeDeduced.decl [concrete = constants.%TakesTypeDeduced]
 // CHECK:STDOUT:     %y.ref: @CallsWithExtraWhere.%U.as_type.loc4_60.2 (%U.as_type) = name_ref y, %y
@@ -1329,18 +1306,18 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @CallsWithExtraWhereExplicit(%U.loc9_32.1: %type_where) {
-// CHECK:STDOUT:   %U.loc9_32.2: %type_where = bind_symbolic_name U, 0 [symbolic = %U.loc9_32.2 (constants.%U)]
-// CHECK:STDOUT:   %U.patt.loc9_32.2: %type_where = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_32.2 (constants.%U.patt)]
+// CHECK:STDOUT: generic fn @CallsWithExtraWhereExplicit(%U.loc9_32.1: %type) {
+// CHECK:STDOUT:   %U.loc9_32.2: %type = bind_symbolic_name U, 0 [symbolic = %U.loc9_32.2 (constants.%U)]
+// CHECK:STDOUT:   %U.patt.loc9_32.2: %type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_32.2 (constants.%U.patt)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %U.as_type.loc10_22.2: type = facet_access_type %U.loc9_32.2 [symbolic = %U.as_type.loc10_22.2 (constants.%U.as_type)]
 // CHECK:STDOUT:   %TakesTypeExplicit.specific_fn.loc10_3.2: <specific function> = specific_function constants.%TakesTypeExplicit, @TakesTypeExplicit(%U.as_type.loc10_22.2) [symbolic = %TakesTypeExplicit.specific_fn.loc10_3.2 (constants.%TakesTypeExplicit.specific_fn)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%U.patt.loc9_32.1: %type_where) {
+// CHECK:STDOUT:   fn(%U.patt.loc9_32.1: %type) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %TakesTypeExplicit.ref: %TakesTypeExplicit.type = name_ref TakesTypeExplicit, file.%TakesTypeExplicit.decl [concrete = constants.%TakesTypeExplicit]
-// CHECK:STDOUT:     %U.ref: %type_where = name_ref U, %U.loc9_32.1 [symbolic = %U.loc9_32.2 (constants.%U)]
+// CHECK:STDOUT:     %U.ref: %type = name_ref U, %U.loc9_32.1 [symbolic = %U.loc9_32.2 (constants.%U)]
 // CHECK:STDOUT:     %U.as_type.loc10_22.1: type = facet_access_type %U.ref [symbolic = %U.as_type.loc10_22.2 (constants.%U.as_type)]
 // CHECK:STDOUT:     %.loc10: type = converted %U.ref, %U.as_type.loc10_22.1 [symbolic = %U.as_type.loc10_22.2 (constants.%U.as_type)]
 // CHECK:STDOUT:     %TakesTypeExplicit.specific_fn.loc10_3.1: <specific function> = specific_function %TakesTypeExplicit.ref, @TakesTypeExplicit(constants.%U.as_type) [symbolic = %TakesTypeExplicit.specific_fn.loc10_3.2 (constants.%TakesTypeExplicit.specific_fn)]
@@ -1365,7 +1342,7 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %T.patt.loc3_21.2 => constants.%T.patt
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete => constants.%require_complete.220
+// CHECK:STDOUT:   %require_complete => constants.%require_complete.5eb
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @TakesTypeDeduced(@CallsWithExtraWhere.%U.as_type.loc4_60.2) {}
@@ -1389,26 +1366,30 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @TakesTypeExplicit(@CallsWithExtraWhereExplicit.%U.as_type.loc10_22.2) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: --- fail_todo_no_interfaces.carbon
+// CHECK:STDOUT: --- no_interfaces.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
-// CHECK:STDOUT:   %T: %type_where = bind_symbolic_name T, 0 [symbolic]
-// CHECK:STDOUT:   %T.patt: %type_where = symbolic_binding_pattern T, 0 [symbolic]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
+// CHECK:STDOUT:   %T: %type = bind_symbolic_name T, 0 [symbolic]
+// CHECK:STDOUT:   %T.patt: %type = symbolic_binding_pattern T, 0 [symbolic]
 // CHECK:STDOUT:   %T.as_type: type = facet_access_type %T [symbolic]
 // CHECK:STDOUT:   %TakesExtraWhereDeduced.type: type = fn_type @TakesExtraWhereDeduced [concrete]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %TakesExtraWhereDeduced: %TakesExtraWhereDeduced.type = struct_value () [concrete]
-// CHECK:STDOUT:   %require_complete.220: <witness> = require_complete_type %T.as_type [symbolic]
+// CHECK:STDOUT:   %require_complete.5eb: <witness> = require_complete_type %T.as_type [symbolic]
 // CHECK:STDOUT:   %U: type = bind_symbolic_name U, 0 [symbolic]
 // CHECK:STDOUT:   %U.patt: type = symbolic_binding_pattern U, 0 [symbolic]
 // CHECK:STDOUT:   %CallsWithType.type: type = fn_type @CallsWithType [concrete]
 // CHECK:STDOUT:   %CallsWithType: %CallsWithType.type = struct_value () [concrete]
 // CHECK:STDOUT:   %require_complete.4ae: <witness> = require_complete_type %U [symbolic]
+// CHECK:STDOUT:   %facet_value: %type = facet_value %U, () [symbolic]
+// CHECK:STDOUT:   %TakesExtraWhereDeduced.specific_fn: <specific function> = specific_function %TakesExtraWhereDeduced, @TakesExtraWhereDeduced(%facet_value) [symbolic]
 // CHECK:STDOUT:   %TakesExtraWhereExplicit.type: type = fn_type @TakesExtraWhereExplicit [concrete]
 // CHECK:STDOUT:   %TakesExtraWhereExplicit: %TakesExtraWhereExplicit.type = struct_value () [concrete]
 // CHECK:STDOUT:   %CallsWithTypeExplicit.type: type = fn_type @CallsWithTypeExplicit [concrete]
 // CHECK:STDOUT:   %CallsWithTypeExplicit: %CallsWithTypeExplicit.type = struct_value () [concrete]
+// CHECK:STDOUT:   %TakesExtraWhereExplicit.specific_fn: <specific function> = specific_function %TakesExtraWhereExplicit, @TakesExtraWhereExplicit(%facet_value) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1427,21 +1408,21 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Core.import = import Core
 // CHECK:STDOUT:   %TakesExtraWhereDeduced.decl: %TakesExtraWhereDeduced.type = fn_decl @TakesExtraWhereDeduced [concrete = constants.%TakesExtraWhereDeduced] {
-// CHECK:STDOUT:     %T.patt.loc3_27.1: %type_where = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc3_27.2 (constants.%T.patt)]
+// CHECK:STDOUT:     %T.patt.loc3_27.1: %type = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc3_27.2 (constants.%T.patt)]
 // CHECK:STDOUT:     %x.patt: @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type) = binding_pattern x
 // CHECK:STDOUT:     %x.param_patt: @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type) = value_param_pattern %x.patt, call_param0
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc3_36.1: type = splice_block %.loc3_36.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc3_36.1: type = splice_block %.loc3_36.2 [concrete = constants.%type] {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.loc3_36.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       %.loc3_36.2: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc3_27.1: %type_where = bind_symbolic_name T, 0 [symbolic = %T.loc3_27.2 (constants.%T)]
+// CHECK:STDOUT:     %T.loc3_27.1: %type = bind_symbolic_name T, 0 [symbolic = %T.loc3_27.2 (constants.%T)]
 // CHECK:STDOUT:     %x.param: @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type) = value_param call_param0
 // CHECK:STDOUT:     %.loc3_63.1: type = splice_block %.loc3_63.2 [symbolic = %T.as_type.loc3_63.2 (constants.%T.as_type)] {
-// CHECK:STDOUT:       %T.ref: %type_where = name_ref T, %T.loc3_27.1 [symbolic = %T.loc3_27.2 (constants.%T)]
+// CHECK:STDOUT:       %T.ref: %type = name_ref T, %T.loc3_27.1 [symbolic = %T.loc3_27.2 (constants.%T)]
 // CHECK:STDOUT:       %T.as_type.loc3_63.1: type = facet_access_type %T.ref [symbolic = %T.as_type.loc3_63.2 (constants.%T.as_type)]
 // CHECK:STDOUT:       %.loc3_63.2: type = converted %T.ref, %T.as_type.loc3_63.1 [symbolic = %T.as_type.loc3_63.2 (constants.%T.as_type)]
 // CHECK:STDOUT:     }
@@ -1458,33 +1439,33 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:     %y: @CallsWithType.%U.loc4_18.2 (%U) = bind_name y, %y.param
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %TakesExtraWhereExplicit.decl: %TakesExtraWhereExplicit.type = fn_decl @TakesExtraWhereExplicit [concrete = constants.%TakesExtraWhereExplicit] {
-// CHECK:STDOUT:     %T.patt.loc15_28.1: %type_where = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc15_28.2 (constants.%T.patt)]
+// CHECK:STDOUT:     %T.patt.loc8_28.1: %type = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc8_28.2 (constants.%T.patt)]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc15_37.1: type = splice_block %.loc15_37.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc8_37.1: type = splice_block %.loc8_37.2 [concrete = constants.%type] {
 // CHECK:STDOUT:       %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:       %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.loc15_37.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       %.loc8_37.2: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:         requirement_impls %.Self.ref, type
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %T.loc15_28.1: %type_where = bind_symbolic_name T, 0 [symbolic = %T.loc15_28.2 (constants.%T)]
+// CHECK:STDOUT:     %T.loc8_28.1: %type = bind_symbolic_name T, 0 [symbolic = %T.loc8_28.2 (constants.%T)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %CallsWithTypeExplicit.decl: %CallsWithTypeExplicit.type = fn_decl @CallsWithTypeExplicit [concrete = constants.%CallsWithTypeExplicit] {
-// CHECK:STDOUT:     %U.patt.loc16_26.1: type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc16_26.2 (constants.%U.patt)]
+// CHECK:STDOUT:     %U.patt.loc9_26.1: type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_26.2 (constants.%U.patt)]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %U.loc16_26.1: type = bind_symbolic_name U, 0 [symbolic = %U.loc16_26.2 (constants.%U)]
+// CHECK:STDOUT:     %U.loc9_26.1: type = bind_symbolic_name U, 0 [symbolic = %U.loc9_26.2 (constants.%U)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @TakesExtraWhereDeduced(%T.loc3_27.1: %type_where) {
-// CHECK:STDOUT:   %T.loc3_27.2: %type_where = bind_symbolic_name T, 0 [symbolic = %T.loc3_27.2 (constants.%T)]
-// CHECK:STDOUT:   %T.patt.loc3_27.2: %type_where = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc3_27.2 (constants.%T.patt)]
+// CHECK:STDOUT: generic fn @TakesExtraWhereDeduced(%T.loc3_27.1: %type) {
+// CHECK:STDOUT:   %T.loc3_27.2: %type = bind_symbolic_name T, 0 [symbolic = %T.loc3_27.2 (constants.%T)]
+// CHECK:STDOUT:   %T.patt.loc3_27.2: %type = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc3_27.2 (constants.%T.patt)]
 // CHECK:STDOUT:   %T.as_type.loc3_63.2: type = facet_access_type %T.loc3_27.2 [symbolic = %T.as_type.loc3_63.2 (constants.%T.as_type)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
-// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type) [symbolic = %require_complete (constants.%require_complete.220)]
+// CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type) [symbolic = %require_complete (constants.%require_complete.5eb)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn[%T.patt.loc3_27.1: %type_where](%x.param_patt: @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type)) {
+// CHECK:STDOUT:   fn[%T.patt.loc3_27.1: %type](%x.param_patt: @TakesExtraWhereDeduced.%T.as_type.loc3_63.2 (%T.as_type)) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -1496,37 +1477,51 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %require_complete: <witness> = require_complete_type @CallsWithType.%U.loc4_18.2 (%U) [symbolic = %require_complete (constants.%require_complete.4ae)]
+// CHECK:STDOUT:   %facet_value.loc5_27.3: %type = facet_value %U.loc4_18.2, () [symbolic = %facet_value.loc5_27.3 (constants.%facet_value)]
+// CHECK:STDOUT:   %TakesExtraWhereDeduced.specific_fn.loc5_3.2: <specific function> = specific_function constants.%TakesExtraWhereDeduced, @TakesExtraWhereDeduced(%facet_value.loc5_27.3) [symbolic = %TakesExtraWhereDeduced.specific_fn.loc5_3.2 (constants.%TakesExtraWhereDeduced.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn[%U.patt.loc4_18.1: type](%y.param_patt: @CallsWithType.%U.loc4_18.2 (%U)) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %TakesExtraWhereDeduced.ref: %TakesExtraWhereDeduced.type = name_ref TakesExtraWhereDeduced, file.%TakesExtraWhereDeduced.decl [concrete = constants.%TakesExtraWhereDeduced]
 // CHECK:STDOUT:     %y.ref: @CallsWithType.%U.loc4_18.2 (%U) = name_ref y, %y
+// CHECK:STDOUT:     %facet_value.loc5_27.1: %type = facet_value constants.%U, () [symbolic = %facet_value.loc5_27.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc5_27.1: %type = converted constants.%U, %facet_value.loc5_27.1 [symbolic = %facet_value.loc5_27.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %facet_value.loc5_27.2: %type = facet_value constants.%U, () [symbolic = %facet_value.loc5_27.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc5_27.2: %type = converted constants.%U, %facet_value.loc5_27.2 [symbolic = %facet_value.loc5_27.3 (constants.%facet_value)]
+// CHECK:STDOUT:     %TakesExtraWhereDeduced.specific_fn.loc5_3.1: <specific function> = specific_function %TakesExtraWhereDeduced.ref, @TakesExtraWhereDeduced(constants.%facet_value) [symbolic = %TakesExtraWhereDeduced.specific_fn.loc5_3.2 (constants.%TakesExtraWhereDeduced.specific_fn)]
+// CHECK:STDOUT:     %TakesExtraWhereDeduced.call: init %empty_tuple.type = call %TakesExtraWhereDeduced.specific_fn.loc5_3.1(%y.ref)
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @TakesExtraWhereExplicit(%T.loc15_28.1: %type_where) {
-// CHECK:STDOUT:   %T.loc15_28.2: %type_where = bind_symbolic_name T, 0 [symbolic = %T.loc15_28.2 (constants.%T)]
-// CHECK:STDOUT:   %T.patt.loc15_28.2: %type_where = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc15_28.2 (constants.%T.patt)]
+// CHECK:STDOUT: generic fn @TakesExtraWhereExplicit(%T.loc8_28.1: %type) {
+// CHECK:STDOUT:   %T.loc8_28.2: %type = bind_symbolic_name T, 0 [symbolic = %T.loc8_28.2 (constants.%T)]
+// CHECK:STDOUT:   %T.patt.loc8_28.2: %type = symbolic_binding_pattern T, 0 [symbolic = %T.patt.loc8_28.2 (constants.%T.patt)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%T.patt.loc15_28.1: %type_where) {
+// CHECK:STDOUT:   fn(%T.patt.loc8_28.1: %type) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @CallsWithTypeExplicit(%U.loc16_26.1: type) {
-// CHECK:STDOUT:   %U.loc16_26.2: type = bind_symbolic_name U, 0 [symbolic = %U.loc16_26.2 (constants.%U)]
-// CHECK:STDOUT:   %U.patt.loc16_26.2: type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc16_26.2 (constants.%U.patt)]
+// CHECK:STDOUT: generic fn @CallsWithTypeExplicit(%U.loc9_26.1: type) {
+// CHECK:STDOUT:   %U.loc9_26.2: type = bind_symbolic_name U, 0 [symbolic = %U.loc9_26.2 (constants.%U)]
+// CHECK:STDOUT:   %U.patt.loc9_26.2: type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc9_26.2 (constants.%U.patt)]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %facet_value.loc10_28.2: %type = facet_value %U.loc9_26.2, () [symbolic = %facet_value.loc10_28.2 (constants.%facet_value)]
+// CHECK:STDOUT:   %TakesExtraWhereExplicit.specific_fn.loc10_3.2: <specific function> = specific_function constants.%TakesExtraWhereExplicit, @TakesExtraWhereExplicit(%facet_value.loc10_28.2) [symbolic = %TakesExtraWhereExplicit.specific_fn.loc10_3.2 (constants.%TakesExtraWhereExplicit.specific_fn)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%U.patt.loc16_26.1: type) {
+// CHECK:STDOUT:   fn(%U.patt.loc9_26.1: type) {
 // CHECK:STDOUT:   !entry:
 // CHECK:STDOUT:     %TakesExtraWhereExplicit.ref: %TakesExtraWhereExplicit.type = name_ref TakesExtraWhereExplicit, file.%TakesExtraWhereExplicit.decl [concrete = constants.%TakesExtraWhereExplicit]
-// CHECK:STDOUT:     %U.ref: type = name_ref U, %U.loc16_26.1 [symbolic = %U.loc16_26.2 (constants.%U)]
+// CHECK:STDOUT:     %U.ref: type = name_ref U, %U.loc9_26.1 [symbolic = %U.loc9_26.2 (constants.%U)]
+// CHECK:STDOUT:     %facet_value.loc10_28.1: %type = facet_value constants.%U, () [symbolic = %facet_value.loc10_28.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc10: %type = converted %U.ref, %facet_value.loc10_28.1 [symbolic = %facet_value.loc10_28.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %TakesExtraWhereExplicit.specific_fn.loc10_3.1: <specific function> = specific_function %TakesExtraWhereExplicit.ref, @TakesExtraWhereExplicit(constants.%facet_value) [symbolic = %TakesExtraWhereExplicit.specific_fn.loc10_3.2 (constants.%TakesExtraWhereExplicit.specific_fn)]
+// CHECK:STDOUT:     %TakesExtraWhereExplicit.call: init %empty_tuple.type = call %TakesExtraWhereExplicit.specific_fn.loc10_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
@@ -1542,16 +1537,36 @@ fn CallsWithTypeExplicit(U:! type) {
 // CHECK:STDOUT:   %U.patt.loc4_18.2 => constants.%U.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @TakesExtraWhereDeduced(constants.%facet_value) {
+// CHECK:STDOUT:   %T.loc3_27.2 => constants.%facet_value
+// CHECK:STDOUT:   %T.patt.loc3_27.2 => constants.%T.patt
+// CHECK:STDOUT:   %T.as_type.loc3_63.2 => constants.%U
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
+// CHECK:STDOUT:   %require_complete => constants.%require_complete.4ae
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @TakesExtraWhereDeduced(@CallsWithType.%facet_value.loc5_27.3) {}
+// CHECK:STDOUT:
 // CHECK:STDOUT: specific @TakesExtraWhereExplicit(constants.%T) {
-// CHECK:STDOUT:   %T.loc15_28.2 => constants.%T
-// CHECK:STDOUT:   %T.patt.loc15_28.2 => constants.%T.patt
+// CHECK:STDOUT:   %T.loc8_28.2 => constants.%T
+// CHECK:STDOUT:   %T.patt.loc8_28.2 => constants.%T.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @CallsWithTypeExplicit(constants.%U) {
-// CHECK:STDOUT:   %U.loc16_26.2 => constants.%U
-// CHECK:STDOUT:   %U.patt.loc16_26.2 => constants.%U.patt
+// CHECK:STDOUT:   %U.loc9_26.2 => constants.%U
+// CHECK:STDOUT:   %U.patt.loc9_26.2 => constants.%U.patt
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @TakesExtraWhereExplicit(constants.%facet_value) {
+// CHECK:STDOUT:   %T.loc8_28.2 => constants.%facet_value
+// CHECK:STDOUT:   %T.patt.loc8_28.2 => constants.%T.patt
+// CHECK:STDOUT:
+// CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: specific @TakesExtraWhereExplicit(@CallsWithTypeExplicit.%facet_value.loc10_28.2) {}
+// CHECK:STDOUT:
 // CHECK:STDOUT: --- include_files/facet_types.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {

toolchain/check/testdata/impl/fail_impl_bad_interface.carbon

@@ -35,15 +35,24 @@ impl bool as type {}
 
 library "[[@TEST_NAME]]";
 
-// Note: This code is not expected to pass checking, even once the TODO is
-// addressed.
-
 // CHECK:STDERR: fail_impl_as_type_where.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
 // CHECK:STDERR: impl f64 as type where .Self impls type {}
 // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR:
 impl f64 as type where .Self impls type {}
 
+// --- fail_impl_as_type_where_impls_interface.carbon
+
+library "[[@TEST_NAME]]";
+
+interface I {}
+
+// CHECK:STDERR: fail_impl_as_type_where_impls_interface.carbon:[[@LINE+4]]:1: error: impl as 0 interfaces, expected 1 [ImplOfNotOneInterface]
+// CHECK:STDERR: impl {.a: bool} as type where .Self impls I {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl {.a: bool} as type where .Self impls I {}
+
 // CHECK:STDOUT: --- fail_impl_as_false.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -118,7 +127,7 @@ impl f64 as type where .Self impls type {}
 // CHECK:STDOUT:   %Float.type: type = fn_type @Float [concrete]
 // CHECK:STDOUT:   %Float: %Float.type = struct_value () [concrete]
 // CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -137,17 +146,71 @@ impl f64 as type where .Self impls type {}
 // CHECK:STDOUT:   impl_decl @impl [concrete] {} {
 // CHECK:STDOUT:     %int_64: Core.IntLiteral = int_value 64 [concrete = constants.%int_64]
 // CHECK:STDOUT:     %float.make_type: init type = call constants.%Float(%int_64) [concrete = f64]
-// CHECK:STDOUT:     %.loc11_6.1: type = value_of_initializer %float.make_type [concrete = f64]
-// CHECK:STDOUT:     %.loc11_6.2: type = converted %float.make_type, %.loc11_6.1 [concrete = f64]
+// CHECK:STDOUT:     %.loc8_6.1: type = value_of_initializer %float.make_type [concrete = f64]
+// CHECK:STDOUT:     %.loc8_6.2: type = converted %float.make_type, %.loc8_6.1 [concrete = f64]
 // CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:     %.loc11_18: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc8_18: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:       requirement_impls %.Self.ref, type
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: %.loc11_6.2 as %.loc11_18 {
+// CHECK:STDOUT: impl @impl: %.loc8_6.2 as %.loc8_18 {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = <error>
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_impl_as_type_where_impls_interface.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %I.type: type = facet_type <@I> [concrete]
+// CHECK:STDOUT:   %Self: %I.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %Bool.type: type = fn_type @Bool [concrete]
+// CHECK:STDOUT:   %Bool: %Bool.type = struct_value () [concrete]
+// CHECK:STDOUT:   %struct_type.a: type = struct_type {.a: bool} [concrete]
+// CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @I> [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT:   %Core: <namespace> = namespace file.%Core.import, [concrete] {
+// CHECK:STDOUT:     .Bool = %Core.Bool
+// CHECK:STDOUT:     import Core//prelude
+// CHECK:STDOUT:     import Core//prelude/...
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .Core = imports.%Core
+// CHECK:STDOUT:     .I = %I.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %Core.import = import Core
+// CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %bool.make_type: init type = call constants.%Bool() [concrete = bool]
+// CHECK:STDOUT:     %.loc10_11.1: type = value_of_initializer %bool.make_type [concrete = bool]
+// CHECK:STDOUT:     %.loc10_11.2: type = converted %bool.make_type, %.loc10_11.1 [concrete = bool]
+// CHECK:STDOUT:     %struct_type.a: type = struct_type {.a: bool} [concrete = constants.%struct_type.a]
+// CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
+// CHECK:STDOUT:     %.loc10_25: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       requirement_impls %.Self.ref, %I.ref
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @I {
+// CHECK:STDOUT:   %Self: %I.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %struct_type.a as %.loc10_25 {
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   witness = <error>
 // CHECK:STDOUT: }

toolchain/check/testdata/impl/lookup/min_prelude/impl_cycle.carbon

@@ -40,7 +40,7 @@ fn F() {
   Point as Z;
 }
 
-// --- todo_fail_impl_simple_where_cycle.carbon
+// --- fail_impl_simple_where_cycle.carbon
 library "[[@TEST_NAME]]";
 
 interface Y {}
@@ -48,15 +48,21 @@ interface Z {}
 
 // This creates a dependency cycle with itself.
 impl forall [T:! type where .Self impls Z] T as Z {}
-// TODO: Remove these two when the above impl can match Point as the self type
-// (and makes a cycle).
-impl forall [T:! Y] T as Z {}
-impl forall [T:! type] T as Y {}
 
 class Point {}
 
 fn F() {
-  // TODO: A cycle should be found in the `impl forall T as Z` above.
+  // CHECK:STDERR: fail_impl_simple_where_cycle.carbon:[[@LINE+11]]:3: error: cycle found in search for impl of `type where .Self impls Z` for type `Point` [ImplLookupCycle]
+  // CHECK:STDERR:   Point as Z;
+  // CHECK:STDERR:   ^~~~~~~~~~
+  // CHECK:STDERR: fail_impl_simple_where_cycle.carbon:[[@LINE-8]]:1: note: determining if this impl clause matches [ImplLookupCycleNote]
+  // CHECK:STDERR: impl forall [T:! type where .Self impls Z] T as Z {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  // CHECK:STDERR: fail_impl_simple_where_cycle.carbon:[[@LINE+4]]:3: error: cannot convert type `Point` into type implementing `Z` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR:   Point as Z;
+  // CHECK:STDERR:   ^~~~~~~~~~
+  // CHECK:STDERR:
   Point as Z;
 }
 

toolchain/check/testdata/impl/no_prelude/fail_undefined_interface.carbon

@@ -37,6 +37,40 @@ class C {}
 // CHECK:STDERR:
 impl C as J {}
 
+// --- fail_incomplete_where.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+interface I {}
+interface Incomplete;
+
+// CHECK:STDERR: fail_incomplete_where.carbon:[[@LINE+7]]:1: error: definition of impl as incomplete facet type `I where .Self impls Incomplete` [ImplAsIncompleteFacetTypeDefinition]
+// CHECK:STDERR: impl C as I where .Self impls Incomplete {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_incomplete_where.carbon:[[@LINE-5]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
+// CHECK:STDERR: interface Incomplete;
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as I where .Self impls Incomplete {}
+
+// --- fail_declaration_incomplete_where_rewrite.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+interface J { let T:! type; }
+interface Incomplete;
+
+// CHECK:STDERR: fail_declaration_incomplete_where_rewrite.carbon:[[@LINE+7]]:1: error: declaration of impl as incomplete facet type `J where .Self impls Incomplete and .(J.T) = ()` with rewrites [ImplAsIncompleteFacetTypeRewrites]
+// CHECK:STDERR: impl C as J where .Self impls Incomplete and .T = ();
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR: fail_declaration_incomplete_where_rewrite.carbon:[[@LINE-5]]:1: note: interface was forward declared here [InterfaceForwardDeclaredHere]
+// CHECK:STDERR: interface Incomplete;
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+impl C as J where .Self impls Incomplete and .T = ();
+
 // CHECK:STDOUT: --- fail_empty_struct.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
@@ -100,3 +134,147 @@ impl C as J {}
 // CHECK:STDOUT:   .Self = constants.%C
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_incomplete_where.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %C: type = class_type @C [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %I.type: type = facet_type <@I> [concrete]
+// CHECK:STDOUT:   %Self: %I.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %Incomplete.type: type = facet_type <@Incomplete> [concrete]
+// CHECK:STDOUT:   %.Self: %I.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %I_where.type: type = facet_type <@I where .Self impls @Incomplete> [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .C = %C.decl
+// CHECK:STDOUT:     .I = %I.decl
+// CHECK:STDOUT:     .Incomplete = %Incomplete.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %C.decl: type = class_decl @C [concrete = constants.%C] {} {}
+// CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
+// CHECK:STDOUT:   %Incomplete.decl: type = interface_decl @Incomplete [concrete = constants.%Incomplete.type] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %C.ref: type = name_ref C, file.%C.decl [concrete = constants.%C]
+// CHECK:STDOUT:     %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
+// CHECK:STDOUT:     %.Self: %I.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: %I.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %Incomplete.ref: type = name_ref Incomplete, file.%Incomplete.decl [concrete = constants.%Incomplete.type]
+// CHECK:STDOUT:     %.Self.as_type: type = facet_access_type %.Self.ref [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc15_19: type = converted %.Self.ref, %.Self.as_type [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc15_13: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       requirement_impls %.loc15_19, %Incomplete.ref
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @I {
+// CHECK:STDOUT:   %Self: %I.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @Incomplete;
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %C.ref as %.loc15_13 {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = <error>
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @C {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%C
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_declaration_incomplete_where_rewrite.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %C: type = class_type @C [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %J.type: type = facet_type <@J> [concrete]
+// CHECK:STDOUT:   %Self: %J.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %J.assoc_type: type = assoc_entity_type @J [concrete]
+// CHECK:STDOUT:   %assoc0: %J.assoc_type = assoc_entity element0, @J.%T [concrete]
+// CHECK:STDOUT:   %Incomplete.type: type = facet_type <@Incomplete> [concrete]
+// CHECK:STDOUT:   %.Self: %J.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
+// CHECK:STDOUT:   %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self, element0 [symbolic_self]
+// CHECK:STDOUT:   %J.facet: %J.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
+// CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
+// CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
+// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where .Self impls @Incomplete and %impl.elem0 = %empty_tuple.type> [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .C = %C.decl
+// CHECK:STDOUT:     .J = %J.decl
+// CHECK:STDOUT:     .Incomplete = %Incomplete.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %C.decl: type = class_decl @C [concrete = constants.%C] {} {}
+// CHECK:STDOUT:   %J.decl: type = interface_decl @J [concrete = constants.%J.type] {} {}
+// CHECK:STDOUT:   %Incomplete.decl: type = interface_decl @Incomplete [concrete = constants.%Incomplete.type] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %C.ref: type = name_ref C, file.%C.decl [concrete = constants.%C]
+// CHECK:STDOUT:     %J.ref: type = name_ref J, file.%J.decl [concrete = constants.%J.type]
+// CHECK:STDOUT:     %.Self: %J.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref.loc15_19: %J.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %Incomplete.ref: type = name_ref Incomplete, file.%Incomplete.decl [concrete = constants.%Incomplete.type]
+// CHECK:STDOUT:     %.Self.as_type.loc15_19: type = facet_access_type %.Self.ref.loc15_19 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc15_19: type = converted %.Self.ref.loc15_19, %.Self.as_type.loc15_19 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.Self.ref.loc15_46: %J.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %T.ref: %J.assoc_type = name_ref T, @T.%assoc0 [concrete = constants.%assoc0]
+// CHECK:STDOUT:     %.Self.as_type.loc15_46: type = facet_access_type %.Self.ref.loc15_46 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.loc15_46: type = converted %.Self.ref.loc15_46, %.Self.as_type.loc15_46 [symbolic_self = constants.%.Self.as_type]
+// CHECK:STDOUT:     %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self.ref.loc15_46, element0 [symbolic_self = constants.%.Self.as_wit.iface0]
+// CHECK:STDOUT:     %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self = constants.%impl.elem0]
+// CHECK:STDOUT:     %.loc15_52.1: %empty_tuple.type = tuple_literal ()
+// CHECK:STDOUT:     %.loc15_52.2: type = converted %.loc15_52.1, constants.%empty_tuple.type [concrete = constants.%empty_tuple.type]
+// CHECK:STDOUT:     %.loc15_13: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       requirement_impls %.loc15_19, %Incomplete.ref
+// CHECK:STDOUT:       requirement_rewrite %impl.elem0, %.loc15_52.2
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @J {
+// CHECK:STDOUT:   %Self: %J.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:   %T: type = assoc_const_decl @T [concrete] {
+// CHECK:STDOUT:     %assoc0: %J.assoc_type = assoc_entity element0, @J.%T [concrete = constants.%assoc0]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   .T = @T.%assoc0
+// CHECK:STDOUT:   witness = (%T)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @Incomplete;
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic assoc_const @T(@J.%Self: %J.type) {
+// CHECK:STDOUT:   assoc_const T:! type;
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %C.ref as %.loc15_13;
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @C {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%C
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @T(constants.%Self) {}
+// CHECK:STDOUT:
+// CHECK:STDOUT: specific @T(constants.%J.facet) {}
+// CHECK:STDOUT:

toolchain/check/testdata/interface/no_prelude/fail_lookup_in_type_type.carbon

@@ -54,7 +54,7 @@ let U: (type where .Self impls type).missing = {};
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
+// CHECK:STDOUT:   %type: type = facet_type <type> [concrete]
 // CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -68,7 +68,7 @@ let U: (type where .Self impls type).missing = {};
 // CHECK:STDOUT:   %.1: <error> = splice_block <error> [concrete = <error>] {
 // CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:     %.loc8: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc8: type = where_expr %.Self [concrete = constants.%type] {
 // CHECK:STDOUT:       requirement_impls %.Self.ref, type
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:     %missing.ref: <error> = name_ref missing, <error> [concrete = <error>]

toolchain/check/testdata/where_expr/constraints.carbon

@@ -74,7 +74,7 @@ library "[[@TEST_NAME]]";
 // CHECK:STDERR:
 fn ImplsOfNonFacetType(U:! type where .Self impls i32);
 
-// --- fail_todo_enforce_constraint.carbon
+// --- fail_enforce_impls_constraint.carbon
 
 library "[[@TEST_NAME]]";
 
@@ -84,12 +84,11 @@ import library "state_constraints";
 class C {}
 impl C as J {}
 
-// TODO: Should report that `C` does not meet the constraint.
 fn DoesNotImplI() {
-  // CHECK:STDERR: fail_todo_enforce_constraint.carbon:[[@LINE+8]]:3: error: cannot convert type `C` into type implementing `J where...` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_enforce_impls_constraint.carbon:[[@LINE+8]]:3: error: cannot convert type `C` into type implementing `J where .Self impls I` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   Impls(C);
   // CHECK:STDERR:   ^~~~~~~~
-  // CHECK:STDERR: fail_todo_enforce_constraint.carbon:[[@LINE-11]]:1: in import [InImport]
+  // CHECK:STDERR: fail_enforce_impls_constraint.carbon:[[@LINE-10]]:1: in import [InImport]
   // CHECK:STDERR: state_constraints.carbon:13:10: note: initializing generic parameter `V` declared here [InitializingGenericParam]
   // CHECK:STDERR: fn Impls(V:! J where .Self impls I);
   // CHECK:STDERR:          ^
@@ -97,14 +96,25 @@ fn DoesNotImplI() {
   Impls(C);
 }
 
+// --- fail_todo_enforce_equality_constraint.carbon
+
+library "[[@TEST_NAME]]";
+
+import library "state_constraints";
+
+class C {}
+impl C as J {}
+
 fn EmptyStruct(Y:! J where .Self == {});
 
-// TODO: Should report that `C` does not meeet the constraint.
+// TODO: Should report that `C` does not meeet the `==` constraint. Right
+// now there is no support for `==` constraints so it rejects it as an
+// "other currently unsupported constraint."
 fn NotEmptyStruct() {
-  // CHECK:STDERR: fail_todo_enforce_constraint.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `J where...` [ConversionFailureTypeToFacet]
+  // CHECK:STDERR: fail_todo_enforce_equality_constraint.carbon:[[@LINE+7]]:3: error: cannot convert type `C` into type implementing `J where...` [ConversionFailureTypeToFacet]
   // CHECK:STDERR:   EmptyStruct(C);
   // CHECK:STDERR:   ^~~~~~~~~~~~~~
-  // CHECK:STDERR: fail_todo_enforce_constraint.carbon:[[@LINE-7]]:16: note: initializing generic parameter `Y` declared here [InitializingGenericParam]
+  // CHECK:STDERR: fail_todo_enforce_equality_constraint.carbon:[[@LINE-9]]:16: note: initializing generic parameter `Y` declared here [InitializingGenericParam]
   // CHECK:STDERR: fn EmptyStruct(Y:! J where .Self == {});
   // CHECK:STDERR:                ^
   // CHECK:STDERR:
@@ -123,14 +133,14 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   %assoc1: %I.assoc_type = assoc_entity element1, @I.%Second [concrete]
 // CHECK:STDOUT:   %.Self.258: %I.type = bind_symbolic_name .Self [symbolic_self]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
-// CHECK:STDOUT:   %I_where.type: type = facet_type <@I where TODO> [concrete]
-// CHECK:STDOUT:   %U: %I_where.type = bind_symbolic_name U, 0 [symbolic]
-// CHECK:STDOUT:   %U.patt: %I_where.type = symbolic_binding_pattern U, 0 [symbolic]
+// CHECK:STDOUT:   %I_where.type.cad: type = facet_type <@I where TODO> [concrete]
+// CHECK:STDOUT:   %U: %I_where.type.cad = bind_symbolic_name U, 0 [symbolic]
+// CHECK:STDOUT:   %U.patt: %I_where.type.cad = symbolic_binding_pattern U, 0 [symbolic]
 // CHECK:STDOUT:   %EqualEqual.type: type = fn_type @EqualEqual [concrete]
 // CHECK:STDOUT:   %EqualEqual: %EqualEqual.type = struct_value () [concrete]
 // CHECK:STDOUT:   %.Self.968: %J.type = bind_symbolic_name .Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_type.78d: type = facet_access_type %.Self.968 [symbolic_self]
-// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where TODO> [concrete]
+// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where .Self impls @I> [concrete]
 // CHECK:STDOUT:   %V: %J_where.type = bind_symbolic_name V, 0 [symbolic]
 // CHECK:STDOUT:   %V.patt: %J_where.type = symbolic_binding_pattern V, 0 [symbolic]
 // CHECK:STDOUT:   %Impls.type: type = fn_type @Impls [concrete]
@@ -139,8 +149,9 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self.258, element0 [symbolic_self]
 // CHECK:STDOUT:   %I.facet: %I.type = facet_value %.Self.as_type.541, (%.Self.as_wit.iface0) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
-// CHECK:STDOUT:   %W: %I_where.type = bind_symbolic_name W, 0 [symbolic]
-// CHECK:STDOUT:   %W.patt: %I_where.type = symbolic_binding_pattern W, 0 [symbolic]
+// CHECK:STDOUT:   %I_where.type.427: type = facet_type <@I where .Self impls @J and TODO> [concrete]
+// CHECK:STDOUT:   %W: %I_where.type.427 = bind_symbolic_name W, 0 [symbolic]
+// CHECK:STDOUT:   %W.patt: %I_where.type.427 = symbolic_binding_pattern W, 0 [symbolic]
 // CHECK:STDOUT:   %And.type: type = fn_type @And [concrete]
 // CHECK:STDOUT:   %And: %And.type = struct_value () [concrete]
 // CHECK:STDOUT: }
@@ -165,18 +176,18 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   %J.decl: type = interface_decl @J [concrete = constants.%J.type] {} {}
 // CHECK:STDOUT:   %I.decl: type = interface_decl @I [concrete = constants.%I.type] {} {}
 // CHECK:STDOUT:   %EqualEqual.decl: %EqualEqual.type = fn_decl @EqualEqual [concrete = constants.%EqualEqual] {
-// CHECK:STDOUT:     %U.patt.loc11_15.1: %I_where.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc11_15.2 (constants.%U.patt)]
+// CHECK:STDOUT:     %U.patt.loc11_15.1: %I_where.type.cad = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc11_15.2 (constants.%U.patt)]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc11_21.1: type = splice_block %.loc11_21.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:     %.loc11_21.1: type = splice_block %.loc11_21.2 [concrete = constants.%I_where.type.cad] {
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:       %.Self: %I.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self.258]
 // CHECK:STDOUT:       %.Self.ref: %I.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.258]
 // CHECK:STDOUT:       %.loc11_37: %empty_tuple.type = tuple_literal ()
-// CHECK:STDOUT:       %.loc11_21.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       %.loc11_21.2: type = where_expr %.Self [concrete = constants.%I_where.type.cad] {
 // CHECK:STDOUT:         requirement_equivalent %.Self.ref, %.loc11_37
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %U.loc11_15.1: %I_where.type = bind_symbolic_name U, 0 [symbolic = %U.loc11_15.2 (constants.%U)]
+// CHECK:STDOUT:     %U.loc11_15.1: %I_where.type.cad = bind_symbolic_name U, 0 [symbolic = %U.loc11_15.2 (constants.%U)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Impls.decl: %Impls.type = fn_decl @Impls [concrete = constants.%Impls] {
 // CHECK:STDOUT:     %V.patt.loc13_10.1: %J_where.type = symbolic_binding_pattern V, 0 [symbolic = %V.patt.loc13_10.2 (constants.%V.patt)]
@@ -195,9 +206,9 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:     %V.loc13_10.1: %J_where.type = bind_symbolic_name V, 0 [symbolic = %V.loc13_10.2 (constants.%V)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %And.decl: %And.type = fn_decl @And [concrete = constants.%And] {
-// CHECK:STDOUT:     %W.patt.loc15_8.1: %I_where.type = symbolic_binding_pattern W, 0 [symbolic = %W.patt.loc15_8.2 (constants.%W.patt)]
+// CHECK:STDOUT:     %W.patt.loc15_8.1: %I_where.type.427 = symbolic_binding_pattern W, 0 [symbolic = %W.patt.loc15_8.2 (constants.%W.patt)]
 // CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc15_14.1: type = splice_block %.loc15_14.2 [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:     %.loc15_14.1: type = splice_block %.loc15_14.2 [concrete = constants.%I_where.type.427] {
 // CHECK:STDOUT:       %I.ref: type = name_ref I, file.%I.decl [concrete = constants.%I.type]
 // CHECK:STDOUT:       %.Self: %I.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self.258]
 // CHECK:STDOUT:       %.Self.ref.loc15_20: %I.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self.258]
@@ -211,12 +222,12 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:       %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self.ref.loc15_38, element0 [symbolic_self = constants.%.Self.as_wit.iface0]
 // CHECK:STDOUT:       %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self = constants.%impl.elem0]
 // CHECK:STDOUT:       %.loc15_50: %empty_tuple.type = tuple_literal ()
-// CHECK:STDOUT:       %.loc15_14.2: type = where_expr %.Self [concrete = constants.%I_where.type] {
+// CHECK:STDOUT:       %.loc15_14.2: type = where_expr %.Self [concrete = constants.%I_where.type.427] {
 // CHECK:STDOUT:         requirement_impls %.loc15_20, %J.ref
 // CHECK:STDOUT:         requirement_equivalent %impl.elem0, %.loc15_50
 // CHECK:STDOUT:       }
 // CHECK:STDOUT:     }
-// CHECK:STDOUT:     %W.loc15_8.1: %I_where.type = bind_symbolic_name W, 0 [symbolic = %W.loc15_8.2 (constants.%W)]
+// CHECK:STDOUT:     %W.loc15_8.1: %I_where.type.427 = bind_symbolic_name W, 0 [symbolic = %W.loc15_8.2 (constants.%W)]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
@@ -253,11 +264,11 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   assoc_const Second:! %J.type;
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @EqualEqual(%U.loc11_15.1: %I_where.type) {
-// CHECK:STDOUT:   %U.loc11_15.2: %I_where.type = bind_symbolic_name U, 0 [symbolic = %U.loc11_15.2 (constants.%U)]
-// CHECK:STDOUT:   %U.patt.loc11_15.2: %I_where.type = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc11_15.2 (constants.%U.patt)]
+// CHECK:STDOUT: generic fn @EqualEqual(%U.loc11_15.1: %I_where.type.cad) {
+// CHECK:STDOUT:   %U.loc11_15.2: %I_where.type.cad = bind_symbolic_name U, 0 [symbolic = %U.loc11_15.2 (constants.%U)]
+// CHECK:STDOUT:   %U.patt.loc11_15.2: %I_where.type.cad = symbolic_binding_pattern U, 0 [symbolic = %U.patt.loc11_15.2 (constants.%U.patt)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%U.patt.loc11_15.1: %I_where.type);
+// CHECK:STDOUT:   fn(%U.patt.loc11_15.1: %I_where.type.cad);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: generic fn @Impls(%V.loc13_10.1: %J_where.type) {
@@ -267,11 +278,11 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   fn(%V.patt.loc13_10.1: %J_where.type);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @And(%W.loc15_8.1: %I_where.type) {
-// CHECK:STDOUT:   %W.loc15_8.2: %I_where.type = bind_symbolic_name W, 0 [symbolic = %W.loc15_8.2 (constants.%W)]
-// CHECK:STDOUT:   %W.patt.loc15_8.2: %I_where.type = symbolic_binding_pattern W, 0 [symbolic = %W.patt.loc15_8.2 (constants.%W.patt)]
+// CHECK:STDOUT: generic fn @And(%W.loc15_8.1: %I_where.type.427) {
+// CHECK:STDOUT:   %W.loc15_8.2: %I_where.type.427 = bind_symbolic_name W, 0 [symbolic = %W.loc15_8.2 (constants.%W)]
+// CHECK:STDOUT:   %W.patt.loc15_8.2: %I_where.type.427 = symbolic_binding_pattern W, 0 [symbolic = %W.patt.loc15_8.2 (constants.%W.patt)]
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%W.patt.loc15_8.1: %I_where.type);
+// CHECK:STDOUT:   fn(%W.patt.loc15_8.1: %I_where.type.427);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @Member(constants.%Self.826) {}
@@ -572,7 +583,7 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   %U.patt.loc8_24.2 => constants.%U.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: --- fail_todo_enforce_constraint.carbon
+// CHECK:STDOUT: --- fail_enforce_impls_constraint.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %C: type = class_type @C [concrete]
@@ -584,16 +595,9 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   %DoesNotImplI: %DoesNotImplI.type = struct_value () [concrete]
 // CHECK:STDOUT:   %Impls.type: type = fn_type @Impls [concrete]
 // CHECK:STDOUT:   %Impls: %Impls.type = struct_value () [concrete]
-// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where TODO> [concrete]
+// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where .Self impls @I> [concrete]
 // CHECK:STDOUT:   %V.patt: %J_where.type = symbolic_binding_pattern V, 0 [symbolic]
 // CHECK:STDOUT:   %V: %J_where.type = bind_symbolic_name V, 0 [symbolic]
-// CHECK:STDOUT:   %.Self: %J.type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %Y: %J_where.type = bind_symbolic_name Y, 0 [symbolic]
-// CHECK:STDOUT:   %Y.patt: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic]
-// CHECK:STDOUT:   %EmptyStruct.type: type = fn_type @EmptyStruct [concrete]
-// CHECK:STDOUT:   %EmptyStruct: %EmptyStruct.type = struct_value () [concrete]
-// CHECK:STDOUT:   %NotEmptyStruct.type: type = fn_type @NotEmptyStruct [concrete]
-// CHECK:STDOUT:   %NotEmptyStruct: %NotEmptyStruct.type = struct_value () [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -607,7 +611,12 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:     import Core//prelude/...
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Main.import_ref.8fd = import_ref Main//state_constraints, inst18 [no loc], unloaded
-// CHECK:STDOUT:   %Main.import_ref.9d4: %J_where.type = import_ref Main//state_constraints, loc13_10, loaded [symbolic = @Impls.%V (constants.%V)]
+// CHECK:STDOUT:   %Main.import_ref.e5d = import_ref Main//state_constraints, inst22 [no loc], unloaded
+// CHECK:STDOUT:   %Main.import_ref.ce7 = import_ref Main//state_constraints, loc7_13, unloaded
+// CHECK:STDOUT:   %Main.import_ref.731 = import_ref Main//state_constraints, loc8_13, unloaded
+// CHECK:STDOUT:   %Main.Member = import_ref Main//state_constraints, Member, unloaded
+// CHECK:STDOUT:   %Main.Second = import_ref Main//state_constraints, Second, unloaded
+// CHECK:STDOUT:   %Main.import_ref.d1a: %J_where.type = import_ref Main//state_constraints, loc13_10, loaded [symbolic = @Impls.%V (constants.%V)]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -620,8 +629,6 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:     .Core = imports.%Core
 // CHECK:STDOUT:     .C = %C.decl
 // CHECK:STDOUT:     .DoesNotImplI = %DoesNotImplI.decl
-// CHECK:STDOUT:     .EmptyStruct = %EmptyStruct.decl
-// CHECK:STDOUT:     .NotEmptyStruct = %NotEmptyStruct.decl
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %Core.import = import Core
 // CHECK:STDOUT:   %default.import = import <none>
@@ -632,21 +639,6 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete = constants.%impl_witness]
 // CHECK:STDOUT:   %DoesNotImplI.decl: %DoesNotImplI.type = fn_decl @DoesNotImplI [concrete = constants.%DoesNotImplI] {} {}
-// CHECK:STDOUT:   %EmptyStruct.decl: %EmptyStruct.type = fn_decl @EmptyStruct [concrete = constants.%EmptyStruct] {
-// CHECK:STDOUT:     %Y.patt.loc23_16.1: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic = %Y.patt.loc23_16.2 (constants.%Y.patt)]
-// CHECK:STDOUT:   } {
-// CHECK:STDOUT:     %.loc23_22.1: type = splice_block %.loc23_22.2 [concrete = constants.%J_where.type] {
-// CHECK:STDOUT:       %J.ref: type = name_ref J, imports.%Main.J [concrete = constants.%J.type]
-// CHECK:STDOUT:       %.Self: %J.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.Self.ref: %J.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
-// CHECK:STDOUT:       %.loc23_38: %empty_struct_type = struct_literal ()
-// CHECK:STDOUT:       %.loc23_22.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
-// CHECK:STDOUT:         requirement_equivalent %.Self.ref, %.loc23_38
-// CHECK:STDOUT:       }
-// CHECK:STDOUT:     }
-// CHECK:STDOUT:     %Y.loc23_16.1: %J_where.type = bind_symbolic_name Y, 0 [symbolic = %Y.loc23_16.2 (constants.%Y)]
-// CHECK:STDOUT:   }
-// CHECK:STDOUT:   %NotEmptyStruct.decl: %NotEmptyStruct.type = fn_decl @NotEmptyStruct [concrete = constants.%NotEmptyStruct] {} {}
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @J [from "state_constraints.carbon"] {
@@ -655,6 +647,14 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
+// CHECK:STDOUT: interface @I [from "state_constraints.carbon"] {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref.e5d
+// CHECK:STDOUT:   .Member = imports.%Main.import_ref.ce7
+// CHECK:STDOUT:   .Second = imports.%Main.import_ref.731
+// CHECK:STDOUT:   witness = (imports.%Main.Member, imports.%Main.Second)
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: %C.ref as %J.ref {
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   witness = file.%impl_witness
@@ -675,18 +675,110 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   return
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @Impls(imports.%Main.import_ref.9d4: %J_where.type) [from "state_constraints.carbon"] {
+// CHECK:STDOUT: generic fn @Impls(imports.%Main.import_ref.d1a: %J_where.type) [from "state_constraints.carbon"] {
 // CHECK:STDOUT:   %V: %J_where.type = bind_symbolic_name V, 0 [symbolic = %V (constants.%V)]
 // CHECK:STDOUT:   %V.patt.2: %J_where.type = symbolic_binding_pattern V, 0 [symbolic = %V.patt.2 (constants.%V.patt)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn(%V.patt.1: %J_where.type);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: generic fn @EmptyStruct(%Y.loc23_16.1: %J_where.type) {
-// CHECK:STDOUT:   %Y.loc23_16.2: %J_where.type = bind_symbolic_name Y, 0 [symbolic = %Y.loc23_16.2 (constants.%Y)]
-// CHECK:STDOUT:   %Y.patt.loc23_16.2: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic = %Y.patt.loc23_16.2 (constants.%Y.patt)]
+// CHECK:STDOUT: specific @Impls(constants.%V) {
+// CHECK:STDOUT:   %V => constants.%V
+// CHECK:STDOUT:   %V.patt.2 => constants.%V.patt
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_todo_enforce_equality_constraint.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %C: type = class_type @C [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %J.type: type = facet_type <@J> [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete]
+// CHECK:STDOUT:   %.Self: %J.type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %J_where.type: type = facet_type <@J where TODO> [concrete]
+// CHECK:STDOUT:   %Y: %J_where.type = bind_symbolic_name Y, 0 [symbolic]
+// CHECK:STDOUT:   %Y.patt: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic]
+// CHECK:STDOUT:   %EmptyStruct.type: type = fn_type @EmptyStruct [concrete]
+// CHECK:STDOUT:   %EmptyStruct: %EmptyStruct.type = struct_value () [concrete]
+// CHECK:STDOUT:   %NotEmptyStruct.type: type = fn_type @NotEmptyStruct [concrete]
+// CHECK:STDOUT:   %NotEmptyStruct: %NotEmptyStruct.type = struct_value () [concrete]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT:   %Main.J: type = import_ref Main//state_constraints, J, loaded [concrete = constants.%J.type]
+// CHECK:STDOUT:   %Main.I = import_ref Main//state_constraints, I, unloaded
+// CHECK:STDOUT:   %Main.EqualEqual = import_ref Main//state_constraints, EqualEqual, unloaded
+// CHECK:STDOUT:   %Main.Impls = import_ref Main//state_constraints, Impls, unloaded
+// CHECK:STDOUT:   %Main.And = import_ref Main//state_constraints, And, unloaded
+// CHECK:STDOUT:   %Core: <namespace> = namespace file.%Core.import, [concrete] {
+// CHECK:STDOUT:     import Core//prelude
+// CHECK:STDOUT:     import Core//prelude/...
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %Main.import_ref = import_ref Main//state_constraints, inst18 [no loc], unloaded
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .J = imports.%Main.J
+// CHECK:STDOUT:     .I = imports.%Main.I
+// CHECK:STDOUT:     .EqualEqual = imports.%Main.EqualEqual
+// CHECK:STDOUT:     .Impls = imports.%Main.Impls
+// CHECK:STDOUT:     .And = imports.%Main.And
+// CHECK:STDOUT:     .Core = imports.%Core
+// CHECK:STDOUT:     .C = %C.decl
+// CHECK:STDOUT:     .EmptyStruct = %EmptyStruct.decl
+// CHECK:STDOUT:     .NotEmptyStruct = %NotEmptyStruct.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %Core.import = import Core
+// CHECK:STDOUT:   %default.import = import <none>
+// CHECK:STDOUT:   %C.decl: type = class_decl @C [concrete = constants.%C] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %C.ref: type = name_ref C, file.%C.decl [concrete = constants.%C]
+// CHECK:STDOUT:     %J.ref: type = name_ref J, imports.%Main.J [concrete = constants.%J.type]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete = constants.%impl_witness]
+// CHECK:STDOUT:   %EmptyStruct.decl: %EmptyStruct.type = fn_decl @EmptyStruct [concrete = constants.%EmptyStruct] {
+// CHECK:STDOUT:     %Y.patt.loc9_16.1: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic = %Y.patt.loc9_16.2 (constants.%Y.patt)]
+// CHECK:STDOUT:   } {
+// CHECK:STDOUT:     %.loc9_22.1: type = splice_block %.loc9_22.2 [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:       %J.ref: type = name_ref J, imports.%Main.J [concrete = constants.%J.type]
+// CHECK:STDOUT:       %.Self: %J.type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.Self.ref: %J.type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:       %.loc9_38: %empty_struct_type = struct_literal ()
+// CHECK:STDOUT:       %.loc9_22.2: type = where_expr %.Self [concrete = constants.%J_where.type] {
+// CHECK:STDOUT:         requirement_equivalent %.Self.ref, %.loc9_38
+// CHECK:STDOUT:       }
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:     %Y.loc9_16.1: %J_where.type = bind_symbolic_name Y, 0 [symbolic = %Y.loc9_16.2 (constants.%Y)]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %NotEmptyStruct.decl: %NotEmptyStruct.type = fn_decl @NotEmptyStruct [concrete = constants.%NotEmptyStruct] {} {}
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT:   fn(%Y.patt.loc23_16.1: %J_where.type);
+// CHECK:STDOUT: interface @J [from "state_constraints.carbon"] {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = imports.%Main.import_ref
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %C.ref as %J.ref {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = file.%impl_witness
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @C {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%C
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: generic fn @EmptyStruct(%Y.loc9_16.1: %J_where.type) {
+// CHECK:STDOUT:   %Y.loc9_16.2: %J_where.type = bind_symbolic_name Y, 0 [symbolic = %Y.loc9_16.2 (constants.%Y)]
+// CHECK:STDOUT:   %Y.patt.loc9_16.2: %J_where.type = symbolic_binding_pattern Y, 0 [symbolic = %Y.patt.loc9_16.2 (constants.%Y.patt)]
+// CHECK:STDOUT:
+// CHECK:STDOUT:   fn(%Y.patt.loc9_16.1: %J_where.type);
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @NotEmptyStruct() {
@@ -696,13 +788,8 @@ fn NotEmptyStruct() {
 // CHECK:STDOUT:   return
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @Impls(constants.%V) {
-// CHECK:STDOUT:   %V => constants.%V
-// CHECK:STDOUT:   %V.patt.2 => constants.%V.patt
-// CHECK:STDOUT: }
-// CHECK:STDOUT:
 // CHECK:STDOUT: specific @EmptyStruct(constants.%Y) {
-// CHECK:STDOUT:   %Y.loc23_16.2 => constants.%Y
-// CHECK:STDOUT:   %Y.patt.loc23_16.2 => constants.%Y.patt
+// CHECK:STDOUT:   %Y.loc9_16.2 => constants.%Y
+// CHECK:STDOUT:   %Y.patt.loc9_16.2 => constants.%Y.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:

toolchain/check/testdata/where_expr/designator.carbon

@@ -110,7 +110,7 @@ class D {
 // CHECK:STDOUT:   %PeriodMember.type: type = fn_type @PeriodMember [concrete]
 // CHECK:STDOUT:   %PeriodMember: %PeriodMember.type = struct_value () [concrete]
 // CHECK:STDOUT:   %.Self.644: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
+// CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @I> [concrete]
 // CHECK:STDOUT:   %V: %type_where = bind_symbolic_name V, 0 [symbolic]
 // CHECK:STDOUT:   %V.patt: %type_where = symbolic_binding_pattern V, 0 [symbolic]
 // CHECK:STDOUT:   %TypeSelfImpls.type: type = fn_type @TypeSelfImpls [concrete]

toolchain/check/testdata/where_expr/equal_rewrite.carbon

@@ -140,20 +140,34 @@ interface I {
 // CHECK:STDERR:
 fn RewriteTypeMismatch(X:! I where .Member = 2);
 
-// --- fail_todo_let.carbon
+// --- todo_let.carbon
 
 library "[[@TEST_NAME]]";
 
 interface A {}
 class D {}
 impl D as A {}
-// TODO: This should be a compile-time binding, once that is supported.
-// CHECK:STDERR: fail_todo_let.carbon:[[@LINE+4]]:35: error: cannot convert type `D` into type implementing `type where...` [ConversionFailureTypeToFacet]
-// CHECK:STDERR: let B: type where .Self impls A = D;
-// CHECK:STDERR:                                   ^
-// CHECK:STDERR:
+// TODO: This should be a compile-time binding, once that is supported at file scope.
 let B: type where .Self impls A = D;
 
+fn F() {
+  let E:! type where .Self impls A = D;
+}
+
+// --- fail_todo_let_compile_time.carbon
+
+library "[[@TEST_NAME]]";
+
+interface A {}
+class D {}
+impl D as A {}
+// TODO: Compile-time binding are not yet supported at file scope.
+// CHECK:STDERR: fail_todo_let_compile_time.carbon:[[@LINE+4]]:5: error: semantics TODO: ``let` compile time binding outside function or interface` [SemanticsTodo]
+// CHECK:STDERR: let B:! type where .Self impls A = D;
+// CHECK:STDERR:     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
+// CHECK:STDERR:
+let B:! type where .Self impls A = D;
+
 // --- fail_type_does_not_implement_where.carbon
 
 library "[[@TEST_NAME]]";
@@ -823,7 +837,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %.Self: %O.type = bind_symbolic_name .Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self, element0 [symbolic_self]
-// CHECK:STDOUT:   %O.facet.22f: %O.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
+// CHECK:STDOUT:   %O.facet: %O.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
 // CHECK:STDOUT:   %int_32: Core.IntLiteral = int_value 32 [concrete]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
@@ -842,8 +856,8 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %WithBool: %WithBool.type = struct_value () [concrete]
 // CHECK:STDOUT:   %R.as_wit.iface0: <witness> = facet_access_witness %R, element0 [symbolic]
 // CHECK:STDOUT:   %R.as_type: type = facet_access_type %R [symbolic]
-// CHECK:STDOUT:   %O.facet.3ed: %O_where.type.fe1 = facet_value %R.as_type, (%R.as_wit.iface0) [symbolic]
-// CHECK:STDOUT:   %WithInteger.specific_fn: <specific function> = specific_function %WithInteger, @WithInteger(%O.facet.3ed) [symbolic]
+// CHECK:STDOUT:   %facet_value: %O_where.type.fe1 = facet_value %R.as_type, (%R.as_wit.iface0) [symbolic]
+// CHECK:STDOUT:   %WithInteger.specific_fn: <specific function> = specific_function %WithInteger, @WithInteger(%facet_value) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -942,8 +956,8 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %R.as_wit.iface0.loc12_16.2: <witness> = facet_access_witness %R.loc10_13.2, element0 [symbolic = %R.as_wit.iface0.loc12_16.2 (constants.%R.as_wit.iface0)]
 // CHECK:STDOUT:   %R.as_type.loc12_16.2: type = facet_access_type %R.loc10_13.2 [symbolic = %R.as_type.loc12_16.2 (constants.%R.as_type)]
-// CHECK:STDOUT:   %O.facet.loc12_16.2: %O_where.type.fe1 = facet_value %R.as_type.loc12_16.2, (%R.as_wit.iface0.loc12_16.2) [symbolic = %O.facet.loc12_16.2 (constants.%O.facet.3ed)]
-// CHECK:STDOUT:   %WithInteger.specific_fn.loc12_3.2: <specific function> = specific_function constants.%WithInteger, @WithInteger(%O.facet.loc12_16.2) [symbolic = %WithInteger.specific_fn.loc12_3.2 (constants.%WithInteger.specific_fn)]
+// CHECK:STDOUT:   %facet_value.loc12_16.2: %O_where.type.fe1 = facet_value %R.as_type.loc12_16.2, (%R.as_wit.iface0.loc12_16.2) [symbolic = %facet_value.loc12_16.2 (constants.%facet_value)]
+// CHECK:STDOUT:   %WithInteger.specific_fn.loc12_3.2: <specific function> = specific_function constants.%WithInteger, @WithInteger(%facet_value.loc12_16.2) [symbolic = %WithInteger.specific_fn.loc12_3.2 (constants.%WithInteger.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn(%R.patt.loc10_13.1: %O_where.type.741) {
 // CHECK:STDOUT:   !entry:
@@ -951,9 +965,9 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:     %R.ref: %O_where.type.741 = name_ref R, %R.loc10_13.1 [symbolic = %R.loc10_13.2 (constants.%R)]
 // CHECK:STDOUT:     %R.as_wit.iface0.loc12_16.1: <witness> = facet_access_witness constants.%R, element0 [symbolic = %R.as_wit.iface0.loc12_16.2 (constants.%R.as_wit.iface0)]
 // CHECK:STDOUT:     %R.as_type.loc12_16.1: type = facet_access_type constants.%R [symbolic = %R.as_type.loc12_16.2 (constants.%R.as_type)]
-// CHECK:STDOUT:     %O.facet.loc12_16.1: %O_where.type.fe1 = facet_value %R.as_type.loc12_16.1, (%R.as_wit.iface0.loc12_16.1) [symbolic = %O.facet.loc12_16.2 (constants.%O.facet.3ed)]
-// CHECK:STDOUT:     %.loc12: %O_where.type.fe1 = converted %R.ref, %O.facet.loc12_16.1 [symbolic = %O.facet.loc12_16.2 (constants.%O.facet.3ed)]
-// CHECK:STDOUT:     %WithInteger.specific_fn.loc12_3.1: <specific function> = specific_function %WithInteger.ref, @WithInteger(constants.%O.facet.3ed) [symbolic = %WithInteger.specific_fn.loc12_3.2 (constants.%WithInteger.specific_fn)]
+// CHECK:STDOUT:     %facet_value.loc12_16.1: %O_where.type.fe1 = facet_value %R.as_type.loc12_16.1, (%R.as_wit.iface0.loc12_16.1) [symbolic = %facet_value.loc12_16.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc12: %O_where.type.fe1 = converted %R.ref, %facet_value.loc12_16.1 [symbolic = %facet_value.loc12_16.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %WithInteger.specific_fn.loc12_3.1: <specific function> = specific_function %WithInteger.ref, @WithInteger(constants.%facet_value) [symbolic = %WithInteger.specific_fn.loc12_3.2 (constants.%WithInteger.specific_fn)]
 // CHECK:STDOUT:     %WithInteger.call: init %empty_tuple.type = call %WithInteger.specific_fn.loc12_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -961,7 +975,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @P(constants.%Self) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @P(constants.%O.facet.22f) {}
+// CHECK:STDOUT: specific @P(constants.%O.facet) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @WithInteger(constants.%Q) {
 // CHECK:STDOUT:   %Q.loc8_16.2 => constants.%Q
@@ -973,14 +987,14 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %R.patt.loc10_13.2 => constants.%R.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @WithInteger(constants.%O.facet.3ed) {
-// CHECK:STDOUT:   %Q.loc8_16.2 => constants.%O.facet.3ed
+// CHECK:STDOUT: specific @WithInteger(constants.%facet_value) {
+// CHECK:STDOUT:   %Q.loc8_16.2 => constants.%facet_value
 // CHECK:STDOUT:   %Q.patt.loc8_16.2 => constants.%Q.patt
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @WithInteger(@WithBool.%O.facet.loc12_16.2) {}
+// CHECK:STDOUT: specific @WithInteger(@WithBool.%facet_value.loc12_16.2) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- todo_fail_rewrites_mismatch_left.carbon
 // CHECK:STDOUT:
@@ -993,7 +1007,7 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %.Self: %S.type = bind_symbolic_name .Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_type: type = facet_access_type %.Self [symbolic_self]
 // CHECK:STDOUT:   %.Self.as_wit.iface0: <witness> = facet_access_witness %.Self, element0 [symbolic_self]
-// CHECK:STDOUT:   %S.facet.140: %S.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
+// CHECK:STDOUT:   %S.facet: %S.type = facet_value %.Self.as_type, (%.Self.as_wit.iface0) [symbolic_self]
 // CHECK:STDOUT:   %impl.elem0: type = impl_witness_access %.Self.as_wit.iface0, element0 [symbolic_self]
 // CHECK:STDOUT:   %empty_tuple.type: type = tuple_type () [concrete]
 // CHECK:STDOUT:   %S_where.type.15b: type = facet_type <@S where %impl.elem0 = %empty_tuple.type> [concrete]
@@ -1009,8 +1023,8 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %WithU: %WithU.type = struct_value () [concrete]
 // CHECK:STDOUT:   %W.as_wit.iface0: <witness> = facet_access_witness %W, element0 [symbolic]
 // CHECK:STDOUT:   %W.as_type: type = facet_access_type %W [symbolic]
-// CHECK:STDOUT:   %S.facet.6fe: %S_where.type.15b = facet_value %W.as_type, (%W.as_wit.iface0) [symbolic]
-// CHECK:STDOUT:   %WithT.specific_fn: <specific function> = specific_function %WithT, @WithT(%S.facet.6fe) [symbolic]
+// CHECK:STDOUT:   %facet_value: %S_where.type.15b = facet_value %W.as_type, (%W.as_wit.iface0) [symbolic]
+// CHECK:STDOUT:   %WithT.specific_fn: <specific function> = specific_function %WithT, @WithT(%facet_value) [symbolic]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1114,8 +1128,8 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT:   %W.as_wit.iface0.loc13_10.2: <witness> = facet_access_witness %W.loc11_10.2, element0 [symbolic = %W.as_wit.iface0.loc13_10.2 (constants.%W.as_wit.iface0)]
 // CHECK:STDOUT:   %W.as_type.loc13_10.2: type = facet_access_type %W.loc11_10.2 [symbolic = %W.as_type.loc13_10.2 (constants.%W.as_type)]
-// CHECK:STDOUT:   %S.facet.loc13_10.2: %S_where.type.15b = facet_value %W.as_type.loc13_10.2, (%W.as_wit.iface0.loc13_10.2) [symbolic = %S.facet.loc13_10.2 (constants.%S.facet.6fe)]
-// CHECK:STDOUT:   %WithT.specific_fn.loc13_3.2: <specific function> = specific_function constants.%WithT, @WithT(%S.facet.loc13_10.2) [symbolic = %WithT.specific_fn.loc13_3.2 (constants.%WithT.specific_fn)]
+// CHECK:STDOUT:   %facet_value.loc13_10.2: %S_where.type.15b = facet_value %W.as_type.loc13_10.2, (%W.as_wit.iface0.loc13_10.2) [symbolic = %facet_value.loc13_10.2 (constants.%facet_value)]
+// CHECK:STDOUT:   %WithT.specific_fn.loc13_3.2: <specific function> = specific_function constants.%WithT, @WithT(%facet_value.loc13_10.2) [symbolic = %WithT.specific_fn.loc13_3.2 (constants.%WithT.specific_fn)]
 // CHECK:STDOUT:
 // CHECK:STDOUT:   fn(%W.patt.loc11_10.1: %S_where.type.0be) {
 // CHECK:STDOUT:   !entry:
@@ -1123,9 +1137,9 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:     %W.ref: %S_where.type.0be = name_ref W, %W.loc11_10.1 [symbolic = %W.loc11_10.2 (constants.%W)]
 // CHECK:STDOUT:     %W.as_wit.iface0.loc13_10.1: <witness> = facet_access_witness constants.%W, element0 [symbolic = %W.as_wit.iface0.loc13_10.2 (constants.%W.as_wit.iface0)]
 // CHECK:STDOUT:     %W.as_type.loc13_10.1: type = facet_access_type constants.%W [symbolic = %W.as_type.loc13_10.2 (constants.%W.as_type)]
-// CHECK:STDOUT:     %S.facet.loc13_10.1: %S_where.type.15b = facet_value %W.as_type.loc13_10.1, (%W.as_wit.iface0.loc13_10.1) [symbolic = %S.facet.loc13_10.2 (constants.%S.facet.6fe)]
-// CHECK:STDOUT:     %.loc13: %S_where.type.15b = converted %W.ref, %S.facet.loc13_10.1 [symbolic = %S.facet.loc13_10.2 (constants.%S.facet.6fe)]
-// CHECK:STDOUT:     %WithT.specific_fn.loc13_3.1: <specific function> = specific_function %WithT.ref, @WithT(constants.%S.facet.6fe) [symbolic = %WithT.specific_fn.loc13_3.2 (constants.%WithT.specific_fn)]
+// CHECK:STDOUT:     %facet_value.loc13_10.1: %S_where.type.15b = facet_value %W.as_type.loc13_10.1, (%W.as_wit.iface0.loc13_10.1) [symbolic = %facet_value.loc13_10.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %.loc13: %S_where.type.15b = converted %W.ref, %facet_value.loc13_10.1 [symbolic = %facet_value.loc13_10.2 (constants.%facet_value)]
+// CHECK:STDOUT:     %WithT.specific_fn.loc13_3.1: <specific function> = specific_function %WithT.ref, @WithT(constants.%facet_value) [symbolic = %WithT.specific_fn.loc13_3.2 (constants.%WithT.specific_fn)]
 // CHECK:STDOUT:     %WithT.call: init %empty_tuple.type = call %WithT.specific_fn.loc13_3.1()
 // CHECK:STDOUT:     return
 // CHECK:STDOUT:   }
@@ -1135,28 +1149,28 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @U(constants.%Self) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @T(constants.%S.facet.140) {}
+// CHECK:STDOUT: specific @T(constants.%S.facet) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @WithT(constants.%V) {
 // CHECK:STDOUT:   %V.loc9_10.2 => constants.%V
 // CHECK:STDOUT:   %V.patt.loc9_10.2 => constants.%V.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @U(constants.%S.facet.140) {}
+// CHECK:STDOUT: specific @U(constants.%S.facet) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @WithU(constants.%W) {
 // CHECK:STDOUT:   %W.loc11_10.2 => constants.%W
 // CHECK:STDOUT:   %W.patt.loc11_10.2 => constants.%W.patt
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @WithT(constants.%S.facet.6fe) {
-// CHECK:STDOUT:   %V.loc9_10.2 => constants.%S.facet.6fe
+// CHECK:STDOUT: specific @WithT(constants.%facet_value) {
+// CHECK:STDOUT:   %V.loc9_10.2 => constants.%facet_value
 // CHECK:STDOUT:   %V.patt.loc9_10.2 => constants.%V.patt
 // CHECK:STDOUT:
 // CHECK:STDOUT: !definition:
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: specific @WithT(@WithU.%S.facet.loc13_10.2) {}
+// CHECK:STDOUT: specific @WithT(@WithU.%facet_value.loc13_10.2) {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: --- fail_import_rewrites.carbon
 // CHECK:STDOUT:
@@ -1360,7 +1374,112 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:
 // CHECK:STDOUT: specific @RewriteTypeMismatch(<error>) {}
 // CHECK:STDOUT:
-// CHECK:STDOUT: --- fail_todo_let.carbon
+// CHECK:STDOUT: --- todo_let.carbon
+// CHECK:STDOUT:
+// CHECK:STDOUT: constants {
+// CHECK:STDOUT:   %A.type: type = facet_type <@A> [concrete]
+// CHECK:STDOUT:   %Self: %A.type = bind_symbolic_name Self, 0 [symbolic]
+// CHECK:STDOUT:   %D: type = class_type @D [concrete]
+// CHECK:STDOUT:   %empty_struct_type: type = struct_type {} [concrete]
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete]
+// CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
+// CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @A> [concrete]
+// CHECK:STDOUT:   %facet_value: %type_where = facet_value %D, (%impl_witness) [concrete]
+// CHECK:STDOUT:   %F.type: type = fn_type @F [concrete]
+// CHECK:STDOUT:   %F: %F.type = struct_value () [concrete]
+// CHECK:STDOUT:   %E: %type_where = bind_symbolic_name E, 0 [symbolic]
+// CHECK:STDOUT:   %E.patt: %type_where = symbolic_binding_pattern E, 0 [symbolic]
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: imports {
+// CHECK:STDOUT:   %Core: <namespace> = namespace file.%Core.import, [concrete] {
+// CHECK:STDOUT:     import Core//prelude
+// CHECK:STDOUT:     import Core//prelude/...
+// CHECK:STDOUT:   }
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: file {
+// CHECK:STDOUT:   package: <namespace> = namespace [concrete] {
+// CHECK:STDOUT:     .Core = imports.%Core
+// CHECK:STDOUT:     .A = %A.decl
+// CHECK:STDOUT:     .D = %D.decl
+// CHECK:STDOUT:     .B = %B
+// CHECK:STDOUT:     .F = %F.decl
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %Core.import = import Core
+// CHECK:STDOUT:   %A.decl: type = interface_decl @A [concrete = constants.%A.type] {} {}
+// CHECK:STDOUT:   %D.decl: type = class_decl @D [concrete = constants.%D] {} {}
+// CHECK:STDOUT:   impl_decl @impl [concrete] {} {
+// CHECK:STDOUT:     %D.ref: type = name_ref D, file.%D.decl [concrete = constants.%D]
+// CHECK:STDOUT:     %A.ref: type = name_ref A, file.%A.decl [concrete = constants.%A.type]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete = constants.%impl_witness]
+// CHECK:STDOUT:   name_binding_decl {
+// CHECK:STDOUT:     %B.patt: %type_where = binding_pattern B
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %.loc8_13.1: type = splice_block %.loc8_13.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %A.ref: type = name_ref A, %A.decl [concrete = constants.%A.type]
+// CHECK:STDOUT:     %.loc8_13.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       requirement_impls %.Self.ref, %A.ref
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %facet_value: %type_where = facet_value constants.%D, (constants.%impl_witness) [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %.loc8_35: %type_where = converted @__global_init.%D.ref, %facet_value [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %B: %type_where = bind_name B, %.loc8_35
+// CHECK:STDOUT:   %F.decl: %F.type = fn_decl @F [concrete = constants.%F] {} {}
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: interface @A {
+// CHECK:STDOUT:   %Self: %A.type = bind_symbolic_name Self, 0 [symbolic = constants.%Self]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = %Self
+// CHECK:STDOUT:   witness = ()
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: impl @impl: %D.ref as %A.ref {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = file.%impl_witness
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: class @D {
+// CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete = constants.%complete_type]
+// CHECK:STDOUT:   complete_type_witness = %complete_type
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   .Self = constants.%D
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: fn @F() {
+// CHECK:STDOUT: !entry:
+// CHECK:STDOUT:   name_binding_decl {
+// CHECK:STDOUT:     %E.patt: %type_where = symbolic_binding_pattern E, 0 [symbolic = constants.%E.patt]
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %D.ref: type = name_ref D, file.%D.decl [concrete = constants.%D]
+// CHECK:STDOUT:   %.loc11_16.1: type = splice_block %.loc11_16.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
+// CHECK:STDOUT:     %A.ref: type = name_ref A, file.%A.decl [concrete = constants.%A.type]
+// CHECK:STDOUT:     %.loc11_16.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:       requirement_impls %.Self.ref, %A.ref
+// CHECK:STDOUT:     }
+// CHECK:STDOUT:   }
+// CHECK:STDOUT:   %facet_value: %type_where = facet_value constants.%D, (constants.%impl_witness) [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %.loc11_38: %type_where = converted %D.ref, %facet_value [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %E: %type_where = bind_symbolic_name E, 0, %.loc11_38 [symbolic = constants.%E]
+// CHECK:STDOUT:   return
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: fn @__global_init() {
+// CHECK:STDOUT: !entry:
+// CHECK:STDOUT:   %D.ref: type = name_ref D, file.%D.decl [concrete = constants.%D]
+// CHECK:STDOUT:   return
+// CHECK:STDOUT: }
+// CHECK:STDOUT:
+// CHECK:STDOUT: --- fail_todo_let_compile_time.carbon
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %A.type: type = facet_type <@A> [concrete]
@@ -1370,7 +1489,8 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   %complete_type: <witness> = complete_type_witness %empty_struct_type [concrete]
 // CHECK:STDOUT:   %impl_witness: <witness> = impl_witness () [concrete]
 // CHECK:STDOUT:   %.Self: type = bind_symbolic_name .Self [symbolic_self]
-// CHECK:STDOUT:   %type_where: type = facet_type <type where TODO> [concrete]
+// CHECK:STDOUT:   %type_where: type = facet_type <type where .Self impls @A> [concrete]
+// CHECK:STDOUT:   %facet_value: %type_where = facet_value %D, (%impl_witness) [concrete]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: imports {
@@ -1398,15 +1518,17 @@ let K: (E where .F = .Self.G) = bool;
 // CHECK:STDOUT:   name_binding_decl {
 // CHECK:STDOUT:     %B.patt: %type_where = binding_pattern B
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %.loc12_13.1: type = splice_block %.loc12_13.2 [concrete = constants.%type_where] {
+// CHECK:STDOUT:   %.loc12_14.1: type = splice_block %.loc12_14.2 [concrete = constants.%type_where] {
 // CHECK:STDOUT:     %.Self: type = bind_symbolic_name .Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %.Self.ref: type = name_ref .Self, %.Self [symbolic_self = constants.%.Self]
 // CHECK:STDOUT:     %A.ref: type = name_ref A, %A.decl [concrete = constants.%A.type]
-// CHECK:STDOUT:     %.loc12_13.2: type = where_expr %.Self [concrete = constants.%type_where] {
+// CHECK:STDOUT:     %.loc12_14.2: type = where_expr %.Self [concrete = constants.%type_where] {
 // CHECK:STDOUT:       requirement_impls %.Self.ref, %A.ref
 // CHECK:STDOUT:     }
 // CHECK:STDOUT:   }
-// CHECK:STDOUT:   %B: %type_where = bind_name B, <error>
+// CHECK:STDOUT:   %facet_value: %type_where = facet_value constants.%D, (constants.%impl_witness) [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %.loc12_36: %type_where = converted @__global_init.%D.ref, %facet_value [concrete = constants.%facet_value]
+// CHECK:STDOUT:   %B: %type_where = bind_name B, %.loc12_36
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: interface @A {

toolchain/check/testdata/where_expr/min_prelude/dot_self_impls.carbon

@@ -0,0 +1,259 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+// INCLUDE-FILE: toolchain/testing/min_prelude/facet_types.carbon
+// EXTRA-ARGS: --no-dump-sem-ir --custom-core
+//
+// AUTOUPDATE
+// TIP: To test this file alone, run:
+// TIP:   bazel test //toolchain/testing:file_test --test_arg=--file_tests=toolchain/check/testdata/where_expr/min_prelude/dot_self_impls.carbon
+// TIP: To dump output, run:
+// TIP:   bazel run //toolchain/testing:file_test -- --dump_output --file_tests=toolchain/check/testdata/where_expr/min_prelude/dot_self_impls.carbon
+
+// --- compound_member_access_through_where_self_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  fn FNonInstance();
+  fn FSelf[self: Self]();
+}
+
+interface J {
+  fn GNonInstance();
+  fn GSelf[self: Self]();
+}
+
+fn INotJ[T:! I where .Self impls J](x: T) {
+  // Can access members of `I` using either kind of member access.
+  T.FNonInstance();
+  T.(I.FNonInstance)();
+
+  x.FNonInstance();
+  x.FSelf();
+  x.(I.FSelf)();
+
+  // Can still find members of `J` using compound member access,
+  // even though they are not available via `T.GNonInstance` or
+  // `x.GSelf`.
+  T.(J.GNonInstance)();
+  x.(J.GSelf)();
+}
+
+fn TypeNotJ[T:! type where .Self impls J](x: T) {
+  T.(J.GNonInstance)();
+  x.(J.GSelf)();
+}
+
+// --- no_name_conflict_with_where_self_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  fn F() -> ();
+}
+
+interface J {
+  fn F() -> {};
+}
+
+fn INotJ(T:! I where .Self impls J) {
+  // Gets `T.(I.F)`. Doesn't consider `T.(J.F)`, so no ambiguity.
+  let x: () = T.F();
+}
+
+// --- fail_name_lookup_through_where_self_impls.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  fn F();
+}
+
+interface J {
+  fn G();
+}
+
+fn INotJ(T:! I where .Self impls J) {
+  // CHECK:STDERR: fail_name_lookup_through_where_self_impls.carbon:[[@LINE+4]]:3: error: member name `G` not found in `I` [MemberNameNotFoundInInstScope]
+  // CHECK:STDERR:   T.G();
+  // CHECK:STDERR:   ^~~
+  // CHECK:STDERR:
+  T.G();
+}
+
+// --- fail_name_lookup_with_type.carbon
+library "[[@TEST_NAME]]";
+
+interface J {
+  fn G();
+}
+
+fn TypeNotJ(T:! type where .Self impls J) {
+  // CHECK:STDERR: fail_name_lookup_with_type.carbon:[[@LINE+4]]:3: error: member name `G` not found [MemberNameNotFound]
+  // CHECK:STDERR:   T.G();
+  // CHECK:STDERR:   ^~~
+  // CHECK:STDERR:
+  T.G();
+}
+
+// --- fail_facet_type_simple_member_access.carbon
+library "[[@TEST_NAME]]";
+
+interface A {}
+interface B { fn Bfn(); }
+
+fn F(T:! A & B) {
+  // CHECK:STDERR: fail_facet_type_simple_member_access.carbon:[[@LINE+4]]:6: error: member name `Bfn` not found in `A` [MemberNameNotFoundInInstScope]
+  // CHECK:STDERR:   T.((A where .Self impls B).Bfn)();
+  // CHECK:STDERR:      ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  T.((A where .Self impls B).Bfn)();
+
+  // CHECK:STDERR: fail_facet_type_simple_member_access.carbon:[[@LINE+4]]:3: error: member name `Bfn` not found in `A` [MemberNameNotFoundInInstScope]
+  // CHECK:STDERR:   (A where .Self impls B).Bfn;
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  (A where .Self impls B).Bfn;
+}
+
+// --- fail_name_lookup_instance.carbon
+library "[[@TEST_NAME]]";
+
+interface I {
+  fn FNonInstance();
+  fn FSelf[self: Self]();
+}
+
+interface J {
+  fn GNonInstance();
+  fn GSelf[self: Self]();
+}
+
+fn INotJ[T:! I where .Self impls J](x: T) {
+  // CHECK:STDERR: fail_name_lookup_instance.carbon:[[@LINE+4]]:3: error: member name `GNonInstance` not found in `I` [MemberNameNotFoundInInstScope]
+  // CHECK:STDERR:   x.GNonInstance();
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  x.GNonInstance();
+
+  // CHECK:STDERR: fail_name_lookup_instance.carbon:[[@LINE+4]]:3: error: member name `GSelf` not found in `I` [MemberNameNotFoundInInstScope]
+  // CHECK:STDERR:   x.GSelf();
+  // CHECK:STDERR:   ^~~~~~~
+  // CHECK:STDERR:
+  x.GSelf();
+}
+
+// --- compare_equal.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn AssertSame[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I;
+interface J;
+interface K;
+
+fn Test() {
+  AssertSame(Type(I), Type(I where .Self impls I));
+  AssertSame(Type(I), Type(I where .Self impls I & I));
+  AssertSame(Type(I & J), Type(J & I where .Self impls I));
+  AssertSame(Type(I & J), Type(J & I where .Self impls J));
+  AssertSame(Type(I & J), Type(J & I where .Self impls I & J));
+  AssertSame(Type(I & J where .Self impls K), Type(J & I where .Self impls I & K));
+  AssertSame(Type(I & J where .Self impls K), Type(J & I where .Self impls J & K));
+  AssertSame(Type(I & J where .Self impls K), Type(J & I where .Self impls K & I & J));
+  AssertSame(Type(I where .Self impls J & K), Type(I where .Self impls K & I & J));
+  AssertSame(Type(I where .Self impls J & K),
+             Type(I where .Self impls (J where .Self impls K)));
+  AssertSame(Type(I where .Self impls J & K),
+             Type(I where .Self impls (K where .Self impls J)));
+  AssertSame(Type(I where .Self impls J & K),
+             Type(I where .Self impls (type where .Self impls (J where .Self impls K))));
+}
+
+interface I {}
+interface J {}
+interface K {}
+
+// --- compare_equal_with_associated_constant.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn AssertSame[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I { let A:! type; }
+interface J { let A:! type; }
+
+fn Test() {
+  AssertSame(Type((I where .A = ()) & J),
+             Type(I & J where .Self impls (I where .A = ())));
+  AssertSame(Type(I & (J where .A = {})),
+             Type(I & J where .Self impls (J where .A = {})));
+
+  AssertSame(Type((I where .A = ()) & (J where .A = {})),
+             Type(I & J where .Self impls (I where .A = ())
+                    and .Self impls (J where .A = {})));
+  AssertSame(Type((I where .A = ()) & (J where .A = {})),
+             Type(I & J where .Self impls (I where .A = ()) & (J where .A = {})));
+}
+
+// --- fail_compare_not_equal.carbon
+library "[[@TEST_NAME]]";
+
+class WrapType(T:! type) {}
+fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+fn Type(T:! type) -> WrapType(T) { return {}; }
+
+interface I {}
+interface J {}
+
+fn Test() {
+  // CHECK:STDERR: fail_compare_not_equal.carbon:[[@LINE+7]]:3: error: inconsistent deductions for value of generic parameter `T` [DeductionInconsistent]
+  // CHECK:STDERR:   Same(Type(I where .Self impls J), Type(J where .Self impls I));
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR: fail_compare_not_equal.carbon:[[@LINE-10]]:1: note: while deducing parameters of generic declared here [DeductionGenericHere]
+  // CHECK:STDERR: fn Same[T:! type](a: WrapType(T), b: WrapType(T)) {}
+  // CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  // CHECK:STDERR:
+  Same(Type(I where .Self impls J), Type(J where .Self impls I));
+}
+
+// --- impl_as.carbon
+library "[[@TEST_NAME]]";
+
+class C {}
+
+interface I {}
+interface J { let T:! type; }
+
+// Interfaces to the right of the `where` don't interfere with the
+// "can only impl a facet type with a single interface" rule. Only
+// the interface being implemented needs to have all of its
+// associated constants set
+impl {.a: C} as I where .Self impls J {}
+impl {.b: C} as J where .Self impls I and .T = () {}
+
+// Rewrite constraints can appear inside the `where .Self impls`.
+impl {.c: C} as J where .Self impls (I & J where .T = ()) {}
+
+// --- impl_with_rewrite_of_interface_not_being_implemented.carbon
+library "[[@TEST_NAME]]";
+
+interface I { let A:! type; }
+interface J { let A:! type; }
+
+class C {}
+
+// Implementation of `C as J`.
+impl C as J where .A = {} {}
+
+// This is an implementation of `I` with `I.A = ()`. The requirement
+// that `C` also impls `J where .A = {}` is an additional constraint
+// that must be satisfied (and is satisfied by the impl above, though
+// that currently isn't checked), but doesn't affect `C as I`.
+impl C as I where .Self impls
+    (J where .A = {} and .Self impls (I where .A = ())) {}
+
+let x: C.(I.A) = ();
+let y: C.(J.A) = {};

toolchain/check/type_completion.cpp

@@ -616,20 +616,11 @@ auto RequireIdentifiedFacetType(Context& context,
   const auto& facet_type_info =
       context.facet_types().Get(facet_type.facet_type_id);
 
-  SemIR::IdentifiedFacetType result;
   // TODO: expand named constraints
-  result.set_required_interfaces(facet_type_info.impls_constraints);
-
-  // TODO: Distinguish interfaces that are required but would not be
-  // implemented, such as those from `where .Self impls I`.
-  if (result.required_interfaces().size() == 1) {
-    result.set_interface_to_impl(result.required_interfaces().front());
-  } else {
-    result.set_num_interfaces_to_impl(result.required_interfaces().size());
-  }
-
   // TODO: Process other kinds of requirements.
-  return context.identified_facet_types().Add(facet_type.facet_type_id, result);
+  return context.identified_facet_types().Add(
+      facet_type.facet_type_id, {facet_type_info.extend_constraints,
+                                 facet_type_info.self_impls_constraints});
 }
 
 auto AsCompleteType(Context& context, SemIR::TypeId type_id,

toolchain/diagnostics/diagnostic_kind.def

@@ -294,6 +294,7 @@ CARBON_DIAGNOSTIC_KIND(ExtendImplSelfAs)
 CARBON_DIAGNOSTIC_KIND(ExtendImplSelfAsDefault)
 CARBON_DIAGNOSTIC_KIND(ImplAccessMemberBeforeSet)
 CARBON_DIAGNOSTIC_KIND(ImplAsIncompleteFacetTypeDefinition)
+CARBON_DIAGNOSTIC_KIND(ImplAsIncompleteFacetTypeRewrites)
 CARBON_DIAGNOSTIC_KIND(ImplAsNonFacetType)
 CARBON_DIAGNOSTIC_KIND(ImplAsOutsideClass)
 CARBON_DIAGNOSTIC_KIND(ImplAssociatedConstantNeedsValue)

toolchain/sem_ir/dump.cpp

@@ -114,7 +114,14 @@ LLVM_DUMP_METHOD auto Dump(const File& file, FacetTypeId facet_type_id)
 
   const auto& facet_type = file.facet_types().Get(facet_type_id);
   out << ": " << facet_type;
-  for (auto impls : facet_type.impls_constraints) {
+  for (auto impls : facet_type.extend_constraints) {
+    out << "\n  - " << Dump(file, impls.interface_id);
+    if (impls.specific_id.has_value()) {
+      out << "; " << DumpSpecificSummary(file, impls.specific_id);
+    }
+    out << " (extend)";
+  }
+  for (auto impls : facet_type.self_impls_constraints) {
     out << "\n  - " << Dump(file, impls.interface_id);
     if (impls.specific_id.has_value()) {
       out << "; " << DumpSpecificSummary(file, impls.specific_id);
@@ -296,10 +303,10 @@ LLVM_DUMP_METHOD auto Dump(const File& file,
     if (req_interface == identified_facet_type.impl_as_target_interface()) {
       out << " (to impl)";
     }
-    if (!identified_facet_type.is_valid_impl_as_target()) {
-      out << "\n  - (" << identified_facet_type.num_interfaces_to_impl()
-          << " to impl)\n";
-    }
+  }
+  if (!identified_facet_type.is_valid_impl_as_target()) {
+    out << "\n  - (" << identified_facet_type.num_interfaces_to_impl()
+        << " to impl)\n";
   }
   return out.TakeStr();
 }

toolchain/sem_ir/facet_type_info.cpp

@@ -34,8 +34,86 @@ static auto RequiredLess(const IdentifiedFacetType::RequiredInterface& lhs,
          std::tie(rhs.interface_id.index, rhs.specific_id.index);
 }
 
+// Assuming both `a` and `b` are sorted and deduplicated, replaces `a` with `a -
+// b` as sets. Assumes there are few elements between them.
+static auto SubtractSorted(
+    llvm::SmallVector<FacetTypeInfo::ImplsConstraint>& a,
+    const llvm::SmallVector<FacetTypeInfo::ImplsConstraint>& b) -> void {
+  using Iter = llvm::SmallVector<FacetTypeInfo::ImplsConstraint>::iterator;
+  Iter a_iter = a.begin();
+  Iter a_end = a.end();
+  using ConstIter =
+      llvm::SmallVector<FacetTypeInfo::ImplsConstraint>::const_iterator;
+  ConstIter b_iter = b.begin();
+  ConstIter b_end = b.end();
+  // Advance the iterator pointing to the smaller element until we find a match.
+  while (a_iter != a_end && b_iter != b_end) {
+    if (ImplsLess(*a_iter, *b_iter)) {
+      ++a_iter;
+    } else if (ImplsLess(*b_iter, *a_iter)) {
+      ++b_iter;
+    } else {
+      break;
+    }
+  }
+  if (a_iter == a_end || b_iter == b_end) {
+    // Nothing to remove from `a`.
+    return;
+  }
+  // Found a match, switch to removing elements of `a`.
+  CARBON_DCHECK(*a_iter == *b_iter);
+  // We copy the elements we want to keep to `*a_new_end`, and skip the elements
+  // of `a` that match something in `b`.
+  Iter a_new_end = a_iter;
+  ++a_iter;
+  ++b_iter;
+  while (a_iter != a_end && b_iter != b_end) {
+    if (ImplsLess(*a_iter, *b_iter)) {
+      *a_new_end = *a_iter;
+      ++a_new_end;
+      ++a_iter;
+    } else if (ImplsLess(*b_iter, *a_iter)) {
+      ++b_iter;
+    } else {
+      CARBON_DCHECK(*a_iter == *b_iter);
+      ++a_iter;
+      ++b_iter;
+    }
+  }
+  // Keep the remaining elements of `a`, if any.
+  for (; a_iter != a_end; ++a_iter) {
+    *a_new_end = *a_iter;
+    ++a_new_end;
+  }
+  // Shrink `a` by the number of elements that we skipped since they matched
+  // something in `b`.
+  a.erase(a_new_end, a_end);
+}
+
+auto FacetTypeInfo::Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
+    -> FacetTypeInfo {
+  FacetTypeInfo info = {.other_requirements = false};
+  info.extend_constraints.reserve(lhs.extend_constraints.size() +
+                                  rhs.extend_constraints.size());
+  llvm::append_range(info.extend_constraints, lhs.extend_constraints);
+  llvm::append_range(info.extend_constraints, rhs.extend_constraints);
+  info.self_impls_constraints.reserve(lhs.self_impls_constraints.size() +
+                                      rhs.self_impls_constraints.size());
+  llvm::append_range(info.self_impls_constraints, lhs.self_impls_constraints);
+  llvm::append_range(info.self_impls_constraints, rhs.self_impls_constraints);
+  info.rewrite_constraints.reserve(lhs.rewrite_constraints.size() +
+                                   rhs.rewrite_constraints.size());
+  llvm::append_range(info.rewrite_constraints, lhs.rewrite_constraints);
+  llvm::append_range(info.rewrite_constraints, rhs.rewrite_constraints);
+  info.other_requirements |= lhs.other_requirements;
+  info.other_requirements |= rhs.other_requirements;
+  return info;
+}
+
 auto FacetTypeInfo::Canonicalize() -> void {
-  SortAndDeduplicate(impls_constraints, ImplsLess);
+  SortAndDeduplicate(extend_constraints, ImplsLess);
+  SortAndDeduplicate(self_impls_constraints, ImplsLess);
+  SubtractSorted(self_impls_constraints, extend_constraints);
   SortAndDeduplicate(rewrite_constraints, RewriteLess);
 }
 
@@ -43,10 +121,21 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
   out << "{";
   llvm::ListSeparator outer_sep("; ");
 
-  if (!impls_constraints.empty()) {
-    out << outer_sep << "impls interface: ";
+  if (!extend_constraints.empty()) {
+    out << outer_sep << "extends interface: ";
     llvm::ListSeparator sep;
-    for (ImplsConstraint req : impls_constraints) {
+    for (ImplsConstraint req : extend_constraints) {
+      out << sep << req.interface_id;
+      if (req.specific_id.has_value()) {
+        out << "(" << req.specific_id << ")";
+      }
+    }
+  }
+
+  if (!self_impls_constraints.empty()) {
+    out << outer_sep << "self impls interface: ";
+    llvm::ListSeparator sep;
+    for (ImplsConstraint req : self_impls_constraints) {
       out << sep << req.interface_id;
       if (req.specific_id.has_value()) {
         out << "(" << req.specific_id << ")";
@@ -69,7 +158,20 @@ auto FacetTypeInfo::Print(llvm::raw_ostream& out) const -> void {
   out << "}";
 }
 
-auto IdentifiedFacetType::CanonicalizeRequiredInterfaces() -> void {
+IdentifiedFacetType::IdentifiedFacetType(
+    llvm::ArrayRef<RequiredInterface> extends,
+    llvm::ArrayRef<RequiredInterface> self_impls) {
+  if (extends.size() == 1) {
+    interface_id_ = extends.front().interface_id;
+    specific_id_ = extends.front().specific_id;
+  } else {
+    interface_id_ = InterfaceId::None;
+    num_interface_to_impl_ = extends.size();
+  }
+
+  required_interfaces_.reserve(extends.size() + self_impls.size());
+  llvm::append_range(required_interfaces_, extends);
+  llvm::append_range(required_interfaces_, self_impls);
   SortAndDeduplicate(required_interfaces_, RequiredLess);
 }
 

toolchain/sem_ir/facet_type_info.h

@@ -15,16 +15,7 @@ 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.
   static auto Combine(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
-      -> FacetTypeInfo {
-    FacetTypeInfo info = {.other_requirements = false};
-    llvm::append_range(info.impls_constraints, lhs.impls_constraints);
-    llvm::append_range(info.impls_constraints, rhs.impls_constraints);
-    llvm::append_range(info.rewrite_constraints, lhs.rewrite_constraints);
-    llvm::append_range(info.rewrite_constraints, rhs.rewrite_constraints);
-    info.other_requirements |= lhs.other_requirements;
-    info.other_requirements |= rhs.other_requirements;
-    return info;
-  }
+      -> FacetTypeInfo;
 
   // TODO: Need to switch to a processed, canonical form, that can support facet
   // type equality as defined by
@@ -36,10 +27,11 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
   // `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`.
-  // TODO: Add whether this is a lookup context. Those that are should sort
-  // first for easy access. Right now, all are assumed to be lookup contexts.
   using ImplsConstraint = SpecificInterface;
-  llvm::SmallVector<ImplsConstraint> impls_constraints;
+  // These are the required interfaces that are lookup contexts.
+  llvm::SmallVector<ImplsConstraint> extend_constraints;
+  // These are the required interfaces that are not lookup contexts.
+  llvm::SmallVector<ImplsConstraint> self_impls_constraints;
 
   // Rewrite constraints of the form `.T = U`
   struct RewriteConstraint {
@@ -65,19 +57,21 @@ struct FacetTypeInfo : Printable<FacetTypeInfo> {
 
   // In some cases, a facet type is expected to represent a single interface.
   // For example, an interface declaration or an associated constant are
-  // associated with a facet type that will always be a single interface.
+  // associated with a facet type that will always be a single interface with no
+  // other constraints. This returns the single interface that this facet type
+  // represents, or `std::nullopt` if it has any other constraints.
   auto TryAsSingleInterface() const -> std::optional<ImplsConstraint> {
-    // We are ignoring other requirements for the moment, since this function is
-    // (hopefully) temporary.
-    if (impls_constraints.size() == 1) {
-      return impls_constraints.front();
+    if (extend_constraints.size() == 1 && self_impls_constraints.empty() &&
+        rewrite_constraints.empty() && !other_requirements) {
+      return extend_constraints.front();
     }
     return std::nullopt;
   }
 
   friend auto operator==(const FacetTypeInfo& lhs, const FacetTypeInfo& rhs)
       -> bool {
-    return lhs.impls_constraints == rhs.impls_constraints &&
+    return lhs.extend_constraints == rhs.extend_constraints &&
+           lhs.self_impls_constraints == rhs.self_impls_constraints &&
            lhs.rewrite_constraints == rhs.rewrite_constraints &&
            lhs.other_requirements == rhs.other_requirements;
   }
@@ -90,17 +84,14 @@ constexpr FacetTypeInfo::RewriteConstraint
 struct IdentifiedFacetType {
   using RequiredInterface = SpecificInterface;
 
-  IdentifiedFacetType() {}
+  IdentifiedFacetType(llvm::ArrayRef<RequiredInterface> extends,
+                      llvm::ArrayRef<RequiredInterface> self_impls);
 
+  // The order here defines the order of impl witnesses for this facet type.
   auto required_interfaces() const -> llvm::ArrayRef<RequiredInterface> {
     return required_interfaces_;
   }
 
-  auto set_required_interfaces(const llvm::ArrayRef<RequiredInterface> set_to) {
-    required_interfaces_.assign(set_to.begin(), set_to.end());
-    CanonicalizeRequiredInterfaces();
-  }
-
   // Can this be used to the right of an `as` in an `impl` declaration?
   auto is_valid_impl_as_target() const -> bool {
     return interface_id_.has_value();
@@ -124,26 +115,7 @@ struct IdentifiedFacetType {
     }
   }
 
-  // Call this function if num != 1, otherwise call `set_interface_to_impl`.
-  auto set_num_interfaces_to_impl(int num) -> void {
-    CARBON_CHECK(num != 1);
-    interface_id_ = InterfaceId::None;
-    num_interface_to_impl_ = num;
-  }
-
-  // If there is a single interface to implement, specify which it is.
-  // Should be an element of `required_interfaces()`.
-  auto set_interface_to_impl(SpecificInterface interface) -> void {
-    CARBON_CHECK(interface.interface_id.has_value());
-    interface_id_ = interface.interface_id;
-    specific_id_ = interface.specific_id;
-  }
-
  private:
-  // Sorts and deduplicates `required_interfaces`. Call after building the sets
-  // of interfaces, and then don't mutate the value afterwards.
-  auto CanonicalizeRequiredInterfaces() -> void;
-
   // Interfaces mentioned explicitly in the facet type expression, or
   // transitively through a named constraint. Sorted and deduplicated.
   llvm::SmallVector<RequiredInterface> required_interfaces_;
@@ -165,7 +137,8 @@ struct IdentifiedFacetType {
 inline auto CarbonHashValue(const FacetTypeInfo& value, uint64_t seed)
     -> HashCode {
   Hasher hasher(seed);
-  hasher.HashSizedBytes(llvm::ArrayRef(value.impls_constraints));
+  hasher.HashSizedBytes(llvm::ArrayRef(value.extend_constraints));
+  hasher.HashSizedBytes(llvm::ArrayRef(value.self_impls_constraints));
   hasher.HashSizedBytes(llvm::ArrayRef(value.rewrite_constraints));
   hasher.HashRaw(value.other_requirements);
   // `complete_id` is not part of the state to hash.

toolchain/sem_ir/formatter.cpp

@@ -1245,10 +1245,10 @@ class FormatterImpl {
     out_ << "<";
 
     llvm::ListSeparator sep(" & ");
-    if (info.impls_constraints.empty()) {
+    if (info.extend_constraints.empty()) {
       out_ << "type";
     } else {
-      for (auto interface : info.impls_constraints) {
+      for (auto interface : info.extend_constraints) {
         out_ << sep;
         FormatName(interface.interface_id);
         if (interface.specific_id.has_value()) {
@@ -1258,10 +1258,22 @@ class FormatterImpl {
       }
     }
 
-    if (info.other_requirements || !info.rewrite_constraints.empty()) {
-      // TODO: Include specifics.
+    if (info.other_requirements || !info.self_impls_constraints.empty() ||
+        !info.rewrite_constraints.empty()) {
       out_ << " where ";
       llvm::ListSeparator and_sep(" and ");
+      if (!info.self_impls_constraints.empty()) {
+        out_ << and_sep << ".Self impls ";
+        llvm::ListSeparator amp_sep(" & ");
+        for (auto interface : info.self_impls_constraints) {
+          out_ << amp_sep;
+          FormatName(interface.interface_id);
+          if (interface.specific_id.has_value()) {
+            out_ << ", ";
+            FormatName(interface.specific_id);
+          }
+        }
+      }
       for (auto rewrite : info.rewrite_constraints) {
         out_ << and_sep;
         FormatConstant(rewrite.lhs_const_id);

toolchain/sem_ir/inst_fingerprinter.cpp

@@ -211,7 +211,11 @@ struct Worklist {
 
   auto Add(FacetTypeId facet_type_id) -> void {
     const auto& facet_type = sem_ir->facet_types().Get(facet_type_id);
-    for (auto [interface_id, specific_id] : facet_type.impls_constraints) {
+    for (auto [interface_id, specific_id] : facet_type.extend_constraints) {
+      Add(interface_id);
+      Add(specific_id);
+    }
+    for (auto [interface_id, specific_id] : facet_type.self_impls_constraints) {
       Add(interface_id);
       Add(specific_id);
     }

toolchain/sem_ir/inst_namer.cpp

@@ -613,13 +613,14 @@ auto InstNamer::CollectNamesInBlock(ScopeId top_scope_id,
         const auto& facet_type_info =
             sem_ir_->facet_types().Get(inst.facet_type_id);
         bool has_where = facet_type_info.other_requirements ||
+                         !facet_type_info.self_impls_constraints.empty() ||
                          !facet_type_info.rewrite_constraints.empty();
-        if (auto interface = facet_type_info.TryAsSingleInterface()) {
-          const auto& interface_info =
-              sem_ir_->interfaces().Get(interface->interface_id);
+        if (facet_type_info.extend_constraints.size() == 1) {
+          const auto& interface_info = sem_ir_->interfaces().Get(
+              facet_type_info.extend_constraints.front().interface_id);
           add_inst_name_id(interface_info.name_id,
                            has_where ? "_where.type" : ".type");
-        } else if (facet_type_info.impls_constraints.empty()) {
+        } else if (facet_type_info.extend_constraints.empty()) {
           add_inst_name(has_where ? "type_where" : "type");
         } else {
           add_inst_name("facet_type");

toolchain/sem_ir/stringify_type.cpp

@@ -312,18 +312,29 @@ class Stringifier {
       step_stack_->Push(" ", lhs_const_id, " = ", rhs_const_id);
       some_where = true;
     }
+    if (!facet_type_info.self_impls_constraints.empty()) {
+      if (some_where) {
+        step_stack_->PushString(" and");
+      }
+      llvm::ListSeparator sep(" & ");
+      for (auto impls : llvm::reverse(facet_type_info.self_impls_constraints)) {
+        step_stack_->Push(impls, &sep);
+      }
+      step_stack_->PushString(" .Self impls ");
+      some_where = true;
+    }
     // TODO: Other restrictions from facet_type_info.
     if (some_where) {
       step_stack_->PushString(" where");
     }
 
-    // Output interface requirements.
-    if (facet_type_info.impls_constraints.empty()) {
+    // Output extend interface requirements.
+    if (facet_type_info.extend_constraints.empty()) {
       step_stack_->PushString("type");
       return;
     }
     llvm::ListSeparator sep(" & ");
-    for (auto impls : llvm::reverse(facet_type_info.impls_constraints)) {
+    for (auto impls : llvm::reverse(facet_type_info.extend_constraints)) {
       step_stack_->Push(impls, &sep);
     }
   }
@@ -402,9 +413,11 @@ class Stringifier {
           sem_ir_->insts().Get(witness->facet_value_inst_id).type_id();
       auto facet_type = sem_ir_->types().GetAs<FacetType>(witness_type_id);
       // TODO: Support != 1 interface better.
-      return sem_ir_->facet_types()
-          .Get(facet_type.facet_type_id)
-          .TryAsSingleInterface();
+      const auto& facet_type_info =
+          sem_ir_->facet_types().Get(facet_type.facet_type_id);
+      if (facet_type_info.extend_constraints.size() == 1) {
+        return facet_type_info.extend_constraints.front();
+      }
     }
 
     // TODO: Handle other cases.