Found by the Numerics N6d-i grounding-audit (2026-07-02, HEAD c8a425f).
The spec registry keys by BARE symbol with silent last-write-wins:
register-spec! (macros.rkt:480-482)
- import spec-propagation (driver.rkt:2810-2811)
- implicit-hole counting strips FQNs before lookup (elaborator.rkt:567-576)
Two same-named specs from different modules (e.g. nat's spec add Nat Nat -> Nat vs a generic spec add {A} ... where (Add A); or any two libs both defining reduce) overwrite each other in any module importing both. The loser's call sites get WRONG implicit-argument counts — silently (no diagnostic; wrong elaboration downstream).
Fix direction: FQN-keyed spec store, or module-scoped shadowing with deliberate resolution order. Crosses the module system — PM-series candidate.
Blocks: lifting the add/sub/mult method-wrapper derive skips (DEFERRED.md § "Numerics N6d-i follow-ups" item 1).
Found by the Numerics N6d-i grounding-audit (2026-07-02, HEAD c8a425f).
The spec registry keys by BARE symbol with silent last-write-wins:
register-spec!(macros.rkt:480-482)Two same-named specs from different modules (e.g. nat's
spec add Nat Nat -> Natvs a genericspec add {A} ... where (Add A); or any two libs both definingreduce) overwrite each other in any module importing both. The loser's call sites get WRONG implicit-argument counts — silently (no diagnostic; wrong elaboration downstream).Fix direction: FQN-keyed spec store, or module-scoped shadowing with deliberate resolution order. Crosses the module system — PM-series candidate.
Blocks: lifting the add/sub/mult method-wrapper derive skips (DEFERRED.md § "Numerics N6d-i follow-ups" item 1).