Type completeness in extend (#6395)

Define rules for `extend` declarations (`extend require`, `extend impl
as`, `extend base`, `extend adapt`) that say the target scope they name
must be complete at the point of the declaration. Define completeness
for a facet type to include all interfaces and named constraints that
provide unqualified name lookup through the facet type.

---------

Co-authored-by: Carbon Infra Bot <[email protected]>
Co-authored-by: Richard Smith <[email protected]>

Author: 3 people

proposals/p6395.md

@@ -0,0 +1,190 @@
+# Type completeness in extend
+
+<!--
+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/6395)
+
+<!-- toc -->
+
+## Table of contents
+
+-   [Abstract](#abstract)
+-   [Problem](#problem)
+-   [Background](#background)
+-   [Proposal](#proposal)
+-   [Details](#details)
+-   [Rationale](#rationale)
+-   [Alternatives considered](#alternatives-considered)
+
+<!-- tocstop -->
+
+## 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();
+}
+```