Declared-type inhabitance: one obligation carrier, one deciding relation, first position wired

dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag

@@ -0,0 +1,138 @@
+module test.claim.declared_type_inhabitance_list_element_witness
+
+import gunbc.compile_diagnostic_census {
+  CompileDiagnosticCensus,
+  CensusObserved,
+  CensusNotRunnable,
+  census_rows_of_class,
+  census_total_count
+}
+import std.types { String, Bool, Int }
+import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
+
+// SUBSTRATE-ONLY, AND THE EARLIER ReadsLiveTree DECLARATION MADE EVERY ARM BELOW INERT. A
+// ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED -- so these
+// arms were enrolled, reviewed, cited as this PR's executable evidence, and executed by nothing.
+// That is the specification-without-execution trap DESIGN 5 calls the deepest one, and it is
+// worse here than a missing test would have been, because the arms were named as the reason the
+// class had climbed. The sibling test.claim.direct_call_argument_type_witness had already made
+// this exact move and said why: an assertion in a live-tree module is "enrolled and inert ...
+// wearing the costume of a populated probe corpus". This file needs no live read -- every arm
+// hands compile_dag_diagnostic_census a source STRING it authors itself -- so nothing is lost by
+// declaring what it actually consumes.
+data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly
+
+// THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that
+// declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression
+// rather than a missing nicety, and it is not softened to mitigatable anywhere in this file.
+//
+// WHY ONE CARRIER AND NOT ONE CHECK PER POSITION. The grammar has fourteen type positions;
+// twelve can receive a source value. Before the obligation carrier, each position that judged
+// anything judged it with its own local chain of predicates -- one rule in N representations,
+// where a position added later inherits nothing and a rule repaired at one position stays
+// broken at the rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was
+// declared and WHAT was produced; declared_type_inhabitance is the single relation that
+// decides; the position rides along so the diagnostic can locate the refusal without the
+// decision procedure forking. This file is the executing evidence for the FIRST position wired
+// through that carrier, and its arms are the shape every later position reuses.
+//
+// THE RELATION CONSUMES, IT DOES NOT RE-DERIVE. Alias identity is decided once in the tree:
+// coproduct_payload_where_parent_required peels transparent aliases through
+// transparent_alias_identity_agrees, and the kernel arm defers to
+// kernel_value_declared_type_mismatch. A second answer to either question authored here would
+// be the nicknaming failure at the level of judgments.
+//
+// PATH SCOPE, per DESIGN 4b's rung-per-path rule: this asserts source -> .dag acceptance only.
+// The refusal sits in inference, so nothing reaches emission with a non-inhabiting list
+// element -- but that is a consequence of where the wall sits, not a second measurement, and
+// it is not claimed as one.
+
+fn violation_count(source: String, wanted: String) -> Int {
+  match compile_dag_diagnostic_census(source) {
+    CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted))
+    CensusNotRunnable { cause: _ } => 0 - 1
+  }
+}
+
+// RED ARM ONE -- the plain kernel at a structured declared type. This is the floor case, and it
+// is in this file because the FIRST wiring of the carrier ACCEPTED it: the relation consulted
+// only the payload-at-parent predicate, so RefusedKernelAtStructured was a declared verdict
+// variant that no code path could produce. A variant nothing constructs is a decoration that
+// reads as coverage, which is the rung inflation DESIGN 4b names. This arm exists so that
+// deleting the kernel route from the relation goes red rather than quiet.
+data kernel_at_structured_source: String = "module probe_inhabit_nega\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List<Rel> { [7] }\n"
+
+test fn w_plain_kernel_at_declared_list_element_is_refused() -> Bool {
+  violation_count(source: kernel_at_structured_source, wanted: "DeclaredTypeNotInhabited") >= 1
+}
+
+// RED ARM TWO -- an arm's PAYLOAD type standing where the PARENT coproduct is declared. The
+// shape gunbc#8865 recorded, measured here at the list-element position rather than inferred
+// from the record-field one: two positions are two paths, and a wall proven at one says
+// nothing about the other.
+data payload_at_parent_source: String = "module probe_inhabit_negb\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk_inner() -> Inner { Inner { v: 1 } }\nfn probe() -> List<Rel> { [mk_inner()] }\n"
+
+test fn w_arm_payload_where_parent_declared_is_refused() -> Bool {
+  violation_count(source: payload_at_parent_source, wanted: "DeclaredTypeNotInhabited") >= 1
+}
+
+// GREEN ARM -- the control that stops the wall being a wrecking ball. A genuine member of the
+// declared coproduct must still compile and must raise NO inhabitance diagnostic. Without it,
+// a relation that refused every list element would score identically on both red arms above,
+// and the reds would establish nothing.
+data inhabiting_member_source: String = "module probe_inhabit_pos\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List<Rel> { [SameRev] }\n"
+
+test fn w_declared_coproduct_member_is_accepted() -> Bool {
+  violation_count(source: inhabiting_member_source, wanted: "DeclaredTypeNotInhabited") == 0
+}
+
+// REACHABILITY -- an undefined name at the same position must refuse whether or not the
+// inhabitance wall exists. This separates "the position is judged and the value was refused"
+// from "the position is never reached at all", which the accepting arms above cannot
+// distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately:
+// keying it on DeclaredTypeNotInhabited would make it a second copy of arm one.
+//
+// THE ASSERTION MUST BE POSITIVE, AND AN EARLIER REVISION OF IT WAS NOT. This arm shipped
+// asserting DeclaredTypeNotInhabited == 0 -- the wall's OWN class, at zero -- while the prose
+// above claimed it keyed on a different one. That assertion is satisfied identically by "the
+// position is judged and our wall correctly stayed silent" and by "the position is never
+// reached by anything", which is precisely the distinction the arm exists to make, so it read
+// as coverage while carrying none. It is DESIGN's reachability-read-as-occupancy failure
+// turned on a control: a zero is only readable beside a nonzero. Corrected to demand the
+// refusal it was named for (review 54993).
+//
+// WHY InternalError IS THE CLASS: an unresolved value name is refused by v1.compiler.04_infer
+// through inference_error, which constructs InternalError { message } -- measured, not assumed
+// ("undefined variable 'nosuchname_zzz_probe'" against this exact source). It is coarser than
+// the shape deserves, and that coarseness is why the paired green arm below is not optional:
+// alone, a positive InternalError count could be produced by any unrelated defect in the
+// probe. The pair is what makes the undefined NAME the thing being measured.
+data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List<Rel> { [nosuchname_zzz_probe] }\n"
+
+// The same source with the name DEFINED and nothing else changed. It is the discriminator for
+// the arm above: if this also reported InternalError, the positive count there would be an
+// artifact of the probe rather than evidence about the name.
+data defined_name_source: String = "module probe_inhabit_reach_ok\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk() -> Rel { SameRev }\nfn probe() -> List<Rel> { [mk()] }\n"
+
+test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool {
+  violation_count(source: undefined_name_source, wanted: "InternalError") > 0
+    && violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0
+}
+
+test fn w_reachability_control_discriminates_on_the_name() -> Bool {
+  violation_count(source: defined_name_source, wanted: "InternalError") == 0
+    && violation_count(source: defined_name_source, wanted: "DeclaredTypeNotInhabited") == 0
+}
+
+// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the
+// declared position is genuinely undecidable at this seam -- optionality lives in
+// return_cardinality while the produced value carries the nominal coproduct, so the two are
+// not comparable here without peeling a representation this relation does not own. It must
+// therefore NOT refuse. This arm is what keeps Undecidable honest: if the relation ever starts
+// refusing optionals it goes red, and if a future author repurposes an Undecidable reason to
+// mean "unimplemented" this is the arm that notices.
+data optional_carrier_source: String = "module probe_inhabit_opt\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn maybe() -> Rel? { none }\nfn probe() -> List<Rel?> { [maybe()] }\n"
+
+test fn w_optional_carrier_is_undecidable_not_refused() -> Bool {
+  violation_count(source: optional_carrier_source, wanted: "DeclaredTypeNotInhabited") == 0
+}

src/v1/00_core.dag

@@ -195,6 +195,7 @@ type CompilerDiagnostic
       span: SourceSpan
     }
   | AdmitCallersEntryNotDeclRef { constructor_decl_name: String, span: SourceSpan }
+  | DeclaredTypeNotInhabited { position: String, expected: String, got: String, span: SourceSpan }
   | UnlistedImportUse { name: String, span: SourceSpan }
   | AmbiguousReference { name: String, candidates: List<String>, span: SourceSpan }
   | CallArgumentNameUnknown { callee: String, argument: String, declared: List<String>, span: SourceSpan }
@@ -334,6 +335,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan {
       span: s
     } => s
     AdmitCallersEntryNotDeclRef { constructor_decl_name: _, span: s } => s
+    DeclaredTypeNotInhabited { position: _, expected: _, got: _, span: s } => s
     UnlistedImportUse { name: _, span: s } => s
     AmbiguousReference { name: _, candidates: _, span: s } => s
     CallArgumentNameUnknown { callee: _, argument: _, declared: _, span: s } => s
@@ -407,6 +409,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String {
       )
     AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, span: _ } =>
       concat("admit_callers entry on '", cn, "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored")
+    DeclaredTypeNotInhabited { position: pos, expected: e, got: g, span: _ } =>
+      concat("value does not inhabit its declared type at the ", pos, ": declared '", e, "', produced '", g, "'")
     UnlistedImportUse { name: n, span: _ } => concat("unlisted import use '", n, "' (referenced but not in any import's name list)")
     AmbiguousReference { name: n, candidates: cs, span: _ } => concat("ambiguous reference '", n, "': ", to_string(value: cs |> count), " candidates: ", join(cs, separator: ", "), " — qualify by containment path, alias, or rename")
     CallArgumentNameUnknown { callee: c, argument: a, declared: ds, span: _ } =>

src/v1/04_infer.dag

@@ -2085,6 +2085,122 @@ fn coproduct_variant_payload_admits_type_name(
 // makes "the actual is one of this coproduct's payload types" undecidable from the declaration
 // alone; refusing there would be a fabricated refusal, which DESIGN section 5 forbids exactly as it
 // forbids a fabricated success.
+// ONE OBLIGATION, ONE AUTHORITY. The grammar has fourteen type positions and twelve of them
+// can receive a source value. Before this carrier each position that judged anything judged it
+// with its own local chain of else-if predicates, which is one rule in N representations: a
+// position added later inherits nothing, and a rule fixed at one position stays broken at the
+// rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was declared and WHAT
+// was produced; declared_type_inhabitance is the single relation that decides; the position
+// travels with the obligation so the diagnostic can locate the refusal without the decision
+// procedure forking per position.
+type DeclaredTypePosition
+  = PositionRecordLiteralField
+  | PositionListElement
+  | PositionMapValue
+  | PositionDataInitializer
+  | PositionDeclaredReturn
+  | PositionLetAnnotation
+  | PositionVariantPayload
+  | PositionGenericTypeArgument
+  | PositionCastTarget
+  | PositionParameterDefault
+  | PositionCallableReturn
+  | PositionDirectCallArgument
+
+type DeclaredTypeObligation {
+  position: DeclaredTypePosition
+  declared: Node
+  produced: Node
+  span: SourceSpan
+}
+
+// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. Each reason names something the
+// modeled facts genuinely cannot settle at this seam. A position that has not been wired yet is
+// NOT undecidable -- it is a missing obligation producer, and it is absent from the census
+// rather than present with a verdict. Reading "we did not look" as "it cannot be decided" is
+// the rung inflation DESIGN 4b names, applied to this relation's own self-description.
+type InhabitanceUndecidableReason
+  = UndecidableGenericFormal
+  | UndecidableOptionalCarrier
+  | UndecidableFormalUnresolved
+  | UndecidableProducedIdentityErased
+
+type InhabitanceRefusalReason
+  = RefusedPayloadAtParent
+  | RefusedKernelAtStructured
+
+type InhabitanceVerdict
+  = Inhabits
+  | InhabitanceRefused { reason: InhabitanceRefusalReason }
+  | InhabitanceUndecidable { reason: InhabitanceUndecidableReason }
+
+fn declared_type_position_label(position: DeclaredTypePosition) -> String {
+  match position {
+    PositionRecordLiteralField => "record literal field"
+    PositionListElement => "list element"
+    PositionMapValue => "map value"
+    PositionDataInitializer => "data initializer"
+    PositionDeclaredReturn => "declared return"
+    PositionLetAnnotation => "let annotation"
+    PositionVariantPayload => "variant payload"
+    PositionGenericTypeArgument => "generic type argument"
+    PositionCastTarget => "cast target"
+    PositionParameterDefault => "parameter default"
+    PositionCallableReturn => "callable return"
+    PositionDirectCallArgument => "direct call argument"
+  }
+}
+
+// THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating
+// them: coproduct_payload_where_parent_required already peels transparent aliases through
+// transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the
+// tree and this relation inherits it instead of re-deriving a second answer.
+fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferScope) -> InhabitanceVerdict {
+  let declared = obligation.declared
+  let produced = obligation.produced
+  let source_indices = scope.type_env.source_indices
+  let declared_name = authored_name_at(source_indices: source_indices, node: declared)
+  let produced_name = authored_name_at(source_indices: source_indices, node: produced)
+  let either_optional = declared.return_cardinality == CardOptional || produced.return_cardinality == CardOptional
+  let declared_is_generic = (declared.params |> count) > 0
+  if either_optional {
+    InhabitanceUndecidable { reason: UndecidableOptionalCarrier }
+  } else if declared_is_generic {
+    InhabitanceUndecidable { reason: UndecidableGenericFormal }
+  } else if declared_name == "" {
+    InhabitanceUndecidable { reason: UndecidableFormalUnresolved }
+  } else if produced_name == "" {
+    InhabitanceUndecidable { reason: UndecidableProducedIdentityErased }
+  } else if kernel_value_declared_type_mismatch(
+      formal: declared, actual: produced,
+      type_env: scope.type_env, source_indices: source_indices) {
+    InhabitanceRefused { reason: RefusedKernelAtStructured }
+  } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) {
+    InhabitanceRefused { reason: RefusedPayloadAtParent }
+  } else {
+    Inhabits
+  }
+}
+
+// The obligation carries its own position, so ONE emitter locates every refusal. A per-position
+// diagnostic function would be the N-representation problem moved one layer down.
+fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List<ErrorNode> {
+  match declared_type_inhabitance(obligation: obligation, scope: scope) {
+    Inhabits => []
+    InhabitanceUndecidable { reason: _ } => []
+    InhabitanceRefused { reason: _ } =>
+      [make_error_node(
+        diagnostic: DeclaredTypeNotInhabited {
+          position: declared_type_position_label(position: obligation.position),
+          expected: node_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices),
+          got: node_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices),
+          span: obligation.span
+        },
+        module_name: scope.module_name
+      )]
+  }
+}
+
 fn coproduct_payload_where_parent_required(
   formal: Node,
   actual: Node,
@@ -4617,7 +4733,22 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu
       }
       let elem_results = elements |> map(e => infer_expr(texpr: e, scope: scope, expected: elem_expected))
       let typed_elements = elem_results |> map(r => r.typed)
-      let elem_diags = flat_map(elem_results, r => r.diagnostics)
+      let elem_inhabitance_diags = match elem_expected {
+        Present { value: declared_elem } =>
+          flat_map(typed_elements, te =>
+            declared_type_obligation_diags(
+              obligation: DeclaredTypeObligation {
+                position: PositionListElement,
+                declared: declared_elem,
+                produced: resolved_type(n: te),
+                span: te.span
+              },
+              scope: scope
+            )
+          )
+        Absent => []
+      }
+      let elem_diags = concat(flat_map(elem_results, r => r.diagnostics), elem_inhabitance_diags)
       let elem_type_node = if count(elem_results) > 0 {
         match first(elem_results) {
           Present { value: r } => resolved_type(n: r.typed)

src/v1/stage0/src/cli_run.rs

@@ -4740,6 +4740,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc<ErrorNode>) -> (String, Str
             "ConstructorCallAdmissionRefused"
         }
         CompilerDiagnostic::AdmitCallersEntryNotDeclRef { .. } => "AdmitCallersEntryNotDeclRef",
+        CompilerDiagnostic::DeclaredTypeNotInhabited { .. } => "DeclaredTypeNotInhabited",
         CompilerDiagnostic::UnlistedImportUse { .. } => "UnlistedImportUse",
         CompilerDiagnostic::AmbiguousReference { .. } => "AmbiguousReference",
         CompilerDiagnostic::CallArgumentNameUnknown { .. } => "CallArgumentNameUnknown",
@@ -4789,6 +4790,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc<ErrorNode>) -> (String, Str
             constructor_decl_name,
             ..
         } => constructor_decl_name.clone(),
+        CompilerDiagnostic::DeclaredTypeNotInhabited { position, .. } => position.clone(),
         CompilerDiagnostic::UnlistedImportUse { name, .. } => name.clone(),
         CompilerDiagnostic::AmbiguousReference { name, .. } => name.clone(),
         CompilerDiagnostic::CallArgumentNameUnknown { argument, .. } => argument.clone(),