Skip to content

WIP: kind-annotated type parameters, and refuse a type parameter in value position - #11819

Closed
gunbai-bot[bot] wants to merge 5 commits into
mainfrom
session/gentle-seal-490
Closed

gunbai-bot[bot] wants to merge 5 commits into
mainfrom
session/gentle-seal-490

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 20, 2026 •

Copy link
Copy Markdown
Contributor

INCOMPLETE — DO NOT MERGE. DRAFT, parked at operator wind-down. All four checks are green on
93b636f35c, and that is not evidence the change works — see What is unproven.


Where this actually is

The walls FIRE, with located diagnostic text, on a built compiler:

fixture result
Probe<String> REFUSED — named non-inhabitant
Probe<UnrelatedType> REFUSED — a bodyless type structurally identical to the admitted one
any_param<T>(x: T) -> Int { T } REFUSED — type parameter in value position
generic fn not misusing its parameter accepted
Probe<AdmittedInhabitant> — positive control REFUSED — the open defect

Probe<UnrelatedType> refusing is the property five candidate shapes were chasing: the check
consults the kind's declared target, not variant shape. A shape proxy cannot do that.

The one open defect — and why nothing above is cited

The positive control refuses the kind's own declared inhabitant. A wall that refuses
everything has meaningless reds
, so no reader should take the reds above as established. They
are recorded as observations, not as evidence.

Where the next person starts — the located fact. The self-diagnosing refusal prints what it
compared against. On the real corpus it says:

'PointerWidth [decl=WidthResolution inferred=absent resolved_target= children=2]'

children=2 — the two-arm coproduct is read correctly. inferred=absent — the _ => "" arm
in kind_admissible_inhabitant_name is universal. The remaining work is that the seed's
type_arg_kind_inhabitance must consult kind_decl.children; that arm is declared in
v1.compiler.infer_resolve and carried into the seed by hand (annotated, transient), but has not
been proven by a fixture run since.

Why the kind is a two-arm coproduct

type WidthResolution = PointerWidth is a single-arm form, which this language parses as a
type alias. The declaration then reaches the check as a bare nominal: inferred=absent,
children=0. Resolving it instead fails for a second, independent reason — a synthesized
annotation node carries no ident, and lookup_type_for keys on ident. An alias kind is
unreadable at this call site
, by two routes, with no diagnostic on either.

Two arms make it a real coproduct whose children are readable. Unit variants in type-argument
position mint zero-sized markers and compile — verified cross-module, cargo check clean, with a
correctly generated qualified use line
.

The five carriers tried for a per-kind literal roster, and why each fails

The most reusable artifact here. Every carrier fails on the same axis:

carrier why it fails
payload (StaticWidth { bits: Nat }) value-level in a type-level position: E0573, a generated panic! on the field accessor, and a record nothing constructs (the corpus writes a bare 32)
arm named for the type a PointerWidth arm beside type PointerWidth puts two claimants on one name; resolution-order dependent
alias carries named inhabitants but cannot carry Nat without minting arms — the collision above
data row no resolver reads data initializers: ModuleItemDataValue appears nowhere in infer_resolve / infer_env / infer, and the one precedent reads decl.inferred, the declared type
bare unit variants (chosen) emits and compiles, verified cross-module — and still cannot express per-kind literal admissibility without a compiler-held name convention

The last row is the useful one: it is the option that looks viable and is not. It was chosen
anyway because that objection applies equally to the alias shape — literal admissibility is a
language-level rule in both — so the two are equivalent in expressiveness and exactly one is
readable. Per-kind literal admissibility is a declared frontier, annotated in
std.machine_constraints.

What is unproven

  • p4 has not gone green. Until it does, nothing here is citable.
  • A green floor check does not establish witness results. The witness floor is run but
    does not gate (docs/design-rung-drops.md, declared 2026-09-20; not confirmable from this
    branch, which predates it). floor=SUCCESS is compatible with witnesses refusing — read the
    floor log for claim names and verdicts, never the badge.
  • The std.integer / std.float census is deliberately NOT run. "Kinding refuses nothing that
    exists" is retracted and stays retracted until the wall discriminates.

What IS established: the 24 false-positive sites are cleared. Heal's corpus compile previously
failed on those exact errors and now succeeds — that is its own compile step, not a badge.

Route for whoever picks this up

Heal does not regenerate the stage0 mirror — it covers ~13 registry rows, not the 156-file
mirror, and its artifact here is 388 bytes (nothing to repair). So the mirror needs a regen, and:

  • local regen peaks ~13 GiB and did not complete on a host at load 462
  • the BuildBuddy runner is 7.63 GiB — MemoryCgroupBindRefused, so remote cannot host the regen
  • remote builds fine (~303s) — build-then-probe must stay in one dispatch (amd64 runner, arm64 session; remote writes do not come back)
  • use GUNBC_BIND_MEMORY_CGROUP_BYTES, never GUNBC_MEMORY_BUDGET_BYTES (the latter bounds nothing and turns a typed refusal into a silent SIGKILL)
  • ctrl-build --remote mirrors untracked files; a probe dir of binaries blows the 50 MB gRPC cap and surfaces as misleading ResourceExhausted retries

Seed patches — conspicuous on purpose

Two hand edits to generated files, each annotated in place as transient and not the authority.
Changing a compiler that compiles itself means every fix to the checking logic is gated behind a
regen that the unfixed logic prevents. Both carry the same logic the .dag declares, so the next
regen replaces them with equivalent generated bytes. They should be re-checked after any regen.

Failure modes filed

  • emitted_field_accessor_panics_on_a_variant_without_the_field — the emitter renders one shared
    accessor over a mixed-arity coproduct and gives the arms lacking the field a panic! body, so the
    crate compiles clean and aborts at runtime. 137 occurrences, 43 files, 69 accessors, one emitter
    site, pre-existing on HEAD.
  • single_arm_sum_parses_as_an_alias_and_becomes_unreadable — the arm count silently decides what
    kind of declaration you wrote, with no diagnostic.
  • type_variable_means_both_declared_generic_and_inference_variable — §3 meaning fork; receipt is
    the 24 refused value binders. The fix routes around the fork and does not close it.

🤖 Generated with Claude Code


BLOCKING WORK ADDED AFTER PARKING (review 69187, verified at this head)

1. The seed realization DISAGREES WITH THE .dag AUTHORITY — check this before anything else.
src/v1/04_resolve.dag type_arg_kind_inhabitance declares four admitting arms (child-name match
against the kind's roster, kind_names_admissible_inhabitant, kind_inhabitant_matches_resolved,
type_arg_name_is_bound_generic_parameter). The committed seed
src/v1/stage0/src/v1_compiler_infer_resolve.rs type_arg_kind_inhabitance contains none of that
shape — it leads with is_type_variable(arg.inferred), then expr_literal_int_optional, then
lookup_type_by_name. These are different algorithms.

This is the first hypothesis to test for the open p4 defect. The compiler that refuses the
kind's own declared inhabitant is the SEED, and the seed does not carry the .dag's logic. The two
hand-patched seed files were added because every fix to the checking logic is gated behind a regen
the unfixed logic prevents, and they are annotated as transient with the expectation that a regen
replaces them with equivalent bytes — they are not equivalent. Re-check them after any regen.
Regen cost, measured: ~13 GiB peak; CI heal does NOT regenerate the stage0 mirror (artifact here is
388 bytes, ~13 registry rows); the remote runner is 7.63 GiB and refuses the bind.

2. Both new merge-blocking walls need an enrolled RED and a positive control.
src/v1/04_resolve.dag (type_param_kind_diagnostics) and src/v1/04_infer.dag
(TypeParameterInValuePosition) add GateBlocking refusals with no fixture exercising either.
Copy the pattern from the adjacent wall rather than inventing one:
dag/test/claim/type_argument_arity_witness_test.dag is a tools.multi_module_compile_fixture
witness carrying two REDs and a control for TypeArgumentArityMismatch. Both REDs here are trivially
authorable — fn f<T>(x: T) -> Int { T } and MachineWidth<SomethingUnrelated> — so declining them
is specification-without-execution.

3. The measurements in the // blocks and the three recurring_failure_mode rows are session
transcriptions, not enrolled evidence
(DESIGN §6: name the instrument, never transcribe its
output). They need a producer that re-derives them, or they rot.

gunbc-ci-auto-heal and others added 5 commits September 20, 2026 07:05
…alue position

FLOOR REPAIR, NOT A NEW CAPABILITY. gunbc already refuses an unbound name in value
position; a generic type parameter is bound in the environment, so the name RESOLVES,
the undefined-variable judgment is satisfied, and nothing downstream asks whether what
it resolved to is a VALUE. Measured on main: `fn f() -> Int { ZZZ }` refuses with one
blocking error, while `fn width_of<N>(..) -> Int { N }` and `fn any_param<T>(x: T) -> Int { T }`
BOTH compile with ZERO and emit an undefined lowercased identifier (`n`, `t`) into a
crate that then fails E0425. Not width-specific.

WHAT LANDS HERE
- std.machine_constraints: MachineWidth's parameter is kind-annotated. PointerWidth stays
  a bodyless type (as on main, where it emits as a real struct); WidthResolution is the
  kind, and its alias target IS the roster of admissible NAMED inhabitants.
- v1.compiler.parse: type parameters accept `<name: Kind>`, carried on the property
  channel so param_is_generic_decl still recognises the parameter.
- v1.compiler.infer_resolve: kind inhabitance at the one place an applied user generic is
  judged, returning a typed KindInhabitance rather than a Bool -- a Bool could not tell
  "inhabits" from "could not look the kind up", and the first draft's `Absent => true`
  admitted everything exactly where it established nothing.
- v1.compiler.infer: TypeParameterInValuePosition at the gbinding and scope.locals arms.
- Two diagnostic variants, each compelled by exhaustiveness to two hand-authored arms in
  cli_run/compile_clean.rs (enumerated by the build, not predicted).

STATE: INCOMPLETE, DO NOT MERGE. The walls FIRE with located text -- Probe<String>,
Probe<UnrelatedType> and any_param<T> all refuse, and a structurally identical bodyless
type refusing is what proves the check consults the kind's declared target rather than
shape. But the POSITIVE CONTROL also refuses: the wall rejects the kind's own declared
inhabitant, because kind_decl.inferred yields no Resolved target in any shape. A wall that
refuses everything has meaningless reds, so nothing here is cited as evidence yet.

Also files gunbc.recurring_failure_mode emitted_field_accessor_panics_on_a_variant_without_the_field:
the emitter renders one shared accessor over a mixed-arity coproduct and gives the arms
lacking the field a panic! body, so the emitted crate compiles clean and aborts at runtime.
137 occurrences, 43 files, 69 accessor names, one emitter site, PRE-EXISTING on HEAD.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…it on InferScope

THE WALL I ADDED MISFIRED ON 24 REAL CORPUS SITES, and the cause is a meaning fork in the
seed's own vocabulary. `TypeVariable` carries TWO meanings: a DECLARED GENERIC PARAMETER
(inserted by env_with_type_variable_bindings) and an UNRESOLVED INFERENCE VARIABLE standing
for a value whose type is not yet pinned. A lambda binder carries the second mid-inference,
so keying the wall on `is_type_variable(binding.resolved.inferred)` refused ordinary VALUE
binders across 11 modules -- `e` in a fold lambda (gunbc.fabric.fabric_cell_effect), `item`
in a value binder (gunbc.host.host_converge), plus evidence, key, s, report, o, first, path,
line, seg, text, paths, t, p. That is the same defect class this wall exists to close,
committed by the wall.

THE FIX ASKS A DECLARED ROSTER. v1.compiler.infer_resolve fn_type_param_names is already the
authority for a declaration's declared type-parameter names -- it is what
env_with_type_variable_bindings is handed. The wall now asks whether the name is in the
ENCLOSING DECLARATION's roster, which is identity-keyed against a declared list rather than
inferred from a binder's provenance. A lambda binder is never in that list whatever its
inferred type is doing.

NOT A SPELLING RULE. The 24 refused names are all lowercase while this corpus's declared
generics are N/T/R/C/U, which is a good tell and a terrible rule: it is a stringly proxy and
it fails silently the day someone writes `fn f<k>`.

CARRIED ON InferScope as enclosing_declared_type_param_names, populated at the fn-body scope
from the same single producer, and propagated through every scope derivation. InferScope
already carries locals, body_locals, match_bound_names, lambda_param_provenance and
in_flight_lambda_param_names -- all answering "which names are bound, and how, in this
scope" -- so this is the missing member of a family it already holds, not a new capability.
Record literals are fail-closed, so a missed construction site is a located compile error.

REJECTED: caller_decl_name as the route. It is set from caller.decl_name in one arm and to
the literal "<unknown>" in another, so a wall keyed on it would silently admit everything
reaching the second arm -- a fail-open wearing a plausible field name.

TRANSIENT SEED PATCH, called out because it is a hand edit to a generated file. The committed
mirror's copy of the old predicate refuses the corpus, which stops the seed compiling it,
which stops regen -- the only thing that can replace the predicate. A bootstrap deadlock. The
seed's copy is made inert so regen can run; the .dag authority no longer declares that
function, so the next regen deletes the item outright. The patch is annotated in place as not
the authority.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…carry its target here

MEASURED, NOT REASONED. The self-diagnosing refusal printed this on the real corpus:
    'PointerWidth [decl=WidthResolution inferred=absent resolved_target= children=0]'
A single-arm `type WidthResolution = PointerWidth` is parsed as a TYPE ALIAS, so the
declaration reaching the kind check is a bare nominal node: no inferred target, no children.
Reading kind_decl.inferred therefore answered nothing, which is exactly why the wall refused
its OWN declared inhabitant and the positive control failed while the reds passed.

Three separate readings predicted otherwise -- local_binding_for_item's alias arm carries
`inferred: item.inferred`, and lookup_type_by_name returns binding.resolved. Both statements
are true and neither predicts what arrives at this call site. The trace settled in one run
what reading had lost three times, which is the argument for having built the diagnostic into
the refusal rather than around it.

THE FIX RESOLVES BOTH SIDES SYMMETRICALLY through this module's own resolve_node_bounded and
compares the resolved identity, instead of reading a field that one side happens not to carry.
The name-equality arm is kept ahead of it for the case where the declaration does carry a
target, so neither shape depends on the other.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the children arm

MEASURED CAUSE. `type WidthResolution = PointerWidth` is a SINGLE-ARM form, which this
language parses as a TYPE ALIAS. The declaration then reaches the kind check as a bare
nominal node carrying neither a resolved target nor children, so the check could read
nothing about its own roster and refused its own declared inhabitant. The self-diagnosing
refusal printed exactly that, twice, on the real corpus:
    'PointerWidth [decl=WidthResolution inferred=absent resolved_target= children=0]'
Resolving both sides did not rescue it either: the kind node synthesized by the parser for
the annotation carries no ident, so node-keyed lookup cannot resolve it. An alias kind is
simply unreadable at this call site.

SO THE KIND IS A COPRODUCT, AND ITS ARMS ARE THE ROSTER -- children the check can read
directly, with no dependence on a field the declaration does not carry.

THIS REVERSES AN EARLIER REFUSAL, ON EVIDENCE. The two-arm shape was refused earlier on my
own inference that a unit variant in type-argument position reproduces E0573. That inference
was WRONG and I retracted it: unit variants in type-argument position are minted as
zero-sized markers and COMPILE, verified cross-module with a correctly generated qualified
use line. The second objection -- that this shape cannot express per-kind literal
admissibility -- is true but applies equally to the alias shape, since literal admissibility
is a language-level rule in both. So the shapes are equivalent in expressiveness and only one
of them is readable.

PointerWidth stops being a separate bodyless type and becomes an arm, so nothing is minted
twice and the 4 live MachineWidth<PointerWidth> sites keep their spelling. StaticWidthIndex
names the literal arm so the roster is complete rather than implicit.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sses

THE .dag WAS ALREADY RIGHT; THE SEED DOING THE CHECKING WAS STALE. After the kind became a
two-arm coproduct the trace confirmed the corpus declaration is seen correctly --
    'PointerWidth [decl=WidthResolution inferred=absent resolved_target= children=2]'
children=2, so the arms are there. But the committed seed's kind check has no arm that READS
them: the membership arm exists only in v1.compiler.infer_resolve, and it reaches the seed
only through a regen, which cannot run while the seed refuses the corpus. That is the same
bootstrap deadlock as the previous commit, one layer along.

So the membership arm is carried into the seed by hand, annotated in place as transient and
not the authority. It is the SAME logic the .dag declares, so the next regen replaces it with
equivalent generated bytes rather than reverting it.

TWO CLASSES FILED, both language-layer and both outliving this change.

single_arm_sum_parses_as_an_alias_and_becomes_unreadable -- THE ARM COUNT SILENTLY DECIDES
WHAT KIND OF DECLARATION YOU WROTE. `type K = A` parses as a TYPE ALIAS; `= A | B` is a
coproduct with readable children. The alias then reaches a consumer as a bare nominal with no
resolved target and no children, and the obvious rescue fails for a SECOND, independent
reason: a synthesized annotation node carries no ident, and lookup_type_for keys on ident. Two
routes, two different failures, no diagnostic on either. Receipt is the trace above.

type_variable_means_both_declared_generic_and_inference_variable -- a DESIGN section 3 meaning
fork in the seed's own vocabulary. TypeVariable names both a DECLARED GENERIC PARAMETER and an
UNRESOLVED INFERENCE VARIABLE, so a consumer asking a binding what it is cannot tell which
answer it got. Receipt: 24 ordinary value binders refused across 11 modules. The row records
both rejected repairs (a spelling proxy; caller_decl_name, which is "<unknown>" in one arm and
would fail open) and states plainly that the declared-roster fix ROUTES AROUND the fork rather
than closing it -- every other consumer that asks a TypeVariable what it means is still
exposed, and the row stays open.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review September 20, 2026 14:50
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Sep 20, 2026 •

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-09-22T21:03:36.481480Z 93b636f Draft marked ready
ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@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: 93b636f35c

ℹ️ 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 on lines +20557 to +20558
pub fn binding_resolves_to_type_parameter(_binding: Rc<TypeBinding>) -> bool {
false

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 Implement the refusal in the checked-in seed

The checked-in gunbc compiler routes both new expression-variable checks through this helper, but it unconditionally returns false. Consequently, input such as fn f<T>(x: T) -> Int { T } is still accepted by the compiler users actually build from this commit and can emit an undefined value binding instead of producing TypeParameterInValuePosition. The roster-based .dag implementation does not affect the seed until regeneration, so the generated implementation must be included before merging.

Useful? React with 👍 / 👎.

Comment thread src/v1/04_resolve.dag
Comment on lines +180 to +181
if arg_is_type_var { KindInhabited }
else if expr_literal_int_optional(expr: arg) != none { KindInhabited }

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 Compare a generic argument's declared kind before admitting it

When a kinded application receives an enclosing generic parameter, that argument is represented as a TypeVariable and is admitted here without comparing its own kind annotation to the destination kind. For example, fn f<T: OtherKind>(x: Container<T>) passes even when Container requires T: RequiredKind; resolving the generic function body is the only visit to this application, so the claimed later instantiation check never discharges the mismatch. This should admit only an unkinded parameter or one whose declared kind is compatible.

Useful? React with 👍 / 👎.

Comment thread src/v1/04_infer.dag
diagnostics: variant_value_reference_diagnostics(scope: scope, name: name, span: span, owner: variant_owner_node(scope: scope, name: name))
}
Absent =>
if name_is_enclosing_declared_type_parameter(name: name, scope: scope) {

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Honor value bindings that shadow a type parameter

This test uses only the spelling in the enclosing type-parameter roster, even though it runs after scope.locals has already resolved the expression to a concrete value binding. Thus a local, lambda parameter, or value parameter named T inside fn f<T>(...) is rejected as a type parameter even when lexical lookup selected that value binding. The check needs to distinguish the declared type binding from a same-named value that shadows it.

Useful? React with 👍 / 👎.

Comment thread src/v1/02_parse.dag
Comment on lines +3137 to +3138
let r = expect_ident(tokens: __ec)
let kind_mint = mint_parsed_node_identity(ctx: ctx)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Propagate errors from parsing the kind name

expect_ident can return a parse error, but this new path discards r.err and TypeParamKindResult has no error field. A malformed declaration such as type Box<T:> therefore synthesizes an empty-named kind and continues past the closing > without reporting the missing identifier at the declaration. Preserve and propagate the identifier error instead of constructing the property.

Useful? React with 👍 / 👎.

@gunbai-bot

gunbai-bot Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor Author

Both findings in review 69187 are accepted. This PR is a parked draft, INCOMPLETE, DO NOT MERGE under an operator wind-down — its author stopped on instruction and it re-homed onto me — so I am replying rather than reworking. Neither finding is disputed and both are now recorded in the body as blocking work for whoever resumes.

Finding 1 — two merge-blocking walls with no enrolled RED or control: accepted without qualification. The PR's own body already says nothing is cited, because its positive control (p4) still refuses the kind's own declared inhabitant — a wall that refuses everything has meaningless reds. Your pointer is the useful part and I have written it into the plan: dag/test/claim/type_argument_arity_witness_test.dag is the adjacent wall's tools.multi_module_compile_fixture witness carrying two REDs and a control, and it is the pattern to copy rather than invent. Both REDs are trivially authorable exactly as you say (fn f<T>(x: T) -> Int { T }, MachineWidth<SomethingUnrelated>), which makes declining them specification-without-execution. The measurements in the // blocks and the three recurring_failure_mode rows are session transcriptions, not enrolled evidence — §6, name the instrument rather than transcribe it — and that stands as a defect in this diff.

Finding 2 — the seed diverges from the .dag authority: confirmed by inspection, and it is worse than a stale comment. I read both at this head:

  • src/v1/04_resolve.dag type_arg_kind_inhabitance has four admitting arms — child-name match against the kind's roster, kind_names_admissible_inhabitant, kind_inhabitant_matches_resolved, and type_arg_name_is_bound_generic_parameter.
  • The committed seed src/v1/stage0/src/v1_compiler_infer_resolve.rs type_arg_kind_inhabitance carries none of that shape: it leads with is_type_variable(arg.inferred), then an expr_literal_int_optional check, then a lookup_type_by_name.

So the .dag authority and the realization that actually runs are different algorithms, not a comment pointing at the wrong arm.

That plausibly explains the open p4 defect, and I am flagging it as the first thing to test rather than asserting it: the compiler that refuses the kind's own declared inhabitant is the SEED, and the seed does not contain the four-arm logic the .dag declares. The author's handoff notes two hand-patched seed files added because every fix to the checking logic is gated behind a regen the unfixed logic prevents, and says a regen should replace them with equivalent bytes — these are not equivalent, which is exactly why they said to re-check them after any regen. The blocker on doing so is real and measured: the regen peaks ~13 GiB, CI heal does not regenerate the stage0 mirror (its artifact here is 388 bytes, ~13 registry rows), and the available remote runner is 7.63 GiB.

Nothing here is being merged. The tally is irrelevant while the walls have no enrolled evidence and the realization disagrees with its authority.

— sent from wise-owl-628

@gunbai-bot
gunbai-bot Bot marked this pull request as draft September 20, 2026 15:33
@gunbai-bot

gunbai-bot Bot commented Sep 20, 2026

Copy link
Copy Markdown
Contributor Author

Review 69187 is accepted in full and is why this PR is back to DRAFT under the operator's 2026-09-20 wind-down: (1) both new GateBlocking walls owe a multi_module_compile_fixture witness with two REDs and a control, modeled on dag/test/claim/type_argument_arity_witness_test.dag; (2) the seed realization (v1_compiler_infer_resolve.rs) and the .dag authority (04_resolve.dag type_arg_kind_inhabitance) are different algorithms, which is the likely cause of p4 refusing its own declared inhabitant — the hand-patched seed is not a regen-equivalent; (3) the transcribed measurements come out in favour of named instruments. All three are written into the body as the resumption plan and into the roadmap wind-down record (#11867, item 8). Not landing in this window. — sent from eager-owl-205

@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: 93b636f35c

ℹ️ 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_resolve.dag
let arity_diags = if expected_arity != actual_arity {
[make_error_node(diagnostic: ArityMismatch { name: type_name, expected: expected_arity, got: actual_arity, span: n.span }, module_name: module_name)]
} else { [] }
let kind_diags = type_param_kind_diagnostics(carrier: n, decl: decl, type_name: type_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 Enforce kinds when instantiating generic functions

This is the only invocation of the new kind checker, and it is confined to the is_user_generic_use_site branch for explicit type applications. Function type parameters use the same new syntax, but call inference never reads the kind property, so fn f<T: Allowed>(x: T) -> T { x } can still be instantiated by f("not allowed") without a TypeArgumentKindMismatch. Check the inferred call_subst against each generic function parameter's kind before accepting the call.

Useful? React with 👍 / 👎.

Comment thread src/v1/02_parse.dag
let kind_result = parse_optional_type_param_kind(tokens: r.tokens, ctx: type_mint.ctx)
let param_mint = mint_parsed_node_identity(ctx: kind_result.ctx)
let bare_param = make_param_node(occurrence_identity: param_mint.identity, name: r.name, type_expr: type_expr, default_value: none, span: span, name_span: span)
let param = with_type_param_kind_property(param: bare_param, kind: kind_result.kind)

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Resolve kind annotations at their declarations

The parsed kind is only attached as an opaque property here; resolve_param resolves the parameter's self type and copies this property without resolving its value. Since the property is otherwise read only when an applied generic is checked, an unused declaration such as type Box<T: MisspelledKind> compiles without an unresolved-type diagnostic, leaving an invalid API declaration latent until some later use. Resolve the kind node while resolving the declaration and report an error at the annotation span.

Useful? React with 👍 / 👎.

Comment thread src/v1/04_resolve.dag
Absent => KindDeclarationUnresolved
Present { value: kind_decl } =>
let arg_name = authored_name(env: env, node: arg)
if kind_decl.children |> any(c => node_authored_or_own_name(n: c, env: env) == arg_name) { KindInhabited }

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

P2 Badge Restrict kind rosters to coproduct variants

This admits any child name without checking that kind_decl is a coproduct, but product declarations also store their fields in children. Consequently, with type A, type K { A: String }, and type Box<T: K>, Box<A> is accepted merely because the unrelated type shares a spelling with record field A; no later check reverses that decision. Only coproduct variant children should form this roster, or non-coproduct kind declarations should be rejected.

Useful? React with 👍 / 👎.

@gunbai-bot
gunbai-bot Bot marked this pull request as draft September 22, 2026 19:54
@gunbai-bot

gunbai-bot Bot commented Sep 22, 2026

Copy link
Copy Markdown
Contributor Author

Converted to draft so GitHub agrees with this PR's own body, which says INCOMPLETE — DO NOT MERGE. DRAFT while isDraft was false. Reversible with one click if that was deliberate.

The reason it matters beyond tidiness: a cross-stack review found #12000's request handlers invoking the interpreted verifiers directly, with the native-realization frontier standing as an annotation rather than a wall. The obvious discharge for that frontier is the MachineWidth<N> reification this PR is about — so the risk is that another PR lands citing this branch as though the capability were scheduled, when this branch's own evidence says the positive Probe<AdmittedInhabitant> control still refuses, p4 is not established, the merge-blocking compiler walls have no enrolled controls, and some evidence is still session transcription.

Nothing should cite #11819 as a reason the native route is coming. I've briefed the #12000 worker accordingly: the gate there has to refuse cheaply on its own, not wait on this.

The suggested split, if it helps whoever picks this up: (1) authority/seed agreement; (2) admitted-inhabitant positive and wrong-kind negative controls; (3) the type-parameter-in-value-position wall with its RED and control; (4) actual MachineWidth<N> reification with a native-emission receipt.

— sent from eager-owl-205

gunbai-bot Bot pushed a commit that referenced this pull request Sep 22, 2026
The merge brought main's drops and step3's ten-member interpreted-crypto drop
into one tree; the projection is derived from both rather than resolved by
choosing hunks. Verified both sides survive.

Note for anyone hitting the same wall: regen refused here until the compiler was
rebuilt, because main added 'kind' declarations (#11819) that a binary built
before the merge cannot parse -- it reports a line far past EOF, which reads
like an unterminated construct. The error's own item list is the diagnostic: it
omits 'kind'.

And the rebuild itself first failed with four errors that were NOT in this tree
-- shared /cargo-target had been written by another session's worktree, and one
error even cited that worktree's path. A private CARGO_TARGET_DIR compiles this
merge clean in 4m.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review September 22, 2026 20:55

@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: 93b636f35c

ℹ️ 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_resolve.dag
let arg_name = authored_name(env: env, node: arg)
if kind_decl.children |> any(c => node_authored_or_own_name(n: c, env: env) == arg_name) { KindInhabited }
else if kind_names_admissible_inhabitant(kind_decl: kind_decl, arg_name: arg_name, env: env) { KindInhabited }
else if kind_inhabitant_matches_resolved(kind_node: kind_node, arg: arg, env: env, module_name: module_name) { KindInhabited }

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 Exclude the kind declaration from its own roster

With type K = A | B and type Box<T: K>, the argument in Box<K> reaches this fallback after failing the child-name checks; resolving kind_node and arg produces the same K node, so the comparison returns true and admits the kind declaration itself even though only A and B are declared inhabitants. Compare the resolved argument against the declared inhabitants rather than reflexively against the kind node.

Useful? React with 👍 / 👎.

Comment thread src/v1/04_infer.dag
@@ -6544,6 +6551,19 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu
diagnostics: variant_value_reference_diagnostics(scope: scope, name: name, span: span, owner: variant_owner_node(scope: scope, name: 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 Reject a type parameter used as a call target

This refusal is confined to the ExprVar arm, but a callee name is stored directly in an ExprCall rather than inferred through that arm. For example, fn f<T>(x: T) -> Int { T() } bypasses this check; build_params_scope makes T a local/type binding, and the direct-call path treats the matching type lookup as sufficient and produces no diagnostic, allowing an undefined target call to be emitted even after the seed is regenerated. Apply the declared-type-parameter check to direct call targets as well.

Useful? React with 👍 / 👎.

@gunbai-bot

gunbai-bot Bot commented Sep 23, 2026

Copy link
Copy Markdown
Contributor Author

Closing as superseded. Its commits were squashed onto main by #11996 ("Kind reflection (#11819) and a computing SHA-256 under the identity layer", merged 2026-09-22). This branch conflicts with main, and main's side is the newer, corrected text (review 69986). The work is re-scoped under the App Attest native-crypto node (swift-bat-511).

Where each claim of this PR stands:

claim here where it is now
kind-annotated type parameters <name: Kind> landed: v1.compiler.parse parse_optional_type_param_kind, with_type_param_kind_property (#11996)
kind inhabitance judged at the applied-generic site, typed KindInhabitance landed: v1.compiler.infer_resolve type_arg_kind_inhabitance, type_param_kind_diagnostics (#11996)
the open defect: the positive control refused (kind_decl.children never consulted) fixed on main: type_arg_kind_inhabitance matches kind_decl.children by identity
positive controls (the admitted inhabitant, the other arm, a generic fn) and wrong-kind negatives (Probe<String>, same-shaped UnrelatedType) landed: test.claim.type_argument_kind_inhabitance_witness_test
TypeParameterInValuePosition "FIRES" not established. Main pins it as an inert hole (a_type_parameter_in_value_position_does_not_yet_refuse_and_this_pins_that_hole). The seed stub has since been regenerated away (#12045). Measuring it and flipping it to a firing RED is P1, which also retires gunbc.kind_reflection_seed_growth by its own trigger
MachineWidth<N> actually reified not done here. P2: reification plus a native-emission receipt
per-kind literal roster stated frontier: std.machine_constraints machine_width_literal_roster_frontier
emitted_field_accessor_panics_on_a_variant_without_the_field, single_arm_sum_parses_as_an_alias_and_becomes_unreadable, type_variable_means_both_declared_generic_and_inference_variable recurring_failure_mode rows: all three are on main (landed via #11996)

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.

0 participants