Skip to content

fix(abi-emit-manifest): skip GADT-style data … where declarations#34

Merged
hyperpolymath merged 1 commit into
mainfrom
fix/abi-emit-skip-gadt-data
May 20, 2026
Merged

fix(abi-emit-manifest): skip GADT-style data … where declarations#34
hyperpolymath merged 1 commit into
mainfrom
fix/abi-emit-skip-gadt-data

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

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

Summary

Changes

RSR Quality Checklist

Required

  • Tests pass (just test or equivalent)
  • Code is formatted (just fmt or equivalent)
  • Linter is clean (no new warnings or errors)
  • No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
  • No unsafe blocks without // SAFETY: comments
  • No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry)
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • .machine_readable/STATE.a2ml updated (if project state changed)
  • .machine_readable/ECOSYSTEM.a2ml updated (if integrations changed)
  • .machine_readable/META.a2ml updated (if architectural decisions changed)
  • Documentation updated for user-facing changes
  • TOPOLOGY.md updated (if architecture changed)
  • CHANGELOG or release notes updated
  • New dependencies reviewed for license compatibility (PMPL-1.0-or-later / MPL-2.0)
  • ABI/FFI changes validated (src/interface/abi/ and src/interface/ffi/ consistent)

Testing

Screenshots

`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>
@hyperpolymath hyperpolymath merged commit fd3c6d9 into main May 20, 2026
14 of 29 checks passed
@hyperpolymath hyperpolymath deleted the fix/abi-emit-skip-gadt-data branch May 20, 2026 23:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant