Updates to design docs to reflect accepted proposals (#3254)

Includes proposals:
- #990
- #2188
- #2138
- #2200
- #2360
- #2760
- #2964
- #3162

Also tries to use more precise language when talking about:
- implementations, to avoid confusing `impl` declaration and definitions
with the `impls` operator used in `where` clauses, an issue brought up
in #2495 and #2483;
- "binding patterns", like `x: i32`, and "bindings" like `x`.

---------

Co-authored-by: Chandler Carruth <chandlerc@gmail.com>

docs/design/README.md

@@ -1604,14 +1604,13 @@ fn Foo() -> f32 {
 }
 ```
 
-> **Note:** This is provisional, no design for `match` statements has been
-> through the proposal process yet.
-
 > References:
 >
 > -   [Pattern matching](pattern_matching.md)
 > -   Question-for-leads issue
 >     [#1283: how should pattern matching and implicit conversion interact?](https://github.com/carbon-language/carbon-lang/issues/1283)
+> -   Proposal
+>     [#2188: Pattern matching syntax and semantics](https://github.com/carbon-language/carbon-lang/pull/2188)
 
 ## User-defined types
 
@@ -3562,9 +3561,6 @@ imported, so a wrapper may be added without requiring changes to importers?
 
 ### Templates
 
-> **Note:** This is provisional, no design for this has been through the
-> proposal process yet.
-
 Carbon supports both
 [checked and template generics](#checked-and-template-parameters). This provides
 a migration path for C++ template code:
@@ -3591,6 +3587,11 @@ toolchain. However, even when using Carbon's generated C++ headers for interop,
 we will include the ability where possible to use a Carbon generic from C++ as
 if it were a C++ template.
 
+> References:
+>
+> -   Proposal
+>     [#2200: Template generics](https://github.com/carbon-language/carbon-lang/pull/2200)
+
 ### Standard types
 
 > **Note:** This is provisional, no design for this has been through the

docs/design/classes.md

@@ -311,8 +311,8 @@ implemented in descendants.
 While it is typical for this case to be associated with single-level inheritance
 hierarchies, there are some cases where there is an interface at the root of a
 type hierarchy and polymorphic types as interior branches of the tree. The case
-of generic interfaces extending or requiring other interface would also be
-modeled by deeper inheritance hierarchies.
+of interfaces extending or requiring other interface would also be modeled by
+deeper inheritance hierarchies.
 
 An interface as base class needs to either have a virtual destructor or forbid
 deallocation.
@@ -325,7 +325,7 @@ that support dynamic dispatch are called _object-safe_, following
 
 -   They don't have a `Self` in the signature of a method in a contravariant
     position like a parameter.
--   They don't have free associated types or other associated items used in a
+-   They don't have free associated facets or other associated items used in a
     method signature.
 
 The restrictions on object-safe interfaces match the restrictions on base class
@@ -910,7 +910,7 @@ which must be an
 then match pattern '`self:` _type_' against it".
 
 If the method declaration also includes
-[deduced generic parameters](/docs/design/generics/overview.md#deduced-parameters),
+[deduced compile-time parameters](/docs/design/generics/overview.md#deduced-parameters),
 the `self` parameter must be in the same list in square brackets `[`...`]`. The
 `self` parameter may appear in any position in that list, as long as it appears
 after any names needed to describe its type.
@@ -1595,7 +1595,7 @@ class MyDerivedClass {
 
 The properties of a type, whether type is abstract, base, or final, and whether
 the destructor is virtual or non-virtual, determines which
-[type-of-types](/docs/design/generics/terminology.md#facet-type) it satisfies.
+[facet types](/docs/design/generics/terminology.md#facet-type) it satisfies.
 
 -   Non-abstract classes are `Concrete`. This means you can create local and
     member variables of this type. `Concrete` types have destructors that are
@@ -1623,9 +1623,9 @@ conform to the decision on
 | final    | any         | yes        | yes         | yes            |
 
 The compiler automatically determines which of these
-[type-of-types](/docs/design/generics/terminology.md#facet-type) a given type
+[facet types](/docs/design/generics/terminology.md#facet-type) a given type
 satisfies. It is illegal to directly implement `Concrete`, `Deletable`, or
-`Destructible` directly. For more about these constraints, see
+`Destructible`. For more about these constraints, see
 ["destructor constraints" in the detailed generics design](/docs/design/generics/details.md#destructor-constraints).
 
 A pointer to `Deletable` types may be passed to the `Delete` method of the
@@ -1644,8 +1644,9 @@ interface Allocator {
 }
 ```
 
-To pass a pointer to a base class without a virtual destructor to a generic
-function expecting a `Deletable` type, use the `UnsafeAllowDelete`
+To pass a pointer to a base class without a virtual destructor to a
+checked-generic function expecting a `Deletable` type, use the
+`UnsafeAllowDelete`
 [type adapter](/docs/design/generics/details.md#adapting-types).
 
 ```
@@ -1670,7 +1671,7 @@ and not implemented in the current class.
 
 Types satisfy the
 [`TrivialDestructor`](/docs/design/generics/details.md#destructor-constraints)
-type-of-type if:
+facet type if:
 
 -   the class declaration does not define a destructor or the class defines the
     destructor with an empty body `{ }`,
@@ -1949,11 +1950,11 @@ We want four things so that Carbon's object-safe interfaces may interoperate
 with C++ abstract base classes without data members, matching the
 [interface as base class use case](#interface-as-base-class):
 
--   Ability to convert an object-safe interface (a type-of-type) into an
+-   Ability to convert an object-safe interface (a facet type) into an
     C++-compatible base class (a base type), maybe using
     `AsBaseClass(MyInterface)`.
 -   Ability to convert a C++ base class without data members (a base type) into
-    an object-safe interface (a type-of-type), maybe using `AsInterface(MyIBC)`.
+    an object-safe interface (a facet type), maybe using `AsInterface(MyIBC)`.
 -   Ability to convert a (thin) pointer to an abstract base class to a `DynPtr`
     of the corresponding interface.
 -   Ability to convert `DynPtr(MyInterface)` values to a proxy type that extends
@@ -2160,7 +2161,7 @@ implementations for [data classes](#data-classes) more generally. These
 implementations will typically subject to the criteria that all the data fields
 of the type must implement the interface. An example use case would be to say
 that a data class is serializable if all of its fields were. For this we will
-need a type-of-type for capturing that criteria, maybe something like
+need a facet type for capturing that criteria, maybe something like
 `DataFieldsImplement(MyInterface)`. The templated implementation will need some
 way of iterating through the fields so it can perform operations fieldwise. This
 feature should also implement the interfaces for any tuples whose fields satisfy
@@ -2239,7 +2240,7 @@ the type of `U.x`."
     -   [Allow functions to act as destructors](/proposals/p1154.md#allow-functions-to-act-as-destructors)
     -   [Allow private destructors](/proposals/p1154.md#allow-private-destructors)
     -   [Allow multiple conditional destructors](/proposals/p1154.md#allow-multiple-conditional-destructors)
-    -   [Type-of-type naming](/proposals/p1154.md#type-of-type-naming)
+    -   [Facet type naming](/proposals/p1154.md#type-of-type-naming)
     -   [Other approaches to extensible classes without vtables](/proposals/p1154.md#other-approaches-to-extensible-classes-without-vtables)
 
 -   [#2107: Clarify rules around `Self` and `.Self`](https://github.com/carbon-language/carbon-lang/pull/2107)

docs/design/expressions/arithmetic.md

@@ -193,7 +193,7 @@ following family of interfaces:
 ```
 // Unary `-`.
 interface Negate {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self]() -> Result;
 }
 ```
@@ -201,7 +201,7 @@ interface Negate {
 ```
 // Binary `+`.
 interface AddWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint Add {
@@ -212,7 +212,7 @@ constraint Add {
 ```
 // Binary `-`.
 interface SubWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint Sub {
@@ -223,7 +223,7 @@ constraint Sub {
 ```
 // Binary `*`.
 interface MulWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint Mul {
@@ -234,7 +234,7 @@ constraint Mul {
 ```
 // Binary `/`.
 interface DivWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint Div {
@@ -245,7 +245,7 @@ constraint Div {
 ```
 // Binary `%`.
 interface ModWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint Mod {

docs/design/expressions/bitwise.md

@@ -197,7 +197,7 @@ implementing the following family of interfaces:
 ```
 // Unary `^`.
 interface BitComplement {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self]() -> Result;
 }
 ```
@@ -205,7 +205,7 @@ interface BitComplement {
 ```
 // Binary `&`.
 interface BitAndWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint BitAnd {
@@ -216,7 +216,7 @@ constraint BitAnd {
 ```
 // Binary `|`.
 interface BitOrWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint BitOr {
@@ -227,7 +227,7 @@ constraint BitOr {
 ```
 // Binary `^`.
 interface BitXorWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint BitXor {
@@ -238,7 +238,7 @@ constraint BitXor {
 ```
 // Binary `<<`.
 interface LeftShiftWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint LeftShift {
@@ -249,7 +249,7 @@ constraint LeftShift {
 ```
 // Binary `>>`.
 interface RightShiftWith(U:! type) {
-  let Result:! type = Self;
+  default let Result:! type = Self;
   fn Op[self: Self](other: U) -> Result;
 }
 constraint RightShift {

docs/design/expressions/comparison_operators.md

@@ -241,8 +241,8 @@ User-defined types can extend the behavior of the comparison operators by
 implementing interfaces. In this section, various properties are specified that
 such implementations "should" satisfy. These properties are not enforced in
 general, but the standard library might detect violations of some of them in
-some circumstances. These properties may be assumed by generic code, resulting
-in unexpected behavior if they are violated.
+some circumstances. These properties may be assumed by checked-generic code,
+resulting in unexpected behavior if they are violated.
 
 #### Equality
 
@@ -460,7 +460,7 @@ than or equivalent to themselves.
 
 **TODO:** The standard library should provide a way to specify that an ordering
 is a weak, partial, or total ordering, and a way to request such an ordering in
-a generic.
+a checked generic.
 
 #### Compatibility of equality and ordering
 

docs/design/expressions/if.md

@@ -175,8 +175,8 @@ _Note:_ This rule is intended to be considered more specialized than the other
 rules in this document.
 
 Because this `impl` is declared `final`, `T.(CommonType(T)).Result` is always
-assumed to be `T`, even in contexts where `T` involves a generic parameter and
-so the result would normally be an unknown type whose type-of-type is `type`.
+assumed to be `T`, even in contexts where `T` involves a symbolic binding and so
+the result would normally be an unknown type whose facet type is `type`.
 
 ```
 fn F[T:! Hashable](c: bool, x: T, y: T) -> HashCode {

docs/design/expressions/indexing.md

@@ -51,7 +51,7 @@ pointer, and do not automatically chain with customized dereference interfaces.
 
 **Open question:** It's not clear that the lack of chaining is necessary, and it
 might be more expressive for the pointer type returned by the `Addr` methods to
-be an associated type with a default to allow types to produce custom
+be an associated facet with a default to allow types to produce custom
 pointer-like types on their indexing boundary and have them still be
 automatically dereferenced.
 

docs/design/functions.md

@@ -151,14 +151,14 @@ the `a` and `b` parameters of `Add`.
 Other designs build upon basic function syntax to add advanced features:
 
 -   [Generic functions](generics/overview.md#generic-functions) adds support for
-    deduced parameters and generic type parameters.
+    deduced parameters and compile-time parameters.
 -   [Class member functions](classes.md#member-functions) adds support for
     methods and class functions.
 
 ## Alternatives considered
 
 -   [Function keyword](/proposals/p0438.md#function-keyword)
--   [Only allow `auto` return types if parameters are generic](/proposals/p0826.md#only-allow-auto-return-types-if-parameters-are-generic)
+-   [Only allow `auto` return types if parameters are compile-time](/proposals/p0826.md#only-allow-auto-return-types-if-parameters-are-generic)
 -   [Provide alternate function syntax for concise return type inference](/proposals/p0826.md#provide-alternate-function-syntax-for-concise-return-type-inference)
 -   [Allow separate declaration and definition](/proposals/p0826.md#allow-separate-declaration-and-definition)
 

docs/design/generics/README.md

@@ -11,11 +11,14 @@ feature of Carbon:
 
 -   [Overview](overview.md) - A high-level description of the generics design,
     with pointers to other design documents that dive deeper into individual
-    topics.
+    topics
 -   [Goals](goals.md) - The motivation and principles guiding the design
-    direction.
+    direction
 -   [Terminology](terminology.md) - A glossary establishing common terminology
-    for describing the design.
--   [Detailed design](details.md) - In depth description of how generic type
-    parameters work.
--   ~~Rejected alternatives~~ - not implemented yet
+    for describing the design
+-   [Detailed design](details.md) - In-depth description
+    -   [Appendix: Witness tables](appendix-witness.md) - Describes an
+        implementation strategy for checked generics, and Carbon's rationale for
+        only using it for dynamic dispatch.
+    -   [Appendix: Coherence](appendix-coherence.md) - Describes the rationale
+        for Carbon's choice to have coherent generics, and the alternatives.

docs/design/generics/appendix-witness.md

@@ -213,8 +213,8 @@ class Vector {
 }
 ```
 
-The [impl of `Vector` for `Point_Inline`](details.md#inline-impl) would be a
-value of this type:
+The [`impl` definition of `Vector` for `Point_Inline`](details.md#inline-impl)
+would be a value of this type:
 
 ```
 var VectorForPoint_Inline: Vector  = {

docs/design/generics/goals.md

@@ -12,7 +12,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 
 -   [Purpose of this document](#purpose-of-this-document)
 -   [Background](#background)
-    -   [Generic parameters](#generic-parameters)
+    -   [Compile-time parameters](#compile-time-parameters)
     -   [Interfaces](#interfaces)
 -   [Templates](#templates)
 -   [Checked-generic goals](#checked-generic-goals)
@@ -66,34 +66,35 @@ the
 [compile-time duck typing](https://en.wikipedia.org/wiki/Duck_typing#Templates_or_generic_types)
 approach of C++ templates.
 
-### Generic parameters
+### Compile-time parameters
 
-Generic functions and generic types will all take some "generic parameters",
+Generic functions and generic types will all take some compile-time parameters,
 which will frequently be types, and in some cases will be
 [deduced](terminology.md#deduced-parameter) from the types of the values of
 explicit parameters.
 
-If a generic parameter is a type, the generic function's signature can specify
-constraints that the caller's type must satisfy. For example, a resizable array
-type (like C++'s `std::vector`) might have a generic type parameter with the
-constraint that the type must be movable and have a static size. A sort function
-might apply to any array whose elements are comparable and movable.
+If a compile-time parameter is a type, the generic function's signature can
+specify constraints that the caller's type must satisfy. For example, a
+resizable array type (like C++'s `std::vector`) might have a compile-time type
+parameter with the constraint that the type must be movable and have a static
+size. A sort function might apply to any array whose elements are comparable and
+movable.
 
-A constraint might involve multiple generic parameters. For example, a merge
-function might apply to two arbitrary containers so long as their elements have
-the same type.
+A constraint might involve multiple compile-time parameters. For example, a
+merge function might apply to two arbitrary containers so long as their elements
+have the same type.
 
 ### Interfaces
 
-We need some way to express the constraints on a generic type parameter. In
+We need some way to express the constraints on a compile-time type parameter. In
 Carbon we express these "type constraints" by saying we restrict to types that
 implement specific [_interfaces_](terminology.md#interface). Interfaces describe
 an API a type could implement; for example, it might specify a set of functions,
 including names and signatures. A type implementing an interface may be passed
-as a generic type argument to a function that has that interface as a
-requirement of its generic type parameter. Then, the functions defined in the
-interface may be called in the body of the function. Further, interfaces have
-names that allow them to be reused.
+as a compile-time type argument to a function that has that interface as a
+requirement of its compile-time type parameter. Then, the functions defined in
+the interface may be called in the body of the function. Further, interfaces
+have names that allow them to be reused.
 
 Similar compile-time and run-time constructs may be found in other programming
 languages:
@@ -350,10 +351,10 @@ Enable simple user control of whether to use dynamic or static dispatch.
 checked-generic functions:
 
 -   Static strategy: Like template parameters, the values for checked parameters
-    must be statically known at the callsite, or known to be a generic parameter
-    to the calling function. This can generate separate, specialized versions of
-    each combination of checked and template arguments, in order to optimize for
-    those types or values.
+    must be statically known at the callsite, or known to be a compile-time
+    parameter to the calling function. This can generate separate, specialized
+    versions of each combination of checked and template arguments, in order to
+    optimize for those types or values.
 -   Dynamic strategy: This is when the compiler generates a single version of
     the function that uses runtime dispatch to get something semantically
     equivalent to separate instantiation, but likely with different size, build
@@ -390,7 +391,7 @@ following features would benefit substantially from guaranteed monomorphization:
 -   Allocating local variables in stack storage. Without monomorphization, we
     would need to perform dynamic memory allocation -- whether on the stack or
     the heap -- for local variables whose sizes depend on checked parameters.
--   Passing parameters to functions. We cannot pass values of generic types in
+-   Passing parameters to functions. We cannot pass values of types in
     registers.
 -   Finding [specialized](terminology.md#specialization) implementations of
     interfaces beyond those clearly needed from the function signature.
@@ -625,10 +626,10 @@ Checked generics don't need to provide full flexibility of C++ templates:
 
 -   [Carbon templates](#templates) will cover those cases that don't fit inside
     checked generics, such as code that relies on compile-time duck typing.
--   We won't allow a specialization of some generic interface for some
-    particular type to actually expose a _different_ interface, with different
-    methods or different types in method signatures. This would break modular
-    type checking.
+-   We won't allow a specialization of some interface for some particular type
+    to actually expose a _different_ interface, with different methods or
+    different types in method signatures. This would break modular type
+    checking.
 -   [Template metaprogramming](https://en.wikipedia.org/wiki/Template_metaprogramming)
     will not be supported by Carbon checked generics. We expect to address those
     use cases with metaprogramming or [templates](#templates) in Carbon.

docs/design/generics/terminology.md

@@ -323,9 +323,6 @@ time.
 
 ## Facet type
 
-> **TODO:** Documents using the obsolete term "type-of-type" should be updated
-> to say "facet type" instead.
-
 A _facet type_ is a [type](#types-and-type) whose values are some subset of the
 values of `type`, determined by a set of [type constraints](#type-constraints):
 
@@ -573,7 +570,8 @@ permitted, always has the same meaning as an explicit cast.
 A generics or interface system has the _implementation coherence_ property, or
 simply _coherence_, if there is a single answer to the question "what is the
 implementation of this interface for this type, if any?" independent of context,
-such as the libraries imported into a given file.
+such as the libraries imported into a given file. Coherence is
+[a goal of Carbon checked generics](goals.md#coherence).
 
 This is enforced using two kinds of rules:
 
@@ -591,6 +589,9 @@ This is enforced using two kinds of rules:
     [overlap rule or overlap check](https://rust-lang.github.io/chalk/book/clauses/coherence.html#chalk-overlap-check)
     instead produces an error if two implementations apply at once.
 
+The rationale for Carbon choosing coherence and alternatives considered may be
+found in [this appendix](appendix-coherence.md)
+
 ## Adapting a type
 
 A type can be adapted by creating a new type that is

docs/design/lexical_conventions/symbolic_tokens.md

@@ -95,8 +95,8 @@ source file:
 | `{` and `}`     | Struct literals, blocks of control flow statements, and the bodies of definitions (classes, functions, etc.) |
 | `,`             | Separate tuple and struct elements                                                                           |
 | `.`             | Member access                                                                                                |
-| `:`             | Name bindings                                                                                                |
-| `:!`            | Generic binding                                                                                              |
+| `:`             | Name binding patterns                                                                                        |
+| `:!`            | Compile-time binding patterns                                                                                |
 | `;`             | Statement separator                                                                                          |
 
 ## Alternatives considered

docs/design/naming_conventions.md

@@ -41,7 +41,7 @@ In other words:
 | Types                     | `UpperCamelCase`   | Resolved at compile-time.                                                                  |
 | Functions                 | `UpperCamelCase`   | Resolved at compile-time.                                                                  |
 | Methods                   | `UpperCamelCase`   | Methods, including virtual methods, are equivalent to functions.                           |
-| Generic parameters        | `UpperCamelCase`   | May vary based on inputs, but are ultimately resolved at compile-time.                     |
+| Compile-time parameters   | `UpperCamelCase`   | May vary based on inputs, but are ultimately resolved at compile-time.                     |
 | Compile-time constants    | `UpperCamelCase`   | Resolved at compile-time. See [constants](#constants) for more remarks.                    |
 | Variables                 | `lower_snake_case` | May be reassigned and thus require runtime information.                                    |
 | Member variables          | `lower_snake_case` | Behave like variables.                                                                     |

docs/design/pattern_matching.md

@@ -14,11 +14,11 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 -   [Pattern Syntax and Semantics](#pattern-syntax-and-semantics)
     -   [Expression patterns](#expression-patterns)
         -   [Alternatives considered](#alternatives-considered)
-    -   [Bindings](#bindings)
-        -   [Name bindings](#name-bindings)
+    -   [Binding patterns](#binding-patterns)
+        -   [Name binding patterns](#name-binding-patterns)
         -   [Unused bindings](#unused-bindings)
             -   [Alternatives considered](#alternatives-considered-1)
-        -   [Generic bindings](#generic-bindings)
+        -   [Compile-time bindings](#compile-time-bindings)
         -   [`auto` and type deduction](#auto-and-type-deduction)
         -   [Alternatives considered](#alternatives-considered-2)
     -   [`var`](#var)
@@ -46,16 +46,17 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
 A _pattern_ is an expression-like syntax that describes the structure of some
 value. The pattern may contain unknowns, so it can potentially match multiple
 values, and those unknowns may have names, in which case they are called
-_bindings_. When a pattern is executed by giving it a value called the
+_binding patterns_. When a pattern is executed by giving it a value called the
 _scrutinee_, it determines whether the scrutinee matches the pattern, and if so,
 determines the values of the bindings.
 
 ## Pattern Syntax and Semantics
 
 Expressions are patterns, as described below. A pattern that is not an
-expression, because it contains pattern-specific syntax such as a binding, is a
-_proper pattern_. Many expression forms, such as arbitrary function calls, are
-not permitted as proper patterns, so cannot contain bindings.
+expression, because it contains pattern-specific syntax such as a binding
+pattern, is a _proper pattern_. Many expression forms, such as arbitrary
+function calls, are not permitted as proper patterns, so cannot contain binding
+patterns.
 
 -   _pattern_ ::= _proper-pattern_
 
@@ -93,7 +94,7 @@ reusing the result from an earlier comparison:
 
 ```carbon
 class ChattyIntMatcher {
-  external impl as EqWith(i32) {
+  impl as EqWith(i32) {
     fn Eq[me: ChattyIntMatcher](other: i32) {
       Print("Matching {0}", other);
       return other == 1;
@@ -116,24 +117,28 @@ fn F() {
 
 -   [Introducer syntax for expression patterns](/proposals/p2188.md#introducer-syntax-for-expression-patterns)
 
-### Bindings
+### Binding patterns
 
-#### Name bindings
+#### Name binding patterns
 
-A name binding is a pattern.
+A name binding pattern is a pattern.
 
 -   _binding-pattern_ ::= _identifier_ `:` _expression_
 -   _proper-pattern_ ::= _binding-pattern_
 
-The type of the _identifier_ is specified by the _expression_. The scrutinee is
-implicitly converted to that type if necessary.
+The _identifier_ specifies the name of the _binding_. The type of the binding is
+specified by the _expression_. The scrutinee is implicitly converted to that
+type if necessary. The binding is then _bound_ to the converted value.
 
 ```carbon
 fn F() -> i32 {
   match (5) {
     // ✅ `5` is implicitly converted to `i32`.
-    // Returns `5 as i32`.
-    case n: i32 => { return n; }
+    case n: i32 => {
+      // The binding `n` has the value `5 as i32`,
+      // which is the value returned.
+      return n;
+    }
   }
 }
 ```
@@ -144,7 +149,7 @@ value matches the scope of the binding.
 ```carbon
 class NoisyDestructor {
   fn Make() -> Self { return {}; }
-  external impl i32 as ImplicitAs(NoisyDestructor) {
+  impl i32 as ImplicitAs(NoisyDestructor) {
     fn Convert[me: i32]() -> Self { return Make(); }
   }
   destructor {
@@ -214,26 +219,26 @@ fn J(unused n: i32);
 -   [Anonymous, named identifiers](/proposals/p2022.md#anonymous-named-identifiers)
 -   [Attributes](/proposals/p2022.md#attributes)
 
-#### Generic bindings
+#### Compile-time bindings
 
 A `:!` can be used in place of `:` for a binding that is usable at compile time.
 
--   _generic-pattern_ ::= `unused`? `template`? _identifier_ `:!` _expression_
--   _generic-pattern_ ::= `template`? _identifier_ `:!` _expression_
--   _generic-pattern_ ::= `template`? `_` `:!` _expression_
--   _generic-pattern_ ::= `unused` `template`? _identifier_ `:!` _expression_
--   _proper-pattern_ ::= _generic-pattern_
+-   _compile-time-pattern_ ::= `template`? _identifier_ `:!` _expression_
+-   _compile-time-pattern_ ::= `template`? `_` `:!` _expression_
+-   _compile-time-pattern_ ::= `unused` `template`? _identifier_ `:!`
+    _expression_
+-   _proper-pattern_ ::= _compile-time-pattern_
 
 ```carbon
-// ✅ `F` takes a generic type parameter `T` and a parameter `x` of type `T`.
-fn F(T:! Type, x: T) {
+// ✅ `F` takes a symbolic facet parameter `T` and a parameter `x` of type `T`.
+fn F(T:! type, x: T) {
   var v: T = x;
 }
 ```
 
-The `template` keyword indicates the binding is introducing a template
-parameter, so name lookups into the parameter should be deferred until its value
-is known.
+The `template` keyword indicates the binding pattern is introducing a template
+binding, so name lookups into the binding will not be fully resolved until its
+value is known.
 
 #### `auto` and type deduction
 
@@ -256,7 +261,7 @@ The `auto` keyword is only permitted in specific contexts. Currently these are:
 -   As the type of a binding.
 
 It is anticipated that `auto` may be permitted in more contexts in the future,
-for example as a generic argument in a parameterized type that appears in a
+for example as a placeholder argument in a parameterized type that appears in a
 context where `auto` is allowed, such as `Vector(auto)` or `auto*`.
 
 When the type of a binding requires type deduction, the type is deduced against
@@ -265,7 +270,7 @@ before pattern matching is performed.
 
 ```carbon
 fn G[T:! Type](p: T*);
-class X { external impl as ImplicitAs(i32*); }
+class X { impl as ImplicitAs(i32*); }
 // ✅ Deduces `T = i32` then implicitly and
 // trivially converts `p` to `i32*`.
 fn H1(p: i32*) { G(p); }
@@ -288,8 +293,8 @@ scrutinee.
 -   _proper-pattern_ ::= `var` _proper-pattern_
 
 A `var` pattern matches when its nested pattern matches. The type of the storage
-is the resolved type of the nested _pattern_. Any bindings within the nested
-pattern refer to portions of the corresponding storage rather than to the
+is the resolved type of the nested _pattern_. Any binding patterns within the
+nested pattern refer to portions of the corresponding storage rather than to the
 scrutinee.
 
 ```carbon
@@ -441,7 +446,7 @@ match (Optional(i32).None) {
 }
 
 class X {
-  external impl as ImplicitAs(Optional(i32));
+  impl as ImplicitAs(Optional(i32));
 }
 
 match ({} as X) {

docs/design/sum_types.md

@@ -83,7 +83,7 @@ match (my_opt) {
 have limited flexibility. There is no way to control the representation of a
 `choice` type, or define methods or other members for it (although you can
 extend it to implement interfaces, using an
-[external `impl`](generics/overview.md#implementing-interfaces) or
+[out-of-line `impl`](generics/details.md#out-of-line-impl) or
 [adapter](generics/overview.md#adapting-types)). However, a `class` type can be
 extended to behave like a sum type. This is much more verbose than a `choice`
 declaration, but gives the author full control over the representation and class

docs/design/templates.md

@@ -101,11 +101,11 @@ specialization, but that is an area that we want to explore cautiously.
 
 Because we consider only specific _parameters_ to be templated and they could be
 individually migrated to a constrained interface using the
-[generics system](README.md#generics), constraining templates themselves may be
-less critical. Instead, we expect parameterized types and functions may use a
-mixture of generic parameters and templated parameters based on where they are
+[checked-generics system](README.md#generics), constraining templates themselves
+may be less critical. Instead, we expect parameterized types and functions may
+use a mixture of checked and template generic parameters based on where they are
 constrained.
 
 However, if there are still use cases, we would like to explore applying the
-interface constraints of the generics system directly to template parameters
-rather than create a new constraint system.
+interface constraints of the checked-generics system directly to template
+parameters rather than create a new constraint system.

docs/design/type_inference.md

@@ -43,7 +43,8 @@ constant `IntLiteral(1)` value, whereas most languages would suggest a variable
 integer type, such as `i64`. Carbon might also make it an error. Although type
 inference currently only addresses `auto` for variables and function return
 types, this is something that will be considered as part of type inference in
-general, because it also affects generics, templates, lambdas, and return types.
+general, because it also affects checked generics, templates, lambdas, and
+return types.
 
 ## Alternatives considered
 

docs/design/values.md

@@ -338,7 +338,7 @@ that fit into a machine register, but also the efficiency of minimal copies when
 working with types where a copy would require extra allocations or other costly
 resources. This directly helps programmers by providing a simpler model to
 select the mechanism of passing function inputs. But it is also important to
-enable generic code that needs a single type model that will have generically
+enable generic code that needs a single type model that will have consistently
 good performance.
 
 When forming a value expression from a reference expression, Carbon
@@ -591,7 +591,9 @@ storage.
 
 None of this impacts the type system and so an implementation can freely select
 specific strategies here based on concrete types without harming generic code.
-There is always a generic fallback as well if monomorphization isn't desired.
+Even if generics were to be implemented without monomorphization, for example
+dynamic dispatch of object-safe interfaces, there is a conservatively correct
+strategy that will work for any type.
 
 This freedom mirrors that of [input values](#value-expressions) where might be
 implemented as either a reference or a copy without breaking genericity. Here
@@ -1010,8 +1012,8 @@ placeholder `value_rep = T;`, we need to explore exactly what the best
 relationship is with the customization point. For example, should this syntax
 immediately forward declare `impl as ReferenceImplicitAs where .T = T`, thereby
 allowing an out-of-line definition of the `Convert` method and `... where _` to
-pick up the associated type from the syntax. Alternatively, the syntactic marker
-might be integrated into the `impl` declaration for `ReferenceImplicitAs`
+pick up the associated constant from the syntax. Alternatively, the syntactic
+marker might be integrated into the `impl` declaration for `ReferenceImplicitAs`
 itself.
 
 ## Alternatives considered

docs/project/faq.md

@@ -336,9 +336,9 @@ in scope.
 
 It's also worth noting that Carbon
 [doesn't use _any_ kind of brackets](https://github.com/carbon-language/carbon-lang/blob/trunk/docs/design/README.md#checked-and-template-parameters)
-to mark template or generic parameters, so if Carbon had angle brackets, they
-would mean something different than they do in C++, which could cause confusion.
-We do use square brackets to mark _deduced_ parameters, as in:
+to mark template- or checked-generic parameters, so if Carbon had angle
+brackets, they would mean something different than they do in C++, which could
+cause confusion. We do use square brackets to mark _deduced_ parameters, as in:
 
 ```
 fn Sort[T:! Comparable](a: Vector(T)*)
@@ -349,7 +349,7 @@ particular, deduced parameters are never mentioned at the callsite, so those
 square brackets are never part of the expression syntax.
 
 See [Proposal #676: `:!` generic syntax](/proposals/p0676.md) for more
-background on how and why we chose our current generics syntax.
+background on how and why we chose our current compile-time parameter syntax.
 
 ### Why do variable declarations have to start with `var` or `let`?
 
@@ -444,24 +444,24 @@ will handle both templates (matching C++) and checked generics (common in other
 languages: Rust, Swift, Go, Kotlin, Java, and so on).
 
 The key difference between the two is that template arguments can only finish
-type-checking _during_ instantiation, whereas generics specify an interface with
-which arguments can finish type-checking _without_ instantiation. This has a
-couple of important benefits:
-
--   Type-checking errors for generics happen earlier, making it easier for the
-    compiler to produce helpful diagnostics.
--   Generic functions can generate less compiled output, allowing compilation
-    with many uses to be faster.
+type-checking _during_ instantiation, whereas checked generics specify an
+interface with which arguments can finish type-checking _without_ instantiation.
+This has a couple of important benefits:
+
+-   Type-checking errors for checked generics happen earlier, making it easier
+    for the compiler to produce helpful diagnostics.
+-   Checked-generic functions can generate less compiled output, allowing
+    compilation with many uses to be faster.
     -   For comparison, template instantiations are a major factor for C++
         compilation latency.
 
-Although Carbon will prefer generics over templates, templates are provided for
-migration of C++ code.
+Although Carbon will prefer checked generics over templates, templates are
+provided for migration of C++ code.
 
 References:
 
 -   [Generics: Goals: Better compiler experience](/docs/design/generics/goals.md#better-compiler-experience)
--   [Generics: Terminology: Generic versus template parameters](/docs/design/generics/terminology.md#checked-versus-template-parameters)
+-   [Generics: Terminology: Checked versus template parameters](/docs/design/generics/terminology.md#checked-versus-template-parameters)
 
 ### What is Carbon's memory model?