diff --git a/README.md b/README.md
index 459a0ec..5112ff0 100644
--- a/README.md
+++ b/README.md
@@ -98,11 +98,13 @@ main proc() i16 {
 
 the specialization checkpoint supports type arguments and constant integer, boolean, string, callback and null value arguments; declared value-parameter types survive specialization, including narrow checked arithmetic and optional captures/unwrap. integer arguments are range-checked even when unused, and erased argument expressions still receive ordinary checking. immutable constant expressions may use unary signs, `!`, `+`, `-`, `*`, comparisons and logical operators. type-producing procedures accept ordinary parameters as well as `$` parameters: every argument must be supplied explicitly and evaluate to a constant, and every input participates in specialization caching. for example, `Fixed proc(T type, count usize) type { return struct { values [count]T } }` accepts `Fixed(i16, 2)` and reuses its nominal type for equivalent inputs. use `$` when a parameter must be visible in subsequent signature annotations. runaway specialization is diagnosed at 128 nested evaluation/specialization calls or 4096 instances.
 
-type-producing bodies support mutable type and value locals, direct binding assignment, scoped blocks, conditional/early returns, integer range and while loops, break/continue and nested/recursive type-producing calls. for example, start with `Result := T`, repeat `Result = [2]Result` in a loop, then `return Result` to generate nested array storage. snapshots retain each local's current value without changing the source AST; scalar operations reuse checking, typed IR and interpreter execution, preserving exact types and overflow diagnostics. type-control execution is limited to 4096 statement/loop-guard steps shared with nested producers; individual scalar evaluations retain the interpreter limits below. only executed bodies are elaborated, while every body is still parsed and name-resolved. cleanup and type-valued aggregate storage in type-producing bodies remain outside this checkpoint.
+type-producing bodies support mutable type and value locals, direct binding assignment, scoped blocks, conditional/early returns, integer range and while loops, break/continue and nested/recursive type-producing calls. for example, start with `Result := T`, repeat `Result = [2]Result` in a loop, then `return Result` to generate nested array storage. snapshots retain each local's current value without changing the source AST; scalar operations reuse checking, typed IR and interpreter execution, preserving exact types and overflow diagnostics. type-control execution is limited to 4096 statement/loop-guard steps shared with nested producers; individual scalar evaluations retain the interpreter limits below. only executed bodies are elaborated, while every body is still parsed and name-resolved. cleanup and type-valued record storage in type-producing bodies remain outside this checkpoint.
 
-field/index assignments also update initialized, materializable aggregate locals in type-producing bodies, including nested record fields and mutable fixed-array elements. for example, `counts [2]mut usize := [0, 0]` followed by `counts[1] = 2` can generate `[counts[1]]i16` storage. each update uses ordinary checked IR and returns a new owned constant: earlier copies remain unchanged, while later loop iterations, generated lengths and defaults observe the update. ordinary mutability, index-type/bounds, field and exact value-type checks still apply, including immutable payload captures and narrow arithmetic overflow. imported producers and repeated compilation retain source diagnostics and nominal cache identity; pointer/slice-backed mutation and type-valued aggregate storage remain open.
+field/index assignments also update initialized, materializable aggregate locals in type-producing bodies, including nested record fields and mutable fixed-array elements. for example, `counts [2]mut usize := [0, 0]` followed by `counts[1] = 2` can generate `[counts[1]]i16` storage. each update uses ordinary checked IR and returns a new owned constant: earlier copies remain unchanged, while later loop iterations, generated lengths and defaults observe the update. ordinary mutability, index-type/bounds, field and exact value-type checks still apply, including immutable payload captures and narrow arithmetic overflow. imported producers and repeated compilation retain source diagnostics and nominal cache identity; pointer/slice-backed mutation and type-valued record storage remain open.
 
-type-producing bodies also iterate materializable fixed arrays and strings with immutable by-value element captures and optional `usize` indices: `for counts |count, index| { length = length + count + index }` can compute generated storage. nested loops, aggregate captures, empty collections, break/continue and early returns share the type-control execution bound. array places retain their entry-time indices and observe later element updates; temporary arrays and strings are evaluated once. ordinary constant-input procedures additionally support slice and pointer captures through checked IR, provided only materializable results escape. type-producing loop bodies still reject storage-bearing captures rather than retaining temporary interpreter addresses; type-valued elements and `inline for` remain open.
+type-producing bodies also iterate materializable fixed arrays and strings with immutable by-value element captures and optional `usize` indices: `for counts |count, index| { length = length + count + index }` can compute generated storage. nested loops, aggregate captures, empty collections, break/continue and early returns share the type-control execution bound. array places retain their entry-time indices and observe later element updates; temporary arrays and strings are evaluated once. ordinary constant-input procedures additionally support slice and pointer captures through checked IR, provided only materializable results escape. type-producing loop bodies still reject storage-bearing captures rather than retaining temporary interpreter addresses; `inline for` remains open.
+
+initialized fixed arrays of `type` also live entirely inside type-producing execution, including nested arrays, explicit/inferred annotations, `.len`, checked `usize` indexing and collection captures. for example, `types [2]mut type := [i8, bool]`, then `types[1] = i16` and `return [types.len]types[1]`, generates `[2]i16` without runtime type metadata. whole-array and nested indexed assignments preserve shape and mutability at every level; copies and loop captures retain earlier values while borrowed array places observe later updates. selected types work in nested producers, signatures, constructors and field defaults through interpreter/native execution, with imported diagnostics and repeatable compilation. uninitialized arrays, type-valued record storage and type-array procedure parameters/results remain open.
 
 optional `if`/`while` captures also execute in type-producing bodies: `if count |length| { return [length]i16 }` generates storage from an optional `usize`. ordinary checked IR validates each executed guard; present payloads become immutable owned constants with exact scalar/aggregate types and strings, and absent optionals skip the body. while guards observe updated locals on each iteration; captures stay body-local across break/continue and early return. generated lengths/defaults, imported producers, cache identity and repeated compilation preserve these values. null data/function pointers materialize as null, but nonnull pointer/slice/callback-bearing payloads retain the constant-materialization escape boundary.
 
diff --git a/TODO.md b/TODO.md
index 55587c0..bdc0c97 100644
--- a/TODO.md
+++ b/TODO.md
@@ -32,6 +32,8 @@ if/while captures and tagged payload matches select nested constructors, lengths
 array/slice/string/pointer-to-array collection loops support exact copy/pointer
 captures and `usize` indices through both paths; type-producing bodies iterate
 materializable arrays/strings by value without retaining interpreter addresses.
+initialized type-valued fixed arrays support nested copies, indexed/whole updates,
+checked projections and by-value collection captures in type-producing bodies.
 general type-valued execution, reflection and generic library acceptance remain open.
 the driver retains frontend storage and source provenance through
 `@source/compilation`, with compilation-wide AST node identities.
@@ -74,15 +76,16 @@ test discovery and FFI remain outside these completed slices.
   - [x] aggregate/explicit-expression checkpoint: computed nested records/tuples and fixed arrays, contextual/dependent aggregate value parameters, normalized specialization caching and explicit `$()` expressions through interpreter/native execution. preserve by-value isolation, zero-cell shapes, integer widths, string ownership, enum/optional fields and exact IEEE float bits; reject runtime dependencies and values that would retain temporary interpreter storage. repeatable compilation restores erased expressions.
   - [x] conditional specialization checkpoint: explicit compile-time `if` guards and side-effect-free constant guards in concrete generic procedures select a body before specialization/checking. type equality retains aliases, nominal identity and structural signatures; composed error-set identity/cache keys ignore ordering, grouping and repetition. guard checking, selected-body diagnostics, scoped cleanup, runtime guards and repeatable compilation work through interpreter/native execution; both arms remain parsed and name-resolved.
   - [x] constant-input type-procedure checkpoint: type-producing procedures accept ordinary parameters alongside `$` parameters, require every argument explicitly and evaluate/cache/erase all inputs. generated record/array storage, nominal cache identity, nested calls, dependent contextual aggregate inputs, exact erased-argument checking, source diagnostics, imported producers and repeatable compilation work through interpreter/native execution.
-  - [x] mutable type-execution checkpoint: type-producing bodies execute mutable type/value locals, direct binding assignments, scoped blocks, if/else and early returns, integer-range/while loops, break/continue and nested/recursive producers. generated nested types, scalar-computed lengths/defaults, nominal cache identity, exact value types, overflow/guard/assignment diagnostics, imported producers and repeatable compilation work through interpreter/native execution. type-control execution shares a 4096-step bound across nested producers; scalar operations reuse checked IR execution. aggregate field/index updates are covered below; cleanup and type-valued aggregate storage in these bodies remain open.
+  - [x] mutable type-execution checkpoint: type-producing bodies execute mutable type/value locals, direct binding assignments, scoped blocks, if/else and early returns, integer-range/while loops, break/continue and nested/recursive producers. generated nested types, scalar-computed lengths/defaults, nominal cache identity, exact value types, overflow/guard/assignment diagnostics, imported producers and repeatable compilation work through interpreter/native execution. type-control execution shares a 4096-step bound across nested producers; scalar operations reuse checked IR execution. aggregate field/index updates and type-valued arrays are covered below; cleanup and type-valued record storage remain open.
   - [x] type-match checkpoint: type-producing bodies execute scalar/enum match statements and direct type-valued match expressions in initializers, assignments and returns, including nested selected arms. ordinary checking/IR execution select the arm and validate subject/pattern types, ranges, overlap, unreachable arms and exhaustiveness; only the selected body is elaborated. generated storage, scoped locals, loop transfers, early returns, nominal cache identity, selected-body diagnostics, dependency provenance and repeatable compilation work through interpreter/native execution. all bodies remain parsed/name-resolved and execution shares the type-control bound.
   - [x] nested type-match checkpoint: matches select types inside constructors, array lengths, generic arguments, local annotations, callback signatures and field defaults in type-producing bodies. selection precedes ordinary expansion, preserves literal spelling/source provenance and loop snapshots, and caches nominal results before expanding recursive fields. selected-body and pattern diagnostics, failed deferred elaboration, imported producers and repeatable compilation work through interpreter/native execution; deferred selection shares the producer's type-control bound.
   - [x] tagged/fallible constant checkpoint: explicit `$()` expressions, generic value parameters and type-procedure inputs materialize tagged unions and both fallible channels through interpreter/native execution. preserve active tags/payloads, nested raw aggregate projections, string ownership, void/zero-cell variants, composed/payload errors, declared channel types, normalized cache identity and repeatable compilation. `catch` computes generated lengths and runtime values. untagged unions and storage-bearing active payloads remain escape diagnostics rather than retaining temporary interpreter handles.
   - [x] tagged type-match checkpoint: type-producing bodies execute tagged-union matches with immutable by-value payload captures in statement, expression and nested storage positions. ordinary match checking validates every arm's captures, including grouped variants; selected payloads retain exact scalar/aggregate types and owned strings. generated storage/defaults, loop snapshots/transfers, cache identity, selected-body diagnostics, imported producers, dependency provenance and repeatable compilation work through interpreter/native execution. storage-bearing payloads retain the constant-materialization escape boundary.
   - [x] generic match-specialization checkpoint: side-effect-free constant scalar/enum/tagged-union subjects in concrete generic procedures and explicit `match $(subject)` expressions/statements select an arm before body specialization/checking. reuse ordinary checked IR for pattern types, ranges, overlap, exhaustiveness and every arm's capture validation; only the selected body is elaborated. exact by-value payload types/owned strings, runtime parameters, nested expression matches, cleanup, return/loop transfers, imported producers and repeatable compilation work through interpreter/native execution. ordinary call/runtime/mutable subjects stay runtime; contextual aggregates with possible runtime defaults are not implicitly evaluated. all bodies remain parsed/name-resolved; storage-bearing payloads retain the constant-materialization escape boundary.
   - [x] optional type-control checkpoint: type-producing bodies execute optional if/while guards with immutable by-value payload captures. ordinary checked IR validates guards; selected scalar/aggregate payloads retain exact types and owned strings across nested captures, generated storage/defaults, loop updates/transfers and early returns. absent optionals skip unselected bodies; invalid guards, capture mutation/shadowing, overflow and execution bounds retain diagnostics. imported producers, dependency provenance, nominal cache identity and repeatable compilation work through interpreter/native execution. null data/function pointers materialize correctly; nonnull storage-bearing payloads retain the constant-materialization escape boundary.
-  - [x] aggregate type-update checkpoint: type-producing bodies update initialized, materializable aggregate locals through nested record fields and mutable fixed-array indices. ordinary checked IR validates and executes each assignment, retaining exact value types, mutability (including immutable payload captures), index types/bounds, unknown-field and narrow-overflow diagnostics. new owned constants preserve earlier by-value copies while later loops, generated storage and defaults observe updates. imported producers, dependency provenance, nominal cache identity and repeatable compilation work through interpreter/native execution. pointer/slice-backed mutation, uninitialized aggregate construction and type-valued aggregate storage remain open.
-  - [x] collection-iteration checkpoint: arrays, slices, strings and single pointers-to-arrays support immutable exact-type copy captures, storage-qualified pointer captures and optional `usize` indices through interpreter/native execution. iterables/bounds evaluate once, array lvalues remain borrowed and later element updates are visible; temporary arrays, aggregate copy isolation, zero-cell/empty collections, nested loops and cleanup across transfers retain ordinary semantics. ordinary constant-input procedures reuse the same checked IR; type-producing bodies iterate materializable arrays/strings with by-value captures, fixed entry-time place indices, generated storage, nominal cache identity, dependency diagnostics, shared execution bounds and repeatable compilation. storage-bearing type-control captures and type-valued elements retain their existing boundaries.
+  - [x] aggregate type-update checkpoint: type-producing bodies update initialized, materializable aggregate locals through nested record fields and mutable fixed-array indices. ordinary checked IR validates and executes each assignment, retaining exact value types, mutability (including immutable payload captures), index types/bounds, unknown-field and narrow-overflow diagnostics. new owned constants preserve earlier by-value copies while later loops, generated storage and defaults observe updates. imported producers, dependency provenance, nominal cache identity and repeatable compilation work through interpreter/native execution. pointer/slice-backed mutation, uninitialized aggregate construction and type-valued record storage remain open; type-valued arrays are covered below.
+  - [x] collection-iteration checkpoint: arrays, slices, strings and single pointers-to-arrays support immutable exact-type copy captures, storage-qualified pointer captures and optional `usize` indices through interpreter/native execution. iterables/bounds evaluate once, array lvalues remain borrowed and later element updates are visible; temporary arrays, aggregate copy isolation, zero-cell/empty collections, nested loops and cleanup across transfers retain ordinary semantics. ordinary constant-input procedures reuse the same checked IR; type-producing bodies iterate materializable arrays/strings with by-value captures, fixed entry-time place indices, generated storage, nominal cache identity, dependency diagnostics, shared execution bounds and repeatable compilation. storage-bearing type-control captures retain their existing boundary; type-valued elements are covered below.
+  - [x] type-array storage checkpoint: type-producing bodies own initialized fixed arrays of type values, including explicit/inferred nested arrays, `.len`, checked `usize` indexing, whole/indexed updates and immutable by-value collection captures. persistent snapshots preserve copies and exact shape/mutability while borrowed array places observe later updates. selected types generate nested storage, constructors, signatures and defaults through interpreter/native execution, retaining selected-body and index/type/mutability diagnostics, imported provenance, nominal cache identity, shared bounds and repeatable compilation. uninitialized arrays, type-valued record storage, type-array parameters/results and reflection remain open.
   - [ ] remaining gate: general type-valued compile-time execution, inline match/loop expansion and reflection (`typeinfo!`, `field!`, `struct_type!`, generated type/default arrays), broader constant materialization (including untagged unions and storage-bearing values), plus existing-library acceptance. required expression-valued control flow, compound updates, formatting parsing and imported C-binding support may interleave with later gates.
 - [ ] remaining source constructs: expression-valued control flow and `yield`, compound updates and multiline strings. examples: `source/parser/parse.hon`, `source/llvm/runtime.hon`.
 - [ ] standard-library milestone: compile/run a multi-package program exercising existing allocation and IO, including error cleanup; no replacement miniature standard library.
diff --git a/source/ast/ast.hon b/source/ast/ast.hon
index 230d8f5..90040c7 100644
--- a/source/ast/ast.hon
+++ b/source/ast/ast.hon
@@ -1,5 +1,5 @@
 #! grammar:
-#! * type ..... -> type_sum ['!' type]; type_sum -> type_atom {'|' type_atom}; type_atom includes '(' type ')', identifier {'.' member | '(' [expr {',' expr} [',']] ')'}, '?' type_atom, ('@' | '*') ['mut'] type_atom, ['@'] 'proc' '(' parameters ')' type, '[' (expr | '_') ']' ['mut'] type_atom, '[' [';' expr] ']' ['mut'] type_atom, record/enum/union declarations, and ('distinct' | 'alias') type.
+#! * type ..... -> type_sum ['!' type]; type_sum -> type_atom {'|' type_atom}; type_atom includes '(' type ')', identifier {'.' member | '(' [expr {',' expr} [',']] ')' | '[' expr ']'}, '?' type_atom, ('@' | '*') ['mut'] type_atom, ['@'] 'proc' '(' parameters ')' type, '[' (expr | '_') ']' ['mut'] type_atom, '[' [';' expr] ']' ['mut'] type_atom, record/enum/union declarations, and ('distinct' | 'alias') type.
 #! * binding ... -> :: | :=
 #! * literal .. -> int | float | string | 'true' | 'false' | 'null'
 #! * op ....... -> '+' | '-' | '*' | '/' | '==' | '!=' | '<' | '<=' | '>' | '>=' | 'and' | 'or'
diff --git a/source/compilation/compilation.test.hon b/source/compilation/compilation.test.hon
index bf77352..ee0a44d 100644
--- a/source/compilation/compilation.test.hon
+++ b/source/compilation/compilation.test.hon
@@ -158,6 +158,23 @@ recompiles_specialized_calls_without_borrowing_previous_ir test {
             `    for "ok" |byte| { if (byte == u8(107)) Element = i16 }
             `    return [length]Element
             `}
+            `TypeArray proc() type {
+            `    types [2]mut [1]mut type := [[i8], [bool]]
+            `    original :: types
+            `    for types |row, index| {
+            `        copied := row
+            `        copied[0] = u8
+            `        if (row[0] == u8) return bool
+            `        if (index == 0) { (types[1])[0] = i16 }
+            `        if (index == 1 and row[0] != i16) return bool
+            `    }
+            `    if (original[1][0] != bool) return bool
+            `    inferred := [[i8], [bool]]
+            `    inferred = [[i16], [u8]]
+            `    empty [0]type :: []
+            `    for (empty) |_| return bool
+            `    return struct { values [types.len]types[1][0], bias inferred[0][0] = 2 }
+            `}
             `read_selected proc($choice Choice, value i16) i16 {
             `    match choice {
             `        .payload |detail|: {
@@ -190,6 +207,9 @@ recompiles_specialized_calls_without_borrowing_previous_ir test {
             `    total i16 := 0
             `    for same_collected |item| { total = total + item }
             `    if (total != 42) return 0
+            `    type_array TypeArray() :: { values = [19, 21] }
+            `    same_type_array TypeArray() :: type_array
+            `    if (same_type_array.values[0] + same_type_array.values[1] + same_type_array.bias != 42) return 0
             `    payload :: packet.choices[0].payload
             `    if (payload.values[0] != 40 or payload.values[1] != 2 or payload.text.len != 2) return 0
             `    match packet.choices[1] { .empty: {}, .payload: return 0 }
diff --git a/source/parser/parse.hon b/source/parser/parse.hon
index d7f6d11..30f16dc 100644
--- a/source/parser/parse.hon
+++ b/source/parser/parse.hon
@@ -800,6 +800,10 @@ parse_type_atom proc(state @mut State) ast.NodeId ! ParseError {
             type = try parse_call(state, type, token.span.start, false)
             continue
         }
+        if (next_is(state, .open_bracket)) {
+            type = try parse_index(state, type, token.span.start)
+            continue
+        }
         if (!next_is(state, .dot)) break
         state.next_token += 1
         member :: try consume_member(state, false)
diff --git a/source/sema/specialize/specialize.hon b/source/sema/specialize/specialize.hon
index 0361836..128503b 100644
--- a/source/sema/specialize/specialize.hon
+++ b/source/sema/specialize/specialize.hon
@@ -281,6 +281,10 @@ expand proc(state @mut State, id ast.NodeId) void ! Error {
         child :: ast.child(&state.tree, id, i)
         try expand(state, child)
     }
+    if (!try type_array_projection(state, id)) {
+        try reject_evaluation(state, id)
+        return
+    }
     if (class == .expression and ast.expr_kind(&state.tree, id) == .binary) {
         view :: ast.binary_expr(&state.tree, id)
         if (
@@ -1328,9 +1332,212 @@ expand_type_matches proc(state @mut State, id ast.NodeId) bool ! Error {
     for (0..ast.child_count(&state.tree, id)) |i| {
         if (!try expand_type_matches(state, ast.child(&state.tree, id, i))) return false
     }
+    return try type_array_projection(state, id)
+}
+
+@hide:file
+type_array_projection proc(state @mut State, id ast.NodeId) bool ! Error {
+    if (ast.node_class(&state.tree, id) != .expression) return true
+    kind :: ast.expr_kind(&state.tree, id)
+    if (kind == .index or kind == .selection) {
+        base :: if (kind == .index) ast.index_expr(&state.tree, id).base else ast.selection_expr(&state.tree, id).base
+        if (ast.expr_kind(&state.tree, base) != .typed_constant) return true
+        array :: ast.typed_constant(&state.tree, base)
+        if (!try type_array_storage(state, array.type)) return true
+        selected := no_node
+        if (kind == .index) {
+            index :: try type_array_index(state, ast.index_expr(&state.tree, id).index,
+                ast.array_element_count(&state.tree, array.value))
+            if (index == no_index) return false
+            selected = ast.array_element(&state.tree, array.value, index)
+        } else {
+            member :: ast.selection_expr(&state.tree, id).member
+            if (!mem.eql(ast.source_text(&state.tree, ast.node_span(&state.tree, member)), "len")) {
+                state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                    .unknown_field, ast.node_span(&state.tree, member))
+                return false
+            }
+            count :: try ast.add_integer(state.builder, ast.node_span(&state.tree, id),
+                u64(ast.array_element_count(&state.tree, array.value)))
+            selected = try ast.add_typed_constant(state.builder, ast.node_span(&state.tree, id),
+                try builtin(state, id, .usize), count)
+            try refresh(state)
+        }
+        # copying a nominal definition into the projection would create a new
+        # identity on every read. retain its original node behind a type alias.
+        if (nominal_type_value(state, selected)) {
+            selected = try ast.add_type_operand(state.builder, ast.node_span(&state.tree, id), selected, true)
+            try refresh(state)
+        }
+        resolved :: binding(state, selected)
+        try remember(state, id)
+        ast.replace_node_from_source(state.builder, id, selected)
+        try refresh(state)
+        state.bindings.items[usize(id)] = resolved
+    }
     return true
 }
 
+# type arrays are persistent AST values, never runtime storage. keep the same
+# typed-constant snapshots as ordinary aggregates, but validate their leaves here.
+@hide:file
+type_array_storage proc(state @mut State, annotation ast.NodeId) bool ! Error {
+    current := annotation
+    for (0..128) |_| {
+        if (is_type(state, current)) return current != annotation
+        current = try canonical_type(state, current)
+        if (current == no_node or ast.expr_kind(&state.tree, current) != .array_type) return false
+        current = ast.array_type(&state.tree, current).element
+    }
+    return false
+}
+
+@hide:file
+type_array_index proc(state @mut State, expression ast.NodeId, count usize) usize ! Error {
+    usize_type :: try builtin(state, expression, .usize)
+    actual :: try expression_type(state, expression, 0)
+    if (!flexible(state, expression) and (actual == no_node or !try same_type(state, actual, usize_type))) {
+        state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+            .invalid_index_type, ast.node_span(&state.tree, expression))
+        return no_index
+    }
+    value :: try evaluate_ir(state, expression, usize_type)
+    if (value.kind != .integer) return no_index
+    if (value.magnitude >= u64(count)) {
+        state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+            .index_out_of_bounds, ast.node_span(&state.tree, expression))
+        return no_index
+    }
+    return usize(value.magnitude)
+}
+
+@hide:file
+type_array_compatible proc(state @mut State, expected, actual ast.NodeId) bool ! Error {
+    if (is_type(state, expected) or is_type(state, actual))
+        return is_type(state, expected) and is_type(state, actual)
+    left :: try canonical_type(state, expected)
+    right :: try canonical_type(state, actual)
+    if (left == no_node or right == no_node) return false
+    if (ast.expr_kind(&state.tree, left) != .array_type or ast.expr_kind(&state.tree, right) != .array_type) return false
+    a :: ast.array_type(&state.tree, left)
+    b :: ast.array_type(&state.tree, right)
+    if (a.mutable != b.mutable or b.count == null) return false
+    if (a.count) |count| {
+        if (!try value_equal(state, try evaluate(state, count), try evaluate(state, b.count?))) return false
+    }
+    return try type_array_compatible(state, a.element, b.element)
+}
+
+@hide:file
+type_array_value proc(state @mut State, expression, annotation ast.NodeId) ast.NodeId ! Error {
+    type :: try canonical_type(state, annotation)
+    array :: ast.array_type(&state.tree, type)
+    if (ast.expr_kind(&state.tree, expression) == .typed_constant) {
+        actual :: ast.typed_constant(&state.tree, expression)
+        if (try type_array_compatible(state, type, actual.type)) return expression
+    } else if (ast.expr_kind(&state.tree, expression) == .array_literal) {
+        count :: ast.array_element_count(&state.tree, expression)
+        if (array.count) |length| {
+            value :: try evaluate(state, length)
+            if (value.kind != .integer or value.negative) {
+                state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                    .invalid_array_length, ast.node_span(&state.tree, length))
+                return no_node
+            }
+            if (value.magnitude != u64(count)) {
+                state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                    .array_length_mismatch, ast.node_span(&state.tree, expression))
+                return no_node
+            }
+        }
+        elements := arraylist.init(ast.NodeId, state.allocator)
+        defer arraylist.deinit(&elements)
+        element_type := array.element
+        for (0..count) |i| {
+            element :: try type_execution_value(state,
+                ast.array_element(&state.tree, expression, i), element_type)
+            if (element == no_node) return no_node
+            if (ast.expr_kind(&state.tree, element) == .typed_constant)
+                element_type = ast.typed_constant(&state.tree, element).type
+            try arraylist.append(&elements, element)
+        }
+        # empty outer arrays still need concrete, valid child dimensions.
+        if (count == 0) {
+            child := element_type
+            while (!is_type(state, child)) {
+                child = try canonical_type(state, child)
+                descriptor :: ast.array_type(&state.tree, child)
+                value := Value{}
+                if (descriptor.count) |length| value = try evaluate(state, length)
+                if (value.kind != .integer or value.negative) {
+                    state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                        .invalid_array_length, ast.node_span(&state.tree, child))
+                    return no_node
+                }
+                child = descriptor.element
+            }
+        }
+        span :: ast.node_span(&state.tree, expression)
+        length :: try ast.add_integer(state.builder, span, u64(count))
+        concrete :: try ast.add_array_type(state.builder, ast.node_span(&state.tree, annotation),
+            length, element_type, array.mutable)
+        literal :: try ast.add_array_literal(state.builder, span, elements.items)
+        result :: try ast.add_typed_constant(state.builder, span, concrete, literal)
+        try refresh(state)
+        return result
+    }
+    state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+        .type_mismatch, ast.node_span(&state.tree, expression))
+    return no_node
+}
+
+# rebuild only the indexed path so previous snapshots retain their owned values.
+@hide:file
+type_array_update proc(
+    state @mut State, execution @mut TypeExecution, target, root, current, input ast.NodeId,
+) ast.NodeId ! Error {
+    # find the outermost index; rebuild its child before copying this parent.
+    first := target
+    while (true) {
+        if (ast.expr_kind(&state.tree, first) != .index) {
+            state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                .invalid_assignment_target, ast.node_span(&state.tree, target))
+            return no_node
+        }
+        base :: ast.index_expr(&state.tree, first).base
+        if (base == root) break
+        first = base
+    }
+    array :: ast.typed_constant(&state.tree, current)
+    descriptor :: ast.array_type(&state.tree, array.type)
+    if (!descriptor.mutable) {
+        state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+            .invalid_index_assignment, ast.node_span(&state.tree, target))
+        return no_node
+    }
+    expression :: try type_snapshot(state, execution, ast.index_expr(&state.tree, first).index)
+    if (!try expand_type_matches(state, expression)) return no_node
+    count :: ast.array_element_count(&state.tree, array.value)
+    index :: try type_array_index(state, expression, count)
+    if (index == no_index) return no_node
+    previous :: ast.array_element(&state.tree, array.value, index)
+    updated := no_node
+    if (first == target) updated = try type_execution_value(state, input, descriptor.element)
+    else updated = try type_array_update(state, execution, target, first, previous, input)
+    if (updated == no_node) return no_node
+    elements := arraylist.init(ast.NodeId, state.allocator)
+    defer arraylist.deinit(&elements)
+    for (0..count) |i| {
+        element :: if (i == index) updated else ast.array_element(&state.tree, array.value, i)
+        try arraylist.append(&elements, element)
+    }
+    span :: ast.node_span(&state.tree, target)
+    literal :: try ast.add_array_literal(state.builder, span, elements.items)
+    result :: try ast.add_typed_constant(state.builder, span, array.type, literal)
+    try refresh(state)
+    return result
+}
+
 @hide:file
 type_execution_value proc(state @mut State, input, annotation ast.NodeId) ast.NodeId ! Error {
     if (annotation == no_node) return no_node
@@ -1346,6 +1553,7 @@ type_execution_value proc(state @mut State, input, annotation ast.NodeId) ast.No
         return concrete.node
     }
     if (!try expand_type_matches(state, expression)) return no_node
+    if (try type_array_storage(state, annotation)) return try type_array_value(state, expression, annotation)
     try expand(state, expression)
     resolved :: binding(state, expression)
     if (resolved.kind == .invalid) {
@@ -1479,6 +1687,8 @@ execute_type_statement proc(state @mut State, execution @mut TypeExecution, stat
             if (annotation == no_node) return .invalid
             value :: try type_execution_value(state, expression, annotation)
             if (value == no_node) return .invalid
+            if (ast.expr_kind(&state.tree, value) == .typed_constant)
+                annotation = ast.typed_constant(&state.tree, value).type
             try arraylist.append(&execution.locals, TypeLocal{
                 declaration = statement, value = value, annotation = annotation,
             })
@@ -1511,6 +1721,23 @@ execute_type_statement proc(state @mut State, execution @mut TypeExecution, stat
                 return .invalid
             }
             if (root != assignment.target) {
+                if (try type_array_storage(state, execution.locals.items[index].annotation)) {
+                    local :: execution.locals.items[index]
+                    if (
+                        ast.node_class(&state.tree, local.declaration) != .statement
+                        or ast.statement_decl(&state.tree, local.declaration).mutability != .variable
+                    ) {
+                        state.evaluation_diagnostic = try diagnostics.add(state.diagnostics,
+                            .invalid_index_assignment, ast.node_span(&state.tree, assignment.target))
+                        return .invalid
+                    }
+                    input :: try type_snapshot(state, execution, assignment.value)
+                    if (!try expand_type_matches(state, input)) return .invalid
+                    value :: try type_array_update(state, execution, assignment.target, root, local.value, input)
+                    if (value == no_node) return .invalid
+                    execution.locals.items[index].value = value
+                    return .next
+                }
                 value :: try type_assignment_value(state, execution, statement, index)
                 if (value == no_node) return .invalid
                 execution.locals.items[index].value = value
@@ -1686,34 +1913,40 @@ execute_type_collection proc(state @mut State, execution @mut TypeExecution, sta
     if (annotation == no_node) return .invalid
     collection :: try type_execution_value(state, snapshot, annotation)
     if (collection == no_node) return .invalid
-    # validate the loop contract even for empty collections, without executing its
-    # type-valued body. the synthetic body exits before reading any element.
-    stop :: try ast.add_break_stmt(state.builder, span)
-    stops [1]ast.NodeId :: [stop]
-    body :: try ast.add_block(state.builder, span, stops[..])
-    selector :: try ast.add_for_stmt(state.builder, span, collection, loop.capture, loop.index,
-        loop.pointer_capture, loop.index_capture, body)
-    length := no_node
-    if (ast.expr_kind(&state.tree, annotation) == .array_type) length = ast.array_type(&state.tree, annotation).count?
-    else {
-        value :: try evaluate(state, collection)
-        if (value.kind == .string) {
-            text :: ast.literal_text(&state.tree, value.node)
-            cursor := usize(1)
-            count := u64(0)
-            while (cursor < text.len - 1) {
-                _ = ast.string_next(text, &cursor) catch { return .invalid }
-                count += 1
-            }
-            length = try ast.add_integer(state.builder, span, count)
-        } else length = try ast.add_integer(state.builder, span, 0)
+    count := Value{}
+    if (try type_array_storage(state, annotation)) {
+        count = Value{ kind = .integer,
+            magnitude = u64(ast.array_element_count(&state.tree, ast.typed_constant(&state.tree, collection).value)) }
+    } else {
+        # validate the loop contract even for empty collections, without executing
+        # its type-valued body. the synthetic body exits before reading an element.
+        stop :: try ast.add_break_stmt(state.builder, span)
+        stops [1]ast.NodeId :: [stop]
+        body :: try ast.add_block(state.builder, span, stops[..])
+        selector :: try ast.add_for_stmt(state.builder, span, collection, loop.capture, loop.index,
+            loop.pointer_capture, loop.index_capture, body)
+        length := no_node
+        if (ast.expr_kind(&state.tree, annotation) == .array_type) length = ast.array_type(&state.tree, annotation).count?
+        else {
+            value :: try evaluate(state, collection)
+            if (value.kind == .string) {
+                text :: ast.literal_text(&state.tree, value.node)
+                cursor := usize(1)
+                size := u64(0)
+                while (cursor < text.len - 1) {
+                    _ = ast.string_next(text, &cursor) catch { return .invalid }
+                    size += 1
+                }
+                length = try ast.add_integer(state.builder, span, size)
+            } else length = try ast.add_integer(state.builder, span, 0)
+        }
+        returned :: try ast.add_return_stmt(state.builder, span, length)
+        statements [2]ast.NodeId :: [selector, returned]
+        wrapper :: try ast.add_block(state.builder, span, statements[..])
+        try refresh(state)
+        count = try evaluate_ir_body(state, statement, wrapper, try builtin(state, statement, .usize))
+        if (count.kind != .integer) return .invalid
     }
-    returned :: try ast.add_return_stmt(state.builder, span, length)
-    statements [2]ast.NodeId :: [selector, returned]
-    wrapper :: try ast.add_block(state.builder, span, statements[..])
-    try refresh(state)
-    count :: try evaluate_ir_body(state, statement, wrapper, try builtin(state, statement, .usize))
-    if (count.kind != .integer) return .invalid
     if (loop.pointer_capture and loop.capture != null) {
         state.evaluation_diagnostic = try diagnostics.add(state.diagnostics, .comptime_value_escape, span)
         return .invalid
@@ -2154,6 +2387,7 @@ expression_type proc(state @mut State, id ast.NodeId, depth usize) ast.NodeId !
     if (depth >= 128) return no_node
     try expand(state, id)
     resolved :: binding(state, id)
+    if (resolved.kind == .builtin and resolved.data.builtin != .type) return try builtin(state, id, .type)
     if (resolved.kind == .declaration) {
         target :: resolved.data.declaration
         class :: ast.node_class(&state.tree, target)
@@ -2180,6 +2414,9 @@ expression_type proc(state @mut State, id ast.NodeId, depth usize) ast.NodeId !
     }
     kind :: ast.expr_kind(&state.tree, id)
     match kind {
+        .record_type, .array_type, .slice_type, .pointer_type, .function_type, .optional_type,
+        .enum_type, .union_type, .distinct_type, .fallible_type, .sum_type, .alias_expr:
+            return try builtin(state, id, .type)
         .typed_constant: return try canonical_type(state, ast.typed_constant(&state.tree, id).type)
         .literal_int: return try builtin(state, id, .i64)
         .literal_float: return try builtin(state, id, .f64)
@@ -2288,7 +2525,10 @@ expression_type proc(state @mut State, id ast.NodeId, depth usize) ast.NodeId !
             base :: try expression_type(state, view.base, depth + 1)
             if (base == no_node) return no_node
             base_kind :: ast.expr_kind(&state.tree, base)
-            if (base_kind == .array_type) return try canonical_type(state, ast.array_type(&state.tree, base).element)
+            if (base_kind == .array_type) {
+                element :: ast.array_type(&state.tree, base).element
+                return if (is_type(state, element)) element else try canonical_type(state, element)
+            }
             if (base_kind == .slice_type) return try canonical_type(state, ast.slice_type(&state.tree, base).element)
             if (base_kind == .pointer_type) return try canonical_type(state, ast.pointer_type(&state.tree, base).element)
             if (binding(state, base).kind == .builtin and binding(state, base).data.builtin == .string) return try builtin(state, id, .u8)
diff --git a/tests/native.py b/tests/native.py
index c2e5dd7..3c0b140 100644
--- a/tests/native.py
+++ b/tests/native.py
@@ -1127,6 +1127,207 @@ CASES = {
         }
         """, b"42\n", None,
     ),
+    "type_arrays_nested_copies_assignment_and_consumers": (
+        """
+        Box proc(T type) type { return struct { value T } }
+        Selected proc() type {
+            explicit [2]mut [_]mut type := [[i8, bool], [u8, i16]]
+            inferred := [[i8, bool], [u8, i16]]
+            original :: explicit
+            copied [2]mut [_]mut type := explicit
+            (copied[0])[0] = bool
+            explicit[0] = [i16, u8]
+            inferred = [[i16, u8], [bool, i8]]
+            if (original[0][0] != i8 or copied[0][0] != bool) return bool
+            if (explicit[0][0] != i16 or inferred[1][0] != bool) return bool
+            return Box(explicit[0][0])
+        }
+        Storage proc() type {
+            types :: [Selected(), [2]i16]
+            return struct { item types[0], values types[1], bias i16 = 2 }
+        }
+        read proc(value Selected()) i16 { return value.value }
+        main proc() i16 {
+            value Storage() :: { item = { value = 19 }, values = [20, 1] }
+            return read(value.item) + value.values[0] + value.values[1] + value.bias
+        }
+        """, b"42\n", None,
+    ),
+    "type_arrays_iteration_borrows_nested_places_and_copies_captures": (
+        """
+        Selected proc() type {
+            types [2]mut type := [i8, bool]
+            Result := bool
+            for types |T, index| {
+                at usize :: index
+                if (at == 0) types[1] = i16
+                if (at == 1) Result = T
+            }
+            rows [2]mut [1]mut type := [[i8], [bool]]
+            for rows |row, index| {
+                copied := row
+                copied[0] = u8
+                if (row[0] == u8) return bool
+                if (index == 0) { (rows[1])[0] = Result }
+                if (index == 1 and row[0] != i16) return bool
+            }
+            empty [0]type :: []
+            for (empty) |_| return bool
+            if (empty.len != 0 or types.len != 2 or rows[0].len != 1) return bool
+            return rows[1][0]
+        }
+        main proc() i16 { value Selected() :: 42
+            return value
+        }
+        """, b"42\n", None,
+    ),
+    "type_arrays_only_execute_selected_bodies": (
+        """
+        Selected proc(ok bool) type {
+            types :: [i16]
+            if (ok) return types[0]
+            return types[1]
+        }
+        main proc() i16 { value Selected(true) :: 42
+            return value
+        }
+        """, b"42\n", None,
+    ),
+    "type_arrays_selected_invalid_body": (
+        """
+        Selected proc(ok bool) type {
+            types :: [i16]
+            if (ok) return types[0]
+            return types[1]
+        }
+        main proc() Selected(false) { return 42 }
+        """, b"", b"index out of bounds",
+    ),
+    "type_arrays_read_requires_usize_index": (
+        """
+        Bad proc() type {
+            types :: [i16]
+            index u8 :: 0
+            return types[index]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array index must have type usize",
+    ),
+    "type_arrays_write_checks_bounds": (
+        """
+        Bad proc() type {
+            types [1]mut type := [i16]
+            types[1] = bool
+            return types[0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"index out of bounds",
+    ),
+    "type_arrays_write_requires_usize_index": (
+        """
+        Bad proc() type {
+            types [1]mut type := [i16]
+            index u8 :: 0
+            types[index] = bool
+            return types[0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array index must have type usize",
+    ),
+    "type_arrays_write_requires_mutable_elements": (
+        """
+        Bad proc() type {
+            types [1]type := [i16]
+            types[0] = bool
+            return types[0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"indexed assignment requires a writable array element",
+    ),
+    "type_arrays_nested_write_requires_mutable_inner_elements": (
+        """
+        Bad proc() type {
+            types [1]mut [1]type := [[i16]]
+            (types[0])[0] = bool
+            return types[0][0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"indexed assignment requires a writable array element",
+    ),
+    "type_arrays_whole_assignment_requires_mutable_binding": (
+        """
+        Bad proc() type {
+            types :: [i16]
+            types = [bool]
+            return types[0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"assignment requires a mutable local binding",
+    ),
+    "type_arrays_whole_assignment_checks_shape": (
+        """
+        Bad proc() type {
+            types := [[i16]]
+            types = [[i16, bool]]
+            return types[0][0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array literal length does not match its type",
+    ),
+    "type_arrays_indexed_assignment_checks_shape": (
+        """
+        Bad proc() type {
+            types [1]mut [1]mut type := [[i16]]
+            types[0] = [i16, bool]
+            return types[0][0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array literal length does not match its type",
+    ),
+    "type_arrays_indexed_assignment_checks_value": (
+        """
+        Bad proc() type {
+            types [1]mut type := [i16]
+            types[0] = 42
+            return types[0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"incompatible value type",
+    ),
+    "type_arrays_inferred_nested_counts_reject_ragged_initialization": (
+        """
+        Bad proc() type {
+            types [2]mut [_]mut type := [[i8], [i16, bool]]
+            return types[1][0]
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array literal length does not match its type",
+    ),
+    "type_arrays_preserve_anonymous_nominal_identity_across_reads_and_copies": (
+        """
+        Selected proc() type {
+            types :: [struct { value i16 }, struct { value i16 }]
+            copied :: types
+            if (types[0] != copied[0] or types[0] == types[1]) return bool
+            return struct { first types[0], second copied[0] }
+        }
+        main proc() i16 {
+            value Selected() :: { first = { value = 19 }, second = { value = 23 } }
+            copied := value.first
+            copied = value.second
+            return value.first.value + copied.value
+        }
+        """, b"42\n", None,
+    ),
+    "type_arrays_empty_shapes_validate_child_lengths": (
+        """
+        Bad proc() type {
+            types [0][-1]type :: []
+            return i16
+        }
+        main proc() Bad() { return 42 }
+        """, b"", b"array length must be a nonnegative supported compile-time integer",
+    ),
     "type_execution_mutable_types_and_nested_producers": (
         """
         Nest proc(T type, depth usize) type {
@@ -4745,7 +4946,38 @@ def check_specialization_packages(temporary, executable):
     interpreted = run(str(HONEY), "run", str(app))
     assert interpreted.stderr.startswith(f"{sizing.resolve()}:3:".encode()), outcome(interpreted)
     assert len(interpreted.stderr.splitlines()) == 1, outcome(interpreted)
-    return 12
+    sizing.write_text(textwrap.dedent("""
+        TypeArray proc() type {
+            types [2]mut type := [i8, bool]
+            for types |T, index| {
+                if (index == 0) types[1] = i16
+                if (index == 1) return struct { values [2]T, bias T = 2 }
+            }
+            return bool
+        }
+    """).strip() + "\n")
+    source.write_text(textwrap.dedent("""
+        lib :: import "../library"
+        main proc() i16 {
+            value lib.TypeArray() :: { values = [19, 21] }
+            same lib.TypeArray() :: value
+            return same.values[0] + same.values[1] + same.bias
+        }
+    """).strip() + "\n")
+    check(app, executable, (b"42\n", None))
+    sizing.write_text(textwrap.dedent("""
+        TypeArray proc() type {
+            types [1]mut type := [i16]
+            types[1] = bool
+            return types[0]
+        }
+    """).strip() + "\n")
+    source.write_text('lib :: import "../library"\nmain proc() lib.TypeArray() { return 42 }\n')
+    check(app, executable, (b"", b"index out of bounds"))
+    interpreted = run(str(HONEY), "run", str(app))
+    assert interpreted.stderr.startswith(f"{sizing.resolve()}:3:".encode()), outcome(interpreted)
+    assert len(interpreted.stderr.splitlines()) == 1, outcome(interpreted)
+    return 14
 
 
 def check_dependency_provenance(temporary, executable):