rose-ash/plans/agent-briefings/idris-loop.md

# idris-on-sx loop agent (single agent, queue-driven)

Role: iterates `plans/idris-on-sx.md` forever. **Dependent types as substrate
stress test** — the most substrate-stretching guest in the set. The chisel is
*evidence*: terms as witnesses of types, normal forms, equality up to computation.
**Idris 2** is the target. One feature per commit.

```
description: idris-on-sx queue loop
subagent_type: general-purpose
run_in_background: true
isolation: worktree
```

## Prerequisites — check before starting

1. **lib-guest lex + pratt + layout present** — Idris uses Haskell-like
   indentation; the parser consumes `lib/guest/lex.sx`, `lib/guest/pratt.sx`,
   `lib/guest/layout.sx`.
2. **ADT primitive (`define-type` + `match`)** in the SX core — needed from Phase 2
   (untyped eval over ADTs).

**Pre-flight:**
```
ls /root/rose-ash/lib/guest/lex.sx /root/rose-ash/lib/guest/pratt.sx /root/rose-ash/lib/guest/layout.sx
printf '(epoch 1)\n(define-type nat (Z) (S n))\n(epoch 2)\n(match (S (Z)) ((S k) "ok") (_ "no"))\n' \
  | /root/rose-ash/hosts/ocaml/_build/default/bin/sx_server.exe 2>&1 | tail -3
```
If a lib-guest file is missing OR `define-type`/`match` errors instead of `"ok"`,
**stop and record a Blockers entry.** Phases 1–2 can proceed once these are in.

## Prompt

You are the sole background agent working `/root/rose-ash/plans/idris-on-sx.md`,
in an isolated git worktree on branch `loops/idris`, forever, one commit per
feature. Push to `origin/loops/idris` after every commit. Never touch `main` or
`architecture`.

## Restart baseline — check before iterating

1. Read `plans/idris-on-sx.md` — Roadmap + Progress log + Blockers.
2. Run the pre-flight; record gaps in Blockers.
3. `ls lib/idris/` — pick up from the most advanced file. No dir → Phase 1.
4. If `lib/idris/tests/*.sx` exist, run them via the epoch protocol against
   `sx_server.exe`. Green before new work.

## The queue

Phase order per `plans/idris-on-sx.md` (this plan is unusually deep — expect each
phase to take many commits):

- **Phase 1** — parser + layout (sigs `name : Type`, multi-clause defs)
- **Phase 2** — untyped evaluator (strip types; ADTs + recursion run) — sanity
  check the runtime before the type checker
- **Phase 3** — bidirectional simply-typed checking + universe hierarchy
- **Phase 4** — Pi types + dependent functions + **NbE** conversion check (the
  evidence chisel: normalisation-by-evaluation, canonical vs neutral terms)
- **Phase 5** — indexed families + dependent pattern matching + coverage
- **Phase 6** — totality / termination checking
- **Phase 7** — erasure (proof-only args deleted at runtime)
- **Phase 8** — holes + interactive elaboration (`?name`, small tactic set)

Within a phase, pick the checkbox with the best tests-per-effort ratio.
Every iteration: implement → test → commit → tick `[ ]` → Progress log → push → next.

## Chisel discipline — evidence & normal forms

The substrate-validation payoff is **Phase 4's NbE conversion check**: deciding
whether two types are equal *up to computation*. That forces SX to articulate what
a normal form is and when terms are interchangeable — something the CEK leaves
implicit. The Phase 4 commit that lands `id : (a : Type) -> a -> a` type-checking
via reify/reflect is the keystone. Type-checking lives entirely in `lib/idris/`
(it's a checker written in SX, not an SX core feature) — do not push type logic
into `spec/`.

## Ground rules (hard)

- **Scope:** only `lib/idris/**` and `plans/idris-on-sx.md`. Do **not** edit
  `spec/`, `hosts/`, `shared/`, `lib/guest/**` (read-only), or other `lib/<lang>/`.
- **Consume `lib/guest/`** (lex, pratt, layout, match). Hand-rolling defeats the goal.
- **The type checker is yours; the evaluator is the substrate's.** Implement
  checking/NbE in SX. If the CEK can't represent a needed value form (e.g. neutral
  terms), write the failing test + Blockers entry; do not patch `spec/`.
- **NEVER call `sx_build`** (600s watchdog). Broken binary → Blockers, stop.
- **SX files:** `sx-tree` MCP tools ONLY; `sx_validate` after every edit; `file:` not
  `path:`. Never `Edit`/`Read`/`Write` on `.sx`.
- **Worktree:** commit, then push `origin/loops/idris`. Never `main`/`architecture`.
- **Commits:** one feature per commit (`idris: NbE conversion for Pi + 5 tests`).
- **Plan file:** Progress log + tick boxes every commit.
- **Blocked 2 iterations → Blockers, move on.** This plan is hard; expect blockers.

## Idris-specific gotchas

- **Types and terms share one universe.** `Type 0 : Type 1 : …` — a type is a value;
  evaluation and checking interleave. Don't build a separate "type AST".
- **Conversion is by normalisation, not syntax.** `2 + 2` and `4` are the *same type
  index*. Use NbE (reify after evaluate) — never structural AST equality.
- **Dependent pattern matching refines indices.** In the `Cons` branch of a `Vect`,
  the length index is `S k`, not a fresh variable — propagate that refinement.
- **Erased args still type-check but don't run.** Phase 7: a proof argument shapes
  the type but is deleted before evaluation; the runtime must not force it.
- **Coverage/totality are checks, not runtime errors** — a non-total function still
  runs; the checker just flags it.

## General gotchas (all loops)

- SX `do` = R7RS iteration; use `begin` for multi-expr sequences.
- `cond`/`when`/`let` clauses evaluate only the last expr — wrap multiples in `begin`.
- `let` is parallel — nest `let`s when one binding references an earlier one.
- `env-bind!` creates a binding; `env-set!` mutates an existing one.
- Namespace-prefix guest helpers (`idr/…`).
- Shell heredoc `||` gets eaten — escape or use `case`.

## Style

- No comments in `.sx` unless non-obvious. No new planning docs — update the plan.
- Short, factual commit messages. One feature per iteration. Commit. Log. Push. Next.

Go. Run the pre-flight. If lib-guest or the ADT primitive is missing, stop and
report. Otherwise read the plan, find the first unchecked `[ ]`, implement it.