diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag new file mode 100644 index 00000000000..25b0a6312d1 --- /dev/null +++ b/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 { [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 { [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 { [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 { [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 { [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 { [maybe()] }\n" + +test fn w_optional_carrier_is_undecidable_not_refused() -> Bool { + violation_count(source: optional_carrier_source, wanted: "DeclaredTypeNotInhabited") == 0 +} diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index fc274a20dac..9363ee5a25a 100644 --- a/src/v1/00_core.dag +++ b/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, span: SourceSpan } | CallArgumentNameUnknown { callee: String, argument: String, declared: List, 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: _ } => diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 06c96c36d9d..ab59ce42ec8 100644 --- a/src/v1/04_infer.dag +++ b/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 { + 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) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 02f2dec47fa..06b7fe007b4 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4740,6 +4740,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (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) -> (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(), diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 8112a08f73f..ced4032c1ee 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1,7 +1,11 @@ // Generated by v1 compiler -- do not edit. // Source module: v1.compiler.infer +use self::DeclaredTypePosition::*; use self::DescentSizeExpr::*; +use self::InhabitanceRefusalReason::*; +use self::InhabitanceUndecidableReason::*; +use self::InhabitanceVerdict::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, }; @@ -3047,6 +3051,169 @@ pub fn coproduct_variant_payload_admits_type_name( } } +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum DeclaredTypePosition { + PositionRecordLiteralField, + PositionListElement, + PositionMapValue, + PositionDataInitializer, + PositionDeclaredReturn, + PositionLetAnnotation, + PositionVariantPayload, + PositionGenericTypeArgument, + PositionCastTarget, + PositionParameterDefault, + PositionCallableReturn, + PositionDirectCallArgument, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct DeclaredTypeObligation { + pub position: DeclaredTypePosition, + pub declared: Rc, + pub produced: Rc, + pub span: Rc, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceUndecidableReason { + UndecidableGenericFormal, + UndecidableOptionalCarrier, + UndecidableFormalUnresolved, + UndecidableProducedIdentityErased, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceRefusalReason { + RefusedPayloadAtParent, + RefusedKernelAtStructured, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum InhabitanceVerdict { + Inhabits, + InhabitanceRefused { + reason: InhabitanceRefusalReason, + }, + InhabitanceUndecidable { + reason: InhabitanceUndecidableReason, + }, +} + +pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position.clone() { + DeclaredTypePosition::PositionRecordLiteralField => "record literal field".to_string(), + DeclaredTypePosition::PositionListElement => "list element".to_string(), + DeclaredTypePosition::PositionMapValue => "map value".to_string(), + DeclaredTypePosition::PositionDataInitializer => "data initializer".to_string(), + DeclaredTypePosition::PositionDeclaredReturn => "declared return".to_string(), + DeclaredTypePosition::PositionLetAnnotation => "let annotation".to_string(), + DeclaredTypePosition::PositionVariantPayload => "variant payload".to_string(), + DeclaredTypePosition::PositionGenericTypeArgument => "generic type argument".to_string(), + DeclaredTypePosition::PositionCastTarget => "cast target".to_string(), + DeclaredTypePosition::PositionParameterDefault => "parameter default".to_string(), + DeclaredTypePosition::PositionCallableReturn => "callable return".to_string(), + DeclaredTypePosition::PositionDirectCallArgument => "direct call argument".to_string(), + } +} + +pub fn declared_type_inhabitance( + obligation: Rc, + scope: Rc, +) -> Rc { + { + let declared = obligation.declared.clone(); + let produced = obligation.produced.clone(); + let source_indices = scope.type_env.clone().source_indices.clone(); + let declared_name = authored_name_at(source_indices.clone(), declared.clone()); + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let either_optional = ((declared.return_cardinality.clone() == Cardinality::CardOptional) + || (produced.return_cardinality.clone() == Cardinality::CardOptional)); + let declared_is_generic = ((declared.params.clone().len() as i64) > 0); + if either_optional.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableOptionalCarrier, + }) + } else { + if declared_is_generic.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableGenericFormal, + }) + } else { + if (declared_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableFormalUnresolved, + }) + } else { + if (produced_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, + }) + } else { + if kernel_value_declared_type_mismatch( + declared.clone(), + produced.clone(), + scope.type_env.clone(), + source_indices.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + }) + } else { + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + }) + } else { + Rc::new(InhabitanceVerdict::Inhabits) + } + } + } + } + } + } + } +} + +pub fn declared_type_obligation_diags( + obligation: Rc, + scope: Rc, +) -> Rc>> { + match (*declared_type_inhabitance(obligation.clone(), scope.clone())).clone() { + InhabitanceVerdict::Inhabits => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceUndecidable { reason: _, .. } => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { + position: declared_type_position_label(obligation.position.clone()), + expected: node_type_shape( + obligation.declared.clone(), + scope.type_env.clone().source_indices.clone(), + ), + got: node_type_shape( + obligation.produced.clone(), + scope.type_env.clone().source_indices.clone(), + ), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]), + } +} + pub fn coproduct_payload_where_parent_required( formal: Rc, actual: Rc, @@ -8150,13 +8317,38 @@ if ((call_ambiguity_cands.clone().len() as i64) > 0) { } __result }); - let elem_diags = Rc::new({ - let mut __result = Vec::new(); - for r in elem_results.iter().cloned() { - __result.extend((*r.diagnostics.clone()).iter().cloned()); - } - __result - }); + let elem_inhabitance_diags = match elem_expected.clone() { + Some(declared_elem) => Rc::new({ + let mut __result = Vec::new(); + for te in typed_elements.iter().cloned() { + __result.extend( + (*declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionListElement, + declared: declared_elem.clone(), + produced: resolved_type(te.clone()), + span: te.span.clone(), + }), + scope.clone(), + )) + .iter() + .cloned(), + ); + } + __result + }), + None => Rc::new(vec![]), + }; + let elem_diags = v1_rt::concat( + Rc::new({ + let mut __result = Vec::new(); + for r in elem_results.iter().cloned() { + __result.extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + elem_inhabitance_diags.clone(), + ); let elem_type_node = if ((elem_results.clone().len() as i64) > 0) { match elem_results.clone().first().cloned() { Some(r) => resolved_type(r.typed.clone()), @@ -21862,3 +22054,40 @@ pub fn reconcile_with_census_extra( }) } } + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionRecordLiteralField; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionListElement; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionMapValue; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDataInitializer; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDeclaredReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionLetAnnotation; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionVariantPayload; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionGenericTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCastTarget; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionParameterDefault; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCallableReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDirectCallArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableGenericFormal; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableOptionalCarrier; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableFormalUnresolved; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableProducedIdentityErased; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedPayloadAtParent; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedKernelAtStructured; diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index ef800cf006c..cf0d36f6381 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -527,6 +527,12 @@ pub enum CompilerDiagnostic { constructor_decl_name: String, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -678,6 +684,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::CallArgumentNameUnknown { span: s, .. } => s.clone(), @@ -727,6 +734,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, .. } => v1_rt::concat(v1_rt::concat("admit_callers entry on '".to_string(), cn.clone()), "' 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".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::CallArgumentNameUnknown { callee: c, argument: a, declared: ds, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("call shape mismatch calling '".to_string(), c.clone()), "': no parameter named '".to_string()), a.clone()), "' (declared: [".to_string()), ds.clone().join(&", ".to_string())), "])".to_string()), diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index b2e166c3811..8c93523b661 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -1,7 +1,7 @@ module v2.test.execution.emit_on_demand_match_loop_fold_family_witness import std.logic { Bool } -import std.types { String } +import std.types { Int, String } import std.content_hash { ContentHash, Fnv1a64Structural } import std.measure { ByteSize, byte_size } import std.cache_interface { @@ -73,7 +73,6 @@ import v2.test.emit.fold_call_closure_fixture { fold_fixture_param_canonical_arrow, fold_fixture_param_wrong_arrow, } -import v2.std.machine { Byte } import v2.std.collection { List } @@ -122,12 +121,31 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } -data match_expected_octets: List = [0, 1, 0, 0, 0] -data match_alt_expected_octets: List = [0, 2, 0, 0, 0] -data loop_expected_octets: List = [0, 1, 0, 0, 0] -data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] -data fold_expected_octets: List = [0, 7, 0, 0, 0] -data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] +// WHY List AND NOT List, AND WHAT WOULD REPLACE IT. These rows are octet +// values compared against emitted bytes. They were declared List while holding +// integers, which the list-element inhabitance obligation refused: std.bit's Byte is +// `type Byte { bits: List }`, a bit-record, so an Int literal never inhabited it. +// The consumer's signature already carried the right type -- v2.compiler.emit_host +// `emit_host_octets_byte_string(octets: List)` -- so this is the declaration +// agreeing with its single authority, not a carrier weakened to satisfy a wall. +// +// Int is nonetheless weaker than the values deserve: an octet is 0..255 and nothing +// here says so. The correctly shaped type already exists and is grounded -- +// extdeps.network.ipv4 `Octet`, declared as Int refined by range(min: 0, max: 255) -- +// but it is homed in the IPv4 domain, and reaching into a network module for a +// compiler-emission byte would be the layer inversion DESIGN 3 warns about rather +// than a reuse. What is missing is a domain-agnostic octet carrier, not a new +// spelling of one that exists. +// +// So the pointer, deliberately stated as rationale rather than a machine claim: when +// such a carrier lands, these rows and emit_host_octets_byte_string's parameter move +// to it together -- the parameter first, since the declaration follows its consumer. +data match_expected_octets: List = [0, 1, 0, 0, 0] +data match_alt_expected_octets: List = [0, 2, 0, 0, 0] +data loop_expected_octets: List = [0, 1, 0, 0, 0] +data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] +data fold_expected_octets: List = [0, 7, 0, 0, 0] +data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] fn match_fixture_inputs() -> Inputs { inputs_for_emit_host( @@ -212,7 +230,7 @@ fn mlf_family_member_run( source: Medium, member_id: String, expect_compile_skipped: Bool, - expected_octets: List + expected_octets: List ) -> Bool { match run_emit_host_cached_with_run_args( workspace_dir: workspace,