Addressing comments, redeclarations

proposals/p3762.md

@@ -26,8 +26,10 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
         -   [No forward declarations after declarations](#no-forward-declarations-after-declarations)
         -   [Files must either use an imported declaration or declare their own](#files-must-either-use-an-imported-declaration-or-declare-their-own)
         -   [Libraries cannot both define an entity and declare it `extern`](#libraries-cannot-both-define-an-entity-and-declare-it-extern)
+        -   [`impl` files with a forward declaration must contain the definition](#impl-files-with-a-forward-declaration-must-contain-the-definition)
         -   [Type scopes may contain both a forward declaration and definition](#type-scopes-may-contain-both-a-forward-declaration-and-definition)
     -   [Merging `extern` declarations](#merging-extern-declarations)
+    -   [Using `extern` declarations in `extern impl`](#using-extern-declarations-in-extern-impl)
     -   [Modifier keywords](#modifier-keywords)
 -   [Rationale](#rationale)
 -   [Alternatives considered](#alternatives-considered)
@@ -293,6 +295,20 @@ In a library, the `api` might make an `extern` declaration that the `impl`
 imports and uses the definition of. This is consistent because the `impl` file
 is not declaring the entity.
 
+#### `impl` files with a forward declaration must contain the definition
+
+In an `impl` file, if the `impl` file forward declares an entity, it must also
+provide the definition. In libraries with multiple `impl` files, this means that
+using an entity in one `impl` file when it's defined in a different `impl` file
+requires a (possibly `private`) forward declaration in the `api` file. An
+`extern` declaration cannot be used for this purpose because the library defines
+the entity.
+
+This allows Carbon to provide a compile-time diagnostic if an entity declared in
+the `impl` is not defined locally. Note that an entity declared in the `api` may
+still not get a compile-time diagnostic unless the compiler is told it's seeing
+_all_ available `impl` files.
+
 #### Type scopes may contain both a forward declaration and definition
 
 The combination of a forward declaration and a definition is allowed in type
@@ -343,6 +359,15 @@ declaration will:
     -   The `api` may forward declare when the `impl` defines, or the `impl` may
         repeat a forward declaration and also define.
 
+### Using `extern` declarations in `extern impl`
+
+An `extern` type may only be used in the type structure of an `impl` if it's an
+`extern impl`. They are incompatible with non-`extern` `impl`s.
+
+Consider two libraries, one defining `A` and declaring `B` as `extern`, and the
+other defining `B` and declaring `A` as `extern`. Neither should be able to
+define an `impl` involving both `A` and `B`, otherwise both could.
+
 ### Modifier keywords
 
 When considering various modifiers on a forward declaration versus definition: