Identification of a named constraint during definition

proposals/p6902.md

@@ -0,0 +1,136 @@
+# Identification of a named constraint during definition
+
+<!--
+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/6902)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Details](#details)
+-   [Rationale](#rationale)
+-   [Alternatives considered](#alternatives-considered)
+
+<!-- tocstop -->
+
+## Abstract
+
+This proposal updates the criteria for when a facet type is considered
+"identified." Specifically, it relaxes the requirement for named constraints,
+allowing them to be considered identified if they have begun being defined,
+rather than requiring them to be fully complete. This change enables `Self`
+lookups within a constraint's definition to correctly resolve witnesses based on
+prior `require impls` statements in the same scope.
+
+## Problem
+
+Under the rules established in [Proposal #5168](/proposals/p5168.md), a facet
+type can be identified only if all its referenced interfaces were declared and
+all its named constraints were complete.
+
+This definition creates a circularity problem during the definition of a named
+constraint. If a `require impls` statement inside a named constraint definition
+relies on an impl lookup that involves `Self`, that lookup will fail because the
+the facet type of `Self` is not identified before the named constraint is
+complete. This prevents requirements in a named constraints from depending on
+earlier ones.
+
+## Background
+
+-   [Proposal #5168](/proposals/p5168.md): Introduced rules for facet type
+    identification and completion.
+
+## Proposal
+
+We propose redefining the identification criteria for facet types to say that a
+facet type is identified if all the interfaces it references are declared and
+all of its named constraints are complete **or have begun being defined**.
+
+But we also propose to disallow using a named constraint by name inside its own
+definition. This way we can use `Self` to find a witness, but we can not use the
+named constraint as a constraint for a `require impls` statement.
+
+## Details
+
+This change allows the compiler to treat a named constraint as identified for
+the purposes of impl lookup while it is still being typechecked.
+
+As the compiler processes a series of `require impls` statements within a named
+constraint, the identified facet type of `Self` is built up incrementally. The
+identified facet type of `Self` will contain interfaces provided by
+`require impls` statements written prior to that use of `Self`. Thus later
+`require impls` statements can use the partially-built identified facet type of
+`Self` to find witnesses provided by earlier `require impls` statements during
+impl lookup.
+
+The following example demonstrates a scenario that is currently invalid but
+would be enabled by this proposal:
+
+```carbon
+interface Y {}
+
+interface NeedsY(T:! Y) {}
+
+constraint W {
+  require impls Y;
+
+  // This requires an impl lookup where the query self value is `Self`
+  // (which is of type `W`) and the query interface is `Y`. The lookup
+  // requires identifying the facet type of `Self` to find a witness.
+  // After this proposal, W can be identified because it has begun being
+  // defined. The lookup for `Self as Y` can now succeed due to the previous
+  // `require impls` statement.
+  require impls NeedsY(Self);
+}
+```
+
+In this example, identifying `W` while it is being defined allows the lookup for
+`Self as Y` in order to form a facet value for `NeedsY` to succeed because the
+compiler knows `Self` (of type `W`) implements `Y` from the previous
+`require impls` statement.
+
+However, without disallowing the use of the named constraint by name, the
+following becomes possible:
+
+```carbon
+constraint W {
+  require C impls W;
+  require impls Z;
+}
+```
+
+This says that `C` must implement `W`, yet `W` is not fully defined. At that
+line `W` is still empty, so it places no requirements on `C`. The next line
+requires that anything implementing `W` must implement `Z`.
+
+To prevent this, we disallow the use of _the name_ `W` inside `W`, while still
+allowing the use of `Self`.
+
+Together these changes allow a named constraint to _provide_ witnesses for facet
+values, without allowing the named constraint to become a _requirement_ in a
+facet type. To understand the requirements of a named constraint, it must be
+complete.
+
+## Rationale
+
+This change aligns with Carbon's goal of
+[Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write),
+by allowing expressive generics as they have been designed.
+
+This follows the
+[Information accumulation](/docs/project/principles/information_accumulation.md)
+principle by increasing the information available to the program with each
+statement.
+
+## Alternatives considered
+
+None.