diff --git a/dag/gunbc/auth/profile_projection.dag b/dag/gunbc/auth/profile_projection.dag index d564601c675..8097529f3cf 100644 --- a/dag/gunbc/auth/profile_projection.dag +++ b/dag/gunbc/auth/profile_projection.dag @@ -13,7 +13,7 @@ import extdeps.filesystem.filesystem_io { FilesystemReadOutcome, FilesystemReadRefused, FilesystemReadSucceeded, } import extdeps.languages.json.emit { - serialize_json, json_object, json_kv, json_string, JsonValue, + serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue, } import extdeps.languages.json.parse { parse_json_document, json_field_string, json_document_gap_text, @@ -87,21 +87,21 @@ fn principal_profile_json(profile: PrincipalProfile) -> String { ], profile_name_members(name: profile.name)), concat(profile_email_members(email: profile.email), profile_picture_members(picture: profile.picture))))) } -fn profile_name_members(name: String?) -> List { +fn profile_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] } } -fn profile_email_members(email: Email?) -> List { +fn profile_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] } } -fn profile_picture_members(picture: Uri?) -> List { +fn profile_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] diff --git a/dag/gunbc/auth/session_store.dag b/dag/gunbc/auth/session_store.dag index c1c3d50d065..b6fd50b6651 100644 --- a/dag/gunbc/auth/session_store.dag +++ b/dag/gunbc/auth/session_store.dag @@ -28,7 +28,7 @@ import extdeps.filesystem.filesystem_io { filesystem_entry_presence, } import extdeps.languages.json.emit { - serialize_json, json_object, json_kv, json_string, JsonValue, + serialize_json, json_object, json_kv, json_string, JsonValue, JsonKeyValue, } import extdeps.languages.json.parse { parse_json_document, json_field_string, json_document_gap_text, @@ -104,7 +104,7 @@ fn authenticated_session_json(session: AuthenticatedSession) -> String { // THE OPTIONAL PICTURE MEMBER, emitted only when the login projected one: absence is the // member's ABSENCE on the wire, never an empty string standing in for none. The spelling is // the Uri wire form (https://… or http://…), the same claim the ID-token reader admitted. -fn session_profile_picture_members(picture: Uri?) -> List { +fn session_profile_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] @@ -113,7 +113,7 @@ fn session_profile_picture_members(picture: Uri?) -> List { // THE OPTIONAL NAME MEMBER, the same law as the picture: absence is the member's ABSENCE, // never an empty string standing in for none. -fn session_profile_name_members(name: String?) -> List { +fn session_profile_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] @@ -121,7 +121,7 @@ fn session_profile_name_members(name: String?) -> List { } // THE OPTIONAL EMAIL MEMBER, the same law again. -fn session_profile_email_members(email: Email?) -> List { +fn session_profile_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] diff --git a/dag/gunbc/bmc_dry_realization.dag b/dag/gunbc/bmc_dry_realization.dag index 5fe9b888213..373a2e849af 100644 --- a/dag/gunbc/bmc_dry_realization.dag +++ b/dag/gunbc/bmc_dry_realization.dag @@ -1,6 +1,7 @@ module gunbc.bmc_dry_realization import std.types { Bool, Int, List, NonEmptyStr, String } +import std.algebra { list_snoc_item } import std.measure { Second, second } import v2.std.operation_argv { OperationRef } import v2.std.operation_realization { @@ -161,9 +162,9 @@ fn bmc_dry_realization(identity: NonEmptyStr, initial: BmcWorld, epoch: Second) identity: identity, initial: initial, epoch: epoch, - bindings: list_append( - bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }), - virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), + bindings: list_snoc_item( + xs: bmc_bindings(get: fn(w) { w }, put: fn(w, next) { next }), + item: virtual_delay_binding(at: sleep_delay_seconds_operation, seconds_input: "seconds"), ), advance: bmc_advance, } diff --git a/dag/gunbc/bmc_model.dag b/dag/gunbc/bmc_model.dag index a8163b2bae9..f78873b1d0f 100644 --- a/dag/gunbc/bmc_model.dag +++ b/dag/gunbc/bmc_model.dag @@ -3,6 +3,7 @@ module gunbc.bmc_model import std.types { Bool, Int, List, NonEmptyStr } import std.measure { Second, second, second_count } import std.optional { Present, Absent } +import std.algebra { list_snoc_item } import v2.std.algebra { any, filter } import extdeps.bmc.ipmi_channel { IpmiChannelNumber, IpmiUserId, IpmiUserChannelAccess, IpmiChannelPrivilegeLimit } import extdeps.bmc.redfish_telemetry { RedfishLogEntry, RedfishLogService, RedfishTelemetryPoint } @@ -229,7 +230,7 @@ fn bmc_web_login(world: BmcWorld, username: String, password: String) -> BmcWebL if username == account.username && password == account.password { let session = BmcWebSession { id: web.next_session_id, csrf_token: concat("csrf-", to_string(web.next_session_id)), privilege: account.privilege } BmcWebLoginStep { - world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_append(web.sessions, session), next_session_id: web.next_session_id + 1, kvm: web.kvm)), + world: bmc_with_web(world: world, web: bmc_web_with(web: web, sessions: list_snoc_item(xs: web.sessions, item: session), next_session_id: web.next_session_id + 1, kvm: web.kvm)), reply: BmcWebLoginAccepted { session: session }, } } else { @@ -337,7 +338,7 @@ fn bmc_host_boots(world: BmcWorld, now: Second) -> BmcWorld { let via = match world.boot_override { BootOverrideCdromEfiNextBoot => true BootOverrideNone => false } let pending = match world.sol_drop_after_boot { Absent => world.pending - Present { value: after } => list_append(world.pending, BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} }) + Present { value: after } => list_snoc_item(xs: world.pending, item: BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: after)), event: BmcSolSessionDropped {} }) } BmcWorld { power: BmcPowerOn, pending: pending, fired: world.fired, boot_override: BootOverrideNone, sel: world.sel, @@ -357,7 +358,7 @@ fn bmc_chassis_control(world: BmcWorld, action: IpmiChassisControlAction, now: S if bmc_power_is_on(world: world) { let off = bmc_with_power(world: world, power: BmcPowerOff) let restore = BmcScheduledEvent { at: second(count: second_count(s: now) + second_count(s: world.cycle_off_interval)), event: BmcPowerRestored {} } - BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_append(off.pending, restore), fired: off.fired), effect_taken: true } + BmcChassisControlStep { world: bmc_with_pending(world: off, pending: list_snoc_item(xs: off.pending, item: restore), fired: off.fired), effect_taken: true } } else { BmcChassisControlStep { world: world, effect_taken: false } } IpmiChassisHardReset => if bmc_power_is_on(world: world) { BmcChassisControlStep { world: bmc_host_boots(world: world, now: now), effect_taken: true } } @@ -393,7 +394,7 @@ fn bmc_advance(world: BmcWorld, now: Second) -> BmcWorld { Present { value: e } => { let remaining = bmc_without_first(pending: world.pending, event: e) let applied = bmc_apply_event(world: bmc_with_pending(world: world, pending: remaining, fired: world.fired), event: e.event, at: e.at) - bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_append(applied.fired, e)), now: now) + bmc_advance(world: bmc_with_pending(world: applied, pending: applied.pending, fired: list_snoc_item(xs: applied.fired, item: e)), now: now) } } } @@ -425,7 +426,7 @@ fn bmc_without_first(pending: List, event: BmcScheduledEvent) if !acc.removed && second_count(s: e.at) == second_count(s: event.at) && bmc_event_eq(a: e.event, b: event.event) { BmcPendingRemoval { kept: acc.kept, removed: true } } else { - BmcPendingRemoval { kept: list_append(acc.kept, e), removed: acc.removed } + BmcPendingRemoval { kept: list_snoc_item(xs: acc.kept, item: e), removed: acc.removed } } }).kept } @@ -524,7 +525,7 @@ fn bmc_with_ipmi_user_access(world: BmcWorld, rows: List) fn bmc_ipmi_set_user_access(world: BmcWorld, access: IpmiUserChannelAccess) -> BmcIpmiSetUserAccessStep { if any(world.ipmi_users, u => (u.id as Int) == (access.user as Int)) { let others = filter(world.ipmi_user_access, r => !((r.user as Int) == (access.user as Int) && (r.channel as Int) == (access.channel as Int))) - BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_append(others, access)), completed: true } + BmcIpmiSetUserAccessStep { world: bmc_with_ipmi_user_access(world: world, rows: list_snoc_item(xs: others, item: access)), completed: true } } else { BmcIpmiSetUserAccessStep { world: world, completed: false } } diff --git a/dag/gunbc/filesystem_model.dag b/dag/gunbc/filesystem_model.dag index dd5b3d6974f..c3d56516e70 100644 --- a/dag/gunbc/filesystem_model.dag +++ b/dag/gunbc/filesystem_model.dag @@ -1,6 +1,7 @@ module gunbc.filesystem_model import std.types { Bool, List, String } +import std.algebra { list_snoc_item } import std.measure { second, ByteSize, byte_size } import std.bytes { bytes_octets, utf8_encode_bytes } import v2.std.operation_argv { OperationRef, BoundOperationInvocation } @@ -128,7 +129,7 @@ fn fs_write(fs: ModeledFilesystem, path: String, content: String, create_new: Bo fn fs_with_file(fs: ModeledFilesystem, path: String, content: String) -> ModeledFilesystem { ModeledFilesystem { directories: fs.directories, - files: list_append(filter(fs.files, f => f.path != path), ModeledFile { path: path, content: content }), + files: list_snoc_item(xs: filter(fs.files, f => f.path != path), item: ModeledFile { path: path, content: content }), refused_reads: fs.refused_reads, } } diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag index 9c48033b88c..65de04f0baa 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_dry_realization.dag @@ -3,7 +3,7 @@ module gunbc.machine_intake_mtcollins1_boot_dry_realization import extdeps.tools.gnu_coreutils { readlink_command } import std.types { Bool, Int, List, NonEmptyStr, String } import std.measure { Second, second, second_count } -import std.algebra { trim } +import std.algebra { trim, list_snoc_item } import v2.std.operation_argv { OperationRef } import v2.std.operation_realization { OperationRealization, OperationBinding, OperationCall, OperationStep, @@ -236,7 +236,7 @@ fn live_collectors(w: MtCollins1BootWorld) -> List { } fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> MtCollins1BootWorld { - with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_append(w.worker.processes, p), uptime_at_origin: w.worker.uptime_at_origin }) + with_worker(w: with_fs(w: w, fs: if p.alive { process_visible(fs: fs, p: p) } else { fs }), worker: ModeledWorker { next_pid: p.pid + 1, processes: list_snoc_item(xs: w.worker.processes, item: p), uptime_at_origin: w.worker.uptime_at_origin }) } // THE NOTICE WATCHER the boot step starts before the entry (gunbc.ci_spec): its token in the @@ -246,7 +246,7 @@ fn started(w: MtCollins1BootWorld, p: ModeledProcess, fs: ModeledFilesystem) -> fn with_notice_watcher(w: MtCollins1BootWorld, capture_path: String, token: String) -> MtCollins1BootWorld { let p = ModeledProcess { pid: w.worker.next_pid, start_time: start_ticks(w: w, now: second(count: 0)), comm: "bash", cmdline: "bash -c gunbc-sol-notice-watch", capture_path: capture_path, diagnostic_path: "", alive: true } let fs = fs_with_file(fs: fs_with_file(fs: w.fs, path: concat(capture_path, mtcollins1_sol_notice_ready_suffix), content: concat(token, "\n")), path: mtcollins1_sol_notice_watcher_path(capture_path: capture_path), content: process_identity(p: p)) - let env = list_append(w.environment, ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token }) + let env = list_snoc_item(xs: w.environment, item: ModeledVariable { name: mtcollins1_sol_notice_token_env as String, value: token }) started(w: MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: env, agent: w.agent, remote_hosts: w.remote_hosts, clock: w.clock, worker: w.worker, console: w.console, media: w.media, screen: w.screen }, p: p, fs: fs) } @@ -533,7 +533,7 @@ fn owned_launch_handler(w: MtCollins1BootWorld, call: OperationCall) -> Operatio KvmModeledRefused { event_word: word, would_write: line } => OperationHarnessFault { reason: concat("kvm_journal_line refused the modeled ", concat(word, concat(" line: ", line))) as NonEmptyStr } KvmModeledRendered { text: t } => { let fs = appended(fs: fs_write(fs: w.fs, path: pid_path, content: process_identity(p: p), create_new: false).fs, path: concat(dir, "/journal"), text: t) - let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_append(w.screen.observers, ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) } + let screen = ModeledKvmViewer { session: w.screen.session, still_bytes: w.screen.still_bytes, still_sha256: w.screen.still_sha256, observers: list_snoc_item(xs: w.screen.observers, item: ModeledKvmObserver { pid: p.pid, dir: dir, seq: 0, seen_files: 0 }) } exited_step(state: with_screen(w: started(w: w, p: p, fs: fs), screen: screen), stdout: "", exit_code: 0) } } diff --git a/dag/gunbc/megarac_media_model.dag b/dag/gunbc/megarac_media_model.dag index 5f361e81c56..c0a138a0c70 100644 --- a/dag/gunbc/megarac_media_model.dag +++ b/dag/gunbc/megarac_media_model.dag @@ -2,6 +2,7 @@ module gunbc.megarac_media_model import std.types { Bool, Int, List, String } import std.measure { Second, second, second_count } +import std.algebra { list_snoc_item } // THE BMC's VIRTUAL-MEDIA SUBSYSTEM (AMI MegaRAC SP-X, firmware 0.32): the same controller as // gunbc.bmc_model, held as its own record because its state -- web sessions, the NFS share binding, @@ -88,7 +89,7 @@ fn megarac_open_session(world: MegaRacMediaWorld, cookie_jar: String) -> MegaRac let id = world.next_session let token = concat("modeled-csrf-", to_string(id)) MegaRacOpened { - world: megarac_with_sessions(world: world, sessions: list_append(world.sessions, MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1), + world: megarac_with_sessions(world: world, sessions: list_snoc_item(xs: world.sessions, item: MegaRacSession { cookie_jar: cookie_jar, csrf_token: token, open: true }), next_session: id + 1), racsession_id: id, csrf_token: token, } diff --git a/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag new file mode 100644 index 00000000000..8f5d568c8c5 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/generic_product_admitted_where_its_argument_type_is_declared.dag @@ -0,0 +1,22 @@ +module gunbc.recurring_failure_mode.generic_product_admitted_where_its_argument_type_is_declared + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data generic_product_admitted_where_its_argument_type_is_declared: RecurringFailureMode = RecurringFailureMode { + identity: "generic_product_admitted_where_its_argument_type_is_declared" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a value whose type is a generic product application `Wrap` reaches a position declared as `T` (or any other established coproduct), and the program is Accepted. HARM: silent wrongness at the compiler floor -- DESIGN section 4b names `values inhabit declared types` as below-baseline when it fails. SPECIMEN: gunbc#13198 (632b72544e) passed `roadmap_standings_read(layout: ...)` (`-> CarrierClosed`) as `issue_query_snapshot_for_projection.standings` (`standings: RoadmapStandings`). The seed admitted it. At runtime the callee's match on `StandingsObserved | StandingsUnobserved` met a `CarrierClosed` record and aborted with PatternMatchFailure, taking down every srv2 belt tick. The wiring unwrap lives at `gunbc.roadmap.roadmap_served_observation` `served_standings_after_snapshot_close`; this row owns the checker wall, not that unwrap's authorship.", + + "THE CHAIN, per DESIGN section 6b. Candidates ruled OUT. (1) Generic instantiation treated as compatible with T: no arm unwraps an application to its argument and compares that argument to the formal. (2) Named-argument call checking skipping the declared parameter type: `select_formal_for_call_argument` binds `standings` to the `standings` formal; `direct_call_argument_inhabitance_diags` hands that pair to `declared_type_inhabitance`. (3) A unify/hole defaulting to admit at the call seam: the formal is a concrete coproduct, not a type variable. Candidate ruled IN: leaf-shaped exposure agreement where declaration identity should decide. The prior `coproduct_at_record_declared_type` refused only a CoproductHead value at a ProductHead formal. `CarrierClosed` exposes ApplicationHead; `RoadmapStandings` exposes CoproductHead; `nominal_product_inhabitance_refusal` abstains because the declared side is not a product; the relation's terminal arm is `Absent => Inhabits`. The earliest unjustified boundary is that one-direction, ProductHead-only disjointness check, not the call site.", + + "REPAIR: `v1.compiler.infer` `product_versus_coproduct_head_mismatch` refuses either direction and answers `RefusedProductCoproductHeadMismatch` -- not `RefusedKernelAtStructured`. It consumes `nominal_product_head_name` and `nominal_coproduct_head_name` (applied or unapplied, including ApplicationHead). A declared product is `is_product_type` and not `is_where_refinement_type`, so a zero-field `type Wrap {}` is a product. Same-declaration and transparent-alias pairs still abstain. REDS at the relation boundary (census subject carries `[RefusedProductCoproductHeadMismatch]`): `w_a_generic_product_at_the_coproduct_it_wraps_is_refused`, `w_an_unapplied_product_at_a_coproduct_argument_is_refused`, `w_a_zero_field_generic_product_at_the_coproduct_it_wraps_is_refused`, `w_an_applied_product_at_an_applied_coproduct_argument_is_refused`, `w_coproduct_typed_value_at_record_argument_is_refused`. POSITIVE CONTROLS: `w_a_generic_product_at_its_own_declared_application_is_admitted`, `w_a_zero_field_generic_product_at_its_own_declared_application_is_admitted`, `w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted`. SPECIMEN STANDING: `served_observation_issue_query_surface` consumes `served_standings_after_snapshot_close` so the required floor compiles the module; the wall would refuse the pre-unwrap pair.", + + "RUNG FOUND AT: below the floor (silently admitted). RUNG AFTER REPAIR: structurally guaranteed for an established named product (applied or not, zero-field or not) at an established named coproduct (applied or not), and the converse, at every position `declared_type_inhabitance` serves (direct-call argument included). CEILING: structurally guaranteed -- both identities are authorable in source. NOT COVERED, stated rather than implied: a product at a distinct product stays with `nominal_product_inhabitance_refusal`; two distinct unapplied coproducts stay with `coproduct_payload_where_parent_required`; an ApplicationHead whose constructor does not resolve is an abstention. NEXT-RUNG TRIGGER, named as the capability: one inhabitance judgment that compares established heads of any kind (product, coproduct, application) by declaration identity, sufficient to delete the directional product-versus-coproduct arm and the head-kind-keyed siblings.", + + "CORPUS CENSUS. Command A (official whole-root) `gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json --output-dir ` admitted then SIGKILL 137 after frontend+normalize on a 24 GiB host (EmitPopulationCompletenessUnestablished). Command B: per-root typecheck. `src/v2` primary with `dag` pool resolved 3888 sources. `dag/std`, `dag/extdeps`, `dag/examples`, `dag/gunbc/product` as primaries. Command C: `--entry` importer over the 1671 previously-unmentioned production `dag/gunbc` modules (not `dag/test/*`, not `recurring_failure_mode`) resolved 4045 sources. Indexed tree is 7993 `.dag` files (6309 under dag/, 1684 under src/v2). Command D: `--entry` importer over 608 `recurring_failure_mode` modules resolved 616 sources, zero `DeclaredTypeNotInhabited`. Command E: `dag/test` partition -- 17 sequential `--entry` chunks of 200 modules (last chunk the remainder) over the test modules not covered by B/C/D; identity-union of the 17 entry lists is 3329 unique modules, no omissions or duplicates against that universe. Each chunk typechecked; the only this-wall leftover was `dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag` clock-jump `list_append(list, element)` (now `list_snoc_item` at 208143cd). Other `DeclaredTypeNotInhabited` rows on these compiles are a different class. Product-versus-coproduct dispositions: json_kv helpers retyped to `List`; `taskbar_attention_attr` `ActivityUnobservable` returns `[]`; `gunbc.bmc_model` plus `megarac_media_model`, `filesystem_model` write, `bmc_dry_realization` bindings, and three `mtcollins1_boot_dry_realization` sites routed to `list_snoc_item`.", + ], + + evidence: [], +} diff --git a/dag/gunbc/roadmap/roadmap_page.dag b/dag/gunbc/roadmap/roadmap_page.dag index 463ec36fae9..af0ccac7280 100644 --- a/dag/gunbc/roadmap/roadmap_page.dag +++ b/dag/gunbc/roadmap/roadmap_page.dag @@ -1028,7 +1028,7 @@ fn taskbar_attention_attr(view: WorkRowView) -> List { LegacySupersedableAttempt { summary: _, located_reason: _, attempt_key: _, evidence: _ } => [] CompletedWork { outcome: _, evidence: _, obligations: _ } => [] NoActiveWork => [] - ActivityUnobservable { reason } => [ el_class("p", "issue-observation-unavailable", [ txt(concat("Work observation unavailable: ", reason)) ]) ] + ActivityUnobservable { reason: _ } => [] } } diff --git a/dag/gunbc/roadmap/roadmap_serve.dag b/dag/gunbc/roadmap/roadmap_serve.dag index 3770be4d3af..2a89715c183 100644 --- a/dag/gunbc/roadmap/roadmap_serve.dag +++ b/dag/gunbc/roadmap/roadmap_serve.dag @@ -112,6 +112,7 @@ import extdeps.languages.json.emit { json_int, json_array, JsonValue, + JsonKeyValue, } import gunbc.roadmap_launch_admission { LaunchRefusal, @@ -2114,14 +2115,14 @@ fn auth_session_response_over(instance: HostDashboardInstance, request: ServeHtt ) } -fn auth_session_roster_standing_members(roster: ProfileStoreReadAll) -> List { - let unreadable = [ json_kv(key: "profile_standing", value: json_string(s: "profile store unread; session profile only")) ] as List - let partial = [ json_kv(key: "profile_standing", value: json_string(s: "one or more profile records unreadable; the affected members render their fallback")) ] as List +fn auth_session_roster_standing_members(roster: ProfileStoreReadAll) -> List { + let unreadable = [ json_kv(key: "profile_standing", value: json_string(s: "profile store unread; session profile only")) ] + let partial = [ json_kv(key: "profile_standing", value: json_string(s: "one or more profile records unreadable; the affected members render their fallback")) ] match roster { ProfileStoreUnread { step: _, reason: _ } => unreadable ProfileStoreRead { profiles: _, skipped } => if count(skipped) == 0 { - [] as List + [] } else { partial } @@ -2186,7 +2187,7 @@ fn auth_session_body_over(roster: ProfileStoreReadAll, evidence: RequestAuthenti // projected one — absence is the member's ABSENCE, never an empty string standing in for none, // and the client reads absence (like a failed fetch) as the initials fallback, never an // identity claim from a hole in the wire. -fn auth_session_picture_members(picture: Uri?) -> List { +fn auth_session_picture_members(picture: Uri?) -> List { match picture { Present { value: u } => [ json_kv(key: "picture", value: json_string(s: uri_wire(uri: u) as String)) ] Absent => [] @@ -2195,7 +2196,7 @@ fn auth_session_picture_members(picture: Uri?) -> List { // THE OPTIONAL NAME MEMBER, the same law as the picture: absence is the member's ABSENCE, // never an empty string standing in for none. -fn auth_session_name_members(name: String?) -> List { +fn auth_session_name_members(name: String?) -> List { match name { Present { value: n } => [ json_kv(key: "name", value: json_string(s: n)) ] Absent => [] @@ -2203,7 +2204,7 @@ fn auth_session_name_members(name: String?) -> List { } // THE OPTIONAL EMAIL MEMBER, the same law as the name: absence is the member's ABSENCE. -fn auth_session_email_members(email: Email?) -> List { +fn auth_session_email_members(email: Email?) -> List { match email { Present { value: e } => [ json_kv(key: "email", value: json_string(s: e as String)) ] Absent => [] diff --git a/dag/gunbc/roadmap/roadmap_served_observation.dag b/dag/gunbc/roadmap/roadmap_served_observation.dag index 2730c528f18..2f44027a12c 100644 --- a/dag/gunbc/roadmap/roadmap_served_observation.dag +++ b/dag/gunbc/roadmap/roadmap_served_observation.dag @@ -765,7 +765,7 @@ fn served_observation_issue_query_surface(instance: HostDashboardInstance, plan: let attempts = match observed { WorkflowAttemptsObserved { attempts } => attempts WorkflowAttemptsRefused { reason: _ } => [] } let body = issue_query_snapshot_for_projection(proj: plan, attempts: attempts, attempts_refused: match observed { WorkflowAttemptsObserved { attempts: _ } => none WorkflowAttemptsRefused { reason } => Present { value: reason } }, - standings: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance)), launch: launch, + standings: served_standings_after_snapshot_close(read: roadmap_standings_read(layout: roadmap_event_carrier_layout_for_instance(instance: instance))), launch: launch, stale_nodes: stale_attempt_nodes(observations: served_attempt_revision_observations(instance: instance, attempts: attempts), current_revision_hex: served_current_revision_hex(launch: launch)), profiles: served_observation_profiles_for_instance(instance: instance)) match body { 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 affc2453db3..71fe301fb32 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 @@ -24,6 +24,22 @@ fn violation_count(source: String, wanted: String) -> Int { } } +// THE RELATION BOUNDARY, NOT THE CLASS COUNT. DeclaredTypeNotInhabited is shared by every +// inhabitance refusal. The product-versus-coproduct arm locates its own reason on the census +// subject; deleting RefusedProductCoproductHeadMismatch (or routing this pair through +// RefusedKernelAtStructured) changes that subject and this helper goes red. +fn product_coproduct_mismatch_at_parameter(source: String, parameter: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => + census_count_at_key( + rows: rows, + diagnostic_class: "DeclaredTypeNotInhabited", + subject_name: concat("direct call argument for parameter '", parameter, "' [RefusedProductCoproductHeadMismatch]"), + blocking: true) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + // THE PAIR THIS FILE EXISTS FOR. std.nat Nat and test.fixture.structural_peano_nat StructuralNat // are both declared as the Peano coproduct (zero, and the successor of one) and they do NOT // realize the same way: std.nat Nat is bound to the kernel integer @@ -127,7 +143,60 @@ test fn w_record_typed_value_at_scalar_argument_is_counted_until_identity_is_gro data coproduct_value_at_record_source: String = "module probe_inhabit_coproduct_at_record\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_choice() -> Choice { ChoiceA { value: \"forty\" } }\nfn takes_box(box: Box) -> Int { 1 }\nfn probe() -> Int { takes_box(box: make_choice()) }\n" test fn w_coproduct_typed_value_at_record_argument_is_refused() -> Bool { - violation_count(source: coproduct_value_at_record_source, wanted: "DeclaredTypeNotInhabited") > 0 + product_coproduct_mismatch_at_parameter(source: coproduct_value_at_record_source, parameter: "box") > 0 +} + +// THE DUAL, AND THE #13198 SPECIMEN. A generic product APPLICATION (CarrierClosed / Wrap) +// at a parameter declared as the inner coproduct was admitted: ApplicationHead is not ProductHead, +// the declared coproduct is not a product, and declared_type_inhabitance fell through to Inhabits. +// The actual is a CALL, not a record literal, so structured_application_site_type_mismatch cannot +// stand in as the wall. Named argument, same as the production site. +data generic_product_at_its_argument_coproduct_source: String = "module probe_inhabit_generic_product_at_coproduct\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: mk_wrap()) }\n" + +test fn w_a_generic_product_at_the_coproduct_it_wraps_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: generic_product_at_its_argument_coproduct_source, parameter: "x") > 0 +} + +data unapplied_product_at_coproduct_source: String = "module probe_inhabit_product_at_coproduct\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_choice(x: Choice) -> Int { 1 }\nfn probe() -> Int { takes_choice(x: make_box()) }\n" + +test fn w_an_unapplied_product_at_a_coproduct_argument_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: unapplied_product_at_coproduct_source, parameter: "x") > 0 +} + +data generic_product_at_matching_product_source: String = "module probe_inhabit_generic_product_ok\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_wrap(x: Wrap) -> Int { 1 }\nfn probe() -> Int { takes_wrap(x: mk_wrap()) }\n" + +test fn w_a_generic_product_at_its_own_declared_application_is_admitted() -> Bool { + violation_count(source: generic_product_at_matching_product_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +data generic_product_field_projected_source: String = "module probe_inhabit_generic_product_field\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap { result: T, tag: String }\nfn mk_wrap() -> Wrap { Wrap { result: InnerA { v: \"z\" }, tag: \"c\" } }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: mk_wrap().result) }\n" + +test fn w_the_inner_field_of_a_generic_product_at_that_coproduct_is_admitted() -> Bool { + violation_count(source: generic_product_field_projected_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// ZERO-FIELD PRODUCT BY DECLARATION KIND, NOT CHILD COUNT. `type Wrap {}` is Conj with +// zero children; the old `count(children)>0` gate answered "" and the pair reached Inhabits. +// The positive control is the same wrapper at its own application. +data zero_field_product_at_coproduct_source: String = "module probe_inhabit_zero_field_product\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap {}\nfn make_wrap() -> Wrap { Wrap {} }\nfn takes_inner(x: Inner) -> Int { 1 }\nfn probe() -> Int { takes_inner(x: make_wrap()) }\n" + +test fn w_a_zero_field_generic_product_at_the_coproduct_it_wraps_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: zero_field_product_at_coproduct_source, parameter: "x") > 0 +} + +data zero_field_product_at_matching_product_source: String = "module probe_inhabit_zero_field_product_ok\nimport std.types { Int, String }\ntype Inner = | InnerA { v: String } | InnerB\ntype Wrap {}\nfn make_wrap() -> Wrap { Wrap {} }\nfn takes_wrap(x: Wrap) -> Int { 1 }\nfn probe() -> Int { takes_wrap(x: make_wrap()) }\n" + +test fn w_a_zero_field_generic_product_at_its_own_declared_application_is_admitted() -> Bool { + violation_count(source: zero_field_product_at_matching_product_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// APPLIED COPRODUCT ApplicationHead. Box is a product application; Choice is a +// coproduct application. Deleting the ApplicationHead arm of nominal_coproduct_head_name +// turns this red into an admission. +data applied_product_at_applied_coproduct_source: String = "module probe_inhabit_applied_product_at_applied_coproduct\nimport std.types { Int, String }\ntype Box { value: T }\ntype Choice = | ChoiceA { value: T } | ChoiceB\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_choice(x: Choice) -> Int { 1 }\nfn probe() -> Int { takes_choice(x: make_box()) }\n" + +test fn w_an_applied_product_at_an_applied_coproduct_argument_is_refused() -> Bool { + product_coproduct_mismatch_at_parameter(source: applied_product_at_applied_coproduct_source, parameter: "x") > 0 } // The syntax contrast that exposed the application hole. The cast seam already refused the same diff --git a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag index faeb57b682e..574de21fb10 100644 --- a/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag +++ b/dag/test/claim/machine_intake/mtcollins1_boot_acceptance_matrix_test.dag @@ -2,6 +2,7 @@ module test.claim.machine_intake.mtcollins1_boot_acceptance_matrix_test import gunbc.build_cache_instance { ProcessIdentity } import std.types { Bool, Int, List, NonEmptyStr, String } +import std.algebra { list_snoc_item } import std.measure { Second, second } import std.materialization_ladder { Frame, SharedStateFrame } import std.effect_grant { Read, Write, ServiceOpTree, NamespacePosition, ModeledRealization, LifecycleByConstruction, Grant, Envelope } @@ -716,7 +717,7 @@ test fn a_successor_in_another_pid_namespace_refuses_rather_than_recovering() -> fn with_clock_jump(w: MtCollins1BootWorld, at: Second, by: Int) -> MtCollins1BootWorld { MtCollins1BootWorld { bmc: w.bmc, fs: w.fs, environment: w.environment, agent: w.agent, remote_hosts: w.remote_hosts, - clock: ModeledWallClock { unix_at_origin: w.clock.unix_at_origin, step: w.clock.step, jumps: list_append(w.clock.jumps, ModeledClockStep { at: at, by: std.measure.second_displacement(count: by) }) }, + clock: ModeledWallClock { unix_at_origin: w.clock.unix_at_origin, step: w.clock.step, jumps: list_snoc_item(xs: w.clock.jumps, item: ModeledClockStep { at: at, by: std.measure.second_displacement(count: by) }) }, worker: w.worker, console: w.console, media: w.media, screen: w.screen, } } diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 476618d6dc5..cedb708c879 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -109,6 +109,7 @@ import v1.compiler.infer_types { normalize_access_type_node, node_type_shape, node_type_compatible, node_type_equals, prefer_specific_type, is_declared_container_alias_spelling, structural_carrier_template_name, + is_product_type, node_type_deps, method_receiver_element_node, infer_literal_node, infer_binop_type_node, subtraction_refinement_of, @@ -4037,6 +4038,7 @@ type InhabitanceUndecidableReason type InhabitanceRefusalReason = RefusedPayloadAtParent | RefusedKernelAtStructured + | RefusedProductCoproductHeadMismatch | RefusedCollectionAtEstablishedIdentity | RefusedDistinctProductConstructor | RefusedDistinctAppliedTypeArgument @@ -4331,8 +4333,8 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceRefused { reason: RefusedCollectionAtEstablishedIdentity } } else if record_at_scalar_needs_identity(declared: declared, produced: produced, scope: scope) { InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } - } else if coproduct_at_record_declared_type(declared: declared, produced: produced, scope: scope) { - InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if product_versus_coproduct_head_mismatch(declared: declared, produced: produced, scope: scope) { + InhabitanceRefused { reason: RefusedProductCoproductHeadMismatch } } else { match refinement_inhabitance(declared: declared, produced: produced, scope: scope) { Present { value: RefinementWidensToDeclaredBase } => Inhabits @@ -4513,13 +4515,22 @@ fn record_at_scalar_needs_identity(declared: Node, produced: Node, scope: InferS && type_head_exposure_is_product(exposure: expected_type_head_exposure(formal: produced, scope: scope)) } -// Product-vs-coproduct is settled from exact type-head census identities. A second bare-name -// declaration lookup can select a homonym and fabricate a refusal, so it is not an authority here. -fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: InferScope) -> Bool { +// Product and coproduct are disjoint identities. The first spelling of this relation judged +// only a COPRODUCT value at a PRODUCT formal, and it keyed that judgment on ProductHead / +// CoproductHead exposures. A generic product APPLICATION exposes ApplicationHead, so +// CarrierClosed at a T coproduct (gunbc#13198: roadmap_standings_read at +// issue_query_snapshot_for_projection.standings) matched neither side and the inhabitance +// relation fell through to Inhabits. THE HEADS ARE THE SAME AUTHORITIES THE NOMINAL-PRODUCT +// AND GENERIC-COPRODUCT ARMS ALREADY USE: a declared product, applied or not, and a declared +// coproduct, applied or not — including a zero-field product (declaration kind Conj, not +// child count) and an applied coproduct (ApplicationHead whose constructor peels to Disj). +// A second leaf-name lookup is not an authority here. Either direction refuses; +// same-declaration and transparent-alias pairs still abstain. The typed reason is +// RefusedProductCoproductHeadMismatch, not RefusedKernelAtStructured: this is a head-kind +// clash, not a kernel value at a structured formal. +fn product_versus_coproduct_head_mismatch(declared: Node, produced: Node, scope: InferScope) -> Bool { let declared_name = authored_name_at(source_indices: scope.type_env.source_indices, node: declared) let produced_name = authored_name_at(source_indices: scope.type_env.source_indices, node: produced) - let declared_head = expected_type_head_exposure(formal: declared, scope: scope) - let produced_head = expected_type_head_exposure(formal: produced, scope: scope) if application_type_names_compatible( formal_name: declared_name, lit_name: produced_name, type_env: scope.type_env, module_name: scope.module_name, @@ -4528,8 +4539,12 @@ fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: Infe index: scope.type_env.symbol_index, left: declared_name, right: produced_name) { false } else { - type_head_exposure_is_product(exposure: declared_head) - && type_head_exposure_is_coproduct(exposure: produced_head) + let declared_product = nominal_product_head_name(n: declared, scope: scope) + let produced_product = nominal_product_head_name(n: produced, scope: scope) + let declared_coproduct = nominal_coproduct_head_name(n: declared, scope: scope) + let produced_coproduct = nominal_coproduct_head_name(n: produced, scope: scope) + (declared_product != "" && produced_coproduct != "") + || (declared_coproduct != "" && produced_product != "") } } @@ -4633,13 +4648,16 @@ fn declared_realizes_as_kernel_numeric( // MalformedApplicationHead identities are legitimate abstentions when resolution or arity checking // already owns the error (refusing again would cascade). Kernel scalars, collections and coproducts // are excluded because their dedicated judgments run before this arm. Optional values, callables, -// anonymous records and zero-field products are REAL SHAPES but UNHANDLED HERE: respectively, +// anonymous records are REAL SHAPES but UNHANDLED HERE: respectively, // `fn f() -> A? { B{..} }`, `fn f() -> fn(Int) -> Int { B{..} }`, -// `fn f() -> A { { y: 1 } }`, and `fn f() -> EmptyA { EmptyB{} }` can still pass this relation -// silently. Generic applications are likewise a separate, filed half of the inhabitance defect. An OpaqueTypeHead is +// and `fn f() -> A { { y: 1 } }` can still pass this relation +// silently. A declared zero-field product is a product by declaration kind (`is_product_type` +// and not `is_where_refinement_type`), so `EmptyA` versus `EmptyB` and `Wrap {}` at a +// coproduct are judged. Generic applications are a separate, filed half of the inhabitance +// defect. An OpaqueTypeHead is // not automatically unhandled: transparent aliases expose that view, so the declaration is peeled // through the existing alias authority and admitted to this arm only when the peel positively lands -// on a nonempty product. This change closes concrete named products and their transparent aliases; +// on a declared product. This change closes concrete named products and their transparent aliases; // it does not claim the unhandled shapes climbed with them. fn nominal_product_inhabitance_refusal( declared: Node, @@ -4721,7 +4739,45 @@ fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope Present { value: decl } => let peeled = peel_nominal_alias_identity( n: decl, env: scope.type_env, module_name: scope.module_name) - if peeled.connective == Conj && (peeled.children |> count) > 0 { name } else { "" } + if is_product_type(n: peeled) && is_where_refinement_type(ty: peeled) == false { name } else { "" } + Absent => "" + } +} + +// The coproduct dual of nominal_product_head_name: a declared coproduct, applied or not. +// nominal_coproduct_application_head_name requires children and so answers "" for an +// unapplied RoadmapStandings; type_head_exposure_is_coproduct misses an ApplicationHead +// of a generic coproduct. This is the one head both of those questions share. +fn nominal_coproduct_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_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + ExposedTypeHead { view: CoproductHead { type_identity: _ } } => + nominal_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + OpaqueTypeHead { type_identity: _ } => + nominal_coproduct_head_name_if_declared_coproduct(name: name, scope: scope) + _ => "" + } + } +} + +fn nominal_coproduct_head_name_if_declared_coproduct(name: String, scope: InferScope) -> String { + let representative = transparent_alias_representative( + index: scope.type_env.symbol_index, name: name) + match lookup_type_by_name(env: scope.type_env, name: representative) { + Present { value: decl } => + let peeled = peel_nominal_alias_identity( + n: decl, env: scope.type_env, module_name: scope.module_name) + if peeled.connective == Disj { name } else { "" } Absent => "" } } @@ -5006,6 +5062,19 @@ fn applied_type_argument_identity_known(name: String, scope: InferScope) -> Bool // non-blocking in v1.00_core is_interpreter_blocking_diagnostic and advisory in // is_discovery_corpus_advisory_typecheck_diagnostic, so this makes the residue visible without // reddening a corpus whose seams were never judged before this carrier existed either. +fn inhabitance_refusal_position_label( + position: DeclaredTypePosition, + subject: String, + reason: InhabitanceRefusalReason +) -> String { + let base = declared_type_position_label(position: position, subject: subject) + match reason { + RefusedProductCoproductHeadMismatch => + concat(base, " [RefusedProductCoproductHeadMismatch]") + _ => base + } +} + fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> String { match reason { UndecidableGenericFormal => "generic formal: the declared position's payload types can be type variables, so membership is not decidable from the declaration alone" @@ -5056,10 +5125,11 @@ fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: Inf }, module_name: scope.module_name )] - InhabitanceRefused { reason: _ } => + InhabitanceRefused { reason: r } => [make_error_node( diagnostic: DeclaredTypeNotInhabited { - position: declared_type_position_label(position: obligation.position, subject: obligation.subject), + position: inhabitance_refusal_position_label( + position: obligation.position, subject: obligation.subject, reason: r), expected: obligation_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), got: obligation_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), span: obligation.span diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 826f9a3c723..a62a9a1a9b0 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -248,7 +248,7 @@ use crate::v1_compiler_infer_types::TextNotAskedReason::{ pub use crate::v1_compiler_infer_types::{ bare_map_node, bare_set_node, callable_inferred, callable_return_type, child_type_node, emit_map_has, extract_optional_inner_node, for_each_element_type_node, infer_binop_type_node, - infer_literal_node, is_declared_container_alias_spelling, is_fully_resolved, + infer_literal_node, is_declared_container_alias_spelling, is_fully_resolved, is_product_type, is_type_expr_annotation, kernel_profile_lookup, make_callable_type, make_container_type, method_receiver_element_node, node_is_collection, node_is_element_collection, node_is_keyed_collection, node_is_set_collection, node_type_compatible, node_type_deps, @@ -5797,6 +5797,7 @@ pub enum InhabitanceUndecidableReason { pub enum InhabitanceRefusalReason { RefusedPayloadAtParent, RefusedKernelAtStructured, + RefusedProductCoproductHeadMismatch, RefusedCollectionAtEstablishedIdentity, RefusedDistinctProductConstructor, RefusedDistinctAppliedTypeArgument, @@ -6163,13 +6164,13 @@ pub fn declared_type_inhabitance( reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, }) } else { - if coproduct_at_record_declared_type( + if product_versus_coproduct_head_mismatch( declared.clone(), produced.clone(), scope.clone(), ) { Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + reason: InhabitanceRefusalReason::RefusedProductCoproductHeadMismatch, }) } else { match refinement_inhabitance(declared.clone(), produced.clone(), scope.clone()) { @@ -6393,7 +6394,7 @@ pub fn record_at_scalar_needs_identity( )) } -pub fn coproduct_at_record_declared_type( +pub fn product_versus_coproduct_head_mismatch( declared: Rc, produced: Rc, scope: Rc, @@ -6407,8 +6408,6 @@ pub fn coproduct_at_record_declared_type( scope.type_env.clone().source_indices.clone(), produced.clone(), ); - let declared_head = expected_type_head_exposure(declared.clone(), scope.clone()); - let produced_head = expected_type_head_exposure(produced.clone(), scope.clone()); if (application_type_names_compatible( declared_name.clone(), produced_name.clone(), @@ -6422,11 +6421,18 @@ pub fn coproduct_at_record_declared_type( )) { false } else { - (crate::v1_compiler_type_head_exposure::type_head_exposure_is_product( - declared_head.clone(), - ) && crate::v1_compiler_type_head_exposure::type_head_exposure_is_coproduct( - produced_head.clone(), - )) + { + let declared_product = nominal_product_head_name(declared.clone(), scope.clone()); + let produced_product = nominal_product_head_name(produced.clone(), scope.clone()); + let declared_coproduct = + nominal_coproduct_head_name(declared.clone(), scope.clone()); + let produced_coproduct = + nominal_coproduct_head_name(produced.clone(), scope.clone()); + (((declared_product.clone() != "".to_string()) + && (produced_coproduct.clone() != "".to_string())) + || ((declared_coproduct.clone() != "".to_string()) + && (produced_product.clone() != "".to_string()))) + } } } } @@ -6568,9 +6574,95 @@ pub fn nominal_product_head_name_if_declared_product( scope.type_env.clone(), scope.module_name.clone(), ); - if ((peeled.connective.clone() == Connective::Conj) - && ((peeled.children.clone().len() as i64) > 0)) + if (crate::v1_compiler_infer_types::is_product_type(peeled.clone()) + && (is_where_refinement_type(peeled.clone()) == false)) + { + name.clone() + } else { + "".to_string() + } + } + std::option::Option::None => "".to_string(), + } + } +} + +pub fn nominal_coproduct_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_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) + } + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!( + view.as_ref(), + TypeHeadView::CoproductHead { + type_identity: _, + .. + } + ) => { + let TypeHeadView::CoproductHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()) + } + TypeHeadExposure::OpaqueTypeHead { + type_identity: _, .. + } => nominal_coproduct_head_name_if_declared_coproduct(name.clone(), scope.clone()), + _ => "".to_string(), + } + } + } +} + +pub fn nominal_coproduct_head_name_if_declared_coproduct( + name: String, + scope: Rc, +) -> String { + { + let representative = transparent_alias_representative( + scope.type_env.clone().symbol_index.clone(), + name.clone(), + ); + match crate::v1_compiler_infer_env::lookup_type_by_name( + scope.type_env.clone(), + representative.clone(), + ) { + Some(decl) => { + let peeled = crate::v1_compiler_infer_resolve::peel_nominal_alias_identity( + decl.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + if (peeled.connective.clone() == Connective::Disj) { name.clone() } else { "".to_string() @@ -6913,6 +7005,23 @@ pub fn applied_type_argument_identity_known(name: String, scope: Rc) } } +pub fn inhabitance_refusal_position_label( + position: DeclaredTypePosition, + subject: String, + reason: InhabitanceRefusalReason, +) -> String { + { + let base = declared_type_position_label(position.clone(), subject.clone()); + match reason.clone() { + InhabitanceRefusalReason::RefusedProductCoproductHeadMismatch => v1_rt::concat( + base.clone(), + " [RefusedProductCoproductHeadMismatch]".to_string(), + ), + _ => base.clone(), + } + } +} + 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(), @@ -6978,12 +7087,13 @@ pub fn declared_type_obligation_diags( scope.module_name.clone(), )]) } - InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => { + InhabitanceVerdict::InhabitanceRefused { reason: r, .. } => { Rc::new(vec![crate::v1_std_core::make_error_node( Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { - position: declared_type_position_label( + position: inhabitance_refusal_position_label( obligation.position.clone(), obligation.subject.clone(), + r.clone(), ), expected: obligation_type_shape( obligation.declared.clone(), @@ -32361,6 +32471,8 @@ 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 RefusedProductCoproductHeadMismatch; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedCollectionAtEstablishedIdentity; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedDistinctProductConstructor;