fix(abi-emit-manifest): skip GADT-style data … where declarations#37
Merged
Conversation
`iseriser abi-emit-manifest` bombed with "data declaration has no `=`"
on any Idris2 module that declared a GADT — e.g. boj-server's
vordr-mcp `MonotonicDegradation` proof relation:
data MonotonicDegradation : IntegrityState -> IntegrityState -> Type where
StayHealthy : MonotonicDegradation Healthy Healthy
...
These are proof / relation types, not exported enums, and have no
place in the ABI manifest. The emitter must walk past them without
choking the way it must already walk past records, interfaces, and
function definitions.
`collect_data_body` now detects GADT form (body starts with `:`,
not `=`) and delegates to a new `skip_gadt_block` helper that
consumes the type signature + indented constructor block. Empty
variant lists were already silently dropped by `parse_enum_declarations`
so no further plumbing is needed.
Two unit tests added: a vordr-mcp shape (real ADT + sibling GADT +
to-int mapping) and a degenerate signature-only GADT (`data Phantom :
Type` with no `where`). Both pass; all 8 emitter tests + 9 integration
tests stay green.
Verified end-to-end against the real cartridge:
$ iseriser abi-emit-manifest \
--idris …/vordr-mcp/abi/VordrMcp/SafeVordr.idr \
--cartridge vordr-mcp --out /tmp/v.json
abi-emit-manifest: wrote /tmp/v.json (0 enums, 0 transitions)
$ iseriser abi-verify --manifest /tmp/v.json --zig-ffi …/vordr_ffi.zig
abi-verify: OK
exit: 0
Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion).
Refs hyperpolymath/boj-server#111 (the cartridge that motivated the fix).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
iseriser abi-emit-manifestbombed with "data declaration has no=" on any Idris2 module that declared a GADT — e.g. boj-server's vordr-mcpMonotonicDegradationproof relation:These are proof / relation types, not exported enums, and have no place in the ABI manifest. The emitter must walk past them without choking the way it must already walk past records, interfaces, and function definitions.
collect_data_bodynow detects GADT form (body starts with:, not=) and delegates to a newskip_gadt_blockhelper that consumes the type signature + indented constructor block. Empty variant lists were already silently dropped byparse_enum_declarationsso no further plumbing is needed.Two unit tests added: a vordr-mcp shape (real ADT + sibling GADT + to-int mapping) and a degenerate signature-only GADT (
data Phantom : Typewith nowhere). Both pass; all 8 emitter tests + 9 integration tests stay green.Verified end-to-end against the real cartridge:
Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion). Refs hyperpolymath/boj-server#111 (the cartridge that motivated the fix).
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
.machine_readable/STATE.a2mlupdated (if project state changed).machine_readable/ECOSYSTEM.a2mlupdated (if integrations changed).machine_readable/META.a2mlupdated (if architectural decisions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/interface/abi/andsrc/interface/ffi/consistent)Testing
Screenshots