This feature hub pins **where type checking runs** relative to staged semantic rules. End-to-end compile ordering (parse → mods → semantic → lower → codegen) remains under [Build pipeline / Stage ordering](/platform-spec/compiler/build-pipeline/stage-ordering/).

## Implementation anchors

- `compiler/crates/beskid_pipeline/src/phases.rs` — `lower.type_check` phase id
- `compiler/crates/beskid_analysis/src/services/lower.rs` — typed HIR spine (`typed_hir_from_lowered`, `type_check_lowered_hir`)
- `compiler/crates/beskid_analysis/src/hir/index.rs` — `index_program` before type checking
- `compiler/crates/beskid_analysis/src/types/checker/entry.rs` — `TypeChecker::check_entry` (surface → check → lowering prep)
- `compiler/crates/beskid_analysis/src/analysis/rules/staged/type_checking.rs` — structural immutability only
- `compiler/crates/beskid_tests/src/analysis/type_check_diagnostics.rs` — diagnostic code conformance

- [Design model](./design-model/)
- [Verification and traceability](./verification-and-traceability/)

## Decisions
<!-- spec:generate:adr-index -->
No ADRs published under **`adr/`** yet.
<!-- /spec:generate:adr-index -->
## Articles
<!-- spec:generate:article-index -->
- [Semantic pipeline stage ordering - Design model](./articles/design-model/)
- [Semantic pipeline stage ordering - Verification and traceability](./articles/verification-and-traceability/)
<!-- /spec:generate:article-index -->

## Type-check authority

**Normative:** Expression and declaration **type checking** runs exactly once on the **lower spine**, observed as pipeline phase id **`lower.type_check`** (`LOWER_TYPE_CHECK` in `beskid_pipeline::phases`).

The reference compiler **must not** run a second full body-typing pass under **`semantic.type_check`**. That phase id is **not** authoritative for typed HIR or for `E12xx` type diagnostics.

Within **`lower.type_check`**, the reference compiler runs **`index_program`** first, then a **three-pass spine**:

1. **Surface** — build or load per-unit `UnitTypeSurface` values and merge for entry
2. **Check** — [`TypeChecker::check_entry`](compiler/crates/beskid_analysis/src/types/checker/entry.rs) body typing with constraint solving; write `node_types`
3. **Lowering prep** — `LoweringPrep` (`call_kinds`, `cast_intents`) keyed by `HirNodeId`

`TypeResult` assembly follows the three passes. See [Type-system pass contract](/platform-spec/compiler/semantic-pipeline/type-system-pass-contract/design-model/) for the full step list.

```mermaid
flowchart TB
  semantic[semantic staged rules]
  structural[structural checks only]
  lower[lower spine]
  index[index_program]
  surface[surface pass]
  check[TypeChecker::check_entry]
  prep[lowering prep]
  semantic --> structural
  lower --> index --> surface --> check --> prep
```

## What stays in semantic rules

Staged semantic rules (`SemanticPipelineRule` in `staged.rs`) **may** still emit diagnostics that mention types when the check is **structural** and does not require a completed `TypeResult`, for example:

- immutable assignment (`E1214`) in `staged/type_checking.rs`
- invalid `?` shape probes in `staged/error_handling.rs` where resolution alone suffices

Those checks **must not** duplicate full expression typing already performed at **`lower.type_check`**.

## Diagnostic collection

CLI analyze, LSP, and `prepare_compilation_diagnostics` **must** surface type errors by running the lower spine (or collecting `LowerResolveTypeError::Type` into semantic diagnostics via `emit_type_error`). Consumers **must** treat stable **`E12xx`** codes as the conformance surface regardless of whether the error was collected during semantic snapshot assembly or lower failure handling.

## Cross references

- End-to-end phase DAG: [Build pipeline / Stage ordering](/platform-spec/compiler/build-pipeline/stage-ordering/)
- Typed HIR contract: [Type-system pass contract](/platform-spec/compiler/semantic-pipeline/type-system-pass-contract/)
- Staged rule ordering (non-type): [Rules pipeline contract](/platform-spec/compiler/semantic-pipeline/rules-pipeline-contract/)

## Conformance tests

| Evidence | Location | What it proves |
| --- | --- | --- |
| Lower-spine type codes via prepare | `compiler/crates/beskid_tests/src/analysis/type_check_diagnostics.rs` | `prepare_compilation_diagnostics` still emits stable `E12xx` codes after type-check consolidation |
| Issue kind → code mapping | `compiler/crates/beskid_tests/src/analysis/diagnostics.rs` | `SemanticIssueKind::code()` strings unchanged |
| Lower integration typing | `compiler/crates/beskid_tests/src/analysis/types.rs` | `TypeError` shapes and lower helper behavior |
| Semantic structural rules | `compiler/crates/beskid_tests/src/analysis/pipeline/core.rs` | Non-type semantic diagnostics (resolve, control flow, visibility) |

Tests in **`type_check_diagnostics.rs`** assert **diagnostic code sets only**. They **must not** assert relative ordering of `semantic.*` vs `lower.*` observer phases—ordering may change when mods run or when diagnostics are collected during prepare.

## Manual verification

```bash
cd compiler && CARGO_INCREMENTAL=0 cargo test -p beskid_tests analysis::type_check_diagnostics
```

With pipeline tracing enabled, observers **should** show `lower.type_check` during prepare; they **must not** treat a nested `semantic.type_check` observation (if still emitted for structural work) as a second authoritative type pass.