fill-proposal

Author: danakj

proposals/p6395.md

@@ -1,4 +1,4 @@
-# Type completeness in extend require
+# Type completeness in extend
 
 <!--
 Part of the Carbon Language project, under the Apache License v2.0 with LLVM
@@ -24,47 +24,138 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 
 ## Abstract
 
-TODO: Describe, in a succinct paragraph, the gist of this document. This
-paragraph should be reproduced verbatim in the PR summary.
+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
 
-TODO: What problem are you trying to solve? How important is that problem? Who
-is impacted by it?
+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
 
-TODO: Is there any background that readers should consider to fully understand
-this problem and your approach to solving it?
+-   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
 
-TODO: Briefly and at a high level, how do you propose to solve the problem? Why
-will that in fact solve it?
+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 an `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.
 
 ## Details
 
-TODO: Fully explain the details of the proposed solution.
+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.
 
-## Rationale
-
-TODO: How does this proposal effectively advance Carbon's goals? Rather than
-re-stating the full motivation, this should connect that motivation back to
-Carbon's stated goals and principles. This may evolve during review. Use links
-to appropriate sections of [`/docs/project/goals.md`](/docs/project/goals.md),
-and/or to documents in [`/docs/project/principles`](/docs/project/principles).
+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:
 
--   [Community and culture](/docs/project/goals.md#community-and-culture)
--   [Language tools and ecosystem](/docs/project/goals.md#language-tools-and-ecosystem)
--   [Performance-critical software](/docs/project/goals.md#performance-critical-software)
--   [Software and language evolution](/docs/project/goals.md#software-and-language-evolution)
--   [Code that is easy to read, understand, and write](/docs/project/goals.md#code-that-is-easy-to-read-understand-and-write)
--   [Practical safety and testing mechanisms](/docs/project/goals.md#practical-safety-and-testing-mechanisms)
--   [Fast and scalable development](/docs/project/goals.md#fast-and-scalable-development)
--   [Modern OS platforms, hardware architectures, and environments](/docs/project/goals.md#modern-os-platforms-hardware-architectures-and-environments)
--   [Interoperability with and migration from existing C++ code](/docs/project/goals.md#interoperability-with-and-migration-from-existing-c-code)
+```carbon
+interface Z(T:! type) {}
+
+class C(N! i32) {
+  extend impls Z(array(i32, N)) {}
+}
+```
+
+Here the facet yype `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.
+
+## 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
 
-TODO: What alternative solutions have you 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();
+}
+```