v2 infer: a key carrying two different facts refuses; equal facts merge

[gunbai-bot]

Step 1 of node adhoc-3e34606f-ffc: a key in v2 infer's facts table carries one fact.

The diff against main is src/v2/compiler/04_infer.dag and src/v2/test/infer_facts/facts_key_conflict_test.dag. #12549 and #12557, which this was stacked on, have landed.

Change

v2.compiler.infer inferred_facts_map_enter, the one admission point of the node-keyed facts Map (#12557), used to keep the first entry under a key and silently drop a later, different fact. It now:

• refuses with ^infer_facts_key_conflict, located at the key through node_locus, when a key arrives with a different fact;
• merges an equal fact, which is one subject reached twice.

facts_map_from_entries threads the refusal out. Admission stays one map_lookup per entry: review 72444's quadratic-scan finding was fixed by building on the keyed Map.

The key is the whole structural Node, occurrence included. So one node reached twice is one subject, and two structurally different nodes that share a minted id are two keys here. Whether such a pair may exist is the occurrence admission's question (#12790 / #12605), not this table's.

Evidence (gunbc run --function, remote)

claim	head	pre-wall (first-wins insert)
fkc_differing_facts_under_one_key_refuse	true	false
fkc_equal_facts_under_one_key_merge	true	true
fkc_supplied_facts_differ (control: the planted facts differ)	true	true
fkc_same_minted_node_reached_twice_is_one_subject	true	—
fkc_different_nodes_sharing_a_minted_id_are_two_keys	true	—

The first three were run with the refusal reverted to first-wins, and the refusal claim flipped. The last two ran at b27a773; this file and the refusal are unchanged since then.

Audit of claims that passed only because of the defect

The required floor was green when first-wins became a refusal: no enrolled claim was green only because a conflicting fact was dropped. That bound is the floor's selected set. One known specimen off main: #12506's synthetic_facts_key_collision claims assert the disagreement exists. Per ruling, whichever of #12582 or #12506 lands second flips them to assert this refusal, keeping the raw-entry disagreement as the control.

The facts key is within-run only: the Map is built and consumed inside one infer call, and is never persisted or compared across runs, which is compatible with #12604 PR2's allocated occurrence ids.

🤖 Generated with Claude Code

[briansrls]

The subject your conflict check refuses on: the empty synthetic Conj

#12582 is doing its job — this is a report of what it caught, not a request to relax it. Handing it to the facts-identity owner with the producer, parent edge, and consumer named, and with one question that must be answered before any key is proposed.

Build identity for every number below

head	8ea7415dc422068061b5cde7c2902cb9e6dfdb94 (lane/reference-evidence-consumer)
claim_batch	2026-10-01 10:54:55, sha256 90bcc97a016bc876
gunbc	2026-10-01 10:54:56, sha256 80a01a1f1f45273e

An earlier instrument on this lane was stale (six seed commits after its build, including #12550's merge). Every measurement I reported from it is void; everything here is from the binaries above.

The subject, enumerated

The conflicting key is:

Node { kind: TypeNode { connective: Conj }, children: [], occurrence_id: OccurrenceSynthetic }

• Conj, zero children, OccurrenceSynthetic — each measured separately, not inferred from shape.
• Reachable from more than one parent edge in a single resolved tree, so one key genuinely serves several positions.
• Facts consumer: v2.compiler.infer inferred_facts_map_enter, via facts_map_from_entries. The entries list itself is clean — infer_entries_for_tree accepts; the refusal is at map admission.
• Producers include v2.std.algebra, where the empty Conj is the empty FreeMonoid — so every empty list in a program is literally the same node — alongside body_lowering_fold's empty_interior / empty_suffix / NoTypeParams arm and fold_lowering's empty-conj mint.
• The two entries under the key differ, but not in derived-ness of grounding, nor descent, nor denotation as those compare — so the difference is in the grounding's recorded subject, not in a verdict.

The trigger, which is sharper than "a projection fixture"

A named call whose argument is an Int literal refuses; the same call whose argument is a parameter accepts.

fn consumer() -> Int { callee(only_arg: 3) }    // refuses: infer_facts_key_conflict
fn consumer(y: Int) -> Int { callee(only_arg: y) }  // accepts

That cost me two wrong readings before I used the fixture's own text, so it is worth stating plainly: the literal mints a further synthetic node that collides.

Current blast radius on this lane

11 rows red, all one cause: nine of ten in v2.test.claim.callexec.declaration_reference_eval (named-call execution, argument-dependence, the Bool pair separating) and two in v2.test.claim.field_projection.field_projection_stages. These were green before the merge and are not repaired by anything in this lane.

The question that precedes a key, and the two things that do not answer it

Before proposing an identity, the owner needs to decide whether the empty value is the true semantic subject, or a child incorrectly carrying its parent's contextual facts. The second reading is live: an empty list is the same value everywhere, so if two positions legitimately share it, the defect is that facts contextual to a PARENT were recorded against a child that has no context of its own — and a key would then be encoding a mistake rather than fixing one.

• v2 infer: a key carrying two different facts refuses; equal facts merge #12582 stays fail-closed. The refusal is correct against the tree it receives; nothing here asks for first-entry-wins back.
• MQ PR2 (cut): lowering images close at their named root; members get allocated OccurrenceProjected #12790 does not resolve this. Measured, not assumed: composed onto this lane's head (one real conflict, resolved so the single callable-Arrow constructor closes its own image — which makes that cut smaller, since it wraps one site instead of three), both red rows still refuse. It assigns OccurrenceProjected to lowering-image members; it does not assign identities to surviving synthetic nodes, which is what this key is.

Happy to supply the enumeration probes, run any discriminating fixture on the pinned binaries above, or re-run the native eight once a repair lands.

🤖 Generated with Claude Code