Quartz v5.25

Next Session — Maranget Pattern Exhaustiveness Checker

Baseline: ef169d31 (trunk, clean, fixpoint 1991 functions) Plan file: .claude/plans/abstract-herding-gizmo.md Estimated effort: ~5 hours (quartz-time)

Handoff Prompt (copy-paste to start next session)

Read the implementation plan at `.claude/plans/abstract-herding-gizmo.md` and execute it. This is a 7-phase implementation of a Maranget-based pattern match exhaustiveness checker for the Quartz compiler.

Summary: Replace the flat ad-hoc `tc_check_exhaustiveness` in `self-hosted/middle/typecheck_match.qz:364-654` with a proper pattern matrix algorithm based on Maranget (2007) "Warnings for pattern matching" — the same algorithm used by Rust, OCaml, and every production compiler. The new checker handles nested patterns, generates witness patterns for error messages ("missing: `Some(Err(_))`"), detects unreachable arms, and treats guards conservatively.

The plan has 7 phases:
0. Data structures (DeconstructedPat, PatStack, PatMatrix, constructor tags)
1. Constructor helpers (equality, arity, type enumeration)
2. AST → DeconstructedPat conversion (all NODE_* pattern types)
3. Core algorithm (specialize, default matrix, usefulness)
4. Witness generation (human-readable missing pattern display)
5. Integration (replace tc_check_exhaustiveness, retain legacy as fallback)
6. Tests + cleanup (17+ new tests, remove legacy)

Key constraints:
- All new code in `self-hosted/middle/typecheck_match.qz`
- Call site at `typecheck_expr_handlers.qz:1036` unchanged
- Error code QZ0107 for non-exhaustive (existing), QZ0108 for unreachable arms (new warning)
- `quake guard` mandatory after Phase 5 (compiler source changes)
- Existing `match_exhaustiveness_spec.qz` tests must not regress
- The compiler must compile itself at every phase

Prime Directives:
1. World-class only — Maranget algorithm, not ad-hoc
2. Design before building — plan is approved, execute it
3. No holes left behind — nested patterns, guards, redundancy all addressed
4. Report reality — guards are undecidable, treated conservatively
5. Binary discipline — quake guard before every commit touching self-hosted/*.qz
6. Delete freely — the old tc_check_exhaustiveness dies in Phase 6

Tree is clean at ef169d31, guard stamp valid, smoke green. Execute the plan phase by phase with commits after each phase.

Context for the implementing session

What exists now (typecheck_match.qz:364-654)

  • Flat variant counting: builds covered[] array, marks variants as covered, reports first uncovered
  • Special cases for Bool (true/false), Result (Ok/Err), Union types
  • Wildcard early-exit: any _ pattern → skip all checks
  • ~290 lines, handles only top-level patterns
  • Cannot do: nested patterns, guard interaction, redundancy, witness generation

What we’re building

A pattern matrix algorithm with:

  • DeconstructedPat: pattern = constructor + sub-patterns (recursive)
  • PatMatrix: rows of patterns, one per match arm
  • mx_specialize(ctor, matrix): filter rows compatible with constructor
  • mx_default(matrix): keep wildcard rows, drop column 0
  • mx_is_useful(matrix, query): core recursive function
  • Witness generation: build example patterns of what’s missing
  • Redundancy: check each arm against prior arms

Research sources

Key APIs already available

  • tc_lookup_enum(tc, name) → Found(idx) or NotFound
  • tc_enum_variant_names(tc, idx) → Vec
  • tc_enum_variant_payload_count(tc, enum_name, variant_name) → Int
  • tc_error(tc, msg, line, col) / tc_warning(tc, msg, line, col)
  • assert_compile_error(source, expected) / assert_compile_warning(source, expected) in qspec