Skip to content

typecheck: Copy classification + move tracking (RFC 0001 Phase 1)#71

Merged
proofmancer merged 1 commit into
mainfrom
typecheck/copy-classification-and-move-tracking
May 25, 2026
Merged

typecheck: Copy classification + move tracking (RFC 0001 Phase 1)#71
proofmancer merged 1 commit into
mainfrom
typecheck/copy-classification-and-move-tracking

Conversation

@proofmancer
Copy link
Copy Markdown
Member

Lands Phase 1 of the RFC 0001 (memory model) implementation roadmap: type-system support for distinguishing `Copy` from non-`Copy` types, and move tracking that errors on use-after-move for non-`Copy` bindings.

Per the RFC, Phase 1 is the low-risk infrastructure: even if the final memory model is not full Rust-style ownership, type-level `Copy` classification and move tracking are useful and uncontroversial. Lands now; subsequent phases (grammar extensions, codegen heap, stdlib types, `extern host` ABI) can build on top.

What landed

Type-system API

New public function in `typecheck.h`:

```c
int type_is_copy(const Type *t);
```

Classification:

  • Primitives (u8..u256, i8..i64, bool, char, str) -> Copy
  • Unit `()` -> Copy
  • Function types -> Copy (the reference, not the body)
  • Unknown -> permissively Copy (avoid spurious diagnostics on unresolved names)
  • Generic-head aggregates (`Result`, `Vec`, etc.) -> NOT Copy

Move tracking

Each `ScopeEntry` gains a `moved` flag. Three new internal helpers in `typecheck.c`:

  • `scope_lookup_mut` (mutable variant of `scope_lookup`)
  • `scope_mark_moved` (no-op for Copy types or already-moved bindings)
  • `scope_is_moved` (read for the use-after-move check)

Enforcement points:

  • `AST_EXPR_IDENT`: reading a non-Copy binding that's been moved -> `"use of moved value 'x'"` diagnostic
  • `check_call`: each argument that's a bare identifier of a non-Copy type marks the source as moved (after type-checking the read)
  • `check_let`: `let y = x` moves x if non-Copy
  • `check_return`: returning a non-Copy value moves it out of the function

Tests

6 new typecheck tests (52 assertions total, was 34):

  • `test_copy_type_can_be_used_repeatedly`: `let x: u64 = 42; let y = x; let z = x` is fine
  • `test_non_copy_use_after_move_in_let_errors`: `let r: Result = make(); let y = r; let z = r` errors with `"use of moved value 'r'"`
  • `test_non_copy_use_after_move_via_call_errors`: passing `r` to a fn then reading it errors
  • `test_non_copy_single_use_is_fine`: moving once works; only the second use errors
  • `test_copy_after_move_irrelevant`: `u64` is Copy so all use patterns are fine even after looking syntactically like a move
  • `test_type_is_copy_classification`: direct API check

Existing tests

All 5 binaries still green (497 -> 503 assertions total). Existing examples (`counter-mvp.cv`, `minimal-chain.cv`) type-check unchanged: they use only Copy types and see no move-tracking diagnostics.

What this PR does NOT do

  • No grammar changes. `&T` references, `#[derive(Copy)]` attributes, and `impl Drop for ...` blocks land in Phase 2.
  • No codegen changes. Heap allocation and drop emission land in Phase 3. The classification today only affects type-checking diagnostics; runtime behavior is unchanged.
  • No stdlib types. `Vec`, `String`, `HashMap`, `Bytes` land in Phase 4. The non-Copy demonstration in tests uses `Result` (a TY_GENERIC) which already exists in the type checker as an opaque aggregate.
  • No borrow tracking. `&T` and `&mut T` semantics, the borrow checker, and shared-XOR-exclusive enforcement land later in Phase 1 once references exist in the grammar.

Reversibility

High. If RFC 0001 lands on per-tx arena instead of full ownership, this code stays valuable: arena-allocated types still benefit from a Copy classification and from "do not use a moved value" diagnostics. The cost of this PR is the small typecheck.c additions and the public `type_is_copy` API; reverting either is straightforward.

What unblocks next

  • Phase 2 (grammar + AST) can land independently: `&T` type expressions, `#[derive]` attribute syntax, `impl Trait for Type` blocks
  • The position paper Paper: design sketch / position paper for arxiv (defer active drafting) #67 can cite a real, shipped implementation of the linearity foundation rather than just RFC text
  • Subsequent phases can iterate on this Phase 1 foundation without restarting the typecheck design

@proofmancer proofmancer merged commit 52f4430 into main May 25, 2026
2 checks passed
@proofmancer proofmancer deleted the typecheck/copy-classification-and-move-tracking branch May 25, 2026 17:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant