checking: backtrack instance-chain subgoals and bound recursive probes#125
Open
bneiswander wants to merge 14 commits into
Open
checking: backtrack instance-chain subgoals and bound recursive probes#125bneiswander wants to merge 14 commits into
bneiswander wants to merge 14 commits into
Conversation
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
WalkthroughAdds a candidate-constraint probe fast-path, checkpoint/restore for canonical and unification state, makes matching state-aware with per-argument unifications and unsatisfiability probing, adds given-elaboration substitution, adjusts row-kind inference for unions, and adds multiple PureScript integration fixtures. ChangesConstraint Solver Enhancement
Integration Test Fixtures
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Poem
🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
🧹 Nitpick comments (1)
compiler-core/checking/src/core/constraint/matching.rs (1)
522-553: 💤 Low valueMinor: remove unnecessary reference on
index.Line 537 creates an unnecessary reference. Since
indexis already&usizefrom the tuple destructure,&indexcreates&&usize. Thecontainsmethod accepts&usizedirectly.♻️ Suggested fix
- if determined.contains(&index) { + if determined.contains(index) {🤖 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 `@compiler-core/checking/src/core/constraint/matching.rs` around lines 522 - 553, In non_determined_unification_ids, the contains check uses &index which produces &&usize; change the call to determined.contains(index) (use index directly) to pass a &usize as expected; update the tuple destructuring reference (index) usage in the loop so determined.contains(index) is called and nothing else needs to change in collect_blocking or other logic.
🤖 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.
Nitpick comments:
In `@compiler-core/checking/src/core/constraint/matching.rs`:
- Around line 522-553: In non_determined_unification_ids, the contains check
uses &index which produces &&usize; change the call to
determined.contains(index) (use index directly) to pass a &usize as expected;
update the tuple destructuring reference (index) usage in the loop so
determined.contains(index) is called and nothing else needs to change in
collect_blocking or other logic.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 10f2a0d8-1463-4034-a360-a62cda10bc5d
⛔ Files ignored due to path filters (10)
tests-integration/fixtures/checking/1772440440_prim_row_open/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778682360_row_fundep_determined_result/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778685420_polykinded_row_fundep_safe_union/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778700540_instance_subgoal_apart_compare/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778701380_pick_max_compare_eval/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778701500_pick_max_record_fold_order/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778701560_eval_given_visible_type_application/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778720160_example_function_fundep/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778723460_pick_max_attachment_codec_binary/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778805900_recursive_instance_chain_candidate_constraint/Main.snapis excluded by!**/*.snap
📒 Files selected for processing (16)
compiler-core/checking/src/core/constraint.rscompiler-core/checking/src/core/constraint/canonical.rscompiler-core/checking/src/core/constraint/compiler/prim_row.rscompiler-core/checking/src/core/constraint/elaborate.rscompiler-core/checking/src/core/constraint/matching.rscompiler-core/checking/src/source/terms/equations.rscompiler-core/checking/src/state.rstests-integration/fixtures/checking/1778682360_row_fundep_determined_result/Main.purstests-integration/fixtures/checking/1778685420_polykinded_row_fundep_safe_union/Main.purstests-integration/fixtures/checking/1778700540_instance_subgoal_apart_compare/Main.purstests-integration/fixtures/checking/1778701380_pick_max_compare_eval/Main.purstests-integration/fixtures/checking/1778701500_pick_max_record_fold_order/Main.purstests-integration/fixtures/checking/1778701560_eval_given_visible_type_application/Main.purstests-integration/fixtures/checking/1778720160_example_function_fundep/Main.purstests-integration/fixtures/checking/1778723460_pick_max_attachment_codec_binary/Main.purstests-integration/fixtures/checking/1778805900_recursive_instance_chain_candidate_constraint/Main.purs
bneiswander
force-pushed
the
pr/checking-instance-chain-backtracking
branch
from
b05b94c to
58bd63c
Compare
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 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 `@compiler-core/checking/src/core/constraint.rs`:
- Around line 280-289: The loop that checks for recursive probes currently scans
all frames in state.candidate_constraint_probes and therefore matches the
just-pushed current probe; change it to skip the current/top frame and only
compare against ancestor probe frames. Update the check around probe_key(state,
context, wanted) so candidate_constraint_probes iteration excludes the
most-recent frame (e.g., iterate all but the last entry or iterate with index
and skip last) when calling probe.iter().any(|active| active == &wanted_probe),
leaving the rest of the logic (residuals.push(wanted); continue 'work;)
unchanged.
In `@compiler-core/checking/src/state.rs`:
- Around line 103-108: The CheckStateCheckpoint currently omits
candidate_constraint_probe_cache so nested speculative probe memoization leaks
across restores; update the CheckStateCheckpoint struct to include a snapshot of
candidate_constraint_probe_cache, capture it when creating a checkpoint
(alongside unifications, canonicals, canonical_errors, error_count in the code
that constructs CheckStateCheckpoint), and restore it when rolling back (in the
code path that applies a CheckStateCheckpoint to the CheckState). Ensure the
same change is applied to the other checkpoint variant referenced (the one
around the other checkpoint creation/restore code block) so probe-cache entries
created during speculative probes are discarded on restore.
🪄 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: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 6d0aa66b-4612-4af3-b611-dd40122effbb
⛔ Files ignored due to path filters (11)
tests-integration/fixtures/checking/1772440380_prim_row_apart/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1772440500_prim_row_generalization/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1772442660_prim_type_error_warn/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1772442720_prim_type_error_fail/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1777298340_top_level_fail_eager/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778700540_instance_subgoal_apart_compare/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778701380_pick_max_compare_eval/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778701500_pick_max_record_fold_order/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778720160_example_function_fundep/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778723460_pick_max_attachment_codec_binary/Main.snapis excluded by!**/*.snaptests-integration/fixtures/checking/1778805900_recursive_instance_chain_candidate_constraint/Main.snapis excluded by!**/*.snap
📒 Files selected for processing (11)
compiler-core/checking/src/core/constraint.rscompiler-core/checking/src/core/constraint/canonical.rscompiler-core/checking/src/core/constraint/elaborate.rscompiler-core/checking/src/core/constraint/matching.rscompiler-core/checking/src/state.rstests-integration/fixtures/checking/1778700540_instance_subgoal_apart_compare/Main.purstests-integration/fixtures/checking/1778701380_pick_max_compare_eval/Main.purstests-integration/fixtures/checking/1778701500_pick_max_record_fold_order/Main.purstests-integration/fixtures/checking/1778720160_example_function_fundep/Main.purstests-integration/fixtures/checking/1778723460_pick_max_attachment_codec_binary/Main.purstests-integration/fixtures/checking/1778805900_recursive_instance_chain_candidate_constraint/Main.purs
✅ Files skipped from review due to trivial changes (2)
- tests-integration/fixtures/checking/1778700540_instance_subgoal_apart_compare/Main.purs
- tests-integration/fixtures/checking/1778701380_pick_max_compare_eval/Main.purs
🚧 Files skipped from review as they are similar to previous changes (4)
- tests-integration/fixtures/checking/1778805900_recursive_instance_chain_candidate_constraint/Main.purs
- compiler-core/checking/src/core/constraint/elaborate.rs
- tests-integration/fixtures/checking/1778723460_pick_max_attachment_codec_binary/Main.purs
- tests-integration/fixtures/checking/1778701500_pick_max_record_fold_order/Main.purs
bneiswander
changed the title
There was a problem hiding this comment.
🧹 Nitpick comments (1)
compiler-core/checking/src/core/constraint.rs (1)
280-291: 💤 Low valueCollapse redundant nested
ifstatements.The outer
!is_empty()check is redundant sincesplit_last()returnsNonefor empty slices. Collapsing improves readability.♻️ Suggested simplification
- if !state.candidate_constraint_probes.is_empty() { - let wanted_probe = probe_key(state, context, wanted); - if let Some((_, ancestors)) = state.candidate_constraint_probes.split_last() { - if ancestors - .iter() - .any(|probe| probe.iter().any(|active| active == &wanted_probe)) - { - residuals.push(wanted); - continue 'work; - } + if let Some((_, ancestors)) = state.candidate_constraint_probes.split_last() { + let wanted_probe = probe_key(state, context, wanted); + if ancestors + .iter() + .any(|probe| probe.iter().any(|active| active == &wanted_probe)) + { + residuals.push(wanted); + continue 'work; } }🤖 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 `@compiler-core/checking/src/core/constraint.rs` around lines 280 - 291, The outer !state.candidate_constraint_probes.is_empty() check is redundant because split_last() already returns None for an empty slice; remove that check and collapse into a single if-let: call probe_key(state, context, wanted) to get wanted_probe, then use if let Some((_, ancestors)) = state.candidate_constraint_probes.split_last() and keep the existing ancestors.iter().any(...) logic to push onto residuals and continue 'work when matched; leave variable names (state, candidate_constraint_probes, probe_key, wanted_probe, ancestors, residuals, and the 'work label) unchanged to make the change minimal and localized.
🤖 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.
Nitpick comments:
In `@compiler-core/checking/src/core/constraint.rs`:
- Around line 280-291: The outer !state.candidate_constraint_probes.is_empty()
check is redundant because split_last() already returns None for an empty slice;
remove that check and collapse into a single if-let: call probe_key(state,
context, wanted) to get wanted_probe, then use if let Some((_, ancestors)) =
state.candidate_constraint_probes.split_last() and keep the existing
ancestors.iter().any(...) logic to push onto residuals and continue 'work when
matched; leave variable names (state, candidate_constraint_probes, probe_key,
wanted_probe, ancestors, residuals, and the 'work label) unchanged to make the
change minimal and localized.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: c11d90b4-f2b0-46c7-bf94-d9b133d0a992
📒 Files selected for processing (2)
compiler-core/checking/src/core/constraint.rscompiler-core/checking/src/state.rs
🚧 Files skipped from review as they are similar to previous changes (1)
- compiler-core/checking/src/state.rs
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 `@compiler-core/checking/src/core/constraint/matching.rs`:
- Around line 487-490: The current branch treats an already-active exact
recursive probe as "not unsatisfiable" (returning Ok(false)), allowing infinite
re-enqueueing; change the logic in matching.rs so that if
state.candidate_constraint_probes.iter().any(|previous| previous == &probe) you
return Ok(true) (treat as unsatisfiable) instead of Ok(false), while leaving the
existing len() >= 2 check behavior intact — update the conditional around
state.candidate_constraint_probes and probe accordingly so exact recursive
probes short-circuit as unsatisfiable.
🪄 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: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: ef3903a6-0ccb-494c-ba83-ebfda271e4bf
📒 Files selected for processing (3)
compiler-core/checking/src/core/constraint.rscompiler-core/checking/src/core/constraint/matching.rstests-package-set/src/lib.rs
There was a problem hiding this comment.
♻️ Duplicate comments (1)
compiler-core/checking/src/core/constraint.rs (1)
35-63:⚠️ Potential issue | 🟠 Major | ⚡ Quick winMake probe keys reflect solved and distinct variables.
Line 107 still folds every
RigidandUnificationinto oneVariableshape and never consultsstatefor solved unifications. That lets structurally different obligations alias, and a key can stay stale after a variable solves, which can misfire the recursive-probe fast path or any probe cache keyed by this shape.Also applies to: 65-132
🤖 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 `@compiler-core/checking/src/core/constraint.rs` around lines 35 - 63, The ProbeTypeKey currently collapses all Rigid and Unification variables into the single Variant Variable (and ProbeKey arguments) which ignores the solver state and solved values; update the probe-key generation logic that constructs ProbeTypeKey/ProbeArgKey/ProbeKey so that it (1) distinguishes rigid vs unification variables (use separate enum variants or include the original SmolStrId for Rigid and a unique id for Unification), and (2) consults the solver/state when encountering a unification variable to fold it into its solved representation (or a canonical representative id) so keys reflect solved values and distinct variables; change any code paths that currently map variables to ProbeTypeKey::Variable to instead produce the new specific variants or resolved forms so caches and the recursive-probe fast-path remain correct.
🧹 Nitpick comments (1)
compiler-core/checking/src/core/constraint.rs (1)
280-286: ⚡ Quick winAvoid allocating a
ProbeKeywhen there are no ancestor probes.Line 280 builds the full structural key for every dequeued wanted, even when
candidate_constraint_probesis empty or only contains the current frame. On this hot path, moveprobe_key(...)inside the ancestor check so the common case stays allocation-free.As per coding guidelines, `compiler-core/**/*.rs`: "Leverage interning and arena allocation for caching; avoid unnecessary allocations in Rust code".♻️ Proposed change
- let wanted_probe = probe_key(state, context, wanted); - if let Some((_, ancestors)) = state.candidate_constraint_probes.split_last() - && ancestors.iter().any(|probe| probe.iter().any(|active| active == &wanted_probe)) - { - residuals.push(wanted); - continue 'work; + if let Some((_, ancestors)) = state.candidate_constraint_probes.split_last() { + if !ancestors.is_empty() { + let wanted_probe = probe_key(state, context, wanted); + if ancestors.iter().any(|probe| probe.iter().any(|active| active == &wanted_probe)) + { + residuals.push(wanted); + continue 'work; + } + } }🤖 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 `@compiler-core/checking/src/core/constraint.rs` around lines 280 - 286, The code currently computes let wanted_probe = probe_key(state, context, wanted) before checking state.candidate_constraint_probes, causing unnecessary ProbeKey allocations; move the call to probe_key(state, context, wanted) inside the branch that runs only when there are ancestor probes (i.e., after the split_last() and ancestors.iter().any(...) check) so that wanted_probe is only constructed when ancestors exist and you actually compare probes; keep the existing residuals.push(wanted) and continue 'work behavior unchanged and ensure you still compare the produced ProbeKey against probe entries when performing the any(...) check.
🤖 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.
Duplicate comments:
In `@compiler-core/checking/src/core/constraint.rs`:
- Around line 35-63: The ProbeTypeKey currently collapses all Rigid and
Unification variables into the single Variant Variable (and ProbeKey arguments)
which ignores the solver state and solved values; update the probe-key
generation logic that constructs ProbeTypeKey/ProbeArgKey/ProbeKey so that it
(1) distinguishes rigid vs unification variables (use separate enum variants or
include the original SmolStrId for Rigid and a unique id for Unification), and
(2) consults the solver/state when encountering a unification variable to fold
it into its solved representation (or a canonical representative id) so keys
reflect solved values and distinct variables; change any code paths that
currently map variables to ProbeTypeKey::Variable to instead produce the new
specific variants or resolved forms so caches and the recursive-probe fast-path
remain correct.
---
Nitpick comments:
In `@compiler-core/checking/src/core/constraint.rs`:
- Around line 280-286: The code currently computes let wanted_probe =
probe_key(state, context, wanted) before checking
state.candidate_constraint_probes, causing unnecessary ProbeKey allocations;
move the call to probe_key(state, context, wanted) inside the branch that runs
only when there are ancestor probes (i.e., after the split_last() and
ancestors.iter().any(...) check) so that wanted_probe is only constructed when
ancestors exist and you actually compare probes; keep the existing
residuals.push(wanted) and continue 'work behavior unchanged and ensure you
still compare the produced ProbeKey against probe entries when performing the
any(...) check.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro Plus
Run ID: 85c83781-2698-495b-b612-0b0d9b7a893c
📒 Files selected for processing (1)
compiler-core/checking/src/core/constraint.rs
Fixes CannotUnify diagnostics when using polykinded row type classes like SafeUnion (forall k. Row k -> Row k -> Row k -> Constraint) with higher-kinded effect rows (Row (Type -> Type)). Two separate issues were addressed: 1. Functional-dependency positions in canonical constraint elaboration (elaborate_given_substitution) were indexing into canonical argument lists without accounting for implicit kind binders. The canonical representation interleaves kind arguments (from forall k.) before type arguments, so position 0 in a class's type parameters actually maps to canonical argument index 1 when a kind binder is present. Fixed in both elaborate.rs (speculative solving) and matching.rs (can_determine_stuck). 2. The Prim.Row.Union compiler solver created residual open-row tails (the | r part of (a :: A | r)) using a hardcoded Row Type kind. For polykinded classes, this caused the kind to be stuck as Row Type even when the constraint involved Row (Type -> Type). Fixed by inferring the correct row element kind from the other arguments and using that to construct the fresh tail variable. Also adds a regression fixture that reproduces the SafeUnion pattern using Eval/RowList/FromRow/ToRow (mimicking Type.Eval.Row.Util.SafeUnion) and verifies it type-checks correctly.
When functional-dependency elaboration produces a substitution for a forall-bound rigid variable, the improved givens now extend the original givens rather than replacing them. This allows visible type applications against those variables in the function body (e.g. Proxy @x) to still resolve against the explicit constraint while the improved forms are available for argument and result substitution. Regression test: eval_given_visible_type_application
…else candidates non_determined_unification_ids was collecting blocking unification variables from ALL non-FD-determined arguments, including those whose match was already known (Match or Apart). This caused false NoInstanceFound errors when an earlier else candidate matched some arguments but had unification variables in already-resolved positions.
…sted subgoals Add candidate subgoal probing with rollback of solver-local state (unifications, canonical cache, canonical errors, diagnostics) so that invalid branches are rejected before commitment instead of leaking stale NoInstanceFound diagnostics. Extend non-final candidate blocking to track per-argument unifications, deferring candidates that would unify unresolved non-determined input positions.
…ot probe cache in checkpoint The recursion check matched the just-pushed current probe against itself, causing false-positive recursion rejection. Use split_last() to only compare against ancestor probe frames. CheckStateCheckpoint omitted candidate_constraint_probe_cache, so speculative probe memoization leaked across checkpoint restores. Include it in checkpoint/restore to discard cache entries on rollback.
…traint probe loop
bneiswander
force-pushed
the
pr/checking-instance-chain-backtracking
branch
from
354b2e1 to
4d0c08f
Compare
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.
checking: backtrack instance-chain subgoals and bound recursive probes
Base branch:
pr/checking-row-fundep-givensReview Order
This PR is stacked on
pr/checking-row-fundep-givensand should be reviewed after that PR.Base branch for review:
pr/checking-row-fundep-givensIt is otherwise independent from
pr/checking-operator-expected-results; both branches can be reviewed after the row-fundep/givens PR is understood.Summary
Motivation
These fixes address several false positives from real PureScript project code involving overlapping/else instances, type-level comparison, row folds, and derived codec-like instance chains. The analyzer was either selecting the wrong else branch too early, keeping an impossible candidate alive, or recursively probing the same candidate shape without a useful bound.
The common concern is candidate probing: it needs transactional state, precise blocking semantics, and recursion protection. Failed nested probes should not leak solver state, known-unsatisfiable subgoals should reject a candidate, and recursive probes need a bound.
Motivating Example
For overlapping instances, a candidate with an impossible nested subgoal should be rejected so the valid else candidate can be considered:
Before this change, the checker could keep an impossible candidate alive, block on the wrong condition, or recursively reprobe the same candidate shape.
Implementation Notes
pr/checking-row-fundep-givensbecause it shares the constraint matching/given infrastructure introduced there.Tests
Added fixtures:
1778700540_instance_subgoal_apart_compare1778701380_pick_max_compare_eval1778701500_pick_max_record_fold_order1778720160_example_function_fundep1778723460_pick_max_attachment_codec_binary1778805900_recursive_instance_chain_candidate_constraintValidation run locally: