checking: fix row fundep givens and polykinded row constraints

[bneiswander]

checking: fix row fundep givens and polykinded row constraints

Base branch: main

Review Order

This PR should be reviewed first. It introduces checker infrastructure used by the stacked follow-up PRs for instance-chain backtracking and operator expected-result checking.

Follow-up PRs stacked on this branch:

• pr/checking-instance-chain-backtracking
• pr/checking-operator-expected-results

Summary

• Fix false-positive row functional dependency diagnostics where a row result is determined by an available signature/given but the checker reports an ambiguous or unsolved constraint.
• Correct polykinded row constraint handling in the primitive row solver so kind binders line up when elaborating row constraints.
• Preserve original givens alongside improved givens so later constraint evaluation can still use the user-facing/original evidence when the improved form is not enough.

Motivation

These fixes came from comparing analyzer diagnostics against the PureScript compiler on real project code. The analyzer was reporting errors for row-level constraints that PureScript accepts, especially around function dependencies, row unions, and visible type applications carried by givens.

The common theme is that improving constraints must not lose the information needed to elaborate or solve row givens later. In particular, a constraint that becomes determined through a functional dependency should be elaborated with that determined result before the checker decides it is ambiguous.

Motivating Example

The checker should accept code where the result row is determined by the Union functional dependency, even when the result is not written explicitly by the caller:

class Example (left :: Row Type) (right :: Row Type) (result :: Row Type) | left right -> result

useUnion :: forall left right result. Union left right result => Proxy result
useUnion = Proxy

Before this change, similar real-world constraints could remain ambiguous after improvement even though PureScript could determine the result row.

Implementation Notes

• Adds a given-elaboration path that substitutes determined row results before reporting ambiguity.
• Adjusts primitive row constraint matching/solving to account for polykinded row binders safely.
• Retains original givens next to improved givens in checking state so evaluation paths can inspect both forms.
• Keeps the change scoped to checking internals and integration fixtures; no LSP behavior is changed directly.

Tests

Added fixtures:

• 1778682360_row_fundep_determined_result
• 1778685420_polykinded_row_fundep_safe_union
• 1778701560_eval_given_visible_type_application

Updated existing snapshot:

• 1772440440_prim_row_open

Validation run locally:

cargo check -p checking --tests

[coderabbitai]

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro Plus

Run ID: 08b9a9e5-a294-4e8b-92db-ca7a814e91d8

📥 Commits

Reviewing files that changed from the base of the PR and between b8aa234 and eb0eef8.

⛔ Files ignored due to path filters (5)

• tests-integration/fixtures/checking/1772440380_prim_row_apart/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1772440440_prim_row_open/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1772440500_prim_row_generalization/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1772442660_prim_type_error_warn/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1772442720_prim_type_error_fail/Main.snap is excluded by !**/*.snap

📒 Files selected for processing (5)

• compiler-core/checking/src/core/constraint.rs
• compiler-core/checking/src/core/constraint/compiler/prim_row.rs
• compiler-core/checking/src/core/constraint/elaborate.rs
• compiler-core/checking/src/core/constraint/matching.rs
• compiler-core/checking/src/source/terms/equations.rs

🚧 Files skipped from review as they are similar to previous changes (3)

• compiler-core/checking/src/core/constraint/compiler/prim_row.rs
• compiler-core/checking/src/core/constraint/elaborate.rs
• compiler-core/checking/src/core/constraint.rs

---

Summary

This PR addresses false-positive diagnostics in the PureScript analyser related to row functional dependencies and polykinded row constraints. The changes are scoped to the checking module's core constraint-solving infrastructure and integration into equation checking, with no direct LSP behavior modifications.

Key Changes

New Function: elaborate_given_substitution

• Added in both constraint.rs (public wrapper) and constraint/elaborate.rs (implementation with 76 lines added)
• Takes signature constraints and produces a NameToType substitution through iterative functional dependency resolution
• For each functional dependency, extracts determined argument positions, generates fresh unification variables as replacements, solves derived constraints via instances only (empty given slice prevents circular improvement), then registers non-conflicting improvements
• Uses zonking to materialise unification variables before substitution registration
• Employs conflict tracking to handle cases where determined values contradict existing substitutions

Constraint Matching Refactoring (matching.rs)

• Rewritten get_functional_dependencies to use toolkit::lookup_file_class instead of manually extracting from lowered IR
• Passes &mut CheckState through functional dependency lookups
• Eliminates file ID branching logic previously used for context lookups

Row Kind Inference (prim_row.rs)

• Modified match_union to compute row kind dynamically via infer_row_constraint_kind from input types [left, right, union]
• Replaces previous fixed unification against context.prim.row_type, ensuring polykinded row elements are properly aligned

Equation Checking Integration (equations.rs)

• After obtaining signature, elaborates given substitution and applies it to constraints, arguments, and result
• Preserves original constraints alongside substituted versions to allow fallback to original evidence when improved form is insufficient
• Extends constraints with both substituted and original versions for comprehensive checking

Test Fixtures (3 new)

• 1778682360_row_fundep_determined_result: Validates row functional dependencies determine result rows correctly, with record constructors exercising column-label constraints
• 1778685420_polykinded_row_fundep_safe_union: Demonstrates polykinded row handling with union and nub operations, row composition operators, and effectful computation pipelines
• 1778701560_eval_given_visible_type_application: Tests type-level boolean evaluation through givens with visible type application

Snapshot Update

• 1772440440_prim_row_open: Updated to reflect improved row kind handling

Code Quality

The implementation demonstrates solid engineering practices:

• Proper error handling throughout with QueryResult propagation
• Defensive improvement registration with conflict detection
• Clear separation of concerns (wrapper in public API, implementation in elaborate module)
• Appropriate use of zonking for unification variable materialisation
• Comment explaining the rationale for empty given slice in improvement solving to prevent circular derivations
• All three test fixtures exhibit proper PureScript syntax and appropriate scope

No new TODO or FIXME markers were introduced.

Dependencies & Scope

The PR is part of a sequence (follow-up branches: pr/checking-instance-chain-backtracking, pr/checking-operator-expected-results) and provides foundational checker infrastructure for those changes. All modifications remain within the checking module; no LSP or user-facing behaviour changes are direct consequences of this commit.

Merge Confidence: 4/5

Factors increasing confidence:

• Well-structured implementation with proper error handling and state management
• Comprehensive test fixtures covering target use cases
• Clear preservation of original constraints as fallback mechanism
• Defensive conflict tracking in improvement registration
• Proper handling of unification variables through zonking
• No regressions introduced in existing code patterns

Factors moderating confidence:

• Complex changes across multiple interconnected modules (constraint matching, equation checking, primitive row solving)
• The prim_row kind inference change, whilst straightforward, operates at the type-level and may have subtle implications in edge cases
• Dependency on follow-up PRs for complete validation of the broader infrastructure improvements
• The PR addresses real-world PureScript compiler alignment issues, suggesting this code path may not have been heavily exercised previously

Walkthrough

This PR introduces functional dependency elaboration to the type checker, adding elaborate_given_substitution to refine substitutions from given constraints, refactors matching to use state-aware class lookups, applies the elaborated substitutions in equation checking and row inference, and adds three integration test fixtures exercising these behaviours.

Changes

Functional Dependency Elaboration and Integration

Layer / File(s)	Summary
Core elaboration logic and imports compiler-core/checking/src/core/constraint/elaborate.rs	New elaborate_given_substitution function clones the elaborate_given substitution, iterates canonical given constraints, rewrites FD-determined arguments using fresh unification variables, probes solving the generated "wanted" constraints via super::solve_constraints, zonks fresh replacements, and records non-conflicting improvements into the returned NameToType map.
Public API wrapper compiler-core/checking/src/core/constraint.rs	Expose elaborate_given_substitution as a public helper that canonicalises input TypeId values and delegates to the core implementation in elaborate.rs.
Row inference update compiler-core/checking/src/core/constraint/compiler/prim_row.rs	In match_union, infer a concrete row_kind from the input types and intern context.prim.row applied to that row_kind; use the instantiated row type as the fresh unification target for constructing the output row and Union constraint.
Equation checking integration compiler-core/checking/src/source/terms/equations.rs	Import SubstituteName and, in check_value_equations, compute an elaborated given substitution from the signature constraints and apply it to constraints, arguments, and result (preserving original constraints by extending the substituted list).
Integration test fixtures tests-integration/fixtures/checking/1778682360_row_fundep_determined_result/Main.purs, tests-integration/fixtures/checking/1778685420_polykinded_row_fundep_safe_union/Main.purs, tests-integration/fixtures/checking/1778701560_eval_given_visible_type_application/Main.purs	Three new PureScript test modules exercising FD-driven row projection/stripping, safe union of rows with functional dependencies, and visible-type-application-based boolean evaluation respectively.

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~45 minutes

Poem

A rabbit's eyes sparkle with glee,
Given constraints refined carefully—
Fresh vars, zonks, and subtle ties,
Rows align and types apprise.
Hooray for checks that now agree. 🐰

🚥 Pre-merge checks | ✅ 3

✅ Passed checks (3 passed)

Check name	Status	Explanation
Description check	✅ Passed	The pull request description clearly relates to the changeset, detailing fixes for row functional dependency diagnostics, polykinded row constraint handling, and given elaboration.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

🧹 Nitpick comments (1)

compiler-core/checking/src/core/constraint/elaborate.rs (1)

76-78: 💤 Low value

Consider adding a comment explaining why solve_constraints is called with empty given constraints.

The probe constraint at line 77 is solved without passing the original given constraints. This appears intentional—to derive fundep improvements only from instance chains, avoiding circular reasoning where a given constraint might improve itself. Adding a brief comment (e.g., "only instance-based improvement, not given-based, to prevent circular fundep derivations") would clarify this design choice for future maintainers.

🤖 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/elaborate.rs` around lines 76 -
78, Add a clarifying comment above the call to super::solve_constraints(state,
context, wanted, &[]) explaining that we intentionally pass an empty slice for
the "given" constraints so that probe constraint solving only uses
instance-based improvements (e.g., fundep derivations from instances) and does
not include the original given constraints, preventing circular improvement
where a given might improve itself; reference the call to solve_constraints and
the involved variables state, context, and wanted in the comment so future
maintainers understand the rationale.

🤖 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/elaborate.rs`:
- Around line 76-78: Add a clarifying comment above the call to
super::solve_constraints(state, context, wanted, &[]) explaining that we
intentionally pass an empty slice for the "given" constraints so that probe
constraint solving only uses instance-based improvements (e.g., fundep
derivations from instances) and does not include the original given constraints,
preventing circular improvement where a given might improve itself; reference
the call to solve_constraints and the involved variables state, context, and
wanted in the comment so future maintainers understand the rationale.

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro Plus

Run ID: e63ccd19-426b-4349-af67-16b9c846fa03

📥 Commits

Reviewing files that changed from the base of the PR and between 608aeb5 and e59128a.

⛔ Files ignored due to path filters (4)

• tests-integration/fixtures/checking/1772440440_prim_row_open/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1778682360_row_fundep_determined_result/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1778685420_polykinded_row_fundep_safe_union/Main.snap is excluded by !**/*.snap
• tests-integration/fixtures/checking/1778701560_eval_given_visible_type_application/Main.snap is excluded by !**/*.snap

📒 Files selected for processing (8)

• compiler-core/checking/src/core/constraint.rs
• compiler-core/checking/src/core/constraint/compiler/prim_row.rs
• compiler-core/checking/src/core/constraint/elaborate.rs
• compiler-core/checking/src/core/constraint/matching.rs
• compiler-core/checking/src/source/terms/equations.rs
• tests-integration/fixtures/checking/1778682360_row_fundep_determined_result/Main.purs
• tests-integration/fixtures/checking/1778685420_polykinded_row_fundep_safe_union/Main.purs
• tests-integration/fixtures/checking/1778701560_eval_given_visible_type_application/Main.purs