v2 inhabitance: an optional produced at a required declared type is refused, not counted - #12806

Merged

gunbai-bot[bot] merged 61 commits into

mainfrom

session/smart-newt-725-optional-converse

Sep 30, 2026

Commits on Sep 27, 2026

v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted; cut every consumer root-first

Brian Searls
and
claude
committed
03342a3
Merge origin/main; migrate the remaining resolved-tree helpers (typecheck clean)

Brian Searls
and
claude
committed
179c7f1
pick_ingested: the arrow extractor returns the arrow Node (my retype over-reached)

Brian Searls
and
claude
committed
95856ef
Merge origin/main; retype main's new resolved-tree helpers (declared_parameter_order, reference_closure)

Brian Searls
and
claude
committed
84d4768

Commits on Sep 28, 2026

Merge origin/main into the carrier (kinds stays a separate once-prepared input); retype main's new resolved-tree test sites

Brian Searls
and
claude
committed
c12bf6d
Merge origin/main (#12379 landed)
Brian Searls
committed
341a092
Merge origin/main (#12379 landed); #12379's new hand-built infer inputs use the named no-declarations constructor

Brian Searls
and
claude
committed
0fb011f
WIP: v2 floor gap: declared return types are never checked (PositionDeclaredR
Brian Searls
committed
3653f3a
Delete the zz_probe_dr exploratory probe file

briansrls
and
claude
committed
5366696

Commits on Sep 29, 2026

Merge origin/main (declared_signature moved to v2.std.arrow_signature); typecheck clean over 116 files

Brian Searls
and
claude
committed
23697f7
Merge origin/main (#12440 landed)
Brian Searls
committed
66c401b
Merge origin/main (5 commits); one_member_cost_probe keeps main's wanted symbol and reads .root

Brian Searls
and
claude
committed
ec7c3de
Merge origin/main
Brian Searls
committed
cd88b7d
plain_type_decl_lowering (new from main): its assembly helpers carry ResolvedTree and walk .root

Brian Searls
and
claude
committed
2b8dc42
Merge origin/main
Brian Searls
committed
3f95faa
Merge origin/main; body_let_annotation (#12540's new rows) carries ResolvedTree

Brian Searls
and
claude
committed
c90dae3
Merge main into #12566
Brian Searls
committed
778a6f0
Declared-return witness: import declared_signature / list-introduction from their post-split homes

Brian Searls
and
claude
committed
958200b
v2: lower the where-refined head as a type so resolve binds it; ResolvedTree.resolved_declarations (neat-boar-16 ruling)

Brian Searls
and
claude
committed
029efaf
Merge origin/main (#12432 landed as a squash)

Brian Searls
and
claude
committed
9d653a0
Declared return: one inhabitance relation replaces #12379's inline check

Brian Searls
and
claude
committed
40efcd5
function_type_evidence_carries_its_body: cite the surviving return check

Brian Searls
and
claude
committed
dacbf5c
resolve: ResolvedTree comment states symbol_index's consumers once (no later stage reads it; #12407 reads resolved_declarations) (review 72652)

Brian Searls
and
claude
committed
f293dcb
Plan: construct tag as a declaration reference (qualified construction/patterns), reader census

gunbc-ci-auto-heal
and
claude
committed
031639a
Plan: fold in review conditions and landing order; file the live construct-tag misread row (confirmed by execution)

gunbc-ci-auto-heal
and
claude
committed
254cf93
Construct tag as a declaration reference: qualified construction, patterns and nullary values lower through one route

gunbc-ci-auto-heal
and
claude
committed
8cb3894

Commits on Sep 30, 2026

Keep the unmarked Conj arrow-body admission unchanged; construct marker is the only new case

gunbc-ci-auto-heal
and
claude
committed
bc43a41
Merge remote-tracking branch 'origin/session/bold-gull-638' into session/smart-newt-725
gunbc-ci-auto-heal
committed
8eae258
Merge remote-tracking branch 'origin/session/lively-eagle-657-cut' into session/smart-newt-725
gunbc-ci-auto-heal
committed
98d4918
WIP: record construct field inhabitance (pre-#12629 base)

gunbc-ci-auto-heal
and
claude
committed
04c44c0
Merge remote-tracking branch 'origin/session/wise-bat-862-resolved-decls' into session/smart-newt-725
gunbc-ci-auto-heal
committed
fadccfc
WIP: record construct field inhabitance on #12629 base; witness, row, enrolment

gunbc-ci-auto-heal
and
claude
committed
6e5acff
Declared-return witness hands infer a ResolvedTree (fixture wrapper)

gunbc-ci-auto-heal
and
claude
committed
a7e3da2
Declared-return witness: wrap the remaining infer call

gunbc-ci-auto-heal
and
claude
committed
787de75
Merge remote-tracking branch 'origin/main' into session/smart-newt-725
gunbc-ci-auto-heal
committed
f46e701
Merge remote-tracking branch 'origin/main' into session/lively-eagle-657-cut
gunbc-ci-auto-heal
committed
0eb3633
Merge remote-tracking branch 'origin/main' into session/bold-gull-638
gunbc-ci-auto-heal
committed
9dbc537
Merge main; migrate vf_wildcard_pattern_keeps_its_field (added by #12650) to the reference tag

gunbc-ci-auto-heal
and
claude
committed
d50f298
Declared-return witness hands infer a ResolvedTree through the fixture wrapper

gunbc-ci-auto-heal
and
claude
committed
76bc35d
Merge remote-tracking branch 'origin/session/lively-eagle-657-cut' into session/smart-newt-725
gunbc-ci-auto-heal
committed
b589094
Merge commit '76bc35d694e439a4806917f4bc4d8e46bf313509' into session/smart-newt-725
gunbc-ci-auto-heal
committed
edc2853
Record-field witness: one infer per claim, decided controls over the declaration's member

gunbc-ci-auto-heal
and
claude
committed
aa629b0
Record-field row and witness note: the Bool gap is a binding/denotation symbol fork, not a missing spelling

gunbc-ci-auto-heal
and
claude
committed
ee4ff8a
v2 infer: the Cardinality type connective owes no descent (T? no longer refused for infer_descent_not_derived)

Brian Searls
and
claude
committed
9e01617
Merge remote-tracking branch 'origin/main' into session/smart-newt-725
gunbc-ci-auto-heal
committed
09b5bf8
Supplied-tree claims only: keep the discriminating T? red and a correctly-shaped Loop descent control

Brian Searls
and
claude
committed
520fc4b
Merge origin/main
Brian Searls
committed
671246f
Merge remote-tracking branch 'origin/session/cool-cat-831' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
bf905db
WIP: optional produced at a required declared type is refused by the relation

gunbc-ci-auto-heal
and
claude
committed
6cbae2c
Optional-at-required: record the v2 route's rung on the existing failure-mode row

gunbc-ci-auto-heal
and
claude
committed
7ea7a06
Merge remote-tracking branch 'origin/main' into session/smart-newt-725
gunbc-ci-auto-heal
committed
8d02ac1
Merge branch 'session/smart-newt-725' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
8938065
infer: call v2.std.node match_arm_pattern_edge directly instead of through a forwarding second name (review 73309)

gunbc-ci-auto-heal
and
claude
committed
ccc2e07
node: the pattern-edge note cites the infer function that reads it

gunbc-ci-auto-heal
and
claude
committed
be9f54d
Merge branch 'session/smart-newt-725' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
aa53de1
infer: the match-arm pattern note sits above infer_gather_fold_step, not inside it (DESIGN 4c)

gunbc-ci-auto-heal
and
claude
committed
6a45530
Merge branch 'session/smart-newt-725' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
6ff24d8
Merge remote-tracking branch 'origin/main' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
ea2a6a2
Merge remote-tracking branch 'origin/main' into session/smart-newt-725
gunbc-ci-auto-heal
committed
4d649ff
Merge branch 'session/smart-newt-725' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
6962dcf
Merge remote-tracking branch 'origin/main' into session/smart-newt-725-optional-converse
gunbc-ci-auto-heal
committed
7b1ef30