feat(typing): fix panics and add type annotation checking

- Replace panic on string literals with TypeError::UnallocatedStringLiteral
- Add TypeError::AnnotationMismatch for let/let_lin type annotations
- check_let and check_let_lin now verify declared types match inferred
- Add 21 new tests covering pairs, sums, regions, functions, copy/drop,
  modules, arithmetic, and type annotation validation (10 -> 31 total)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: Jonathan D.A. Jewell

STATE.scm

@@ -6,36 +6,132 @@
      (version "1.0")
      (schema-version "1.0")
      (created "2026-02-04")
-     (updated "2026-02-04")
+     (updated "2026-02-06")
      (project "ephapax")
      (repo "hyperpolymath/ephapax"))
 
     (project-context
-     (name "ephapax")
-     (tagline "TODO: Add project description")
-     (tech-stack ()))
+     (name "Ephapax")
+     (tagline "Linear type system with once-only evaluation and formal Coq proofs")
+     (tech-stack ("rust" "idris2" "coq" "zig")))
 
     (current-position
-     (phase "development")
-     (overall-completion 0)
-     (components ())
-     (working-features ()))
+     (phase "type-checker-and-wasm")
+     (overall-completion 55)
+     (components
+       (("lexer" "Tokenization with logos (736 LOC)" 100)
+        ("parser" "Full parser with chumsky (1240 LOC)" 100)
+        ("syntax" "AST definitions (328 LOC)" 100)
+        ("interpreter" "Tree-walking interpreter (832 LOC)" 100)
+        ("typing" "Type checker - in progress (1002 LOC)" 60)
+        ("wasm-backend" "WASM code generation - in progress (1219 LOC)" 40)
+        ("ir" "S-expression intermediate representation (758 LOC)" 100)
+        ("runtime" "Runtime support (211 LOC)" 80)
+        ("stdlib" "Standard library skeleton (290 LOC)" 40)
+        ("repl" "Interactive shell (398 LOC)" 100)
+        ("cli" "Command-line interface (460 LOC)" 100)
+        ("vram-cache" "VRAM caching layer (363 LOC)" 80)
+        ("coq-proofs" "Syntax, typing rules, operational semantics (619 LOC)" 100)
+        ("idris2-abi" "Experimental two-stage compiler (parser/typechecker)" 30)
+        ("zig-ffi" "C ABI compatibility layer (1620 LOC across 40 files)" 70)
+        ("ephapax-proven" "Formally verified data structures (LRU, Buffer, Resource, Queue, Set, Hex)" 90)
+        ("ephapax-proven-ffi" "Zig FFI for proven data structures" 70)
+        ("debugger" "Not started" 0)
+        ("lsp" "Not started" 0)
+        ("package-manager" "Not started" 0)))
+     (working-features
+       ("Full lexer/parser/interpreter/REPL/CLI pipeline"
+        "S-expression intermediate representation"
+        "Formal Coq proofs: syntax formalization, linear typing rules, operational semantics with soundness"
+        "Experimental Idris2 -> Rust two-stage compiler (parser/typechecker in Idris2, WASM backend in Rust)"
+        "ephapax-proven library: 6 formally verified data structures"
+        "  - LRU cache, Buffer, Resource tracker, Queue, Set, Hex encoding"
+        "  - 113 tests (45 unit + 17 integration + 51 doc)"
+        "Zig FFI layer: C ABI compatibility for proven data structures"
+        "15+ example programs (.eph files)"
+        "Conformance test suite (pass/fail directories)"
+        "VRAM caching layer for GPU-accelerated operations"
+        "12-crate Rust workspace (~7,918 LOC total)")))
 
     (route-to-mvp
      (milestones
       ((milestone-id "m1")
-       (name "Initial Setup")
-       (items ("Add project description"
-               "Define tech stack"
-               "Set up initial features")))))
+       (name "Core Language")
+       (status "complete")
+       (completion 100)
+       (items ("Lexer with logos"
+               "Parser with chumsky"
+               "AST definitions"
+               "Tree-walking interpreter"
+               "REPL and CLI"
+               "S-expression IR")))
+
+      ((milestone-id "m2")
+       (name "Formal Verification")
+       (status "complete")
+       (completion 100)
+       (items ("Coq syntax formalization (Syntax.v)"
+               "Linear typing rules (Typing.v)"
+               "Operational semantics with soundness proofs (Semantics.v)")))
+
+      ((milestone-id "m3")
+       (name "Type Checker")
+       (status "in-progress")
+       (completion 60)
+       (items ("Linear type inference engine (in progress)"
+               "Affine type tracking"
+               "Use-once enforcement"
+               "Type error reporting")))
+
+      ((milestone-id "m4")
+       (name "WASM Backend")
+       (status "in-progress")
+       (completion 40)
+       (items ("WASM code generation module (started)"
+               "Linear type lowering to WASM"
+               "Memory management for linear resources"
+               "Browser and server target support")))
+
+      ((milestone-id "m5")
+       (name "Proven Data Structures")
+       (status "in-progress")
+       (completion 90)
+       (items ("LRU cache (done)"
+               "Buffer (done)"
+               "Resource tracker (done)"
+               "Queue (done)"
+               "Set (done)"
+               "Hex encoding (done)"
+               "Rust wrappers (done)"
+               "Zig FFI bindings (done)"
+               "Full integration tests (done)")))))
 
     (blockers-and-issues
-     (critical ())
-     (high ())
-     (medium ())
-     (low ()))
+     (critical
+       ("Type checker incomplete - critical path to MVP"))
+     (high
+       ("WASM backend in early stages"
+        "Standard library is skeletal (290 LOC)"))
+     (medium
+       ("Idris2 two-stage compiler is experimental, not production-ready"
+        "No LSP server"
+        "No debugger"))
+     (low
+       ("VRAM cache needs GPU testing on real hardware")))
 
     (critical-next-actions
-     (immediate ("Update STATE.scm with project details"))
-     (this-week ())
-     (this-month ()))))
+     (immediate
+       ("Complete linear type checker with use-once enforcement"
+        "Expand type error reporting with hints"))
+     (this-week
+       ("Advance WASM code generation for basic programs"
+        "Expand standard library beyond skeleton"))
+     (this-month
+       ("Achieve end-to-end: source -> type check -> WASM output"
+        "Begin LSP server implementation"
+        "Stabilize Idris2 two-stage compiler")))
+
+    (session-history
+     ((date "2026-02-06")
+      (accomplishments
+        ("Updated STATE.scm with accurate project status from code audit"))))))