checking: use expected result types in operator chains and lambdas#126
Open
bneiswander wants to merge 9 commits into
Open
checking: use expected result types in operator chains and lambdas#126bneiswander wants to merge 9 commits into
bneiswander wants to merge 9 commits into
Conversation
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
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Plus Run ID: ⛔ Files ignored due to path filters (9)
📒 Files selected for processing (7)
✅ Files skipped from review due to trivial changes (1)
🚧 Files skipped from review as they are similar to previous changes (5)
WalkthroughAdds a Name->Type elaboration routine for given constraints, refactors functional-dependency lookup to use state-aware toolkit queries, applies elaboration during term/lambda checking, optimizes operator result checking and row-union freshening, and adds multiple PureScript integration fixtures exercising these flows. ChangesFunctional Dependency Elaboration and Constraint System
Sequence DiagramsequenceDiagram
participant TermChecker as TermChecker (equations/forms)
participant Elaborate as elaborate_given_substitution
participant Matching as Matching (get_functional_dependencies)
participant Toolkit as toolkit::lookup_file_class
participant Solve as solve_constraints
TermChecker->>Elaborate: request elaboration for given constraints
Elaborate->>Matching: ask for functional dependencies
Matching->>Toolkit: lookup_file_class(state, context, type_id)
Toolkit-->>Matching: class info with functional_dependencies
Matching-->>Elaborate: functional dependency data
Elaborate->>Elaborate: expand determined args, create fresh vars
Elaborate->>Solve: probe-solve temporary constraint set
Solve-->>Elaborate: derived type improvements
Elaborate-->>TermChecker: NameToType substitution
TermChecker->>TermChecker: apply substitution to constraints/args/result
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 |
…in checking Move the expected-result subtype check before operand traversal in traverse_operator_branch so that unification variables in simple operator signatures are solved before operands are checked. This fixes false- positive CannotUnify diagnostics for flipped application (#) pipelines over polymorphic natural transformations. Higher-rank, constrained, and function-shaped expected results are checked after operands to avoid premature skolemisation. Adds regression fixture 1778726580_operator_chain_expected_result.
Regression for spec requirement 'Operator Chain Inference Remains Unchanged': verify that operator chains inferred without an expected type still produce correct inferred types.
…r results When an operator-chain expression applies a constrained polymorphic function (e.g. MonadEffect m => m a) the early expected-result subtyping can unify the constrained result directly with the expected type in a non-elaborating context, emitting a false CannotUnify. Defer the early result check when the operator result is still an unresolved unification variable, letting operand checking contribute type information so wanted constraints can be solved first.
bneiswander
force-pushed
the
pr/checking-operator-expected-results
branch
from
0f7ea9b to
9ebae49
Compare
bneiswander
changed the title
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: use expected result types in operator chains and lambdas
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-instance-chain-backtracking; both branches can be reviewed after the row-fundep/givens PR is understood.Summary
Motivation
The analyzer reported false positives in code accepted by PureScript when expected types came from surrounding operator chains or lambda contexts. The underlying issue was that expected result information was either not propagated far enough, or was applied too early before operator result constraints had resolved.
Expected result information should improve checking when it is simple and known, but should not force a subtyping decision while the operator result is still constrained by unresolved instance solving.
Motivating Example
The checker should use the expected result type from the surrounding signature when checking an operator chain:
It should also avoid rejecting constrained operator results before instance solving has determined the final result type.
Implementation Notes
pr/checking-row-fundep-givensbecause lambda expected-signature checking uses the given-elaboration support introduced there.Tests
Added fixtures:
1778726580_operator_chain_expected_result1778728380_operator_chain_inference_unchanged1778782440_operator_chain_nested_hoist_context1778784780_operator_constrained_result_monad_effectValidation run locally: