Type completeness in extend

proposals/p6395.md

@@ -0,0 +1,167 @@
+# 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 the facet type in `extend require impls` and `extend impl as`
+declarations to be complete, since `extend` changes the scopes which are looked
+in for name lookup.
+
+## 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 Z` is written, then `Z` must be identified. However it does not
+specify any rule for `extend require impls Z`. or `extend impl as Z`.
+
+If an interface `Y` uses `extend` for another interface `Z`, then a facet type
+for `Y` will also allow name lookup into `Z`. Similarly if a class `Y` uses
+`extend` for an interface `Z`, then an object of type `Y` will also allow name
+lookup into `Z`. In both cases, when the definition of `Y` is complete, we
+should also require `Z` to be complete, as its name scope becomes conceptually a
+part of `Y`.
+
+Additionally, after an `extend ... Z` declaration inside the definition of `Y`,
+the names of `Z` should be immediately available inside the `Y` definition,
+including inside the nested definition of `extend impl as Z { ... }`.
+
+## 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
+
+Require that `extend require impls Z` requires `Z` to be complete where the
+declaration is written. Similarly, require that `extend impl as Z` requires `Z`
+to be complete where the declaration is written. In both cases, this ensures
+that `Z` is complete by the time the definition of the enclosing class,
+interface, or named constraint is complete. And it ensures that we can perform
+name lookup into `Z` from within the enclosing scope of the `extend` declaration
+thereafter.
+
+We call a `extend require` declaration _extend-reachable_ from a facet type if
+it's enclosing interface or named constraint is part of that facet type, or if
+its enclosing interface or named constraint is named by another
+_extend-reachable_ declaration. That is, we can find a path from the facet type
+to the `extend require` declaration through other `extend require` declarations.
+
+We say that a facet type is complete if:
+
+-   All its _extend-reachable_ `extend require` declarations are complete. This
+    follows from the enclosing interface or named constraint being complete.
+-   We are able to form a specific for each interface and named constraint
+    extended by the facet type.
+-   We are able to form a specific for each _extend-reachable_ `extend require`
+    declaration in the context of the specific facet type being completed,
+    without monomorphization errors.
+
+## Details
+
+To `extend` an entity `Y` with another `Z` means that name lookups into `Y` will
+also look into `Z`. At the end of the definition of `Y`, we expect to be able to
+perform name lookup into `Y`, as it is complete. To maintain this property
+through `extend`, we require that `extend require` declarations only name other
+interfaces or named constraints that are themselves complete.
+
+This functions recursively: Since each interface or named constraint is
+complete, we already know the `extend require` declarations inside are complete.
+However it is possible to uncover monomorphization errors once a specific is
+applied to the facet type in an `extend require` or `extend impls` declaration.
+For example:
+
+```carbon
+interface Z(T:! type) {}
+
+class C(N! i32) {
+  extend impls Z(array(i32, N)) {}
+}
+```
+
+Here the facet type `Z(array(i32, N))` is complete at the point where it is
+written, so `C(N)` is complete. However checking `C(-1)` for completeness must
+form a specific for the `extend impls` declaration that will generate an error
+(as -1 is not valid for an array size), failing type completeness.
+
+The same is true for any `extend require` declaration which is
+_extend-reachable_ from the facet type in the `extend` declaration. So we
+require type completeness to form a specific for each extended interface or
+named constraint in the facet type, as well as for each extended interface or
+named constraint in the facet type of a `extend require` declaration that is
+_extend-reachable_ from them. This implies forming a specific for any interface
+or named constraint along the path to an _extend-reachable_ `extend require`
+declaration.
+
+These rules prohibit `extend require` to name its enclosing interface or named
+constraint, since the enclosing definition is trivially not complete yet. 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-reachable_ `extend require` declaration to be incomplete, then name
+lookup will fail ambiguously. Those same names may be valid later once the
+interface is defined.
+
+## Alternatives considered
+
+We considered not requiring that the facet type in an `extend` be complete where
+it is written, but only when the enclosing class, interface, or named constraint
+is required to be complete. However this does not allow the use of names from
+the facet type in the `extend` to be used 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();
+}
+```