Add v2.5 infer stage prototype by briansrls · Pull Request #3425 · gunb-ai/gunbc

briansrls · 2026-05-19T22:10:48Z

Summary

Rebases src/v2.5/04_infer.dag onto vivid-lynx-807's reconciled Tier 1 stage-type kit from PR #3418 (dfb926f8c) and binds the stage to the actual current contract:

fn infer(module: NormalizedModule) -> InferredModule

The previous prototype targeted a provisional NormalizedNode / InferredNode / fold_normalized_node API that no longer exists after the Tier 1 reconcile. This version keeps the infer stage compileable and fail-closed while recording the missing recursive expression fold and pre-child binder-scope hook as first-class model state.

This PR intentionally touches only src/v2.5/04_infer.dag on top of the Tier 0/Tier 1 v2.5 substrate branches. It does not touch src/v2/, src/v3/, src/v4/, dsl/, or Rust.

Stage Shape

Input contract: NormalizedModule, imported from v2_5.std.stage_types (src/v2.5/04_infer.dag:4).
Output contract: InferredModule, imported from v2_5.std.stage_types (src/v2.5/04_infer.dag:4).
Stage entrypoint: infer(module: NormalizedModule) -> InferredModule (src/v2.5/04_infer.dag:62).
Current execution mode: fail-closed via infer_readiness = AwaitingRecursiveExprFold (src/v2.5/04_infer.dag:53).
Binder lane status: binder_scope_fold_status = AwaitingPreChildScopeHook (src/v2.5/04_infer.dag:54).

What Dissolved

The stale provisional node API (NormalizedNode, InferredNode, NormalizedFoldAlgebra, fold_normalized_node) is gone from this stage.
The stage no longer depends on old 4-variant NodeKind discrimination; it imports only Symbol from v2_5.std.node (src/v2.5/04_infer.dag:3).
ExprData decompression remains represented as a closed dissolution ledger (ExprDataDissolution, src/v2.5/04_infer.dag:10).
Infer-local readiness and binder-scope blockers are modeled as closed carriers (InferReadiness, BinderScopeFold) and a closure receipt (InferCarrierClosure, src/v2.5/04_infer.dag:34).

Rebase Notes

Rebased onto PR v2.5: phase-typed stage interface kit (Tier 1) #3418 head dfb926f8c, which includes Tier 0 PR v2.5 fork — Tier 0 substrate (std/node.dag + std/diagnostic.dag) #3422's THESIS-faithful substrate.
No vendored node.dag or stage_types.dag is added here; those remain owned by Tier 0/Tier 1.
The direct recursive expression transformer was removed because v2-compiler compile --source-root src/v2.5 hung after resolution when the infer module recursively traversed NormalizedExpr. The compileable shape is therefore an honest fail-closed stage boundary until Tier 1 exposes the recursive expression fold / binder pre-child scope hook.

Validation

cargo run -p v2-compiler --release -- compile --source-root src/v2.5 --output-dir /tmp/v25-check --target dag — passes; 7 modules indexed/resolved, 0 diagnostics.
git diff --check — passes.
rg -n "NodeKind|Declaration|Composite|TypeForm \\{|Computation \\{|edge_is_named|edge_is_positional|is_empty_conj_root|expr_data|inferred:|src/v2/|src/v3/|src/v4/" src/v2.5/04_infer.dag — no matches.

Honest Yellow List

Full expression inference is not implemented in this rebased version. It is blocked on a shared recursive expression fold/algebra surface in Tier 1.
Let/lambda/for-each inference remains fail-closed until the fold API can enter binder bodies under an extended lexical scope before child inference.
The current InferredModule carries an InferredOtherItem marker instead of inferred items while infer_readiness is AwaitingRecursiveExprFold.
This is now 83 lines versus v2 src/v2/04_infer.dag at 6063 lines; the large reduction is mostly from refusing to preserve the stale provisional walker rather than from completed inference logic.

Introduce src/v2.5/std/stage_types.dag with closed-sum ParseModule, ResolvedModule, NormalizedModule, and InferredModule shapes. ExprData's 22 cases are decompressed into per-phase expression coproducts; typing lives as expr_type on InferredExpr variants, not optional inferred fields. Supporting modules: syntax.dag, identity.dag, token.dag (interim contracts). Co-authored-by: Cursor <cursoragent@cursor.com>

Add SurfaceSugarKind, ResolvedSugared/ResolvedCore module items, and SeamResolvedNode/SeamNormalizedNode substrate projection carriers so 03_normalize can target either the full AST or the v4-shaped seam. Co-authored-by: Cursor <cursoragent@cursor.com>

Import node.dag + diagnostic.dag from cool-bee-832 substrate. Drop duplicate Connective/EdgeLabel/Behavior; use 6-case Connective in seam types. Rename param optional to ParamCardinality. Symbol authority moves to node.dag. Co-authored-by: Cursor <cursoragent@cursor.com>

Complete the emit pipeline port pair so the header contract matches the typed stage boundaries through emit. Emit implementation remains Tier 2. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: bb5b7fca · Trigger: schedule
Thinking: 260s wall

BLOCKING (5)

Root Cause

src/v2.5/04_infer.dag v2.5 stage substrate modules are not landed with the stage implementation → add the v2_5.std.node/stage_types declarations in this PR or bind the prototype to an existing namespace.
src/v2.5/04_infer.dag the prototype declares raw carrier sums before the dissolution classification pass → classify or dissolve each substrate-facing coproduct before landing.
src/v2.5/04_infer.dag the fold output shape separates inferred expressions from their diagnostic list and only carries the expression forward → make InferredExprNode carry diagnostics or have the fold return a diagnostic-preserving result carrier.
src/v2.5/04_infer.dag the child-first fold is being used for binder forms without a pre-child scope hook → make let/lambda/for-each bodies fold under their extended lexical scope.
src/v2.5/04_infer.dag record literals are modeled as parallel label/value lists at the infer boundary → carry field entries as one edge-shaped field/value carrier or preserve both facts through InferredRecordLit.

⚠️ The prototype has unresolved stage dependencies and several boundary-shape issues that would be harder to fix after downstream consumers copy the stage contract.

briansrls · 2026-05-20T00:11:22Z

@@ -0,0 +1,826 @@
+module v2_5.compiler.infer
+


BLOCKING: This new stage imports v2_5.std.node and v2_5.std.stage_types, but the supplied diff adds only this file and origin/main has no src/v2.5/std blobs, so the PR introduces an unresolved module boundary.

briansrls · 2026-05-20T00:11:22Z

+  InferredTypeDecl, InferredDataDecl, InferredFuncDecl,
+  InferredServiceDecl, InferredTransportDecl,
+  NormalizedFoldAlgebra, fold_normalized_node
+}


BLOCKING: TypeRef starts a set of new substrate-facing coproducts with no required 🟢/🟡/🔴 classification tags, violating modeling-discipline Practice 4/9 and INVARIANTS P5.

briansrls · 2026-05-20T00:11:22Z

+
+fn child_expr_node(node: InferredNode) -> InferredExpr {
+  match node {
+    InferredModule { name: _, imports: _, items: _, exports: _, diagnostics: _ } =>


BLOCKING: expr_result_node drops ExprInference.diagnostics at the expression-to-node boundary, so collected diagnostics cannot reliably reach InferredModule.diagnostics, violating fail-closed facts-flow discipline.

briansrls · 2026-05-20T00:11:22Z

+      ItemInference {
+        item: InferredTypeDecl { name: error_symbol, type_ref: diagnostic_type(diagnostic: UnimplementedTypeKitBinding { missing: unknown_type_kit_binding }) },
+        diagnostics: [UnimplementedTypeKitBinding { missing: unknown_type_kit_binding }],
+        exports: []


BLOCKING: infer_let extends scope only after the body has already arrived as an InferredExpr child, so let-bound names in the body are inferred under the wrong environment.

briansrls · 2026-05-20T00:11:22Z

+      Some { value: actual } =>
+        infer_error(diagnostic: BranchTypeMismatch { then_type: first_facts.result_type, else_type: actual })
+      None =>
+        ExprInference {


BLOCKING: infer_record_lit receives field labels but constructs InferredRecordLit from only values, silently dropping record field-name facts needed downstream.

briansrls · 2026-05-20T00:17:19Z

Verified on current head 8bef6ef: this PR still imports v2_5.std.node and v2_5.std.stage_types, and it intentionally does not add those std modules. That boundary is a real cross-PR dependency, but adding Tier 0/Tier 1 substrate and stage-type declarations here would take over sibling-owned fork work rather than fixing infer-stage code. The infer-stage-local blockers from the same review have been addressed in pushed commits: diagnostic-preserving InferredExprNode, binder forms fail-closed behind a binder-scope fold gate, record literals carry field/value entries, and infer-local coproduct carriers have a first-class closure receipt. Remaining resolution for this specific module-boundary point is to land/rebase onto the Tier 0/1 v2.5 std PRs, not to vendor their declarations into PR #3425. — sent from swift-swift-37

briansrls · 2026-05-20T00:39:39Z

Verified on current head bc44ed3: infer_for_each is intentionally fail-closed through binder_scope_fold_diagnostic(), and the unresolved binder lane is represented as first-class model state by binder_scope_fold_status: TypeKitGate = AwaitingStageTypes { gate: binder_scope_fold_gate }. I am not adding a prose code comment because this PR is following the no-annotations modeling rule; the typed gate is the receipt a future implementation should replace when Tier 1 exposes the pre-child binder-scope fold hook. — sent from swift-swift-37

Replace local node.dag/diagnostic.dag with cool-bee-832 Tier 0 (2-variant NodeKind, PathStep, Nat, PortLocus). Drop DeclarationKind/CompositeRole imports from stage_types; discrimination stays in phase variants. Co-authored-by: Cursor <cursoragent@cursor.com>

…(~10,341

briansrls · 2026-05-20T02:04:47Z

Closing per operator wrap-up directive 2026-05-20.

briansrls and others added 2 commits May 19, 2026 22:05

briansrls marked this pull request as ready for review May 19, 2026 22:12

briansrls and others added 2 commits May 19, 2026 22:15

refine(v2.5): add EmitStageOut and TargetSource stage port (Tier 1)

46a1a44

Complete the emit pipeline port pair so the header contract matches the typed stage boundaries through emit. Emit implementation remains Tier 2. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls commented May 20, 2026

View reviewed changes

Merge remote-tracking branch 'origin/main' into session/vivid-lynx-807

3f05b7a

briansrls and others added 12 commits May 20, 2026 00:44

WIP: v2 stage rework — 04_INFER_CONSOLIDATED.dag — 13 files into one …

625afdd

…(~10,341

Align v2.5 infer prototype with edge-shaped children

ab0e151

WIP: v2 stage rework — 04_INFER_CONSOLIDATED.dag — 13 files into one …

531215f

…(~10,341

Fail closed v2.5 infer call and match typing

4b31bba

Use value-list helper for list inference

732177d

Fail closed let scope and block diagnostics

bad798d

WIP: v2 stage rework — 04_INFER_CONSOLIDATED.dag — 13 files into one …

6ec7c4c

…(~10,341

Close infer prototype boundary gaps

734b85c

Fail closed binder folds and preserve function diagnostics

be2f591

WIP: v2 stage rework — 04_INFER_CONSOLIDATED.dag — 13 files into one …

5f0994c

…(~10,341

Reconcile v2.5 infer with tier1 stage types

948cd92

briansrls force-pushed the session/swift-swift-37-v25-infer branch from bc44ed3 to 948cd92 Compare May 20, 2026 00:52

Emit distinct infer unavailable markers

de13dc8

briansrls closed this May 20, 2026

Navigation Menu

Repository navigation

Add v2.5 infer stage prototype - #3425

Add v2.5 infer stage prototype#3425
briansrls wants to merge 18 commits into
mainfrom
session/swift-swift-37-v25-infer

briansrls commented May 19, 2026 •

edited

Loading

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 20, 2026

Uh oh!

briansrls May 20, 2026

Uh oh!

briansrls May 20, 2026

Uh oh!

briansrls May 20, 2026

Uh oh!

briansrls May 20, 2026

Uh oh!

briansrls commented May 20, 2026

Uh oh!

briansrls commented May 20, 2026 •

edited

Loading

Uh oh!

briansrls commented May 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Stage Shape

What Dissolved

Rebase Notes

Validation

Honest Yellow List

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 20, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 20, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 20, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 20, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 20, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 20, 2026

Uh oh!

briansrls commented May 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

briansrls commented May 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 19, 2026 •

edited

Loading

briansrls commented May 20, 2026 •

edited

Loading