Ensure where requirements in named constraints are visible to lookups (#7299)

Require rewrite and same-type constraints that do not depend on `.Self` to be satisfied when a facet type is identified, since those constraints may not be found later.
2026-10-05 08:11:04 +01:00 · 2026-07-22 16:18:57 +00:00
parent a48d14e451
commit 21dc5cde04
2 changed files with 229 additions and 0 deletions
@@ -29,6 +29,8 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 -   [Facet types](#facet-types)
    -   [Identified facet types](#identified-facet-types)
 -   [Named constraints](#named-constraints)
+    -   [Rewrites and same-type constraints in a named constraint](#rewrites-and-same-type-constraints-in-a-named-constraint)
+    -   [Constraints that don't depend on `.Self`](#constraints-that-dont-depend-on-self)
    -   [Subtyping between facet types](#subtyping-between-facet-types)
 -   [Combining interfaces by anding facet types](#combining-interfaces-by-anding-facet-types)
 -   [Interface requiring other interfaces](#interface-requiring-other-interfaces)
@@ -1110,6 +1112,75 @@ class ImplementsS {
 }
 ```

+### Rewrites and same-type constraints in a named constraint
+
+A `require` statement may include rewrite or same-type constraints. In the case
+of `extend require`, the rewrites are
+[preserved as such](appendix-rewrite-constraints.md#combining-constraints-with-extend).
+But otherwise, any rewrite constraint in the
+[identified facet type](#identified-facet-types) of the `require` is
+[treated as a same-type constraint](appendix-rewrite-constraints.md#combining-constraints-with-require-and-impls)
+instead.
+
+### Constraints that don't depend on `.Self`
+
+> **TODO:** Link to section explaining when identifying a facet type happens when
+> [#5168: Forward `impl` declaration of an incomplete interface](/proposals/p005168-forward-impl-declaration-of-an-incomplete-interface.md)
+> is applied to these docs.
+
+When identifying a facet type, we collect all constraints found in the facet
+type and named constraints. Each constraint must depend on `.Self` in some way
+in order to be found in future impl lookups involving the facet being
+constrained. Thus, if there is no dependency on `.Self` in a constraint, it must
+be satisfied immediately for the identify to complete successfully.
+
+```carbon
+constraint N(T: type) {
+  require impls Z where .Z1 = {};
+}
+```
+
+When the above named constraint is identified as part of a facet type as
+`C impls N(.Self)`, the resulting requirement `Z where .Z1 = {}` is only
+constraining `C`, and not `.Self` from the top-level top-level facet type. So we
+require that `C impls (Z where .Z1 = {})` is already true in order to successfully
+identify.
+
+```carbon
+interface Z(V: type) {
+  let Z1: type;
+  let Z2: type;
+}
+
+constraint M(T2: type, U2: type) {
+  extend require impls Z(U2) where .Z1 = {} and .Z2 == ();
+}
+
+interface Y {
+  fn YY();
+}
+
+class C;
+
+fn F(U: Y where C impls Z(.Self) where .Z1 = {} and .Z2 == (),
+     T: Y where C impls M(.Self, U)) {
+  // Member access into `T` causes its type to be identified, which succeeds.
+  // The identified facet type requires
+  // `C impls Z(U) where .Z1 = {} and .Z2 == ()` which is true from the facet
+  // type of `U`.
+  T.YY();
+}
+
+fn G(U: Y where C impls Z(.Self),
+     T: Y where C impls M(.Self, U));
+  // ❌ Error: The type of `T` can not be identified.
+  // Member access into `T` causes its type to be identified, which fails.
+  // The identified facet type requires
+  // `C impls Z(U) where .Z1 = {} and .Z2 == ()` which we don't know to be
+  // true here.
+  T.YY();
+```
+
 ### Subtyping between facet types

 There is a subtyping relationship between facet types that allows calls of one
@@ -0,0 +1,158 @@
+# Ensure `where` requirements in named constraints are visible to lookups
+
+<!--
+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
+-->
+
+[Pull request](https://github.com/carbon-language/carbon-lang/pull/7299)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Rationale](#rationale)
+-   [Alternatives considered](#alternatives-considered)
+    -   [Diagnosing constraints without a connection to the top-level `.Self` from a `require`](#diagnosing-constraints-without-a-connection-to-the-top-level-self-from-a-require)
+
+<!-- tocstop -->
+
+## Abstract
+
+Require rewrite and same-type constraints that do not depend on `.Self` to be
+satisfied when a facet type is identified, since those constraints may not be
+found later.
+
+## Problem
+
+It is possible to construct a named constraint that, when used, produces a
+rewrite or same-type constraint with no connection to the top-level facet. This
+prevents us from finding the constraint.
+
+```carbon
+constraint N(T: type) {
+  extend require impls Z where .Z1 = {};
+}
+
+// No relationship to `U` in `C impls Z where C.Z1 = {}`.
+fn F(generic U: type where C impls N(.Self)) {
+  {} as C.(Z.Z1);
+}
+```
+
+The `extend require` statement constrains `Self` which in this case is `C`.
+Since it does not use `T`, it has no connection to `.Self` in the facet type of
+`U`. That makes the constraint impossible to find in queries that don't involve
+`U` since we will not know to search its facet type. We limit searching to
+components of the involved types to avoid a global search.
+
+## Background
+
+-   The
+    [rules for rewrite constraints](/docs/design/generics/appendix-rewrite-constraints.md)
+    in the design.
+-   The rules are introduced by proposal
+    [#2 for the rewrite left-hand-side that 173](https://github.com/carbon-language/carbon-lang/blob/358df53c482aeaefc8869ff36f8ef332ec34af3c/proposals/p002173-associated-constant-assignment-versus-equality.md).
+
+## Proposal
+
+When identifying a facet type, collect all rewrite and same-type constraints
+found while also collecting `impls` constraints from the facet type and any
+named constraints it depends on. Require that any constraint which does not
+depend on `.Self` is satisfied immediately, in order to identify the facet type.
+
+During identify, rewrite constraints are collected as rewrite constraints when
+they are part of the top-level facet type being identified, or come from an
+uninterrupted chain of `extend requires` statements. Otherwise, rewrite
+constraints that come from a `requires` statement are collected as same-type
+constraints.
+
+Constraints that do not depend on `.Self` must be immediately satisfied by
+performing an impl lookup with that constraint as a condition. In the following
+example, the identified facet type of `T` contains a rewrite `C.(Z(U).Z1) = {}`
+and the same-type constraint `C.(Z(U).Z2) == ()`. So an impl lookup for `C as
+Z(U) where .Z1 = {} and .Z2 == ()` must be satisfied to identify the type of
+`T`. In this example, the lookup succeeds by finding a witness with the required
+constraints in the facet type of `U`.
+
+```carbon
+interface Z(V: type) {
+  let Z1: type;
+  let Z2: type;
+}
+
+constraint N(T2: type, U2: type) {
+  extend require impls Z(U2) where .Z1 = {} and .Z2 == ();
+}
+
+fn F(U: type where C impls Z(.Self) where .Z1 = {} and .Z2 == (),
+     T: type where C impls N(.Self, U));
+```
+
+It is also possible to find an `impls` constraint that does not depend on
+`.Self` in the identified facet type, through a named constraint.
+
+```carbon
+interface Z {}
+constraint A(T: type) {
+  require T impls Z;
+}
+
+// The identified facet type requires `.Self impls Z`, which is then
+// symbolically provided by the facet type of `U`.
+fn F(U: A(.Self)) {}
+
+// The identified facet type requires `i32 impls Z`, which must be
+// immediately satisfied.
+fn G(U: A(i32)) {}
+```
+
+## Rationale
+
+We now ensure that constraints introduced by a `requires` clause in a named
+constraint are either visible for lookups, or are redundant with existing rules.
+This avoids a global search for the constraint, which advances our
+[low context-sensitivity principle](/docs/project/principles/low_context_sensitivity.md).
+
+Bounding the search allows for a faster and simpler toolchain, which aligns with
+the project goal for
+[fast and scalable development](/docs/project/goals.md#fast-and-scalable-development).
+
+## Alternatives considered
+
+### Diagnosing constraints without a connection to the top-level `.Self` from a `require`
+
+In the following, the rewrite constraint `C.(Z.Z1) = {}` has no connection to
+the top-level facet `U` since it does not contain any reference to the top-level
+`.Self`.
+
+```carbon
+class C;
+
+constraint N(T:! type) {
+  require impls Z where .Z1 = {};
+}
+
+// No relationship to `U` in `C impls Z where C.Z1 = {}`.
+fn F(U:! type where C impls N(.Self)) {}
+```
+
+We could diagnose during identifying the type of `U` that the `where` contains a
+constraint `C.(Z.Z1) = {}` which doesn't involve the self type. This would
+reduce the expressiveness of the generics system and produce an error for some
+uses of `N` but not for others.
+
+```carbon
+class G(T:! type);
+
+// Accepted.
+fn F(U:! type where G(.Self) impls N(.Self)) {}
+
+// Rejected.
+fn F(U:! type where G({}) impls N(.Self)) {}
+```