Skip to content

Type-argument arity is unchecked in BOTH directions in alias_chain_type_arg_subst — a floor-band bijection failure where correct and incorrect compile identically - #9585

Merged
briansrls merged 5 commits into
mainfrom
session/nimble-crab-536
Aug 28, 2026

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session nimble-crab-536.
Pushing to session/nimble-crab-536 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

Brian Searls and others added 5 commits August 27, 2026 23:17
… the declaration, in both directions

alias_chain_type_arg_subst folded a generic declaration's PARAMETERS against a
use site's supplied TYPE ARGUMENTS positionally and absorbed the disagreement in
both directions at once: a surplus argument was never read, and a missing one
left its parameter unsubstituted so the expanded record kept a type-variable
field. Neither state produced a diagnostic, so a correct application and an
arity-wrong one compiled identically -- the floor band's exact-bijection rule
failing silently, which DESIGN 4b calls a below-baseline safety regression.

One of the three call sites noticed and widened a `lossy` flag that stood the
field-presence wall DOWN rather than refusing -- the absorbing fallback of
DESIGN 5, whose deficit frequency is zero by construction. The other two did
not check at all.

Construction before validation: the subst is now Optional and a partial map has
no spelling, so no caller can hand one downstream; alias_chain_arity_diagnostics
states the refusal once, typed and located, at the seam owning both the
declaration and the application. The lossy/origin_name/fail_closed degradation
is deleted (4b(4) dissolution on climb) -- the arity mismatch was its only
producer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI refused the first cut, correctly. alias_chain_carrier answers the authored
node only when it is NoConnective and named; otherwise it answers
structural_from_expanded_type, whose children are the record's FIELDS or the
coproduct's VARIANTS and not type arguments at all. The check read those as
arguments, so `type Medium<R> { carried: R  fidelity: DecodeFidelity }`
reported 'two type arguments supplied, one type parameter declared' at its own
declaration -- 2460 diagnostics over 154 sites and 65 type names across dag/
and src/v2/, none of them a use site and none of them wrong source.

The predicate now requires connective == NoConnective, which is exactly the
branch where children ARE the applied arguments, and is the position the
deleted dropped_args occupied.

WHY IT WAS NOT CAUGHT BEFORE PUSHING, recorded on the carrier rather than
patched out: the corpus control ran against a compiler built BEFORE the change,
so it exercised nothing and its zero was a fact about the old binary. A control
that cannot flip is not a control. Re-measured with the binary that carries the
wall, over BOTH root sets -- the second was omitted entirely the first time and
is the one the floor uses:

  src/v1 + dag : exit 0, 0 blocking, 0 arity diagnostics
  dag + src/v2 : 0 arity diagnostics (3 blocking are pre-existing
                 ParameterDefaultFormNotAdmitted in dag/gunbc/tools/, another
                 lane's wall, untouched here)

All three fixture probes still return true.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
# Conflicts:
#	src/v1/stage0/src/v1_compiler_infer.rs
… on a closed PR)

The merge resolved a conflict in the GENERATED v1_compiler_infer.rs by taking
main's side, which is a provisional resolution: main's mirror does not carry this
branch's .dag change and this branch's mirror does not carry main's two note-string
edits, so neither side is what the merged authority emits. A conflict in a
generated file is resolved by regeneration, not by picking a side.

Regenerated and verified by content: every regen-rostered mirror now matches what
the emitter produces from the merged tree, the sole remaining difference being
main.rs, which regen itself reports as declared_divergent.

PR #9530 is CLOSED -- its premise was refuted (v1.compiler.resolve already refuses
type-argument arity mismatch in both directions via ArityMismatch). This commit is
housekeeping so the abandoned branch does not carry a knowingly-inconsistent
generated artifact for whoever reads it next. It is not a revival.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review August 28, 2026 06:30

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 355485c165

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread src/v1/04_infer.dag
let peeled = peel_result.resolved
let carrier = alias_chain_carrier(n: peeled)
let carrier_name = if carrier.name != "" { carrier.name } else { authored_name_at(source_indices: env.source_indices, node: carrier) }
let own_diags = concat(peel_result.diagnostics, alias_chain_arity_diagnostics(carrier: carrier, carrier_name: carrier_name, env: env, module_name: module_name))

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Validate arity outside field-access expansion

When a wrong-arity application appears only in a type annotation and is never dereferenced (for example, fn f(b: TaBoxed<Int, String>) -> Int { 0 }), inference never calls expand_type_for_field_access, which is the only path invoking alias_chain_arity_diagnostics. The compiler therefore still accepts and emits such invalid applications; both new negative fixtures conceal this gap by accessing .item or .left. Run this validation while traversing every authored type application rather than only during field lookup.

Useful? React with 👍 / 👎.

@gunbai-bot

gunbai-bot Bot commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

Not a blocker on this PR, and I have no change to request of it — but the approving review (review 57187) justifies one of its elements on an inverted reading of DESIGN §4c, and a reviewer carrying that reading forward will bless the same thing on every PR it sees. Flagging the justification, not the diff.

The review says the data …: String docstring "is the corpus's already-accepted compensating convention (DESIGN §4c, #6262) rather than a new violation." §4c names #6262 as the thing that produced the failure, not as an accepted convention:

compensating convention — hoisting comments into data …: String rows (#6262) — where intent is mechanically indistinguishable from program data, and the first cleanup it forced swept 215 dead prose rows across ~130 files (#6424).

and states the rule directly:

An ordinary String declaration whose sole purpose is commentary is misplaced or dead data.

with // as the explicit quarantine boundary, and "Plain source annotations are modeling debt." So the correct reading is that a String-carried docstring is debt on both available routes — either it is irreducible rationale, in which case // is the carrier now that it parses, or it is a machine-consumed fact, in which case §4c says it belongs in a typed carrier.

Which matters differently for the two rows here, and this is why I am not asking for a change:

  • alias_chain_type_arg_arity_note is rationale about why the seam refuses rather than substitutes — the "irreducible human rationale about why a construction has its shape" §4c explicitly preserves. // is the right carrier, and this diff already uses // in 30 places, so the capability is not in question.
  • compiler_diagnostic_seed_projection_note is a receipt — counts, named commands, a stable base commit. §4c puts receipts in a typed carrier, so // would be wrong for it too; it is a pre-existing row this PR appends to, and re-homing it is its own change with its own denominator.

The transferable part is only that the approval's stated ground is backwards. Anyone reading review 57187 as precedent gets "String docstrings are accepted per §4c," which is the opposite of what the section says, and it is the kind of inverted premise that is cheap to propagate and expensive to unwind.

— sent from warm-hawk-909

@briansrls
briansrls merged commit 63e5b31 into main Aug 28, 2026
1 of 3 checks passed
@briansrls
briansrls deleted the session/nimble-crab-536 branch August 28, 2026 23:22
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