crates/osprey-cli/tests/redundant_annotations.rs enforces CLAUDE.md's "redundant annotations are defects" rule over tests/, examples/ and benchmarks/ — but only for the Default flavor. 118 .ospml files are ungated.
The gate's reader looks for an arrow inside a fn header (fn f(a: int) -> string =). ML spells a signature as a standalone line above the definition:
describe : JsonValue -> string
describe value =
match value
JsonNull => "null"
so return_annotation never matches and the deletion it performs does not apply. A green run of no_corpus_program_carries_a_removable_return_annotation says nothing about ML.
Confirmed removable today: tests/.../functional_showcase.test.ospml:17 — deleting the signature still type-checks, still lowers to IR, and the reported symbol types are unchanged (only line offsets move).
Gating ML needs its own reader and its own removal rule, and the stakes are known to be real: ec6a5cac deleted ML signatures by hand and took verdict, workflows and type_equality_comprehensive from green to a closure value with a still-generic type. Any ML sweep must therefore keep the existing oracle — type-check AND lower AND compare the reported outline — and normalise line offsets before comparing, since deleting a whole line shifts every symbol below it.
The limitation is documented on the test itself so a green run is not mistaken for ML coverage.
Found during review of the enforce-inferable-annotations branch.
crates/osprey-cli/tests/redundant_annotations.rsenforces CLAUDE.md's "redundant annotations are defects" rule overtests/,examples/andbenchmarks/— but only for the Default flavor. 118.ospmlfiles are ungated.The gate's reader looks for an arrow inside a
fnheader (fn f(a: int) -> string =). ML spells a signature as a standalone line above the definition:so
return_annotationnever matches and the deletion it performs does not apply. A green run ofno_corpus_program_carries_a_removable_return_annotationsays nothing about ML.Confirmed removable today:
tests/.../functional_showcase.test.ospml:17— deleting the signature still type-checks, still lowers to IR, and the reported symbol types are unchanged (only line offsets move).Gating ML needs its own reader and its own removal rule, and the stakes are known to be real:
ec6a5cacdeleted ML signatures by hand and tookverdict,workflowsandtype_equality_comprehensivefrom green toa closure value with a still-generic type. Any ML sweep must therefore keep the existing oracle — type-check AND lower AND compare the reported outline — and normalise line offsets before comparing, since deleting a whole line shifts every symbol below it.The limitation is documented on the test itself so a green run is not mistaken for ML coverage.
Found during review of the
enforce-inferable-annotationsbranch.