SafeRegex/Matcher.idr blocks the build at 211/305 — diagnosed, four classes, file is untracked

[hyperpolymath]

The build frontier now reaches 211/305 (Idris2 0.7.0, measured on the local uncommitted working
tree). The blocker is src/Proven/SafeRegex/Matcher.idr, fully diagnosed but not fixed.

BUILD_RC=1
frontier: 211/305: Building Proven.SafeRegex.Matcher
errors: 16   shadow: 0
Error: While processing right hand side of matchCharClass. Undefined name matchesClassWithFlags.
Error: ... Undefined name Proven.SafeRegex.Matcher.5468:5311:matchQuantified.
Error: findAll is not total, possibly not terminating due to call to ...findFrom
Error: findFirst is not total, possibly not terminating due to call to ...findFrom
Error: match is not total, possibly not terminating due to call to ...findFirst

Four distinct classes, all with known cures

Line	Class	Cure
127	28 — top-level forward reference	Hoist the signature only above the use site, then delete the late signature.
133	36 — rename retargeted SingleChar to the Prelude's Char	CharClass's constructor is SingleChar (Types.idr:24). Safe seds: (Char ' and (Char c. ⚠ (Char alone is UNSAFE — it matches the type.
—	32 — where attaches to ONE clause	The mangled name Matcher.5468:5311:matchQuantified is the tell.
—	totality	3 roots: findFrom → findFirst → match/findAll. Thread internal fuel; only a mutual block needs an explicit Nat.

Class 36 reports Mismatch between: Type and Char -> CharClass — never Undefined name —
so grepping for undefined names will not find it.

⚠ This file is also untracked

f2833c2c deleted it and it was restored to the working tree but never re-added to git
(see the sibling issue). The fix must include git add of the file, or the cure lands
nowhere. Parser.idr in the same directory hit exactly this and is now re-tracked by PR #206.

Sources, both snippets, and the full class catalogue: docs/IDRIS2-BUILD-WORK-PACKAGE.adoc §3–§4.

Idris2 0.7.0; source/CI target 0.8.0. The error count is not a progress metric — the frontier is.