Skip to content

Commit ed70c54

Browse files
hyperpolymathclaude
andcommitted
fix(parser): #558 — honest-reject removed assume(...); fix misnamed fixture
#558's premise is stale. Refinement/dependent types — and the `T where (P)` and `assume(predicate)` forms — were REMOVED 2026-04-10 (spec.md §711-713, §1849). `TRefined` does not exist in the AST and refinement syntax PARSE-ERRORS today; there is no silent-accept / accepts-wrong-program path, so this is not the live soundness hole the issue describes. The genuine residual defects are honesty ones: 1. The `ASSUME` keyword token was left dangling (no production) by the grammar removal, so `assume(...)` surfaced a cryptic generic parse error. Add a conflict-free honest-rejection production (ASSUME is a fresh token — zero new LR conflicts, verified: 68 s/r + 7 r/r unchanged) that raises a deliberate, named error pointing at the removed feature (CORE-05 deferred). 2. test/e2e/fixtures/refinement_types.affine contained only generic functions (no refinement, no `where`) yet produced a green "refinement_types" test — false coverage. Rename to generic_functions.affine + test_parse_generic_functions, and correct its header comment. NOT done here (out of scope / non-viable): - The refinement TYPE form `T where (P)` cannot be honestly fenced without regressing trait where-clauses: the shared `WHERE` token forces a shift/reduce decision before the predicate is visible (menhir resolves it by shifting into the refinement, breaking `fn f() -> T where C`). It still surfaces a generic parse error. - The doc-lies (CAPABILITY-MATRIX.adoc "TRefined parses", STATE/TECH-DEBT CORE-05 rows) are owner-only edits (strict SPDX-header pre-commit gate on .adoc/.md); flagged for manual reconciliation. - Dead error codes E0305/W0701 left in place (harmless; removal is churn). New tests (test/test_e2e.ml, "E2E Parse"): - generic_functions → parses (renamed, honest coverage) - assume() honest-rejection (#558) → deliberate parse error (negative) Full suite 452/452 green. Refs #558 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 9bf8d57 commit ed70c54

5 files changed

Lines changed: 60 additions & 10 deletions

File tree

lib/parser.mly

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1107,6 +1107,23 @@ expr_primary:
11071107
| UNSAFE LBRACE ops = list(unsafe_op) RBRACE
11081108
{ ExprUnsafe ops }
11091109

1110+
/* #558: `assume(predicate)` is the removed refinement-assertion form
1111+
(spec.md §830; refinement / dependent types were removed 2026-04-10,
1112+
CORE-05 deferred post-v1). The `ASSUME` keyword token had no production,
1113+
so it surfaced a cryptic generic parse error. Reject it honestly and
1114+
deliberately instead — the predicate is parsed only so the error can
1115+
point at it, never enforced (there is no silent-accept path). The
1116+
refinement TYPE form `T where (P)` cannot be given the same fence without
1117+
regressing trait where-clauses (the shared `WHERE` token forces a
1118+
shift/reduce decision before the predicate is visible), so it still
1119+
surfaces a generic parse error. */
1120+
| ASSUME LPAREN expr RPAREN
1121+
{ raise (Parser_errors.Parse_action_error
1122+
("refinement assertion `assume(...)` is not supported in v1: \
1123+
refinement and dependent types were removed 2026-04-10 (CORE-05 \
1124+
is deferred post-v1); the predicate is parsed but never enforced. \
1125+
Refs #558.", $startpos, $endpos)) }
1126+
11101127
/* expr_record_body / expr_record_rest: recursive parse of `{ f:v, ..spread }`
11111128
record expressions. Spread is lexed as ROW_VAR when it is a bare
11121129
identifier (e.g. `..record`), or starts with DOTDOT when it is an
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// SPDX-FileCopyrightText: 2026 hyperpolymath
3+
//
4+
// Issue #558 (honest-rejection). `assume(predicate)` is the removed
5+
// refinement-assertion form (CORE-05 deferred post-v1). The parser must reject
6+
// it with a deliberate, named error — not a cryptic generic parse error — and
7+
// must never silently accept it.
8+
fn f(x: Int) -> Int {
9+
assume(x > 0);
10+
x
11+
}
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// End-to-end test: generic function parsing (type parameters).
3+
// Renamed from refinement_types.affine (#558): the fixture exercises generic
4+
// functions, not refinement types — refinement/dependent types were removed
5+
// 2026-04-10. It contains no `where` clause and no refinement predicate.
6+
7+
fn identity[T](x: T) -> T = x;
8+
9+
fn apply[T, U](f: (T) -> U, x: T) -> U = f(x);

test/e2e/fixtures/refinement_types.affine

Lines changed: 0 additions & 7 deletions
This file was deleted.

test/test_e2e.ml

Lines changed: 23 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -173,13 +173,32 @@ let test_parse_dependent_types () =
173173
(* 1 type decl + 3 functions *)
174174
Alcotest.(check int) "declaration count" 4 (List.length prog.prog_decls)
175175

176-
let test_parse_refinement_types () =
177-
match parse_fixture (fixture "refinement_types.affine") with
176+
let test_parse_generic_functions () =
177+
(* Renamed from test_parse_refinement_types (#558): the fixture exercises
178+
generic functions, not refinement types (which were removed 2026-04-10
179+
and never parsed silently). *)
180+
match parse_fixture (fixture "generic_functions.affine") with
178181
| Error msg -> Alcotest.fail msg
179182
| Ok prog ->
180183
Alcotest.(check bool) "has declarations" true
181184
(List.length prog.prog_decls > 0)
182185

186+
let test_parse_assume_rejected () =
187+
(* #558 honest-rejection: `assume(predicate)` (the removed refinement-assert)
188+
must fail with a deliberate, named parse error, never be silently
189+
accepted. *)
190+
match parse_fixture (fixture "assume_rejected.affine") with
191+
| Ok _ ->
192+
Alcotest.fail
193+
"expected `assume(...)` to be rejected (Refs #558); got Ok — the \
194+
removed refinement-assertion form is being silently accepted"
195+
| Error msg ->
196+
let mentions s =
197+
try ignore (Str.search_forward (Str.regexp_string s) msg 0); true
198+
with Not_found -> false in
199+
Alcotest.(check bool) "error names the assume/refinement rejection" true
200+
(mentions "assume" || mentions "refinement")
201+
183202
let test_parse_traits () =
184203
match parse_fixture (fixture "traits.affine") with
185204
| Error msg -> Alcotest.fail msg
@@ -251,7 +270,8 @@ let parse_tests = [
251270
Alcotest.test_case "arithmetic" `Quick test_parse_arithmetic;
252271
Alcotest.test_case "affine_basic" `Quick test_parse_affine_basic;
253272
Alcotest.test_case "dependent_types" `Quick test_parse_dependent_types;
254-
Alcotest.test_case "refinement_types" `Quick test_parse_refinement_types;
273+
Alcotest.test_case "generic_functions" `Quick test_parse_generic_functions;
274+
Alcotest.test_case "assume() honest-rejection (#558)" `Quick test_parse_assume_rejected;
255275
Alcotest.test_case "traits" `Quick test_parse_traits;
256276
Alcotest.test_case "effects" `Quick test_parse_effects;
257277
Alcotest.test_case "ownership" `Quick test_parse_ownership;

0 commit comments

Comments
 (0)