Separate identity admission from semantic grounding

src/v2/compiler/04_infer.dag

@@ -7,7 +7,11 @@ import v2.std.bounded_lattice_completeness {
   partial_bounded_lattice_instances_in_tree
 }
 import v2.compiler.resolve { ResolvedTree }
-import v2.extdeps.languages.dag { dag_node_is_int_literal_atom }
+import v2.extdeps.languages.dag {
+  DagCanonicalBoolLiteral,
+  DagCanonicalIntLiteral,
+  dag_canonical_literal_from_node
+}
 import v2.std.cardinality { TerminationProof, termination_proof_witness_for_node }
 import v2.std.collection {
   List,
@@ -397,7 +401,7 @@ fn concat_inferred_facts_entries(
   })
 }
 
-data infer_node_facts_no_derivation_note: String = "infer_node_facts used to reach solve_constraints with the singleton candidate set [root] and the constraint-satisfaction predicate, whose preservation rule is (algebra == source_facts && candidate == source_facts) with algebra bound to the root itself — so the witness search reduced to root == root and always succeeded. The grounding it minted carried the source node as its own structural evidence, which inferred_facts_resolved_type reads as the node's resolved type. That is source identity standing where a derivation belongs, so this path no longer mints a grounding at all: the descent proof is still derived (it is a real judgment), and the grounding is the typed GroundingNotDerived frontier. solve_constraints itself is untouched — it remains the structural-solve authority named by dag/gunbc/plans/solve_higher_order_design.dag, to be EXTENDED with real candidate generation, never forked."
+data infer_node_facts_no_derivation_note: String = "infer_node_facts used to reach solve_constraints with the singleton candidate set [root] and the constraint-satisfaction predicate, whose preservation rule is (algebra == source_facts && candidate == source_facts) with algebra bound to the root itself — so the witness search reduced to root == root and always succeeded. The grounding it minted carried the source node as its own structural evidence, which inferred_facts_resolved_type reads as the node's resolved type. That is source identity standing where a derivation belongs. The Bool and Int arms now consume the typed canonical-literal query and raise those derivations to leaf facts; every other node on this path carries the typed GroundingNotDerived frontier. solve_constraints itself is untouched — it remains the structural-solve authority named by dag/gunbc/plans/solve_higher_order_design.dag, to be EXTENDED with real candidate generation, never forked."
 
 fn infer_node_facts(n: Node, partials: List<Node>) -> Outcome<InferredFacts> {
   match infer_bounded_lattice_consumer_gate(consumer: n, partials: partials) {
@@ -407,10 +411,25 @@ fn infer_node_facts(n: Node, partials: List<Node>) -> Outcome<InferredFacts> {
         Violates { diagnostic: d } =>
           Rejected { diagnostics: diagnostics_singleton(d: d) }
         Holds { value: descent_proof } =>
-          inferred_facts_not_derived(
-            node: n,
-            descent: Holds { value: descent_proof }
-          )
+          match dag_canonical_literal_from_node(node: n) {
+            Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+              inferred_facts_from_derived_type(
+                node: n,
+                derived_type: bool_node(),
+                descent: Holds { value: descent_proof }
+              )
+            Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+              inferred_facts_from_derived_type(
+                node: n,
+                derived_type: infer_branch_int_binding_type_node(),
+                descent: Holds { value: descent_proof }
+              )
+            Rejected { diagnostics: _ } =>
+              inferred_facts_not_derived(
+                node: n,
+                descent: Holds { value: descent_proof }
+              )
+          }
       }
   }
 }
@@ -520,18 +539,6 @@ fn infer_branch_int_binding_type_node() -> Node {
   }
 }
 
-fn infer_branch_is_bool_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } =>
-      (id == ^dag_token_kw_true) || (id == ^dag_token_kw_false)
-    _ => false
-  }
-}
-
-fn infer_branch_is_int_literal_atom(node: Node) -> Bool {
-  dag_node_is_int_literal_atom(node: node)
-}
-
 fn infer_atom_binding_sym(node: Node) -> Optional<Symbol> {
   match node.kind {
     TypeNode { connective: Atom { identity: sym } } => Present { value: sym }
@@ -598,19 +605,20 @@ fn infer_branch_operand_resolved_type_in_tree(
   facts: InferredFacts,
   tree: Node,
 ) -> Witness<Node> {
-  if infer_branch_is_bool_literal_atom(node: node) {
-    Holds { value: bool_node() }
-  } else if infer_branch_is_int_literal_atom(node: node) {
-    Holds { value: infer_branch_int_binding_type_node() }
-  } else {
-    match infer_atom_binding_sym(node: node) {
-      Present { value: binding } =>
-        match infer_find_arrow_domain_type_in_tree(root: tree, binding: binding) {
-          Present { value: domain_ty } => Holds { value: domain_ty }
-          Absent => inferred_facts_resolved_type(facts: facts)
-        }
-      Absent => inferred_facts_resolved_type(facts: facts)
-    }
+  match dag_canonical_literal_from_node(node: node) {
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+      Holds { value: bool_node() }
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      Holds { value: infer_branch_int_binding_type_node() }
+    Rejected { diagnostics: _ } =>
+      match infer_atom_binding_sym(node: node) {
+        Present { value: binding } =>
+          match infer_find_arrow_domain_type_in_tree(root: tree, binding: binding) {
+            Present { value: domain_ty } => Holds { value: domain_ty }
+            Absent => inferred_facts_resolved_type(facts: facts)
+          }
+        Absent => inferred_facts_resolved_type(facts: facts)
+      }
   }
 }
 
@@ -689,11 +697,17 @@ fn infer_match_bool_arm_body_type(
   body_facts: InferredFacts,
   scrutinee_type: Node
 ) -> Witness<Node> {
-  if infer_branch_type_is_int(type_node: scrutinee_type)
-      && infer_branch_is_bool_literal_atom(node: body_target) {
-    Holds { value: infer_branch_int_binding_type_node() }
-  } else {
-    infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+  match dag_canonical_literal_from_node(node: body_target) {
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } =>
+      if infer_branch_type_is_int(type_node: scrutinee_type) {
+        Holds { value: infer_branch_int_binding_type_node() }
+      } else {
+        infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+      }
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
+    Rejected { diagnostics: _ } =>
+      infer_branch_operand_resolved_type(node: body_target, facts: body_facts)
   }
 }
 
@@ -879,27 +893,15 @@ type InferMatchArmRow {
   body_type: Node
 }
 
-fn infer_branch_is_bool_true_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } => id == ^dag_token_kw_true
-    _ => false
-  }
-}
-
-fn infer_branch_is_bool_false_literal_atom(node: Node) -> Bool {
-  match node.kind {
-    TypeNode { connective: Atom { identity: id } } => id == ^dag_token_kw_false
-    _ => false
-  }
-}
-
 fn infer_bool_literal_pattern_classify(pattern: Node) -> InferBoolLiteralPattern {
-  if infer_branch_is_bool_true_literal_atom(node: pattern) {
-    InferBoolLiteralPatternTrue
-  } else if infer_branch_is_bool_false_literal_atom(node: pattern) {
-    InferBoolLiteralPatternFalse
-  } else {
-    InferBoolLiteralPatternOther
+  match dag_canonical_literal_from_node(node: pattern) {
+    Accepted { value: DagCanonicalBoolLiteral { value: true }, diagnostics: _ } =>
+      InferBoolLiteralPatternTrue
+    Accepted { value: DagCanonicalBoolLiteral { value: false }, diagnostics: _ } =>
+      InferBoolLiteralPatternFalse
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      InferBoolLiteralPatternOther
+    Rejected { diagnostics: _ } => InferBoolLiteralPatternOther
   }
 }
 
@@ -1430,6 +1432,20 @@ fn infer_gather_failed_non_empty(acc: InferGatherFoldAcc) -> NonEmptyDiagnostics
   }
 }
 
+data infer_literal_subtree_diagnostic_discharge_note: String = "An integer literal's modeled type derives from its canonical representation, including its sole named magnitude subtree. Its derivation discharges only that edge's local type frontier; propagating it past the literal would report GroundingNotDerived after Int was derived. Boolean literals are canonical only with no children, so no boolean payload can be discharged. Malformed literals remain GroundingNotDerived and retain every child diagnostic."
+
+fn infer_literal_edge_diagnostics_derived(parent: Node, edge: Edge) -> Bool {
+  match dag_canonical_literal_from_node(node: parent) {
+    Accepted { value: DagCanonicalIntLiteral { magnitude: _ }, diagnostics: _ } =>
+      match edge.label {
+        Named { name: field } => field == ^integer_literal_magnitude_field
+        Positional => false
+      }
+    Accepted { value: DagCanonicalBoolLiteral { value: _ }, diagnostics: _ } => false
+    Rejected { diagnostics: _ } => false
+  }
+}
+
 fn infer_gather_fold_step(
   acc: InferGatherFoldAcc,
   edge: Edge,
@@ -1453,7 +1469,11 @@ fn infer_gather_fold_step(
     )
   } else {
     let merged_entries = concat_inferred_facts_entries(a: acc.entries, b: child.entries)
-    let merged_pending = diagnostics_merge(outer: acc.pending, inner: child.pending)
+    let merged_pending = if infer_literal_edge_diagnostics_derived(parent: acc.node, edge: edge) {
+      acc.pending
+    } else {
+      diagnostics_merge(outer: acc.pending, inner: child.pending)
+    }
     let children_remaining = acc.children_remaining - 1
     if acc.await_branch_row && children_remaining == 0 {
       infer_gather_branch_row_on_entries(

src/v2/compiler/06_translate.dag

@@ -38,6 +38,7 @@ import v2.std.coercion {
   CoercionCandidateSet,
   CoercionResult,
   coercion_candidate_set_from_declared_inhabitants,
+  coercion_identity_from_target_model,
   coercion_fold_with_declared_priority
 }
 import v2.std.diagnostic {
@@ -1245,28 +1246,31 @@ fn coerce_grounded_node(
   tree: InferredTree,
   target: TargetModel
 ) -> Outcome<CoercionResult> {
-  bind_outcome(
-    o: canonical_grounding_for_node(tree: tree, node: source),
-    f: fn(grounding) {
+  match coercion_identity_from_target_model(source: source, target: target) {
+    Accepted { value: identity, diagnostics: d } =>
+      Accepted { value: identity, diagnostics: d }
+    Rejected { diagnostics: _ } =>
       bind_outcome(
         o: target_selection_priority_from_model(target: target),
         f: fn(priority) {
           bind_outcome(
-            o: coercion_candidates_from_target_model(
-              target: target
-            ),
+            o: coercion_candidates_from_target_model(target: target),
             f: fn(candidates) {
-              coercion_fold_with_declared_priority(
-                source: grounding,
-                candidates: candidates,
-                priority: priority
+              bind_outcome(
+                o: canonical_grounding_for_node(tree: tree, node: source),
+                f: fn(grounding) {
+                  coercion_fold_with_declared_priority(
+                    source: grounding,
+                    candidates: candidates,
+                    priority: priority
+                  )
+                }
               )
             }
           )
         }
       )
-    }
-  )
+  }
 }
 fn translate_type_expression_shape_missing_diagnostic(node: Node) -> Diagnostic {
   Diagnostic {

src/v2/extdeps/languages/dag.dag

@@ -144,7 +144,7 @@ import v2.std.compilers.target_model {
   derive_bodied_arrow_scaffold}
 import v2.std.logic { Bool }
 import std.algebra { Cons, Empty }
-import v2.std.algebra { fold_list, for_all, is_empty, list_append, list_snoc_item }
+import v2.std.algebra { fold_list, for_all, is_empty, length, list_append, list_snoc_item }
 import v2.std.diagnostic {
   Accepted,
   Diagnostic,
@@ -4190,6 +4190,40 @@ fn dag_int_literal_magnitude_int_from_node(node: Node) -> Outcome<Int> {
   }
 }
 
+type DagCanonicalLiteral
+  = DagCanonicalBoolLiteral { value: Bool }
+  | DagCanonicalIntLiteral { magnitude: Int }
+
+fn dag_canonical_literal_shape_diagnostic(node: Node) -> Diagnostic {
+  Diagnostic {
+    reason: ^dag_literal_shape_invalid,
+    at: node_locus(node: node),
+    correction: None
+  }
+}
+
+data dag_canonical_literal_query_note: String = "dag_canonical_literal_from_node is the single typed query for inference-facing DAG literal shape. It preserves the Bool-vs-Int distinction and the decoded integer magnitude in a coproduct instead of publishing sibling is_* predicates over Node storage. Bool literals admit exactly the childless true/false atoms. Int literals admit exactly one named, decodable magnitude child. Every other shape is a typed refusal."
+
+fn dag_canonical_literal_from_node(node: Node) -> Outcome<DagCanonicalLiteral> {
+  if dag_node_is_kw_true_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: true })
+  } else if dag_node_is_kw_false_atom(node: node) && (length(xs: node.children) == 0) {
+    outcome_accepted(value: DagCanonicalBoolLiteral { value: false })
+  } else if dag_node_is_int_literal_atom(node: node) && (length(xs: node.children) == 1) {
+    match dag_int_literal_magnitude_int_from_node(node: node) {
+      Accepted { value: magnitude, diagnostics: d } =>
+        Accepted {
+          value: DagCanonicalIntLiteral { magnitude: magnitude },
+          diagnostics: d
+        }
+      Rejected { diagnostics: _ } =>
+        outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+    }
+  } else {
+    outcome_rejected(dag_canonical_literal_shape_diagnostic(node: node))
+  }
+}
+
 fn dag_type_atom_node(identity: Symbol) -> Node {
   Node {
     kind: TypeNode { connective: Atom { identity: identity } },