A2ML normative Idris2 core: A2ML.Parser does not type-check (16 errors) — blocks the core CI gate

[hyperpolymath]

Blocks: a CI gate on the normative Idris2 core, and (transitively) the A2ML dialect factory.

Context

SPEC.adoc §3.1 declares src/A2ML/ normative and authoritative. #555 adds the missing a2ml-core.ipkg and repairs A2ML.Proofs (which failed outright), so the core is now type-checkable — except A2ML.Parser, which is the last blocker. Until it builds we cannot add a CI gate without landing a red required check.

Measured inventory (idris2 0.7.0, idris2 --typecheck a2ml-core.ipkg)

16 errors, all in A2ML.Parser:

Count	Kind
7	When unifying: — type mismatches in peek, char, charIs, skipWhitespace, parseParagraph, parseSection, parseBlock
6	Totality failures under %default total — parseDocument, parseBlocks, parseHeading, parseHeading,countHashes, prettyPrint, prettyPrint,prettyBlock
1	`Undefined name … <
1	Name A2ML.TypedCore.collectIds is private — used from parseAndValidate

Everything else in the core type-checks: TypedCore, Surface, Proofs confirmed (Idris2 only proceeds to build Parser once its dependencies succeed).

Why it matters beyond a red build

A2ML.Parser is the scm/markup dialect front-end — the primary dialect. The plan is one normative core with per-dialect (parser, printer) pairs (Converters.idr already emits Markdown/HTML/Djot/LaTeX/PlainText from Doc). A broken primary parser blocks that factory, and blocks promoting the round-trip checks from Bool tests to proofs.

Note testMarkdownRoundTrip currently compares only length (blocks doc), so it would pass on wrong content — worth strengthening to a propositional round-trip law once the parser builds.

Suggested order

1. Fix the 7 unification errors (likely a parser-combinator type that drifted).
2. Supply <|> (define the Alternative instance for the parser type, or import it).
3. Export TypedCore.collectIds, or move parseAndValidate into TypedCore.
4. Resolve the 6 totality failures — add assert_total only where genuinely justified with a comment, or restructure to a fuel/well-founded recursion. Do not silence them wholesale; %default total is doing real work here.
5. Land the CI gate: idris2 --typecheck a2ml-core.ipkg, a required check, with a pinned Idris2 (0.7.0 locally). Use the ipkg target, never per-file --check (which exits 0 on a missing module — a fake gate).

Related

Same estate shape as the trope-checker Idris2 core (does not compile on 0.7.0, hidden behind a continue-on-error + skip-if-absent gate). Worth pinning one Idris2 across the estate.