# Type completeness in extend [Pull request](https://github.com/carbon-language/carbon-lang/pull/6395) ## Table of contents - [Abstract](#abstract) - [Problem](#problem) - [Background](#background) - [Proposal](#proposal) - [Details](#details) - [Rationale](#rationale) - [Alternatives considered](#alternatives-considered) ## Abstract Require any target scopes in an `extend` declaration to be complete, since `extend` changes the scopes which are looked in for name lookup to include those named in the declaration. ## Problem Proposal [#5168](https://github.com/carbon-language/carbon-lang/blob/trunk/proposals/p5168.md) laid out rules for when a facet type needs to be identified or complete. When `require impls X` is written, then `X` must be identified. However it does not specify any rule for `extend require impls X`. And we lack completeness rules for other `extend` declarations, including `extend impl as X`, `extend base: X`, and `extend adapt X`. An `extend` declaration always names one or more target entities which will be included in the search for names when looking in the enclosing scope of the `extend` declaration. In order to do name lookup into an entity, it must be complete to avoid poisoning names in the entity. ## Background - Proposal [#5168](https://github.com/carbon-language/carbon-lang/blob/trunk/proposals/p5168.md): Forward `impl` declaration of an incomplete interface - Proposal [#2760](https://github.com/carbon-language/carbon-lang/blob/trunk/proposals/p2760.md): Consistent `class` and `interface` syntax - Proposal [#0777](https://github.com/carbon-language/carbon-lang/blob/trunk/proposals/p0777.md): Inheritance ## Proposal An `extend` declaration declares that the enclosing scope extends the scope associated with any target entity named in the declaration. That is to say name lookups into the enclosing scope will also look into the scopes which are nominated by the `extend` declaration. The `extend` declaration requires that the target scopes named in an `extend` declaration are complete, or if the target is a generic parameter, requires the type of the parameter to be complete. The scope of a facet type formed by a `where` declaration extends the scope of its first operand. And the scope of a facet type formed by a `&` operator extends the scopes of both of its operands. In either case, the scope of the facet type is complete if every scope it extends is complete. The facet type `type` is associated with an empty scope and is complete. | Facet type | Requirement | | ---------------------------- | ------------------------------------- | | `I` | Requires `I` is complete. | | `I & J` | Requires `I` and `J` are complete. | | `type where U impls J` | Requires `type` is complete. | | `I & (type where U impls J)` | Requires `I` and `type` are complete. | ## Details To `extend` an entity `Y` with another `Z` means that name lookups into `Y` will also look into `Z`. Immediately after the `extend` operation, members of `Z` should also be found when doing name lookup into `Y`, both from outside and from inside the definition of `Y`. In order to be able to perform lookups into `Z`, we require that `extend` operations only target scopes that are complete. This requirement functions recursively. Given an interface `B` that extends another interface `A`: By naming `A` in an extend declaration, we require `A` is complete. This provides that its entire definition is known, and thus its `extend` relationship to `B`. The `extend` relationship there also provides that `B` is complete. If the target scope of an `extend` declaration is a generic parameter, its type must be complete where the `extend` declaration is written, as name lookups into the extended scope will look into the type of the generic parameter. ```carbon interface I { fn F(); } class C(T:! I) { extend base: T; // `F` names `T.F` here, found in `I`. fn G() { F(); } } ``` As any generic parameter in the enclosing scope is replaced by a more specific value, extended scopes that depend on a generic parameter must remain complete. This includes forming a specific for the extended scope involving the parameter in order to surface any monomorphization errors in the resulting specific. In the next example, the `extend` declaration in interface `A(N)` names a symbolic facet type which can produce monomorphization errors when a negative value is provided for `N`. When a more specific value for the target `B(N)` is provided, we require the specific value to be complete as well by forming the specific. A diagnostic error would be produced while checking `C(-1)` for completeness, as it requires `A(-1)` to be complete, which requires `B(array(i32, -1))` to be complete, and that contains an invalid type. ```carbon interface B(T:! type) {} interface A(N:! i32) { // Requires `B(N)` to be complete. extend require impls B(array(i32, N)) {} } class C(N! i32) { // Requires `A(N)` to be complete, which requires `B(N)` to be complete. extend impl as A(N); } fn F() { // Requires `C(-1)` to be complete, which requires `A(-1)` to be complete, which requires `B(array(i32, -1))` to be complete. var c: C(-1); } ``` These rules prohibit an `extend` declaration from naming its enclosing scope, since by being part of the definition of that scope, it is implied that the enclosing scope is not complete. This seems reasonable as all names available inside the enclosing interface or named constraint are already available or would conflict with the ones that are. ## Rationale This is based on the principle of [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write). For code to be easy to write, the rules need to be consistent. Once an `extend` declaration has been written, the names inside should become available through the enclosing scope immediately. If we allow an interface named in an `extend` declaration to be incomplete, then name lookup will fail ambiguously. Those same names may become valid later once the interface is defined. ## Alternatives considered We considered not requiring that the scope named in an `extend` declaration be complete where it is written, but only when the enclosing scope is required to be complete. This is more flexible, allowing entities to be defined later in the program. However this does not allow the use of names from the target scope in the `extend` to be used from within the enclosing definition scope. They would not become available until the enclosing definition scope was closed and complete. In particular, we want this to work: ```carbon interface Z { let X:! type; fn F() -> X; } class C { extend impl as Z where .X = () { // Names `X` directly. fn F() -> X; } // Names `X` and `F` directly. fn G() -> X { return F(); } } // Now `C` is complete, `C.X` and `C.F` are also available. fn H() -> C.X { return C.F(); } ```