Fix for equirecursive equivalence algebra - #4311
Merged
Merged
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
⏭️ Performance benchmarks were skippedPerf benchmarks (CodSpeed) are opt-in on pull requests — they no longer run on every push. They always run automatically after merge to To run them on this PR, do any of the following, then push a commit (or re-run CI):
|
Contributor
📝 WalkthroughWalkthroughThe PR adds μ-canonicalization for recursive aliases. It updates normalization, compiler coherence, recursive cycle validation, overlap checks, runtime documentation, and regression coverage. ChangesRecursive type normalization
Estimated code review effort: 5 (Critical) | ~120 minutes Sequence Diagram(s)sequenceDiagram
participant TypeInput
participant Normalizer
participant MuCanonicalizer
participant CompilerChecks
TypeInput->>Normalizer: parse aliases and constructors
Normalizer->>MuCanonicalizer: canonicalize recursive terms
MuCanonicalizer-->>Normalizer: return canonical type and recursive display
Normalizer->>CompilerChecks: provide normalized implementation subjects
CompilerChecks-->>TypeInput: resolve equivalence, overlap, or coherence
Possibly related PRs
Suggested reviewers: Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 4
🧹 Nitpick comments (5)
baml_language/crates/baml_type/src/normalize/mu.rs (2)
636-704: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winConsider one shared Tarjan helper for both SCC passes.
epsilon_sccsandcyclic_states(Lines 1332-1404) duplicate the same Tarjan state machine. They differ only in the successor set and in what they record per component. Extract one helper that takes a successor function and a per-component callback, then build both results on top of it. This removes about 60 duplicated lines and keeps the two traversals in sync when the edge model changes.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize/mu.rs` around lines 636 - 704, Extract the duplicated Tarjan traversal used by epsilon_sccs and cyclic_states into one shared helper that accepts a successor-producing function and a per-component callback or recording strategy. Preserve each function’s existing edge filtering and component-result behavior while routing both passes through the shared state machine, and remove their separate Tarjan implementations.
894-907: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueWrite through
resolve(s)to keep this arm safe under future changes.Today every
sfromauto.reachable(root)is live when it is processed, because only the currentsis redirected inside the loop. If a later change adds a redirect fromcollapse_complete_enumsorcollapse_complete_bools,auto.states[s].nodewould write into a dead state whileauto.node(s)reads the live one, and the algebra result would be silently dropped. Resolvesonce at the top of the iteration and use that id for the writes.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize/mu.rs` around lines 894 - 907, Update the iteration in the enum-collapse logic around the shown members.len() match to resolve s once at the start of each iteration, then use the resolved state ID for all auto.states writes and related node operations. Preserve the existing redirect and changed behavior while ensuring writes target the live state if collapse_complete_enums or collapse_complete_bools redirects the original ID.baml_language/crates/baml_compiler2_tir/src/unify.rs (1)
1407-1415: 📐 Maintainability & Code Quality | 🔵 Trivial | 💤 Low valueRename this test to say α-equivalent, not distinct.
distinct_recursive_alias_subjects_overlap(line 1407) anddistinct_recursive_alias_subjects_are_disjoint(line 1464) share a prefix but assert opposite outcomes. In this test only the alias names differ; the denoted types are identical, which is why the result isOverlap::Yes. The current name reads as if two different types overlap.♻️ Suggested rename
- fn distinct_recursive_alias_subjects_overlap() { + fn alpha_equivalent_recursive_alias_subjects_overlap() {Update the cross-reference in
distinct_recursive_alias_subjects_are_disjointaccordingly.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_compiler2_tir/src/unify.rs` around lines 1407 - 1415, Rename the test `distinct_recursive_alias_subjects_overlap` to indicate that the aliases are α-equivalent, reflecting that different names denote identical types and produce `Overlap::Yes`; update the corresponding cross-reference in `distinct_recursive_alias_subjects_are_disjoint` while leaving test behavior unchanged.baml_language/crates/baml_type/src/normalize/tests.rs (1)
1521-1523: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winAdd the idempotence assertion here to match the sibling totality tests.
nested_union_member_recursion_renders_totally(line 1483) andmap_value_union_recursion_renders_totally(line 1538) both assertctx.normalize(&n) == n. This test omits it, so a rendering that is equivalent but not stable under a second pass would still pass. The projection-qualifier cut is the case most likely to produce an unstable rendering.♻️ Suggested addition
let n = ctx.normalize(&alias("A")); assert!(equivalent(&alias("A"), &n, &ctx)); + assert_eq!(ctx.normalize(&n), n, "idempotent"); }🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize/tests.rs` around lines 1521 - 1523, Add an idempotence assertion to the test around the existing `let n = ctx.normalize(&alias("A"));` statement, verifying that normalizing `n` again is equivalent to `n`, consistent with `nested_union_member_recursion_renders_totally` and `map_value_union_recursion_renders_totally`.baml_language/crates/baml_type/src/normalize.rs (1)
2444-2512: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winConsider making the
replace_rec_varmatch exhaustive.Line 2510 uses
_ => self.clone()for leaves and non-matching indices. The sibling walks in this file (contains_muat Line 562,has_free_rec_varat Line 2391,has_unguarded_muat Line 2221,resolve_bindersat Line 1395) all list every variant, so the compiler forces an update when a variant gains children.replace_rec_varloses that protection: a new variant that carries aNormalTychild would be cloned without substitution, and the resulting term would keep a staleRecVar. That failure is silent.List the leaf variants explicitly and keep
RecVar(_)as the only non-matching-index arm.♻️ Proposed exhaustive arm
- // Leaves and non-matching indices are untouched. - _ => self.clone(), + // Leaves and non-matching indices are untouched. + NormalTy::RecVar(_) + | NormalTy::Int + | NormalTy::Bigint + | NormalTy::Float + | NormalTy::String + | NormalTy::Bool + | NormalTy::Null + | NormalTy::Uint8Array + | NormalTy::Media(_) + | NormalTy::Void + | NormalTy::RustType + | NormalTy::Type + | NormalTy::Resource + | NormalTy::PromptAst + | NormalTy::Literal(_) + | NormalTy::Enum(_) + | NormalTy::EnumVariant(_, _) + | NormalTy::TypeVar(_) + | NormalTy::OpaqueAlias(_) + | NormalTy::Never + | NormalTy::BuiltinUnknown + | NormalTy::Unknown + | NormalTy::Error => self.clone(),🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize.rs` around lines 2444 - 2512, Make the match in NormalTy::replace_rec_var exhaustive: replace the catch-all arm with explicit arms for every leaf variant, and retain RecVar(_) as the only arm for non-matching recursive-variable indices. Preserve recursive substitution for all variants containing NormalTy children so future variants cannot silently bypass replacement.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@baml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rs`:
- Around line 172-181: In package_coherence_diagnostics, precompute each owned
and dependency impl’s normalized for_ty_pattern and its is_valid_impl_subject
result once using the existing aliases and bounds context. Update impls_conflict
and the overlap loops over own[i+1..] and dep_impls to consume these cached
subjects and validity flags, removing repeated normalize calls while preserving
the current invalid-subject behavior.
In `@baml_language/crates/baml_type/src/normalize.rs`:
- Around line 770-781: Guard the μ-unfolding branches in is_disjoint_from with
recursion tracking or a depth/assumption limit before calling unfold. Ensure
repeated non-contractive μ terms terminate conservatively instead of re-entering
the same unfolding through union decomposition, while preserving normal
structural comparisons for guarded, contractive μ types.
In `@baml_language/crates/baml_type/src/normalize/mu.rs`:
- Around line 1686-1710: Update the Node::Projection handling in the renderer so
a qualifier that is not Node::Interface returns None instead of reaching
unreachable!. Preserve the existing interface rendering path and let the caller
use its normal fallback behavior for unsupported qualifier shapes.
- Around line 846-853: Introduce a per-pass cache for read_back results keyed by
resolved StateId, and update the materialization logic in minimize_and_absorb to
reuse cached values instead of invoking read_back for every member. Clear
rb_cache in every match members.len() arm that mutates a node or adds a
redirect, ensuring subsequent absorption decisions use fresh read-back results.
---
Nitpick comments:
In `@baml_language/crates/baml_compiler2_tir/src/unify.rs`:
- Around line 1407-1415: Rename the test
`distinct_recursive_alias_subjects_overlap` to indicate that the aliases are
α-equivalent, reflecting that different names denote identical types and produce
`Overlap::Yes`; update the corresponding cross-reference in
`distinct_recursive_alias_subjects_are_disjoint` while leaving test behavior
unchanged.
In `@baml_language/crates/baml_type/src/normalize.rs`:
- Around line 2444-2512: Make the match in NormalTy::replace_rec_var exhaustive:
replace the catch-all arm with explicit arms for every leaf variant, and retain
RecVar(_) as the only arm for non-matching recursive-variable indices. Preserve
recursive substitution for all variants containing NormalTy children so future
variants cannot silently bypass replacement.
In `@baml_language/crates/baml_type/src/normalize/mu.rs`:
- Around line 636-704: Extract the duplicated Tarjan traversal used by
epsilon_sccs and cyclic_states into one shared helper that accepts a
successor-producing function and a per-component callback or recording strategy.
Preserve each function’s existing edge filtering and component-result behavior
while routing both passes through the shared state machine, and remove their
separate Tarjan implementations.
- Around line 894-907: Update the iteration in the enum-collapse logic around
the shown members.len() match to resolve s once at the start of each iteration,
then use the resolved state ID for all auto.states writes and related node
operations. Preserve the existing redirect and changed behavior while ensuring
writes target the live state if collapse_complete_enums or
collapse_complete_bools redirects the original ID.
In `@baml_language/crates/baml_type/src/normalize/tests.rs`:
- Around line 1521-1523: Add an idempotence assertion to the test around the
existing `let n = ctx.normalize(&alias("A"));` statement, verifying that
normalizing `n` again is equivalent to `n`, consistent with
`nested_union_member_recursion_renders_totally` and
`map_value_union_recursion_renders_totally`.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 15d582e3-fffd-450e-b739-f13ebf9962ed
⛔ Files ignored due to path filters (8)
baml_language/crates/baml_tests/snapshots/baml_src/json_alias.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/baml_src/json_parse_stringify.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/baml_src/json_to_from_string.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/compiles/__baml_std__/baml_tests__compiles____baml_std____04_5_mir.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/compiles/json_llm_return_type/baml_tests__compiles__json_llm_return_type__04_5_mir.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/compiles/json_map_literal/baml_tests__compiles__json_map_literal__04_5_mir.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/compiles/json_parse_stringify_intrinsics/baml_tests__compiles__json_parse_stringify_intrinsics__04_5_mir.snapis excluded by!**/*.snapbaml_language/crates/baml_tests/snapshots/compiles/json_parse_stringify_intrinsics/baml_tests__compiles__json_parse_stringify_intrinsics__06_codegen.snapis excluded by!**/*.snap
📒 Files selected for processing (10)
baml_language/TYPE_SYSTEM.mdbaml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rsbaml_language/crates/baml_compiler2_tir/src/normalize.rsbaml_language/crates/baml_compiler2_tir/src/type_context.rsbaml_language/crates/baml_compiler2_tir/src/unify.rsbaml_language/crates/baml_tests/baml_src/ns_json_alias/json_alias.bamlbaml_language/crates/baml_type/src/normalize.rsbaml_language/crates/baml_type/src/normalize/mu.rsbaml_language/crates/baml_type/src/normalize/tests.rsbaml_language/crates/bex_vm/src/type_context.rs
Binary size checks passed✅ 7 passed
Generated by |
2kai2kai2
enabled auto-merge
July 31, 2026 20:20
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@baml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rs`:
- Around line 87-95: Update package_coherence_diagnostics to populate bounds
from the current impl’s declared generic parameters, matching
validate_impl_signatures by collecting data.generic_params into TypeVarBoundsMap
instead of using default(). Ensure the resulting GlobalTypeContext passes this
impl-specific map to PreparedImpl::valid_subject and overlap checks.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: c3c76a23-8ecf-468c-bf50-1db0055e1b3e
📒 Files selected for processing (4)
baml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rsbaml_language/crates/baml_type/src/normalize.rsbaml_language/crates/baml_type/src/normalize/mu.rsbaml_language/crates/baml_type/src/normalize/tests.rs
🚧 Files skipped from review as they are similar to previous changes (2)
- baml_language/crates/baml_type/src/normalize/mu.rs
- baml_language/crates/baml_type/src/normalize.rs
2kai2kai2
force-pushed
the
kai/equirecursive-equivalence
branch
from
July 31, 2026 20:36
971b678 to
2147f9a
Compare
Contributor
There was a problem hiding this comment.
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
baml_language/crates/baml_type/src/normalize.rs (1)
1968-1974: 🩺 Stability & Availability | 🟠 Major | ⚡ Quick winMake the projection qualifier reconstruction handle
into_interface()failures.
into_interface()returnsNonewhen a μ display is notTy::Interface, butNormalTy::AssociatedTypeProjection::into_ty()currently treats that case withunreachable!. If reconstruction is allowed to degrade conservatively, use the existingOption<Interface>path; otherwise reject the projection before reaching this arm. Add a regression test for a recursive projection with an interface-shaped binding that produces a non-interface normal qualifier.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize.rs` around lines 1968 - 1974, Update NormalTy::AssociatedTypeProjection::into_ty() to handle into_interface() returning None instead of reaching unreachable!, using the existing Option<Interface> representation or rejecting the projection before this arm. Preserve valid interface reconstruction and add a regression test covering a recursive projection whose interface-shaped binding yields a non-interface normal qualifier.
🧹 Nitpick comments (1)
baml_language/crates/baml_type/src/normalize.rs (1)
2500-2532: 📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick winMake
replace_rec_varexhaustive.Replace the final catch-all arm with explicit leaf variants and a separate
RecVar(_)arm for non-matching indices. A futureNormalTyvariant with recursive children could otherwise bypass substitution and leave stale recursion variables.🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@baml_language/crates/baml_type/src/normalize.rs` around lines 2500 - 2532, Update the match in replace_rec_var to remove the final catch-all arm, enumerate every leaf NormalTy variant explicitly as unchanged, and add a separate RecVar(_) arm for recursion variables whose index does not match. Ensure variants containing recursive children remain explicitly handled so future additions cannot bypass substitution.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Outside diff comments:
In `@baml_language/crates/baml_type/src/normalize.rs`:
- Around line 1968-1974: Update NormalTy::AssociatedTypeProjection::into_ty() to
handle into_interface() returning None instead of reaching unreachable!, using
the existing Option<Interface> representation or rejecting the projection before
this arm. Preserve valid interface reconstruction and add a regression test
covering a recursive projection whose interface-shaped binding yields a
non-interface normal qualifier.
---
Nitpick comments:
In `@baml_language/crates/baml_type/src/normalize.rs`:
- Around line 2500-2532: Update the match in replace_rec_var to remove the final
catch-all arm, enumerate every leaf NormalTy variant explicitly as unchanged,
and add a separate RecVar(_) arm for recursion variables whose index does not
match. Ensure variants containing recursive children remain explicitly handled
so future additions cannot bypass substitution.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Repository UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 0bf8d904-5c60-4046-bd20-a08d9fc475a4
📒 Files selected for processing (4)
baml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rsbaml_language/crates/baml_type/src/normalize.rsbaml_language/crates/baml_type/src/normalize/mu.rsbaml_language/crates/baml_type/src/normalize/tests.rs
🚧 Files skipped from review as they are similar to previous changes (3)
- baml_language/crates/baml_type/src/normalize/tests.rs
- baml_language/crates/baml_compiler2_tir/src/interfaces/coherence.rs
- baml_language/crates/baml_type/src/normalize/mu.rs
codeshaunted
added a commit
that referenced
this pull request
Aug 13, 2026
Brings the branch up to date with canary (146 conflicted files) and ports every TIR-side change onto the hir_ty substrate: - #4311 equirecursive types: canary's mu-automaton (phase-typed NormalTy<Named|Canonical>, de Bruijn binders, canonical_bottom_up) merged with this branch's B-1091 co-inductive assumption threading; the interned entry re-phased through the same pipeline. Same-shape recursive aliases now provably overlap (coherence twin updated). - #4320 tooling surface: hir_ty gains callable::function_signature_ty (a view over function_signature; own generics only; Self resolved for interface-default and free-impl methods), interfaces:: {InterfaceDeclScope, resolve_interface_fields, resolve_interface_required_methods, interfaces_declaring_associated_type}, and package_interface::exported_function (one place pairing the signature query with the effective-throws oracle). baml_surface is re-pointed tir -> hir_ty with its facts.rs contract intact. - #4308 catch-arm interface facts: reachability respects implements in both directions (the semantic contract compiles with zero diagnostics); the arm lowering keeps the modular Interface narrow rather than the closed-world concrete residual. - #4291 intersection bounds, consumption side: GenericParamData conjunction shapes adopted end to end; class constructor sites register one Implements obligation per declared bound conjunct (register_class_bounds, rustc's ADT well-formedness discipline); interface-member lookup pools declarers across the bound conjunction, dedupes by realized identity through requires, and reports E0121/E0122 ambiguity (rustc's MethodError::Ambiguity shape) instead of first-conjunct-wins; a failing blanket-impl bound names the unsatisfied conjunct (BlanketBoundNotSatisfied) instead of a bare mismatch. - #4352 @spec/ai builtins compile and emit on hir_ty. Four pre-existing engine gaps they exposed are fixed: * a bare AnyFunction's unpinned members read as their declared `unknown` defaults at the oracle and in the engine's same-interface unification (BEP-062 lazy default; no eager fill at lowering); * binding a bounded inference var by direct unification now REPLAYS its accumulated VarBounds against the solution (take_solved_class_bounds + replay in the finish fixpoint) instead of dropping them - the map-lambda + future.all shape no longer strands its type args; * an empty container literal flowing into a ground `unknown` demand commits its establishment slots to the top type (the demand is a consuming use); a literal with NO demand keeps the strict uninferrable-container error; * required interface methods (bodyless items under the unified method model) are excluded from the codegen symbol pool. - Coherence: canary's PreparedImpl refactor adopted on Facts::with_bounds - the subject-validity gate now judges the same normalized spelling E0138 judges, memoized per impl. - baml_project CFG dispatch (canary's interface virtual-call resolution in the visualization) re-pointed onto hir_ty's InferenceResult and impls_for_type. - check.rs: the legacy jinja prompt checker is deleted with canary's `client<llm>`/jinja removal; the associated-type declarer walk uses the conjunction-deduping interfaces_declaring_associated_type. - Tests: fixtures migrated off removed builtins (baml.deep_equals -> ops.Equals `==`; a local generic pair fn where the fixture probes inference); snapshots re-blessed for the unified required-method model ([missing] items), canary's builtin/std content, and canonical union order.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements a more principled approach which produces a unique minimal representation of the potentially infinite type tree that would be produced if type aliases were fully unfolded. Unlike the previous version of this, it is also invariant over type alias binder names (so
type A = A[]andtype B = B[]should be identical since their infinitely expanded type trees are equivalent)Summary by CodeRabbit
New Features
jsontypes.Bug Fixes