Repository navigation
soundness: refinement-type predicates parse but are silently not enforced (TRefined) #558
Description
TRefined predicates parse and are then silently NOT enforced (CAPABILITY-MATRIX.adoc:138-139 'parse-only'; TECH-DEBT CORE-05 row, no prior issue). A user's refinement annotation today is a false assurance — accepts-wrong-program class. v1 options: (a) enforce via predicate reduction (CORE-05 proper, large), or (b) LOUD-REJECT TRefined at typecheck until enforcement exists (cheap, honest). Recommend (b) now, (a) post-v1. Same silent-vs-loud principle as #555/#556. Part of the v1-readiness T0 tier.
Activity
docs: truth-refresh after CORE-01 closure + 2026-06-11 survey — matri…
docs: truth-refresh after CORE-01 closure + 2026-06-11 survey — matri…
docs: truth-refresh after CORE-01 closure + 2026-06-11 survey (matrix…
docs: consolidated session overview — migration corpus + string/float…
hyperpolymath commentedon Jun 14, 2026
Premise is stale — this is not a live soundness hole.
Investigation (see #598):
TRefineddoes not exist in the AST, and refinement/dependent types —T where (P)andassume(predicate)— were removed 2026-04-10 (spec.md§711–713, §1849). Refinement syntax parse-errors today; there is no silent-accept / accepts-wrong-program path, so the "parse but silently not enforced" framing no longer applies.The genuine residual defects are honesty ones:
assume(...)was a dangling keyword token → cryptic parse error; now honest-rejected with a deliberate, named error (conflict-free — zero new LR conflicts).refinement_types.affinetested only generic functions (false "refinement" coverage) → renamedgeneric_functions.affine.CAPABILITY-MATRIX.adoc("TRefinedparses"),STATE/TECH-DEBTCORE-05 rows — still claim parse-only enforcement. These need manual SPDX-gated edits (the strict.adoc/.mdpre-commit owner-header check blocks automated edits).T where (P)honest-rejection would regress trait where-clauses (sharedWHEREtoken → shift/reduce resolved by shifting into the refinement). It still surfaces a generic parse error.Recommendation: reframe from "soundness (T0)" to "doc-truthing + hygiene"; close after the doc reconciliation (item 3).
fix(parser): #558 — honest-reject removed assume(...); fix misnamed f…
hyperpolymath commentedon Jun 14, 2026
Closing per owner direction.
Resolved (#598):
assume(...)is now honest-rejected (the dangling-token defect), and the misnamedrefinement_types.affinefixture — which actually tested generic functions — was corrected togeneric_functions.affine. The original "parse but silently not enforced" premise was stale: refinement/dependent types were removed 2026-04-10, so the syntax parse-errors — there was never a silent-accept / accepts-wrong-program path.Remaining (owner-only, outside this issue): the doc rows that still claim parse-only enforcement —
CAPABILITY-MATRIX.adoc("TRefinedparses"),STATE/TECH-DEBTCORE-05 — need manual SPDX-gated.adocedits (the strict pre-commit owner-header check blocks automated changes).T where (P)honest-rejection remains non-viable (would regress trait where-clauses via the sharedWHEREtoken).docs: author the proof-needs inventory (P-/F-/K- obligation series) (#…
docs: make soundness status a single, test-anchored source of truth (#…