diff --git a/dag/examples/nominal_distinctness_witness/twin.dag b/dag/examples/nominal_distinctness_witness/twin.dag deleted file mode 100644 index 8bef7141137..00000000000 --- a/dag/examples/nominal_distinctness_witness/twin.dag +++ /dev/null @@ -1,14 +0,0 @@ -module examples.nominal_distinctness_twin - -type UserId { - raw: Int -} - -fn lookup(id: UserId) -> Int { - id.raw -} - -fn main() -> Int { - let acct = UserId { raw: 7 } - lookup(id: acct) -} diff --git a/dag/examples/nominal_distinctness_witness/witness.dag b/dag/examples/nominal_distinctness_witness/witness.dag deleted file mode 100644 index 78c17b4a44f..00000000000 --- a/dag/examples/nominal_distinctness_witness/witness.dag +++ /dev/null @@ -1,18 +0,0 @@ -module examples.nominal_distinctness_witness - -type UserId { - raw: Int -} - -type AccountId { - raw: Int -} - -fn lookup(id: UserId) -> Int { - id.raw -} - -fn main() -> Int { - let acct = AccountId { raw: 7 } - lookup(id: acct) -} diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index 7f1125e09f0..d9acd2d48df 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -137,3 +137,114 @@ data record_directly_at_coproduct_arg_source: String = "module probe_inhabit_dc_ test fn w_the_same_wrong_pair_directly_at_the_argument_is_refused() -> Bool { violation_count(source: record_directly_at_coproduct_arg_source, wanted: "DeclaredTypeNotInhabited") > 0 } + +// THE NOMINAL-PRODUCT ARM, AND THE THREE SHAPES IT WAS BUILT FROM. Each source below was +// measured on a compiler built from this tree BEFORE the arm landed, as its own entry compile, +// and each reported ZERO blocking diagnostics -- so these are discriminating REDs against the +// prior compiler, not restatements of behaviour that already held. They are kept enrolled after +// the climb, per DESIGN 4b(4): the evidence that a wall stays real is not the production +// handling it replaced. +// +// WHY THE ACTUAL IS A CALL AND NOT A RECORD LITERAL, in every red arm here. A record literal at +// a non-generic formal was ALREADY refused, by structured_application_site_type_mismatch, which +// judges only an actual whose EXPRESSION is a record literal. Writing these probes with literals +// would therefore have measured that older producer and enrolled its answer as evidence about +// this one -- the mis-design the list-element pair above records having made once. A call is the +// spelling no producer judged. + +// RED BEFORE, GREEN NOW -- DISTINCT APPLIED CONSTRUCTORS. Alpha reaching a Beta +// parameter. Both sides are applications, both constructors resolve to declared products, and +// the two constructors are unrelated by alias, brand or cast. +data applied_distinct_constructor_source: String = "module probe_inhabit_applied_ctor\nimport std.types { String }\ntype Alpha

{ a: P }\ntype Beta

{ b: P }\nfn mk_alpha() -> Alpha { Alpha { a: \"z\" } }\nfn takes_beta(x: Beta) -> String { x.b }\nfn probe() -> String { takes_beta(x: mk_alpha()) }\n" + +test fn w_distinct_applied_constructors_at_a_direct_call_argument_are_refused() -> Bool { + violation_count(source: applied_distinct_constructor_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// RED BEFORE, GREEN NOW -- ONE CONSTRUCTOR, DISTINCT TYPE ARGUMENTS. Wrapper reaching a +// Wrapper parameter. THIS IS THE ARM THAT ISOLATES THE CAUSE: no brand and no refinement +// is involved anywhere in the source, so admitting it could not have been a brand-specific +// deficit. K is phantom -- Wrapper's only field is a String -- which is exactly the shape whose +// separation nothing downstream can recover: a runtime equality over the stored fields cannot +// see the lost K and would CONFIRM a match the types deny. +data applied_distinct_type_argument_source: String = "module probe_inhabit_applied_arg\nimport std.types { String }\ntype KindA { ka: String }\ntype KindB { kb: String }\ntype Wrapper { v: String }\nfn mk_b() -> Wrapper { Wrapper { v: \"z\" } }\nfn takes_a(x: Wrapper) -> String { x.v }\nfn probe() -> String { takes_a(x: mk_b()) }\n" + +test fn w_distinct_applied_type_arguments_at_a_direct_call_argument_are_refused() -> Bool { + violation_count(source: applied_distinct_type_argument_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// RED BEFORE, GREEN NOW -- AND IT IS WHY THIS ARM IS NOT NAMED FOR GENERICS. The same distinct +// constructors with no type parameters anywhere, the actual a call. The class was never about +// application: it was about which PRODUCER sees the pair, and the record-literal producer is the +// only one that ever did. +data unapplied_distinct_constructor_source: String = "module probe_inhabit_unapplied_ctor\nimport std.types { String }\ntype Alpha { a: String }\ntype Beta { b: String }\nfn mk_alpha() -> Alpha { Alpha { a: \"z\" } }\nfn takes_beta(x: Beta) -> String { x.b }\nfn probe() -> String { takes_beta(x: mk_alpha()) }\n" + +test fn w_distinct_unapplied_product_constructors_through_a_call_are_refused() -> Bool { + violation_count(source: unapplied_distinct_constructor_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// THE ANTI-REFUSE-EVERYTHING CONTROL, and it is not a formality: an arm that refused every +// applied product would make all three reds above pass while destroying the corpus. Identical +// constructor, identical type argument, same call spelling as the reds. +data applied_matching_source: String = "module probe_inhabit_applied_match\nimport std.types { String }\ntype KindA { ka: String }\ntype Wrapper { v: String }\nfn mk_a() -> Wrapper { Wrapper { v: \"z\" } }\nfn takes_a(x: Wrapper) -> String { x.v }\nfn probe() -> String { takes_a(x: mk_a()) }\n" + +test fn w_matching_applied_product_at_a_direct_call_argument_is_admitted() -> Bool { + violation_count(source: applied_matching_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// THE SECOND CONTROL, over the guard that keeps this arm from reaching a class it cannot decide. +// A type argument that is still a TYPE VARIABLE resolves to no declared type and is not a kernel +// type, so the argument scan leaves the position unjudged rather than reading P and String as a +// disagreement. If that guard is ever dropped, this admits nothing and goes red -- which is the +// only way a false-positive class of that shape becomes visible here rather than in the corpus. +data applied_type_variable_argument_source: String = "module probe_inhabit_applied_tyvar\nimport std.types { String }\ntype Wrapper { v: String }\nfn takes_w(x: Wrapper) -> String { x.v }\nfn mk_s() -> Wrapper { Wrapper { v: \"z\" } }\nfn probe() -> String { takes_w(x: mk_s()) }\n" + +test fn w_a_type_variable_type_argument_is_not_read_as_a_disagreement() -> Bool { + violation_count(source: applied_type_variable_argument_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// THE PHANTOM ARM, AND IT IS NOT THE Wrapper ARM TWICE -- THE TWO FAIL ON DIFFERENT BUGS, which +// is the test for whether a second control earns its place. In the Wrapper probe above the two +// candidate arguments are KindA and KindB, DISTINCT RECORDS with distinct fields, so any +// comparison that reaches representation at all sees a difference. Here the two candidates are +// representationally IDENTICAL -- DemandKey and WorkKey have the same single String field -- and +// the parameter they occupy is PHANTOM: K appears in the parameter list and in no field. The two +// instantiations therefore differ ONLY nominally, at every level below the type. +// +// THE BUG THIS CATCHES AND THE OTHER DOES NOT: "a type argument that does not affect layout +// cannot affect inhabitance" is a reasonable-sounding optimization that would leave the Wrapper +// arm green while silently reopening this class whole. Enrolled at the request of the lane that +// found the original defect (zesty-crane-477), whose objection to omitting it was correct. +// +// WHY THIS SHAPE IS THE PRODUCTION ONE. product.fabric's demand/work/attempt/grant/offer/receipt +// identities are non-interchangeable ONLY because of a phantom K in FabricIdentity, and +// there is NO runtime fallback: the carrier stores principal and key, fabric_identity_eq compares +// exactly those two, so a wrong-kind identity admitted at a parameter is not merely uncaught +// downstream -- the equality CONFIRMS it on equal principal and key. This arm is the only thing +// standing between that and a silent false match. +data phantom_distinct_type_argument_source: String = "module probe_inhabit_phantom\nimport std.types { String }\ntype DemandKey { v: String }\ntype WorkKey { v: String }\ntype FabricIdentity { principal: P, key: String }\nfn mk_work() -> FabricIdentity { FabricIdentity { principal: \"p\", key: \"k\" } }\nfn takes_demand(x: FabricIdentity) -> String { x.key }\nfn probe() -> String { takes_demand(x: mk_work()) }\n" + +test fn w_a_phantom_type_argument_with_identical_representation_is_still_separated() -> Bool { + violation_count(source: phantom_distinct_type_argument_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +// WHERE THE examples.nominal_distinctness_witness PAIR WENT, recorded here because deleting a +// module takes its evidence with it unless the evidence is named first. That pair was +// dag/examples/nominal_distinctness_witness/{witness,twin}.dag: witness.dag passed an AccountId +// to a parameter declared UserId and twin.dag passed a UserId, an ordinary RED/GREEN discriminator +// over exactly this class, authored long before this arm. +// +// IT WAS INERT, AND ITS INERTNESS WAS THIS DEFECT. Consumed by nothing (it appears in the +// unconsumed-module census with no consumer), the RED half COMPILED CLEAN -- so the pair recorded +// a distinction the compiler was not making, and nothing anywhere reported that. The moment this +// arm landed, witness.dag stopped compiling, which is the pair finally working and also the reason +// it can no longer live in the corpus: strict preparation compiles every module, so a module that +// must not compile stops the line. +// +// A DELIBERATELY INVALID PROGRAM BELONGS AT THE FIXTURE BOUNDARY, NOT IN THE CORPUS -- DESIGN 4b's +// distinction between what an Accepted program may contain and what a fixture may author. The +// discrimination the pair carried is exactly w_distinct_unapplied_product_constructors_through_a +// _call_are_refused above plus w_matching_applied_product_at_a_direct_call_argument_is_admitted, +// both of which EXECUTE on every floor run. So the evidence did not move to a weaker home; it +// moved from a home where it could never fire to one where it fires every run. +data nominal_distinctness_example_disposition: String = "examples.nominal_distinctness_witness and examples.nominal_distinctness_twin were deleted when this arm landed: the RED half was a corpus module that must not compile, and its discrimination is carried by the enrolled fixture arms in this file." diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 27aedd72b6d..4342dcd3810 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2608,6 +2608,8 @@ type InhabitanceUndecidableReason type InhabitanceRefusalReason = RefusedPayloadAtParent | RefusedKernelAtStructured + | RefusedDistinctProductConstructor + | RefusedDistinctAppliedTypeArgument type InhabitanceVerdict = Inhabits @@ -2661,7 +2663,10 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { InhabitanceRefused { reason: RefusedPayloadAtParent } } else { - Inhabits + match nominal_product_inhabitance_refusal(declared: declared, produced: produced, scope: scope) { + Present { value: r } => InhabitanceRefused { reason: r } + Absent => Inhabits + } } } @@ -2717,6 +2722,253 @@ fn declared_realizes_as_kernel_numeric( } } +// THE NOMINAL-PRODUCT ARM (DESIGN 4b floor: "values inhabit declared types"). +// +// The state this refuses: a value whose type is one nominal PRODUCT reaches a position declared +// as a different nominal product. Two shapes, measured 2026-08-28 on a compiler built from the +// tree, each its own entry compile, each admitted with ZERO blocking diagnostics before this arm: +// Alpha at a Beta parameter -- distinct constructors, both applied +// Wrapper at a Wrapper parameter -- one constructor, distinct type arguments +// Alpha at a Beta parameter, the actual a CALL rather than a record literal -- distinct +// constructors, neither applied, and silent for the same reason +// The third is the one that shows the class is not about generics at all: the ONLY spelling +// that refused was a record LITERAL at a non-generic formal, which is a different producer. +// +// WHY NOTHING ELSE CAUGHT IT, read off the producers rather than inferred from the silence: +// kernel_value_declared_type_mismatch returns false at its first gate for any actual carrying +// children AND requires the actual to be a kernel type, so a product value is never judged +// there; coproduct_payload_where_parent_required requires the formal's declaration to be a +// concrete COPRODUCT, so a product formal leaves its body immediately; and +// structured_application_site_type_mismatch judges only an actual whose EXPRESSION is a record +// literal, which the overwhelmingly common spelling -- a call -- is not. Three total judgments, +// none of them reaching this pair. +// +// IT CONSUMES THE EXPOSURE AUTHORITY, IT DOES NOT RE-DERIVE ONE. v1.compiler.type_head_exposure +// already answers "what head does this type expose, and if it is an application, which +// constructor and which arguments", and exposure_view_for_node is that view's single producer. +// Deriving application-ness here from connective and children would be the second representation +// DESIGN 3 forbids. The constructor comparison likewise DELEGATES to +// application_type_names_compatible, the predicate the neighbouring seams already use for this +// exact question (aliases, brands, declared casts), so alias identity keeps one home. +// +// EVERY GUARD FAILS OPEN. A head this relation cannot establish, a container carrier, a callable, +// an anonymous record, an unresolvable name -- each answers "not judgeable" and the pair is +// admitted, never refused. The arm can therefore only convert silence into a refusal for a pair +// whose two identities are both established. +fn nominal_product_inhabitance_refusal( + declared: Node, + produced: Node, + scope: InferScope +) -> InhabitanceRefusalReason? { + let declared_head = nominal_product_head_name(n: declared, scope: scope) + let produced_head = nominal_product_head_name(n: produced, scope: scope) + if declared_head == "" || produced_head == "" { + none + } else if nominal_product_head_names_agree( + declared_name: declared_head, produced_name: produced_head, scope: scope) == false { + Present { value: RefusedDistinctProductConstructor } + } else if applied_type_arguments_conflict( + declared: declared, produced: produced, scope: scope) { + Present { value: RefusedDistinctAppliedTypeArgument } + } else { + none + } +} + +// expected_type_head_exposure is consulted rather than exposure_view_for_node directly: a leaf +// TYPE REFERENCE carries no connective and no children of its own, so the direct view answers +// OpaqueTypeHead for `Alpha` and the head would be invisible on exactly the spelling the third +// red arm uses. The entry point falls back to the symbol index's recorded exposure for that +// identity, which is where a declaration's head actually lives. Its name says `expected` +// because its first consumer asks about a formal; the function takes any node and is the single +// exposure entry point, so consuming it for the produced side is reuse, not a second producer. +// The head name of a NOMINAL product -- a declared record, applied or not -- and "" for +// everything else. The container carriers are excluded because List and Map expose an +// ApplicationHead too and their element compatibility is a different judgment with its own +// established producer (container_element_nominal_brand_mismatch). +fn nominal_product_head_name(n: Node, scope: InferScope) -> String { + let source_indices = scope.type_env.source_indices + let name = authored_name_at(source_indices: source_indices, node: n) + if name == "" || n.return_cardinality == CardOptional || type_node_is_callable(n: n) + || is_kernel_type(name: name) + || qualified_last_segment(name: name) == "Optional" + || node_is_element_collection(n: n, source_indices: source_indices) + || node_is_keyed_collection(n: n, source_indices: source_indices) { + "" + } else { + match expected_type_head_exposure(formal: n, scope: scope) { + ExposedTypeHead { view: ApplicationHead { constructor_identity: _, argument_identities: _ } } => + nominal_product_head_name_if_declared_product(name: name, scope: scope) + ExposedTypeHead { view: ProductHead { type_identity: _ } } => + nominal_product_head_name_if_declared_product(name: name, scope: scope) + _ => "" + } + } +} + +fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { + match lookup_type_by_name(env: scope.type_env, name: name) { + Present { value: decl } => + if decl.connective == Conj && (decl.children |> count) > 0 { name } else { "" } + Absent => "" + } +} + +fn nominal_product_head_names_agree( + declared_name: String, + produced_name: String, + scope: InferScope +) -> Bool { + application_type_names_compatible( + formal_name: declared_name, + lit_name: produced_name, + type_env: scope.type_env, + module_name: scope.module_name, + source_indices: scope.type_env.source_indices) + || transparent_alias_identity_agrees( + index: scope.type_env.symbol_index, left: declared_name, right: produced_name) +} + +// ARITY DIFFERENCE IS NOT THIS CLASS, and neither is an unapplied side. Two applications of one +// constructor at different arities mean the constructor identity was not what it looked like, or +// a substitution is incomplete; either way this relation has nothing to say and says nothing +// rather than inventing a verdict. +fn applied_type_arguments_conflict( + declared: Node, + produced: Node, + scope: InferScope +) -> Bool { + let declared_args = declared.children + let produced_args = produced.children + if (declared_args |> count) == 0 || (declared_args |> count) != (produced_args |> count) { + false + } else { + applied_type_arguments_conflict_scan( + declared_args: declared_args, produced_args: produced_args, scope: scope) + } +} + +fn applied_type_arguments_conflict_scan( + declared_args: List, + produced_args: List, + scope: InferScope +) -> Bool { + match declared_args |> first { + Present { value: d } => + match produced_args |> first { + Present { value: p } => + if applied_type_argument_conflicts(declared_arg: d, produced_arg: p, scope: scope) { + true + } else { + applied_type_arguments_conflict_scan( + declared_args: declared_args |> skip(1), + produced_args: produced_args |> skip(1), + scope: scope) + } + Absent => false + } + Absent => false + } +} + +// A TYPE VARIABLE IS NOT A DISAGREEMENT, AND FINDING A TEST FOR ONE TOOK THREE MEASUREMENTS. +// +// WHAT DOES NOT WORK, both refuted by execution rather than by reading. Asking whether the +// argument's NAME resolves in the type environment does not work: type parameters ARE bound +// there, so `S` and `R` answer "declared type" exactly as `KindA` does. Measured on the v2 +// pipeline entry, that test produced fifteen refusals and every single one had a type variable +// on one side -- Measure receiving Measure, NodeFoldTopDown receiving +// NodeFoldTopDown -- with zero true positives among them. Comparing the exposure's +// constructor_identity does not work either, and it is worth recording why since it looks like +// the obvious authority: the identity is keyed on the REFERENCING file, so one Measure read from +// two modules yields dag/std/measure.dag::Measure and dag/std/realization_measurement.dag::Measure +// for the same declaration. It can therefore never establish agreement across modules, which is +// the only case where establishing it would matter. +// +// WHAT DOES WORK, and it is a property of the substrate rather than a trick: a type VARIABLE +// resolves to nothing, so child_type_node leaves it with no authored name, while a real argument +// resolves to its declaration and carries that declaration's name. The empty resolved name is +// therefore the decidable test, and it fails open -- an argument this relation cannot resolve is +// never read as a disagreement. This is also why node_type_shape renders these as `Primitive()`: +// the renderer already followed the same resolution and found the same nothing. +// +// THE NESTEDNESS TEST STILL READS THE AUTHORED NODE while the name reads the RESOLVED one, and +// the split is not an inconsistency: whether an argument is itself an application is a question +// about how it was WRITTEN, and what it denotes is a question about what it RESOLVES TO. Reading +// nestedness off the resolved node was the second cut of this arm and it silenced the whole +// class, because a resolved record declaration carries its fields as children and every argument +// then looked nested. +fn applied_type_argument_conflicts( + declared_arg: Node, + produced_arg: Node, + scope: InferScope +) -> Bool { + let source_indices = scope.type_env.source_indices + if declared_arg.return_cardinality == CardOptional || produced_arg.return_cardinality == CardOptional + || applied_type_argument_is_nested_application(n: declared_arg, scope: scope) + || applied_type_argument_is_nested_application(n: produced_arg, scope: scope) + || type_node_is_callable(n: declared_arg) || type_node_is_callable(n: produced_arg) { + false + } else { + let d = child_type_node(ch: declared_arg) + let p = child_type_node(ch: produced_arg) + let d_name = authored_name_at(source_indices: source_indices, node: d) + let p_name = authored_name_at(source_indices: source_indices, node: p) + if applied_type_argument_identity_known(name: d_name, scope: scope) == false + || applied_type_argument_identity_known(name: p_name, scope: scope) == false { + false + } else { + nominal_product_head_names_agree( + declared_name: d_name, produced_name: p_name, scope: scope) == false + } + } +} + +// The DIRECT view, deliberately not expected_type_head_exposure: the index fallback answers for +// a leaf reference by looking up what it names, and a leaf naming a parameterised record would +// come back as a head with arguments -- which is the opposite of what this asks. Here the +// question is about the argument's own written form. +fn applied_type_argument_is_nested_application(n: Node, scope: InferScope) -> Bool { + match exposure_view_for_node(n: n, source_indices: scope.type_env.source_indices) { + ExposedTypeHead { view: ApplicationHead { constructor_identity: _, argument_identities: _ } } => true + _ => false + } +} + +// A TYPE VARIABLE MUST RESOLVE TO A STRUCTURE, NOT MERELY TO A BINDING, and the third refuted +// test is the reason this clause is spelled this way rather than the two shorter ways. +// +// REFUTED ONCE: "the name resolves in the type environment". Type PARAMETERS are bound there, so +// S and R answer exactly as a declared record does. Fifteen false positives on the v2 pipeline +// entry. +// +// REFUTED TWICE, and this is the subtler one: "the resolved node has no authored name". On the +// v2 entry a type variable's resolved node was nameless and the test looked sound. Over the WHOLE +// corpus it is not -- measured on the required floor, `Measure`, `MembershipPlan` +// and `ContainmentPath` all resolve their variables to nodes that KEEP the authored name, so +// the test admitted them as concrete and refused four live modules. A property observed on one +// entry was read as a property of the substrate; it is a property of that entry's resolution +// state. +// +// WHAT HOLDS OVER THE CORPUS: a type parameter binds to a bare leaf standing for itself, while a +// real type resolves to a declaration WITH STRUCTURE -- a record's fields, a coproduct's variants. +// So the test is structural rather than nominal, and it fails open twice over: an argument whose +// name does not resolve, and an argument that resolves to something structureless (a bare alias, +// a parameter), are both left unjudged. +fn applied_type_argument_identity_known(name: String, scope: InferScope) -> Bool { + if name == "" { + false + } else if is_kernel_type(name: name) { + true + } else { + match lookup_type_by_name(env: scope.type_env, name: name) { + Present { value: decl } => + (decl.connective == Conj || decl.connective == Disj) && (decl.children |> count) > 0 + Absent => false + } + } +} + // THE UNDECIDABLE ARM IS COUNTED, NOT SILENT, AND NOT A REFUSAL. It used to read // `InhabitanceUndecidable { reason: _ } => []`, which is total over the verdict and blind one // level down: the four reasons are declared precisely because they are different facts, and the diff --git a/src/v1/04_types.dag b/src/v1/04_types.dag index 84e86bac2ec..814613a3d1d 100644 --- a/src/v1/04_types.dag +++ b/src/v1/04_types.dag @@ -763,6 +763,27 @@ fn normalize_access_type_node(n: Node) -> Node { } } +// AN APPLICATION RENDERS ITS ARGUMENTS in node_type_shape below, because without them the two +// sides of a type-ARGUMENT refusal print identically. Wrapper at a Wrapper +// position is a real refusal whose diagnostic read "declared 'Node(Wrapper)', produced +// 'Node(Wrapper)'" -- typed and located but carrying nothing a reader could act on, which is +// the located-but-uninformative half of DESIGN 5's typed-diagnostic duty. The container arm +// already renders its element for the same reason; this is that rule applied to the general +// application rather than a second idea. +fn node_type_shape_argument_list(args: List, source_indices: Map) -> String { + match args |> first { + Present { value: a } => + let head = node_type_shape(n: child_type_node(ch: a), source_indices: source_indices) + let rest = args |> skip(1) + if (rest |> count) == 0 { + head + } else { + concat(head, concat(",", node_type_shape_argument_list(args: rest, source_indices: source_indices))) + } + Absent => "" + } +} + fn node_type_shape(n: Node, source_indices: Map) -> String { let __is_leaf = n.connective == NoConnective && n.children |> count == 0 && n.properties |> count == 0 let n_name = authored_name_at(source_indices: source_indices, node: n) @@ -801,6 +822,8 @@ fn node_type_shape(n: Node, source_indices: Map) -> String concat("Optional(", inner_shape, ")") } else if is_map { "Map(...)" + } else if (n.children |> count) > 0 { + concat("Node(", n_name, "<", node_type_shape_argument_list(args: n.children, source_indices: source_indices), ">)") } else { concat("Node(", n_name, ")") } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index c6ef4fa1d7b..27146525ca9 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -3705,6 +3705,8 @@ pub enum InhabitanceUndecidableReason { pub enum InhabitanceRefusalReason { RefusedPayloadAtParent, RefusedKernelAtStructured, + RefusedDistinctProductConstructor, + RefusedDistinctAppliedTypeArgument, } #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] @@ -3797,7 +3799,18 @@ pub fn declared_type_inhabitance( reason: InhabitanceRefusalReason::RefusedPayloadAtParent, }) } else { - Rc::new(InhabitanceVerdict::Inhabits) + match nominal_product_inhabitance_refusal( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Some(r) => { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: r.clone(), + }) + } + None => Rc::new(InhabitanceVerdict::Inhabits), + } } } } @@ -3828,6 +3841,267 @@ pub fn declared_realizes_as_kernel_numeric( } } +pub fn nominal_product_inhabitance_refusal( + declared: Rc, + produced: Rc, + scope: Rc, +) -> Option { + { + let declared_head = nominal_product_head_name(declared.clone(), scope.clone()); + let produced_head = nominal_product_head_name(produced.clone(), scope.clone()); + if ((declared_head.clone() == "".to_string()) || (produced_head.clone() == "".to_string())) + { + None + } else { + if (nominal_product_head_names_agree( + declared_head.clone(), + produced_head.clone(), + scope.clone(), + ) == false) + { + Some(InhabitanceRefusalReason::RefusedDistinctProductConstructor) + } else { + if applied_type_arguments_conflict( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Some(InhabitanceRefusalReason::RefusedDistinctAppliedTypeArgument) + } else { + None + } + } + } + } +} + +pub fn nominal_product_head_name(n: Rc, scope: Rc) -> String { + { + let source_indices = scope.type_env.clone().source_indices.clone(); + let name = crate::v1_std_core::authored_name_at(source_indices.clone(), n.clone()); + if (((((((name.clone() == "".to_string()) + || (n.return_cardinality.clone() == Cardinality::CardOptional)) + || type_node_is_callable(n.clone())) + || crate::std_types::is_kernel_type(name.clone())) + || (crate::v1_std_core::qualified_last_segment(name.clone()) + == "Optional".to_string())) + || crate::v1_compiler_infer_types::node_is_element_collection( + n.clone(), + source_indices.clone(), + )) + || crate::v1_compiler_infer_types::node_is_keyed_collection( + n.clone(), + source_indices.clone(), + )) + { + "".to_string() + } else { + match (*expected_type_head_exposure(n.clone(), scope.clone())).clone() { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::ApplicationHead { .. }) => + { + let TypeHeadView::ApplicationHead { .. } = view.as_ref() else { + unreachable!() + }; + nominal_product_head_name_if_declared_product(name.clone(), scope.clone()) + } + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::ProductHead { .. }) => + { + let TypeHeadView::ProductHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + nominal_product_head_name_if_declared_product(name.clone(), scope.clone()) + } + _ => "".to_string(), + } + } + } +} + +pub fn nominal_product_head_name_if_declared_product( + name: String, + scope: Rc, +) -> String { + match crate::v1_compiler_infer_env::lookup_type_by_name(scope.type_env.clone(), name.clone()) { + Some(decl) => { + if ((decl.connective.clone() == Connective::Conj) + && ((decl.children.clone().len() as i64) > 0)) + { + name.clone() + } else { + "".to_string() + } + } + None => "".to_string(), + } +} + +pub fn nominal_product_head_names_agree( + declared_name: String, + produced_name: String, + scope: Rc, +) -> bool { + (application_type_names_compatible( + declared_name.clone(), + produced_name.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + scope.type_env.clone().source_indices.clone(), + ) || transparent_alias_identity_agrees( + scope.type_env.clone().symbol_index.clone(), + declared_name.clone(), + produced_name.clone(), + )) +} + +pub fn applied_type_arguments_conflict( + declared: Rc, + produced: Rc, + scope: Rc, +) -> bool { + { + let declared_args = declared.children.clone(); + let produced_args = produced.children.clone(); + if (((declared_args.clone().len() as i64) == 0) + || ((declared_args.clone().len() as i64) != (produced_args.clone().len() as i64))) + { + false + } else { + applied_type_arguments_conflict_scan( + declared_args.clone(), + produced_args.clone(), + scope.clone(), + ) + } + } +} + +pub fn applied_type_arguments_conflict_scan( + mut declared_args: Rc>>, + mut produced_args: Rc>>, + mut scope: Rc, +) -> bool { + loop { + match declared_args.clone().first().cloned() { + Some(d) => match produced_args.clone().first().cloned() { + Some(p) => { + if applied_type_argument_conflicts(d.clone(), p.clone(), scope.clone()) { + break true; + } else { + { + let __tco_0 = Rc::new( + declared_args + .iter() + .cloned() + .skip(1 as usize) + .collect::>(), + ); + let __tco_1 = Rc::new( + produced_args + .iter() + .cloned() + .skip(1 as usize) + .collect::>(), + ); + declared_args = __tco_0; + produced_args = __tco_1; + continue; + } + } + } + None => { + break false; + } + }, + None => { + break false; + } + } + } +} + +pub fn applied_type_argument_conflicts( + declared_arg: Rc, + produced_arg: Rc, + scope: Rc, +) -> bool { + { + let source_indices = scope.type_env.clone().source_indices.clone(); + if ((((((declared_arg.return_cardinality.clone() == Cardinality::CardOptional) + || (produced_arg.return_cardinality.clone() == Cardinality::CardOptional)) + || applied_type_argument_is_nested_application(declared_arg.clone(), scope.clone())) + || applied_type_argument_is_nested_application(produced_arg.clone(), scope.clone())) + || type_node_is_callable(declared_arg.clone())) + || type_node_is_callable(produced_arg.clone())) + { + false + } else { + { + let d = crate::v1_compiler_infer_types::child_type_node(declared_arg.clone()); + let p = crate::v1_compiler_infer_types::child_type_node(produced_arg.clone()); + let d_name = + crate::v1_std_core::authored_name_at(source_indices.clone(), d.clone()); + let p_name = + crate::v1_std_core::authored_name_at(source_indices.clone(), p.clone()); + if ((applied_type_argument_identity_known(d_name.clone(), scope.clone()) == false) + || (applied_type_argument_identity_known(p_name.clone(), scope.clone()) + == false)) + { + false + } else { + (nominal_product_head_names_agree( + d_name.clone(), + p_name.clone(), + scope.clone(), + ) == false) + } + } + } + } +} + +pub fn applied_type_argument_is_nested_application(n: Rc, scope: Rc) -> bool { + match (*exposure_view_for_node(n.clone(), scope.type_env.clone().source_indices.clone())) + .clone() + { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::ApplicationHead { .. }) => + { + let TypeHeadView::ApplicationHead { .. } = view.as_ref() else { + unreachable!() + }; + true + } + _ => false, + } +} + +pub fn applied_type_argument_identity_known(name: String, scope: Rc) -> bool { + if (name.clone() == "".to_string()) { + false + } else { + if crate::std_types::is_kernel_type(name.clone()) { + true + } else { + match crate::v1_compiler_infer_env::lookup_type_by_name( + scope.type_env.clone(), + name.clone(), + ) { + Some(decl) => { + (((decl.connective.clone() == Connective::Conj) + || (decl.connective.clone() == Connective::Disj)) + && ((decl.children.clone().len() as i64) > 0)) + } + None => false, + } + } + } +} + pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { match reason.clone() { InhabitanceUndecidableReason::UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone".to_string(), @@ -23710,3 +23984,7 @@ pub struct UndecidableProducedIdentityErased; pub struct RefusedPayloadAtParent; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedKernelAtStructured; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedDistinctProductConstructor; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedDistinctAppliedTypeArgument; diff --git a/src/v1/stage0/src/v1_compiler_infer_types.rs b/src/v1/stage0/src/v1_compiler_infer_types.rs index d49af591b8e..8fa89e54a63 100644 --- a/src/v1/stage0/src/v1_compiler_infer_types.rs +++ b/src/v1/stage0/src/v1_compiler_infer_types.rs @@ -1999,6 +1999,38 @@ pub fn normalize_access_type_node(mut n: Rc) -> Rc { } } +pub fn node_type_shape_argument_list( + args: Rc>>, + source_indices: Rc>>, +) -> String { + stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || { + match args.clone().first().cloned() { + Some(a) => { + let head = node_type_shape(child_type_node(a.clone()), source_indices.clone()); + let rest = Rc::new( + args.clone() + .iter() + .cloned() + .skip(1 as usize) + .collect::>(), + ); + if ((rest.clone().len() as i64) == 0) { + head + } else { + v1_rt::concat( + head, + v1_rt::concat( + ",".to_string(), + node_type_shape_argument_list(rest.clone(), source_indices.clone()), + ), + ) + } + } + None => "".to_string(), + } + }) +} + pub fn node_type_shape( n: Rc, source_indices: Rc>>, @@ -2115,10 +2147,29 @@ pub fn node_type_shape( if is_map.clone() { "Map(...)".to_string() } else { - v1_rt::concat( - v1_rt::concat("Node(".to_string(), n_name.clone()), - ")".to_string(), - ) + if ((n.children.clone().len() as i64) > 0) { + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + v1_rt::concat( + "Node(".to_string(), + n_name.clone(), + ), + "<".to_string(), + ), + node_type_shape_argument_list( + n.children.clone(), + source_indices.clone(), + ), + ), + ">)".to_string(), + ) + } else { + v1_rt::concat( + v1_rt::concat("Node(".to_string(), n_name.clone()), + ")".to_string(), + ) + } } } }