Follow-up to #558 (closed) / #598.
#558's premise was stale — refinement/dependent types were removed 2026-04-10, so refinement syntax parse-errors (no silent-accept path). #598 landed the code-side honest-rejection (assume(...)) + the misnamed-fixture fix. This issue tracks the remaining doc reconciliation, which is owner-only: the strict pre-commit SPDX / literal-owner-header check gates .adoc/.md edits, so automated changes are blocked (and --no-verify must not be used — the hook is a load-bearing LLM-attribution-drift detector).
Stale claims to correct
docs/CAPABILITY-MATRIX.adoc (~line 152): "TRefined parses; predicates do not reduce; no SMT" — false. TRefined does not exist; T where (P) and assume(...) parse-error today. Should read: refinement types unsupported (grammar removed 2026-04-10; CORE-05 deferred post-v1).docs/STATE-2026-*.adoc CORE-05 row(s): "parse-only" → "removed / deferred post-v1".docs/TECH-DEBT.adoc (CORE-05 row): same reconciliation.
Non-goals / notes
T where (P) parser-level honest-rejection is non-viable — the shared WHERE token forces a shift/reduce that menhir resolves by shifting into the refinement, regressing trait where-clauses (fn f() -> T where C). It remains a generic parse error by design; do not add a grammar production for it.- Optional low-priority hygiene: dead error codes
E0305 / W0701 (defined in lib/error.ml, never constructed) could be removed.
Why this is owner-only
The .adoc files need the owner's SPDX + literal-owner header to pass the strict pre-commit gate; these are manual owner edits, same constraint that parked the #554 doc prose.
Follow-up to #558 (closed) / #598.
#558's premise was stale — refinement/dependent types were removed 2026-04-10, so refinement syntax parse-errors (no silent-accept path). #598 landed the code-side honest-rejection (
assume(...)) + the misnamed-fixture fix. This issue tracks the remaining doc reconciliation, which is owner-only: the strict pre-commit SPDX / literal-owner-header check gates.adoc/.mdedits, so automated changes are blocked (and--no-verifymust not be used — the hook is a load-bearing LLM-attribution-drift detector).Stale claims to correct
docs/CAPABILITY-MATRIX.adoc(~line 152): "TRefinedparses; predicates do not reduce; no SMT" — false.TRefineddoes not exist;T where (P)andassume(...)parse-error today. Should read: refinement types unsupported (grammar removed 2026-04-10; CORE-05 deferred post-v1).docs/STATE-2026-*.adocCORE-05 row(s): "parse-only" → "removed / deferred post-v1".docs/TECH-DEBT.adoc(CORE-05 row): same reconciliation.Non-goals / notes
T where (P)parser-level honest-rejection is non-viable — the sharedWHEREtoken forces a shift/reduce that menhir resolves by shifting into the refinement, regressing trait where-clauses (fn f() -> T where C). It remains a generic parse error by design; do not add a grammar production for it.E0305/W0701(defined inlib/error.ml, never constructed) could be removed.Why this is owner-only
The
.adocfiles need the owner's SPDX + literal-owner header to pass the strict pre-commit gate; these are manual owner edits, same constraint that parked the #554 doc prose.