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.
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.