From 7612b3d821c23a851b7b373dbe83a67f54564363 Mon Sep 17 00:00:00 2001
From: Chandler Carruth <chandlerc@gmail.com>
Date: Mon, 13 Jul 2026 12:22:35 -0700
Subject: [PATCH] Address post-merge review comments on #7254 and terminology
 discussions (#7490)

Document the phase of associated constants, which the discussions of
contextual phase defaults never covered: an associated constant is
always a checked generic binding. This is deliberately not presented as
a contextual default, because no other phase is possible for the
construct; correspondingly, no phase keyword (including `template`) is
allowed on one. Also rework the associated constants section of the
design README where the migration left a non-sequitur ("set to
compile-time values ... and so are defined using a `let` declaration"):
describe the `let` syntax and the binding's contextual phase separately.

Use consistent terminology for bindings versus constants. Bindings are
"checked" or "template" (generic) bindings, replacing the "symbolic
binding" and bare "generic binding" terms, so "symbolic" now only
describes constants and values. The "Symbolic facet bindings" section of
the generics details becomes "Checked facet bindings". The
expression-phase terms "symbolic constant" and "template constant" are
unchanged, and the binding-pattern definitions now name the constant
each kind binds. Template bindings are additionally described as
dependent and late checked, with each instantiation providing the
binding's value.

Also normalize the remaining "regular parameter" mentions to "runtime
parameter" to match the binding terminology, and describe the
compile-time "let template" as introducing a template generic binding
"T: C" whose uses are template constants.

Assisted-by: Claude Code
---
 docs/design/README.md                         | 30 ++++++-----
 docs/design/expressions/if.md                 |  2 +-
 docs/design/expressions/member_access.md      |  8 +--
 .../generics/appendix-rewrite-constraints.md  |  2 +-
 docs/design/generics/details.md               | 54 +++++++++----------
 docs/design/generics/overview.md              | 12 ++---
 docs/design/generics/terminology.md           | 35 +++++++-----
 docs/design/pattern_matching.md               | 20 ++++---
 docs/design/variadics.md                      |  2 +-
 9 files changed, 93 insertions(+), 72 deletions(-)

diff --git a/docs/design/README.md b/docs/design/README.md
index 498c05757b84..54adabc84f65 100644
--- a/docs/design/README.md
+++ b/docs/design/README.md
@@ -739,7 +739,7 @@ Value expressions are further broken down into three _expression phases_:
     [monomorphization](https://en.wikipedia.org/wiki/Monomorphization) happens,
     but is not known during type checking. This includes
     [checked-generic parameters](#checked-and-template-parameters), and type
-    expressions with checked-generic arguments, like `Optional(T*)`.
+    expressions with symbolic constant arguments, like `Optional(T*)`.
 -   A _runtime value_ has a dynamic value only known at runtime.
 
 Template constants and symbolic constants are collectively called _compile-time
@@ -1059,19 +1059,23 @@ Every binding pattern has a _phase_ (either compile-time or runtime). A
 [compile-time constants](#expression-phases), not run-time values.
 
 To minimize keyword noise, Carbon uses contextual defaults to determine the
-phase (compile-time vs runtime) of a binding in parameter lists:
+phase (compile-time vs runtime) of a binding:
 
 -   Parameters to compile-time entities (such as `interface`, `impl`, and
     `class`) are checked generics by default.
 -   Deduced function parameters (declared in `[]`) are checked generics by
     default.
--   Explicit function parameters and local bindings (declared in `()`) are
+-   Explicit function parameters (declared in `()`) and local bindings are
     runtime by default.
 
 These defaults can be overridden by using the `template`, `generic`, or
 `runtime` keywords. However, using a keyword that matches the contextual default
 is disallowed to maintain consistency. A `template` keyword before the binding
-selects a template binding instead of a symbolic binding.
+selects a template binding instead of a checked binding.
+
+[Associated constants](#associated-constants) are always checked generic
+bindings. This is not a contextual default: no other phase is possible for an
+associated constant, and so no phase keyword is allowed there.
 
 Binding patterns default to _`let` bindings_. The `var` keyword is used to make
 it a _`var` binding_.
@@ -2806,7 +2810,7 @@ The [expression phase](#expression-phases) of a checked parameter is a symbolic
 constant whereas the expression phase of a template parameter is template
 constant. A binding pattern for a compile-time parameter is a _compile-time
 binding pattern_; more specifically a _template binding pattern_ if it uses
-`template`, and a _symbolic binding pattern_ if it uses `generic` or defaults to
+`template`, and a _checked binding pattern_ if it uses `generic` or defaults to
 it.
 
 Although checked generics are generally preferred, templates enable translation
@@ -3028,13 +3032,15 @@ to a checked parameter.
 
 An associated constant is a member of an interface whose value is determined by
 the implementation of that interface for a specific type. These values are set
-to compile-time values in implementations, and so are defined using a
-[`let` declaration](#constant-let-declarations) without an initializer, which
-defines an associated constant in this context. This allows types in the
-signatures of functions in the interface to vary. For example, an interface
-describing a [stack](<https://en.wikipedia.org/wiki/Stack_(abstract_data_type)>)
-might use an associated constant to represent the type of elements stored in the
-stack.
+to compile-time values in implementations, which allows types in the signatures
+of functions in the interface to vary. An associated constant is defined using a
+[`let` declaration](#constant-let-declarations) without an initializer. Since an
+interface is a compile-time entity, the binding is a
+[checked generic binding](#checked-and-template-parameters) by context; no phase
+keyword is allowed, so an associated constant cannot be made `template`. For
+example, an interface describing a
+[stack](<https://en.wikipedia.org/wiki/Stack_(abstract_data_type)>) might use an
+associated constant to represent the type of elements stored in the stack.
 
 ```
 interface StackInterface {
diff --git a/docs/design/expressions/if.md b/docs/design/expressions/if.md
index c51043bb176a..5e117b3d7892 100644
--- a/docs/design/expressions/if.md
+++ b/docs/design/expressions/if.md
@@ -175,7 +175,7 @@ _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 symbolic binding and so
+assumed to be `T`, even in contexts where `T` involves a checked binding and so
 the result would normally be an unknown type whose facet type is `type`.
 
 ```
diff --git a/docs/design/expressions/member_access.md b/docs/design/expressions/member_access.md
index 3f7bc622e98b..1efb7d17fac4 100644
--- a/docs/design/expressions/member_access.md
+++ b/docs/design/expressions/member_access.md
@@ -468,7 +468,7 @@ fn CallsDrawChecked(c: Cowboy) {
 
 If the value or type depends on any template bindings, the lookup is redone from
 a context where the values of those bindings are known, but where the values of
-any symbolic bindings are still unknown. The lookup results from these two
+any checked bindings are still unknown. The lookup results from these two
 contexts are [combined](#lookup-ambiguity).
 
 ```carbon
@@ -525,9 +525,9 @@ fn CallH(a: DerivingWrapper(HasField),
 }
 ```
 
-**Note:** All lookups are done from a context where the values of any symbolic
+**Note:** All lookups are done from a context where the values of any checked
 bindings that are in scope are unknown. Unlike for a template binding, the
-actual value of a symbolic binding never affects the result of member
+actual value of a checked binding never affects the result of member
 resolution.
 
 #### Lookup ambiguity
@@ -628,7 +628,7 @@ For a simple member access `a.b` where `b` names a member of an interface `I`:
 -   Otherwise, `impl` lookup is not performed.
 
 The appropriate `impl T as I` implementation is located. The program is invalid
-if no such `impl` exists. When `T` or `I` depends on a symbolic binding, a
+if no such `impl` exists. When `T` or `I` depends on a checked binding, a
 suitable constraint must be specified to ensure that such an `impl` will exist.
 When `T` or `I` depends on a template binding, this check is deferred until the
 value for the template binding is known.
diff --git a/docs/design/generics/appendix-rewrite-constraints.md b/docs/design/generics/appendix-rewrite-constraints.md
index 2ff05d3a2f8b..27c8d2dfb1f6 100644
--- a/docs/design/generics/appendix-rewrite-constraints.md
+++ b/docs/design/generics/appendix-rewrite-constraints.md
@@ -197,7 +197,7 @@ When a facet type is used as the declared type of a facet `T`, the constraints
 that were specified within that facet type are _resolved_ to determine the
 constraints that apply to `T`. This happens:
 
--   When the constraint is used explicitly when declaring a symbolic binding,
+-   When the constraint is used explicitly when declaring a checked binding,
     like a generic parameter or associated constant, of the form
     `T: Constraint`.
 -   When declaring that a type implements a constraint with an `impl`
diff --git a/docs/design/generics/details.md b/docs/design/generics/details.md
index 6f20d8fc80d7..c2e76dbfcbb5 100644
--- a/docs/design/generics/details.md
+++ b/docs/design/generics/details.md
@@ -23,7 +23,7 @@ SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
     -   [Qualified member names and compound member access](#qualified-member-names-and-compound-member-access)
     -   [Access](#access)
 -   [Checked-generic functions](#checked-generic-functions)
-    -   [Symbolic facet bindings](#symbolic-facet-bindings)
+    -   [Checked facet bindings](#checked-facet-bindings)
     -   [Return type](#return-type)
 -   [Interfaces recap](#interfaces-recap)
 -   [Facet types](#facet-types)
@@ -685,13 +685,13 @@ fn AddAndScaleGeneric[T: Vector](a: T, b: T, s: f64) -> T {
 var v: Point_Extend = AddAndScaleGeneric(a, w, 2.5);
 ```
 
-Here `T` is a facet whose type is `Vector`. It declares a _symbolic binding_
+Here `T` is a facet whose type is `Vector`. It declares a _checked binding_
 since it did not use the `template` keyword to mark it as a _template binding_.
 
 > **References:** The syntax for compile-time bindings was decided in
 > [proposal #7254](https://github.com/carbon-language/carbon-lang/pull/7254).
 
-Since this symbolic binding pattern is in a function declaration, it marks a
+Since this checked binding pattern is in a function declaration, it marks a
 _[checked](terminology.md#checked-versus-template-parameters)
 [generic parameter](terminology.md#generic-means-compile-time-parameterized)_.
 That means its value must be known to the caller at compile-time, but we will
@@ -701,11 +701,11 @@ the body of `AddAndScaleGeneric`'s definition.
 Note that types may also be given compile-time parameters, see the
 ["parameterized types" section](#parameterized-types).
 
-### Symbolic facet bindings
+### Checked facet bindings
 
 In our example, `T` is a facet which may be used in type position in the rest of
 the function. Furthermore, since it omits the keyword `template` prefix, this is
-a symbolic binding. so we need to be able to typecheck the body of the function
+a checked binding, so we need to be able to typecheck the body of the function
 without knowing the specific value `T` from the caller.
 
 This typechecking is done by looking at the constraint on `T`. In the example,
@@ -863,7 +863,7 @@ An interface's name may be used in a few different contexts:
 -   as a namespace name in
     [a qualified name](#qualified-member-names-and-compound-member-access), and
 -   as a [facet type](terminology.md#facet-type) for
-    [a facet binding](#symbolic-facet-bindings).
+    [a facet binding](#checked-facet-bindings).
 
 While interfaces are examples of facet types, facet types are a more general
 concept, for which interfaces are a building block.
@@ -893,8 +893,8 @@ This recovers the original type for the facet, so
 `(Point_Inline as Vector) as type` is `Point_Inline` again.
 
 However, when a facet type like `Vector` is used as the binding type of a
-symbolic binding, the
-[symbolic facet binding](#symbolic-facet-bindings) `T` is disassociated with
+checked binding, the
+[checked facet binding](#checked-facet-bindings) `T` is disassociated with
 whatever facet value `T` is eventually bound to. Instead, `T` is treated as an
 [archetype](terminology.md#archetype), with the members and
 [member access](/docs/design/expressions/member_access.md) determined by the
@@ -1022,7 +1022,7 @@ whenever an interface may be. This includes all of these
     [a qualified name](#qualified-member-names-and-compound-member-access). For
     example, `VectorLegoFish.VAdd` refers to the same name as `Vector.Add`.
 -   A named constraint may be used as a [facet type](terminology.md#facet-type)
-    for [a facet binding](#symbolic-facet-bindings).
+    for [a facet binding](#checked-facet-bindings).
 
 We don't expect developers to directly define many named constraints, but other
 constructs we do expect them to use will be defined in terms of them. For
@@ -1115,7 +1115,7 @@ class ImplementsS {
 There is a subtyping relationship between facet types that allows calls of one
 generic function from another as long as it has a subset of the requirements.
 
-Given a symbolic facet binding `T` with facet type `I1`, it satisfies a facet
+Given a checked facet binding `T` with facet type `I1`, it satisfies a facet
 type `I2` as long as the requirements of `I1` are a superset of the requirements
 of `I2`. This means a value `x: T` may be passed to functions requiring types to
 satisfy `I2`, as in this example:
@@ -1844,7 +1844,7 @@ var thriller_count: Optional(i32) =
     play_count.Find(Song("Thriller"));
 ```
 
-Since the `KeyT` and `ValueT` are symbolic parameters, the `Find` function is a
+Since the `KeyT` and `ValueT` are checked parameters, the `Find` function is a
 checked generic, and it can only use the capabilities of `KeyT` and `ValueT`
 specified as requirements. This allows us to evaluate when we can convert
 between two different arguments to a parameterized type. Consider two adapters
@@ -2383,7 +2383,7 @@ fn PeekAtTopOfStack[StackType: StackAssociatedFacet](s: StackType*)
 Inside the checked-generic function `PeekAtTopOfStack`, the `ElementType`
 associated facet member of `StackType` is an
 [archetype](terminology.md#archetype), like other
-[symbolic facet bindings](#symbolic-facet-bindings). This means
+[checked facet bindings](#checked-facet-bindings). This means
 `StackType.ElementType` has the API dictated by the declaration of `ElementType`
 in the interface `StackAssociatedFacet`.
 
@@ -2557,8 +2557,8 @@ class Complex {
 All interface parameters are checked by default. This reflects these two
 properties of these parameters:
 
--   They must be resolved at compile-time, and so can't be passed regular
-    dynamic values.
+-   They must be resolved at compile-time, and so can't be passed runtime
+    values.
 -   We allow either symbolic or template values to be passed in.
 
 **Future work:** We might also allow `template` bindings for interface
@@ -2628,7 +2628,7 @@ support parameters. Those parameters work the same way as for interfaces.
 
 ## Where constraints
 
-So far, we have restricted a [symbolic facet binding](#symbolic-facet-bindings)
+So far, we have restricted a [checked facet binding](#checked-facet-bindings)
 by saying it has to implement an interface or a set of interfaces. There are a
 variety of other constraints we would like to be able to express, such as
 applying restrictions to associated constants. This is done using the `where`
@@ -2858,7 +2858,7 @@ constraint ContainerIsSlice {
 
 The `.Self` construct follows these rules:
 
--   A generic binding `X` introduces a checked generic binding `.Self: type`, where
+-   A checked binding `X` introduces a checked generic binding `.Self: type`, where
 
     references to `.Self` are resolved to `X`. This allows you to use `.Self` as
     an interface parameter as in `X: I(.Self)`.
@@ -2874,7 +2874,7 @@ The `.Self` construct follows these rules:
     to the same facet binding.
 -   `.Self` may not be on the left side of the `=` in a rewrite constraint.
 
-So in `X: A where ...` (where `X` is a generic binding), `.Self` is
+So in `X: A where ...` (where `X` is a checked binding), `.Self` is
 
 introduced twice, after the `:` and the `where`. This is allowed since both
 times it means `X`. After the `:`, `.Self` has the type `type`, which gets
@@ -3387,7 +3387,7 @@ there is a `where` clause modifying it.
 An implements constraint can be applied to [`.Self`](#recursive-constraints), as
 in `I where .Self impls C`. This has the same requirements as `I & C`, but that
 `where` clause does not affect the API. This means that a
-[symbolic facet binding](#symbolic-facet-bindings) with that facet type, so `T`
+[checked facet binding](#checked-facet-bindings) with that facet type, so `T`
 in `T: I where .Self impls C`, is represented by an
 [archetype](terminology.md#archetype) that implements both `I` and `C`, but only
 [extends](terminology.md#extending-an-impl) `I`.
@@ -3433,7 +3433,7 @@ fn PrintValueOrDefault[
 ```
 
 In this case, Carbon will accept the definition and infer the needed constraints
-on the symbolic facet parameter. This is both more concise for the author of the
+on the checked facet parameter. This is both more concise for the author of the
 code and follows the
 ["don't repeat yourself" principle](https://en.wikipedia.org/wiki/Don%27t_repeat_yourself).
 This redundancy is undesirable since it means if the needed constraints for
@@ -3445,7 +3445,7 @@ will have already satisfied these constraints.
 This implied constraint is equivalent to the explicit constraint that each
 parameter and return type [is legal](#must-be-legal-type-argument-constraints).
 
-> **Note:** These implied constraints affect the _requirements_ of a symbolic
+> **Note:** These implied constraints affect the _requirements_ of a checked
 > facet parameter, but not its _member names_. This way you can always look at
 > the declaration to see how name resolution works, without having to look up
 > the definitions of everything it is used as an argument to.
@@ -3758,7 +3758,7 @@ interface Graph {
 #### Parameterized type implements interface
 
 There are times when a function will pass a
-[symbolic facet parameter](#symbolic-facet-bindings) of the function as an
+[checked facet parameter](#checked-facet-bindings) of the function as an
 argument to a [parameterized type](#parameterized-types), and the function needs
 the result to implement a specific interface.
 
@@ -3796,7 +3796,7 @@ PrintThree(i, i, i);
 #### Another type implements parameterized interface
 
 In this case, we need some other type to implement an interface parameterized by
-a [symbolic facet parameter](#symbolic-facet-bindings). The syntax for this case
+a [checked facet parameter](#checked-facet-bindings). The syntax for this case
 follows the previous case, except now the `.Self` parameter is on the interface
 to the right of the `impls`. For example, we might need a type parameter `T` to
 support explicit conversion from an `i32`:
@@ -3813,7 +3813,7 @@ fn Double[T: Mul where i32 impls As(.Self)](x: T) -> T {
 
 #### Must be legal type argument constraints
 
-Now consider the case that the symbolic facet parameter is going to be used as
+Now consider the case that the checked facet parameter is going to be used as
 an argument to a [parameterized type](#parameterized-types) in a function body,
 but not in the signature. If the parameterized type was explicitly mentioned in
 the signature, the [implied constraint](#implied-constraints) feature would
@@ -4229,8 +4229,8 @@ extend `C`, as an alternative to
 [using an adapter](#use-case-accessing-interface-names), or to simplify inlining
 of a generic function while preserving semantics.
 
-To get a template binding instead of symbolic binding, add the `template`
-keyword before the binding pattern, as in:
+To get a template generic binding instead of a checked generic binding, use
+`let template`, as in:
 
 ```carbon
 fn TemplateLet(...) {
@@ -4242,8 +4242,8 @@ fn TemplateLet(...) {
 }
 ```
 
-which introduces a template constant `T` with type `C` and value `U`. This is
-roughly equivalent to:
+which introduces a template generic binding `T: C`, bound to the value `U`.
+Uses of `T` are then template constants. This is roughly equivalent to:
 
 ```carbon
 fn TemplateLet(...) {
diff --git a/docs/design/generics/overview.md b/docs/design/generics/overview.md
index 5716bb97292e..b62ca3f7ab1e 100644
--- a/docs/design/generics/overview.md
+++ b/docs/design/generics/overview.md
@@ -107,7 +107,7 @@ Summary of how Carbon generics work:
 -   _Deduced parameters_ are parameters whose values are determined by the types
     of the explicit arguments. Generic facet parameters are typically deduced.
 -   A function with a generic parameter can have the same function body as an
-    unparameterized one. Functions can freely mix checked, template, and regular
+    unparameterized one. Functions can freely mix checked, template, and runtime
     parameters.
 -   Interfaces can require other interfaces be implemented.
 -   Interfaces can [extend](terminology.md#extending-an-interface) required
@@ -368,11 +368,11 @@ You may also refer to any of the methods of interfaces required by the facet
 type using a
 [qualified member access expression](#accessing-members-of-interfaces).
 
-A function can have a mix of checked, template, and regular parameters. Each
-kind of parameter is defined using a different syntax: a checked parameter is
-uses a symbolic binding pattern, a template parameter uses a template binding
-pattern, and a regular parameter uses a runtime binding pattern. Likewise, it's
-allowed to pass a symbolic or template constant value to a checked or regular
+A function can have a mix of checked, template, and runtime parameters. Each
+kind of parameter is defined using a different syntax: a checked parameter uses
+a checked binding pattern, a template parameter uses a template binding
+pattern, and a runtime parameter uses a runtime binding pattern. Likewise, it's
+allowed to pass a symbolic or template constant value to a checked or runtime
 parameter. _We have decided to support passing a symbolic constant to a template
 parameter, see
 [leads issue #2153: Checked generics calling templates](https://github.com/carbon-language/carbon-lang/issues/2153),
diff --git a/docs/design/generics/terminology.md b/docs/design/generics/terminology.md
index 0325b5ea06aa..d1f66cbd11b0 100644
--- a/docs/design/generics/terminology.md
+++ b/docs/design/generics/terminology.md
@@ -99,6 +99,11 @@ checked generic, and template generic parameters.
 
 Keywords matching the contextual default are disallowed to ensure consistency.
 
+[Associated constants](#interface-parameters-and-associated-constants) are
+always checked generic bindings. This is not a contextual default: no other
+phase is possible for an associated constant, and so no phase keyword is allowed
+there.
+
 The syntax for checked and template parameters was decided in
 [leads issue #6932](https://github.com/carbon-language/carbon-lang/issues/6932).
 
@@ -278,7 +283,7 @@ that don’t instantiate the implementation (for example,
 
 Early type checking is where expressions and statements are type checked when
 the definition of the function body is compiled, as part of definition checking.
-This occurs for regular and checked-generic values.
+This occurs for runtime values and symbolic constants.
 
 Late type checking is where expressions and statements may only be fully
 typechecked once calling information is known. Late type checking delays
@@ -296,22 +301,28 @@ corresponding to
 
 -   A _runtime binding pattern_ binds to a dynamic value at runtime. It is the
     default for explicit function parameters.
--   A _symbolic binding pattern_ (or generic binding) binds to a compile-time
-    value that is not known when type checking. It is the default for deduced
-    function parameters and parameters to compile-time entities.
--   A _template binding pattern_ binds to a compile-time value that is known
-    when type checking. It is indicated by the `template` keyword.
+-   A _checked generic binding pattern_ binds to a _symbolic constant_: a
+    compile-time value that is not known when type checking. It is the default
+    for deduced function parameters and parameters to compile-time entities, and
+    the only kind allowed for [associated constants](#associated-entity).
+-   A _template generic binding pattern_ binds to a _template constant_: a
+    compile-time value that is known when type checking. It is indicated by the
+    `template` keyword. Expressions using such a binding are
+    [dependent](#dependent-names) and are
+    [late type checked](#early-versus-late-type-checking) once an instantiation
+    provides the binding's value.
 
 These patterns use the keywords `runtime`, `generic`, and `template` to override
 the contextual defaults when necessary.
 
 The name being declared, which is the identifier to the left of the `:` is
 called a _binding_, or more specifically a _runtime binding_, _compile-time
-binding_, _symbolic binding_, or _template binding_. The expression to the right
-defining the type of the binding pattern is called the _binding type
-expression_, a kind of [type expression](#type-expression). For example, in a
-generic binding pattern `T: Hashable`, `T` is the binding (a symbolic binding in
-this case), and `Hashable` is the binding type expression.
+binding_, _checked generic binding_, or _template generic binding_. The
+expression to the right defining the type of the binding pattern is called the
+_binding type expression_, a kind of [type expression](#type-expression). For
+example, in a checked generic binding pattern `T: Hashable`, `T` is the binding
+(a checked generic binding in this case), and `Hashable` is the binding type
+expression.
 
 ## Types and `type`
 
@@ -367,7 +378,7 @@ cases, we are concerned with the type value after the implicit conversion.
 We use the term _facet binding_ to refer to the name introduced by a
 [compile-time binding pattern](#bindings) (indicated by context or keywords like
 `generic` or `template`) where the declared type is a [facet type](#facet-type).
-In a generic binding pattern `T: Hashable`, `T` is a facet binding, and the
+In a checked binding pattern `T: Hashable`, `T` is a facet binding, and the
 value of `T` is a [facet](#facet).
 
 ## Deduced parameter
diff --git a/docs/design/pattern_matching.md b/docs/design/pattern_matching.md
index 8181ac8bfe1f..c5a49c1002d7 100644
--- a/docs/design/pattern_matching.md
+++ b/docs/design/pattern_matching.md
@@ -156,19 +156,23 @@ or template compile-time:
 
 -   A _runtime binding pattern_ binds to a dynamic value at runtime. It is the
     default for explicit function parameters and local bindings.
--   A _symbolic binding pattern_ (or generic binding pattern) binds to a
+-   A _checked generic binding pattern_ binds to a symbolic constant: a
     compile-time value that is not known when type checking. It is the default
     for deduced function parameters and parameters to compile-time entities.
-    Explicit function parameters are only symbolic binding patterns if they are
-    declared using the `generic` keyword.
--   A _template binding pattern_ binds to a compile-time value that is known
-    when type checking. It is declared using the `template` keyword.
+    Explicit function parameters are only checked generic binding patterns if
+    they are declared using the `generic` keyword.
+    [Associated constants](generics/details.md#associated-constants) are always
+    checked generic binding patterns, and do not allow a phase keyword.
+-   A _template generic binding pattern_ binds to a template constant: a
+    compile-time value that is known when type checking. It is declared using
+    the `template` keyword. Expressions using such a binding are dependent and
+    are late type checked once the binding's value is known.
 
 > **Future work:** If Carbon supports deduced runtime parameters in the future,
 > the `runtime` keyword will be used to explicitly declare those runtime binding
 > patterns.
 
-A symbolic or template binding pattern is collectively called a _compile-time
+A checked or template binding pattern is collectively called a _compile-time
 binding pattern_. A compile-time binding pattern cannot appear inside a `var`
 pattern.
 
@@ -181,13 +185,13 @@ components:
     entire reference" if it's a variable binding pattern, or "durable non-entire
     reference" if it's a non-variable reference binding pattern.
 -   The phase is "runtime", "symbolic", or "template" depending on whether the
-    pattern is a runtime, symbolic, or template binding pattern.
+    pattern is a runtime, checked, or template binding pattern.
 
 During pattern matching, the scrutinee is implicitly converted as needed to have
 the same extended type, and the binding is _bound_ to (and consumes) the result
 of these conversions. This makes a runtime or template binding a kind of
 reusable alias for the converted scrutinee expression, with the same extended
-type and value. Symbolic bindings are more complex: the binding will have the
+type and value. Checked bindings are more complex: the binding will have the
 same type, category, and phase as the converted scrutinee expression, but its
 constant value is an opaque symbol introduced by the binding, which the type
 system knows to be equal to the converted scrutinee expression.
diff --git a/docs/design/variadics.md b/docs/design/variadics.md
index 25cf9abe8077..620522780772 100644
--- a/docs/design/variadics.md
+++ b/docs/design/variadics.md
@@ -784,7 +784,7 @@ segment, and let `Ys` be a sequence of tuple segments.
 ### Equivalence, equality, and convertibility
 
 _Pack renaming:_ Let `Ns` be a sequence of names, let `⟬Ns⟭: «T; N»` be a name
-binding pattern (which may be a symbolic or template binding as well as a
+binding pattern (which may be a checked or template binding as well as a
 runtime binding), and let `__A` be an identifier that does not collide with any
 name that's visible where `⟬Ns⟭` is visible. We can rewrite all occurrences of
 `⟬Ns⟭` to `each __A` in the scope of the binding pattern (including the pattern