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

src/v2/compiler/04_infer.dag

@@ -937,14 +937,28 @@ fn lookup_inferred_facts_in_entries(
   )
 }
 
-// THE FACTS MAP IS A NODE-KEYED MAP, BUILT ONCE PER RUN (DESIGN section 6, bare minimum cost): a
-// lookup against the admitted entries list was a scan, so every lookup was linear in the tree and
-// a consumer walking the tree paid quadratic. Entry order still decides a repeated node: the FIRST
-// admitted entry answers, exactly as the scan it replaces did, so a later entry never displaces it.
-fn inferred_facts_map_enter(facts: Map<Node, InferredFacts>, entry: InferredFactsEntry) -> Map<Node, InferredFacts> {
+// ONE KEY, ONE FACT. The facts map is a node-keyed Map built once per run (DESIGN section 6, bare
+// minimum cost: a scan per entry made admission quadratic), and it is admitted here and nowhere else,
+// so this is where a key carrying two DIFFERENT facts refuses. The first-entry-wins rule it replaces
+// dropped a second, differing fact silently, and every consumer read whichever gather produced first.
+// Equal facts under one key are one fact and merge.
+fn infer_facts_key_conflict_diagnostic(key: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^infer_facts_key_conflict,
+    at: node_locus(node: key),
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn inferred_facts_map_enter(facts: Map<Node, InferredFacts>, entry: InferredFactsEntry) -> Outcome<Map<Node, InferredFacts>> {
   match map_lookup(m: facts, key: entry.node) {
-    Present { value: _ } => facts
-    Absent => map_insert(m: facts, key: entry.node, value: entry.facts)
+    Absent => Accepted { value: map_insert(m: facts, key: entry.node, value: entry.facts), diagnostics: None }
+    Present { value: held } =>
+      if held == entry.facts {
+        Accepted { value: facts, diagnostics: None }
+      } else {
+        Rejected { diagnostics: diagnostics_singleton(d: infer_facts_key_conflict_diagnostic(key: entry.node)) }
+      }
   }
 }
 
@@ -954,7 +968,10 @@ fn facts_map_from_entries(entries: List<InferredFactsEntry>) -> Outcome<PartialF
       Rejected { diagnostics: r } => Rejected { diagnostics: r }
       Accepted { value: admitted, diagnostics: d } =>
         if inferred_facts_cover_node(facts: entry.facts, node: entry.node) {
-          Accepted { value: inferred_facts_map_enter(facts: admitted, entry: entry), diagnostics: d }
+          match inferred_facts_map_enter(facts: admitted, entry: entry) {
+            Rejected { diagnostics: r } => Rejected { diagnostics: r }
+            Accepted { value: entered, diagnostics: _ } => Accepted { value: entered, diagnostics: d }
+          }
         } else {
           Rejected {
             diagnostics: diagnostics_singleton(

src/v2/test/infer_facts/facts_key_conflict_test.dag

@@ -0,0 +1,122 @@
+module v2.test.infer_facts.facts_key_conflict
+
+import std.occurrence_identity { OccurrenceId, OccurrenceMinted, OccurrenceSynthetic }
+import std.algebra { Cons, Empty }
+import v2.compiler.infer {
+  facts_map_from_entries,
+  infer_canonical_grounding_incoherent_diagnostic,
+  infer_facts_lookup_miss_diagnostic
+}
+import v2.compiler.inferred_tree { GroundingNotDerived, InferredFacts, InferredFactsEntry }
+import v2.std.diagnostic { Accepted, Rejected, Some, diagnostics_has_reason }
+import v2.std.node { Atom, Node, Symbol, TypeNode }
+import v2.std.optional { Absent, Present }
+import v2.std.witness { Violates }
+
+// The table's admission is the interface under test, so its entries are SUPPLIED: two facts that
+// differ only in their descent witness, under one key. The route through gather is the integration
+// program's qualification, not this module's subject.
+
+fn fkc_key() -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: ^fkc_key } },
+    children: [],
+    occurrence_id: OccurrenceSynthetic
+  }
+}
+
+fn fkc_facts_a() -> InferredFacts {
+  InferredFacts {
+    grounding: GroundingNotDerived { node: fkc_key() },
+    descent: Violates { diagnostic: infer_facts_lookup_miss_diagnostic(key: fkc_key()) }
+  }
+}
+
+fn fkc_facts_b() -> InferredFacts {
+  InferredFacts {
+    grounding: GroundingNotDerived { node: fkc_key() },
+    descent: Violates { diagnostic: infer_canonical_grounding_incoherent_diagnostic(node: fkc_key()) }
+  }
+}
+
+fn fkc_entry(facts: InferredFacts) -> InferredFactsEntry {
+  InferredFactsEntry { node: fkc_key(), facts: facts }
+}
+
+// Differing facts under one key refuse with the conflict reason -- asserted by reason, so a refusal
+// for any other cause does not green this.
+test fn fkc_differing_facts_under_one_key_refuse() -> Bool {
+  match facts_map_from_entries(entries: [fkc_entry(facts: fkc_facts_a()), fkc_entry(facts: fkc_facts_b())]) {
+    Rejected { diagnostics: d } => diagnostics_has_reason(d: Some { diagnostics: d }, reason: ^infer_facts_key_conflict)
+    Accepted { value: _, diagnostics: _ } => false
+  }
+}
+
+// Equal facts under one key are one fact: admitted, and the lookup answers that fact.
+test fn fkc_equal_facts_under_one_key_merge() -> Bool {
+  match facts_map_from_entries(entries: [fkc_entry(facts: fkc_facts_a()), fkc_entry(facts: fkc_facts_a())]) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: table, diagnostics: _ } =>
+      match table.lookup(fkc_key()) {
+        Present { value: f } => f == fkc_facts_a()
+        Absent => false
+      }
+  }
+}
+
+// Positive control for the discriminator: the two supplied facts really differ.
+test fn fkc_supplied_facts_differ() -> Bool {
+  fkc_facts_a() != fkc_facts_b()
+}
+
+// THE KEY IS THE WHOLE STRUCTURAL NODE, OCCURRENCE INCLUDED. A node reached twice -- same minted
+// occurrence, same structure -- is ONE subject: its equal facts are admitted as one entry, never
+// refused. Two structurally DIFFERENT nodes that share a minted occurrence are two keys here; whether
+// such a pair may exist at all is the occurrence admission's question (v2.compiler.inferred_tree
+// authored_occurrence_collisions), not this table's, so the table must not refuse it as a conflict.
+fn fkc_minted_atom(name: Symbol) -> Node {
+  Node {
+    kind: TypeNode { connective: Atom { identity: name } },
+    children: [],
+    occurrence_id: OccurrenceMinted { id: OccurrenceId { value: 7 } }
+  }
+}
+
+fn fkc_minted_entry(node: Node) -> InferredFactsEntry {
+  InferredFactsEntry {
+    node: node,
+    facts: InferredFacts {
+      grounding: GroundingNotDerived { node: node },
+      descent: Violates { diagnostic: infer_facts_lookup_miss_diagnostic(key: node) }
+    }
+  }
+}
+
+test fn fkc_same_minted_node_reached_twice_is_one_subject() -> Bool {
+  let n = fkc_minted_atom(name: ^fkc_same)
+  match facts_map_from_entries(entries: [fkc_minted_entry(node: n), fkc_minted_entry(node: n)]) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: table, diagnostics: _ } =>
+      match table.lookup(n) {
+        Present { value: _ } => true
+        Absent => false
+      }
+  }
+}
+
+test fn fkc_different_nodes_sharing_a_minted_id_are_two_keys() -> Bool {
+  let a = fkc_minted_atom(name: ^fkc_left)
+  let b = fkc_minted_atom(name: ^fkc_right)
+  match facts_map_from_entries(entries: [fkc_minted_entry(node: a), fkc_minted_entry(node: b)]) {
+    Rejected { diagnostics: _ } => false
+    Accepted { value: table, diagnostics: _ } =>
+      match table.lookup(a) {
+        Present { value: fa } =>
+          match table.lookup(b) {
+            Present { value: fb } => fa != fb
+            Absent => false
+          }
+        Absent => false
+      }
+  }
+}