diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md index c4006229afd8..7b8c1a38127a 100644 --- a/docs/design/generics/details.md +++ b/docs/design/generics/details.md @@ -27,6 +27,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception - [Return type](#return-type) - [Interfaces recap](#interfaces-recap) - [Facet types](#facet-types) + - [Identified facet types](#identified-facet-types) - [Named constraints](#named-constraints) - [Subtyping between facet types](#subtyping-between-facet-types) - [Combining interfaces by anding facet types](#combining-interfaces-by-anding-facet-types) @@ -894,6 +895,25 @@ names of the facet type. This general structure of facet types holds not just for interfaces, but others described in the rest of this document. +### Identified facet types + +A facet type is _identified_ if all the interfaces it references are declared +and all of its named constraints are complete. An identified facet type is +associated with a known set of interfaces. + +A facet type is _partially identified_ if any of its named constraints are in +the process of being defined. The interfaces associated with a partially +identified facet type change as the named constraint is fully defined. + +Types can implicitly convert to facet types when the requirements of the facet +type are satisfied, but only if the facet type is identified. Attempting to +convert to a facet type that is not identified is an error, since the +requirements of the target facet type are not yet fully determined. + +A facet with an unidentified or partially identified facet type may be converted +_to_ other facet types. While its set of requirements are not fully determined, +the requirements that are known at that time may be used. + ## Named constraints If the interfaces discussed above are the building blocks for facet types, @@ -933,6 +953,54 @@ constraint DrawVectorLegoFish { } ``` +However a named constraint may not refer to itself as a requirement, as that +produces a cycle. In general, any use of named constraint inside its own +definition is disallowed, except through the use of `Self`. + +```carbon +constraint SelfReferential { + // ❌ Error: Can not refer to `SelfReferential` inside its own definition. + require impls SelfReferential; +} +``` + +The facet type of `Self` is partially identified inside the definition of a +named constraint. This allows `Self` to be converted to other facet types based +on the known requirements of the partially identified facet type. Those +requirements include any `require` ... `impls` statements written before the use +of `Self`. + +```carbon +interface Z {} +class UsesZ(T:! Z) {} + +interface Y(T:! type) {} +interface X {} + +constraint Constraint { + // The partially identified facet type of `Self` includes `Z` after this + // statement. + require impls Z; + + // OK, the partially identified facet type of `Self` can convert to facet + // type `Z` to match the parameter of `UsesZ`. + require impls Y(UsesZ(Self)); + + // Also OK, as `Self` converts to `Z` again. + require UsesZ(Self) impls X; +} + +constraint UseOfFutureRequirement { + // ❌ Error: The partially identified facet type of `Self` does not yet + // include `Z` since the requirement for `Z` comes later in the definition. + require impls Y(UsesZ(Self)); + + // The partially identified facet type of `Self` includes `Z` after this + // statement. + require impls Z; +} +``` + In general, Carbon makes no syntactic distinction between the uses of named constraints and interfaces, so one may be replaced with the other without affecting users. To accomplish this, Carbon allows a named constraint to be used @@ -1229,6 +1297,27 @@ var x: Iota; DoAdvanceAndEquals(x); ``` +The facet type at the end of a `require` ... `impls` statement must be +identified. + +```carbon +constraint N; + +interface I { + // ❌ Error: Facet type `N` is not identified since the constraint `N` is not + // complete. + require impls N; +} + +interface J; + +interface K { + // OK, the facet type `J` is identified because the interface `J` is + // declared. + require impls J; +} +``` + Like with named constraints, an interface implementation requirement doesn't by itself add any names to the interface, but again those can be added with `alias` declarations: diff --git a/proposals/p6902.md b/proposals/p6902.md new file mode 100644 index 000000000000..637842ee1ed7 --- /dev/null +++ b/proposals/p6902.md @@ -0,0 +1,253 @@ +# Identification of a named constraint during definition + + + +[Pull request](https://github.com/carbon-language/carbon-lang/pull/6902) + + + +## Table of contents + +- [Abstract](#abstract) +- [Problem](#problem) +- [Background](#background) +- [Proposal](#proposal) + - [Example with `Self`](#example-with-self) + - [Motivating the partially identified state](#motivating-the-partially-identified-state) + - [Disallowing conversions to incomplete named constraint](#disallowing-conversions-to-incomplete-named-constraint) +- [Rationale](#rationale) +- [Alternatives considered](#alternatives-considered) + - [Considering a facet type of a named constraint to be identified in its definition](#considering-a-facet-type-of-a-named-constraint-to-be-identified-in-its-definition) + - [Restricting to `Self`](#restricting-to-self) + - [Allowing limited conversions to partially identified facet types.](#allowing-limited-conversions-to-partially-identified-facet-types) + + + +## 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 incrementally identified inside the definition, 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 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 with `Self`, that lookup will fail because the facet +type of `Self` is not identified before the named constraint is complete. This +prevents `require impls` statements in a named constraint 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 by introducing +a new partially identified state. + +A facet type can be in one of three states: unidentified, partially identified, +or identified. A facet type's identifiedness is the minimum of that of its +constituents: + +- When a facet type refers to an interface, the facet type is not identified + until the interface is declared, and is fully identified after. This + includes inside the definition of the interface. +- When a facet type refers to a named constraint, the facet type is not + identified until the named constraint is declared. It is partially + identified during the definition of the named constraint, and it is fully + identified after. + +The change from previous rules is that a facet type containing a named +constraint is now partially identified inside the definition of that named +constraint. + +As in [#5168](/proposals/p5168.md), an `impl` declaration and `require` +statement each requires its constraint to be identified. + +We define the rules for facets in impl lookups, which are representable as +` as ` conversions as follows: + +- The target facet type of an impl lookup must be defined. + - This allows the full set of interfaces to be known, which allows a + stable ordering of witnesses for those interfaces to be produced by the + impl lookup. +- If the self is a facet, its facet type may be in any state of + identifiedness. + - The impl lookup may provide a witness from the facet type of self, using + the known constraints of any partially identified or identified + constituent of the facet type. + +In particular, this means that `Self as I` inside the definition of a named +constraint `N` may use any `require impls` statements before that use of `Self` +in order to provide a witness for `I`. + +To improve diagnostics, 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 provides a clear error when a named constraint +appears in the constraint of a `require` statement inside its definition. + +### Example with `Self` + +This change allows the compiler to treat a named constraint as partially +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 partially identified facet type of the named constraint, which +can be accessed through `Self`, is built up incrementally. The partially +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 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 is partially 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. + +### Motivating the partially identified state + +If a facet type for a named constraint was considered identified (not partially +identified) inside its definition, 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, the constraint of a `require` statement must still be +identified, and the facet type of the being-defined named constraint is only +partially-identified. + +Note this also disallows the use of `W` through an alias: + +```carbon +constraint W; +alias X = W; +constraint W { + // Error: X refers to named constraint `W` that is not identified. + require impls X; +} +``` + +### Disallowing conversions to incomplete named constraint + +By requiring the target facet type of an impl lookup to be identified, we +disallow an incomplete named constraint from being part of the target of an impl +lookup. + +The result of an impl lookup stores witnesses for the target facet type. If the +target facet type was partially identified, the same facet type may have a +different set of interfaces later. A change in the set of interfaces would +invalidate the set of stored witnesses. + +For example, if this was allowed: + +```carbon +interface Z {} +interface X {} + +constraint W; +class C(T:! W) {} +class D {} + +interface Y(T:! type) {} + +constraint W { + require impls Z; + // Constructs a `D as W` facet value. + require impls Y(C(D)); + require impls X; +} +``` + +In this example the argument to `C` will be `D as W` which will store a witness +for each interface in the identified facet type `W`. If we allow a partially +identified facet type, then it will store a witness for the interface `Z`. But +later uses of the facet value in `Y(C(D))` would expect witnesses for `Z`, `Y` +and `X`, leading to unsoundness. + +## 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 + +### Considering a facet type of a named constraint to be identified in its definition + +Initial versions of this proposal did not differentiate between partially +identified and identified. This led to unsoundness by allowing conversion to a +facet with the incomplete named constraint in the facet's type, as described in +[Disallowing conversions to incomplete named constraint](#disallowing-conversions-to-incomplete-named-constraint). + +### Restricting to `Self` + +We considered restricting the use of the partially identified facet type to only +be on the `Self` facet value. This provided a way to reduce exposure of the +partially identified facet type. But by differentiating the the partially +identified state from identified, we can form the rules around the state of the +facet type instead of the identity of the facet. + +### Allowing limited conversions to partially identified facet types. + +We considered allowing conversions from `N & J` to `N & K` where `N` is +partially identified, and `J` and `K` are identified. + +It seems possible to support this for symbolic facets, by not storing the set of +witnesses in the facet value. If the facet type is partially identified, we can +defer the collection of witnesses, and just store the facet types that the facet +was converted from. In this model, the facet type itself acts as a type of +witness that we will will be able to find a witness later once the facet type is +identified. + +We leave this to a future proposal if and when we find this additional +complexity worth adding to the language model.