review

Author: danakj

proposals/p6902.md

@@ -19,6 +19,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 -   [Details](#details)
 -   [Rationale](#rationale)
 -   [Alternatives considered](#alternatives-considered)
+    -   [Only allow `Self as N` to be identified in a named constraint `N`](#only-allow-self-as-n-to-be-identified-in-a-named-constraint-n)
 
 <!-- tocstop -->
 
@@ -27,22 +28,22 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 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.
+rather than requiring them to be fully complete, when used through the `Self`
+facet. This change enables impl lookups with `Self` within a constraint's
+definition to correctly resolve witnesses based on prior `require impls`
+statements in the definition.
 
 ## 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.
+type is identified only if all its referenced interfaces are declared and all
+its referenced named constraints are 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.
+relies on an impl lookup with `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 constraint from depending on earlier ones.
 
 ## Background
 
@@ -51,13 +52,24 @@ earlier ones.
 
 ## 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**.
+We propose redefining the identification criteria for facet types.
 
-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.
+A facet type is identified if all the interfaces it references are declared and
+all the named constraints it references are complete. Additionally, the facet
+type of `Self` in a named constraint is identified even though it is not
+complete.
+
+An identified facet type is associated with a known set of interfaces. For the
+facet type of `Self` in a named constraint, the set of interfaces is established
+by the `require impls` statements before that use of `Self`. This means the
+identified facet type of `Self` changes across the definition of a named
+constraint.
+
+We also propose to disallow using a named constraint inside its own definition,
+except through the type of `Self`. Any other use is diagnosed as an error. This
+way we can use `Self` to find a witness, but we can not use the named constraint
+as an independent entity, such as within a constraint for a `require impls`
+statement.
 
 ## Details
 
@@ -98,8 +110,8 @@ In this example, identifying `W` while it is being defined allows the lookup for
 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:
+However, without disallowing the use of the named constraint independent of
+`Self`, the following becomes possible:
 
 ```carbon
 constraint W {
@@ -112,13 +124,14 @@ 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`.
+To prevent this, we disallow the use of `W` inside `W`, except through the type
+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.
+Together these changes allow a named constraint to provide witnesses for facet
+values, while ensuring it is clear that those witnesses are being constructed
+incrementally by coming from `Self`. And we prevent the use of the named
+constraint without going through `Self` since understanding the requirements of
+the named constraint generally requires it to be complete.
 
 ## Rationale
 
@@ -133,4 +146,26 @@ statement.
 
 ## Alternatives considered
 
-None.
+### Only allow `Self as N` to be identified in a named constraint `N`
+
+The rule for when a facet type is identified is written in terms of just a facet
+type. Identifying a facet type is really an operation on a self and a facet type
+together. So we could change the rule to consider the self and only allow `N` to
+be identified in `Self as N`.
+
+This gets us to a similar place as where we are but does disallow:
+
+```carbon
+eval fn TypeOf[T:! type](t: T) -> type { return T; }
+
+class C;
+
+constraint N {
+  require C as TypeOf(Self);
+}
+```
+
+The rule as stated in this proposal allows the above, since the type of `Self`
+can be identified. We allow this because by going through `Self` the developer
+acknowledges that the facet type is incremental and not the complete constraint
+`N`.