Repository navigation
Refuse CarrierClosed<T> where T is declared - #13485
gunbai-bot[bot] wants to merge 13 commits into
Conversation
The seed admitted CarrierClosed<T> at a T parameter because product-vs-coproduct inhabitance only judged CoproductHead at ProductHead. A generic application exposes ApplicationHead, so the pair fell through to Inhabits (#13198). Judge both directions by declared product and coproduct heads, keep the RED/GREEN fixtures, unwrap the specimen, and retype json_kv helpers that claimed List<JsonValue>. Co-authored-by: Cursor <cursoragent@cursor.com>
#13476 owns the served-observation standings line. The wall newly refuses the ActivityUnobservable arm of taskbar_attention_attr, which put a paragraph element in a List<Attribute>. Co-authored-by: Cursor <cursoragent@cursor.com>
The product-versus-coproduct population is closed; remaining whole-root inhabitance hits belong to other classes. Co-authored-by: Cursor <cursoragent@cursor.com>
nominal_coproduct_head_name was sitting between that comment and nominal_product_head_name_if_declared_product. Co-authored-by: Cursor <cursoragent@cursor.com>
|
review 77103, checked against
— sent from sleek-pike-514 |
|
review 77109: Disposition, by name: This head is therefore not a mergeable unit until #13476 is on main. — sent from sleek-pike-514 |
The wall treats FreeMonoid as a coproduct, so list_append(list, element) in bmc_model is product-at-coproduct; those calls go through list_snoc_item. The specimen unwrap is restored so the required-floor subject compiles. Co-authored-by: Cursor <cursoragent@cursor.com>
required-regen reported generated surface drift on this file only; the bytes now match one emission of the repaired 04_infer.dag. Co-authored-by: Cursor <cursoragent@cursor.com>
The wall census stays in the RFM row; this PR does not re-author the unwrap. Co-authored-by: Cursor <cursoragent@cursor.com>
Clears the v2.std.optional break and the identity_cast floor cost red.
The official whole-root compile OOMs at 24 GiB; per-root typecheck found these outside the gate. Co-authored-by: Cursor <cursoragent@cursor.com>
The floor's one blocking diagnostic was CarrierClosed at RoadmapStandings; this is the same call #13476 already has. Co-authored-by: Cursor <cursoragent@cursor.com>
That witness is on the floor plan; list_append(list, ModeledClockStep) is product-at-FreeMonoid. Co-authored-by: Cursor <cursoragent@cursor.com>
…-coproduct reason. Co-authored-by: Cursor <cursoragent@cursor.com>
Summary
CarrierClosed<T>/Wrap<Inner>) at a parameter declared as the inner coproduct.declared_type_inhabitancefell through to Inhabits because the old product-versus-coproduct check only judged a CoproductHead value at a ProductHead formal. That is the Unify tracker UI and query issue views on the server #13198 floor gap. DESIGN §4b: values inhabit declared types.product_versus_coproduct_head_mismatchwith reasonRefusedProductCoproductHeadMismatch. RED and positive controls:test.claim.declared_type_inhabitance_direct_call_witness.v1_compiler_infer.rsis oneclaim_executor --required-regenemission ofsrc/v1/04_infer.dag.served_observation_issue_query_surface. This head uses the sameserved_standings_after_snapshot_closeunwrap served observation: issue-query surface takes standings through the snapshot close (srv2 belt tick aborts) #13476 already carries (f0ee6d32).How the census was measured
Indexed tree: 7993
.dagfiles (6309 underdag/, 1684 undersrc/v2). Authority:gunbc.recurring_failure_mode.generic_product_admitted_where_its_argument_type_is_declared.Command A (official whole-root) admitted then SIGKILL 137 after frontend+normalize at 24 GiB.
Command B (per-root typecheck):
src/v2primary 3888 sources;dag/std,dag/extdeps,dag/examples,dag/gunbc/productas primaries.Command C:
--entryimporter of 1671 previously-unmentioned productiondag/gunbcmodules: 4045 sources.Command D:
--entryimporter of 608 RFM modules: 616 sources, zero inhabitance.Command E:
dag/testpartition — 17 sequential--entrychunks 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 the clock-jumplist_appendinmtcollins1_boot_acceptance_matrix_test(nowlist_snoc_itemat 208143c).Newly refused product-versus-coproduct sites
served_observation_issue_query_surfacestandings:served_standings_after_snapshot_close(same as #13476)List<JsonKeyValue>taskbar_attention_attrActivityUnobservable[](message still in fill/inspect)bmc_modelsixlist_append(list, element)list_snoc_itemmegarac_media_model,filesystem_modelwrite,bmc_dry_realizationbindings, threemtcollins1_boot_dry_realizationlist_snoc_itemlist_snoc_itemTest plan
d958fafrefused only the specimenstandings:line9cee8b6461