Full type checker implementation

.agents/skills/type-checker-tests/SKILL.md

@@ -0,0 +1,136 @@
+---
+name: type-checker-tests
+description: Add integration tests for type checker inference and checking2 functions
+allowed-tools: Bash(mkdir:*)
+---
+
+# Type Checker Integration Tests
+
+Use the command reference at `reference/compiler-scripts.md` for test runner syntax, snapshot workflows, filters, and trace debugging. The category is `checking2`.
+
+**Language:** Fixtures use PureScript syntax, not Haskell.
+
+## Creating a Test
+
+### 1. Create fixture directory
+
+```bash
+just t checking2 --create "descriptive name"
+```
+
+The CLI picks the next fixture number and creates the folder.
+
+Tests are auto-discovered by `build.rs`.
+
+### 2. Write Main.purs
+
+**Standard pattern** - pair typed (checking2) and untyped (inference) variants:
+
+```purescript
+module Main where
+
+-- Checking mode: explicit signature constrains type checker
+test :: Array Int -> Int
+test [x] = x
+
+-- Inference mode: type checker infers unconstrained
+test' [x] = x
+```
+
+**Guidelines:**
+- Test ONE specific behavior per fixture
+- Name tests: `test`, `test'`, `test2`, `test2'`, etc.
+- Include edge cases relevant to the behavior
+
+### 3. Run and review
+
+```bash
+just t checking2 NNN MMM
+```
+
+### 4. Accept or reject snapshots
+
+```bash
+just t checking2 NNN --diff        # Inspect a fixture diff
+just t checking2 NNN --accept      # Accept a specific fixture
+just t checking2 NNN --reject      # Reject a specific fixture
+just t checking2 --accept --confirm # Accept all pending snapshots
+```
+
+## Multi-File Tests
+
+For imports, re-exports, or cross-module behavior:
+
+```
+tests-integration/fixtures/checking2/NNN_import_test/
+├── Main.purs    # Test file (snapshot generated)
+├── Lib.purs     # Supporting module
+└── Main.snap    # Generated snapshot
+```
+
+**Lib.purs:**
+```purescript
+module Lib where
+
+life :: Int
+life = 42
+
+data Maybe a = Just a | Nothing
+```
+
+**Main.purs:**
+```purescript
+module Main where
+
+import Lib (life, Maybe(..))
+
+test :: Maybe Int
+test = Just life
+```
+
+- Module name must match filename
+- Only `Main.purs` generates a snapshot
+
+## Snapshot Structure
+
+```
+Terms
+functionName :: InferredOrCheckedType
+...
+
+Types
+TypeName :: Kind
+...
+
+Errors
+ErrorKind { details } at [location]
+```
+
+## Acceptance Criteria
+
+Before accepting, verify:
+
+1. **Types are correct**
+   - `test :: Array Int -> Int` - signature preserved
+   - `test' :: forall t. Array t -> t` - polymorphism inferred
+
+2. **No unexpected `???`**
+   - `test :: ???` - STOP: inference failure
+   - `CannotUnify { ??? -> ???, Int }` - OK in error tests
+
+3. **Errors appear where expected**
+   - Confirm error kind matches (`NoInstanceFound`, `CannotUnify`)
+   - Verify location points to correct declaration
+
+4. **Polymorphism is appropriate**
+   - Type variables scoped correctly
+   - Constraints propagate as expected
+
+## Common Issues
+
+| Symptom | Likely Cause |
+|---------|--------------|
+| `test :: ???` | Syntax error or undefined names |
+| Unexpected monomorphism | Missing polymorphic context |
+| Wrong error location | Check binder/expression placement |
+| Missing types in snapshot | Module header or imports incorrect |

.agents/skills/type-checker-tests/reference/compiler-scripts.md

@@ -0,0 +1,67 @@
+# Compiler Scripts Command Reference
+
+CLI tools in `compiler-scripts/` for running integration tests.
+
+## Test Runner Commands
+
+### Run tests
+
+```bash
+just t <category> [filters...]         # Run tests (summary output)
+just t <category> --diff [filters...]  # Run with full inline diffs
+just t <category> --count 10 [filters...] # Show more snapshots (default: 3)
+just t <category> --debug [filters...] # Enable tracing
+just t <category> --verbose [filters...] # Show test progress
+just t <category> --create "name"  # Scaffold a new fixture
+just t <category> --delete "name"  # Dry-run fixture deletion (use --confirm)
+```
+
+### Categories
+
+| Category | Alias | Description |
+|----------|-------|-------------|
+| checking | c | Type checker tests |
+| lowering | l | Lowering tests |
+| resolving | r | Resolver tests |
+| lsp | - | LSP tests |
+
+### Snapshot commands
+
+```bash
+just t <category> [filters...] --accept             # Accept matching snapshots
+just t <category> [filters...] --reject             # Reject matching snapshots
+just t <category> --accept --confirm                # Accept all pending snapshots
+```
+
+For safety, unfiltered `--accept` requires `--confirm`.
+
+### Exclusion filters
+
+Hide snapshots ephemerally during a session:
+
+```bash
+just t <category> --exclude "pattern"              # Single exclusion
+just t <category> --exclude "foo" --exclude "bar"  # Multiple exclusions
+EXCLUDE_SNAPSHOTS="foo,bar" just t <category>      # Via environment variable
+```
+
+### Filters
+
+Space-delimited, passed through to nextest. Mix numbers and patterns:
+
+```bash
+just t c 101 102           # Run tests 101 and 102
+just t c pattern           # Filter by name pattern
+just t c 101 102 pattern   # Numbers + pattern together
+```
+
+## Debugging Traces
+
+When `--debug` is used, traces are written to `target/compiler-tracing/{test_id}_{module}.jsonl`.
+
+```bash
+wc -l target/compiler-tracing/*.jsonl              # Check sizes
+shuf -n 20 target/compiler-tracing/NNN_*.jsonl | jq .  # Sample
+jq 'select(.level == "DEBUG")' file.jsonl          # Filter by level
+jq 'select(.target | contains("unification"))' file.jsonl
+```

.claude/skills

@@ -0,0 +1 @@
+../.agents/skills