Fix typeOf failures with higher-rank types in effect handlers#875
Open
TimWhiting wants to merge 1 commit intokoka-lang:devfrom
Open
Fix typeOf failures with higher-rank types in effect handlers#875TimWhiting wants to merge 1 commit intokoka-lang:devfrom
TimWhiting wants to merge 1 commit intokoka-lang:devfrom
Conversation
There was a problem hiding this comment.
Pull request overview
Fixes a typeOf compilation crash (KindMismatch in subNew) triggered by recursive functions whose higher-rank effect-handler types cause TypeApp argument lists to get out of sync with the final generalized scheme.
Changes:
- Update
inferRecDef2to replace recursive references viareplaceRecCallEx, rewritingTypeApp (Var f) [...]as a unit to keep type-argument count/order aligned with the generalizedVarscheme. - Add a new regression test exercising higher-rank handler types with recursion (
test/cgen/type-of.kk) and its expected output. - Introduce
replaceRecCallExAST traversal helper insrc/Type/Infer.hs.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
src/Type/Infer.hs |
Replaces previous `( |
test/cgen/type-of.kk |
Adds a regression program covering the higher-rank handler/recursive-call scenario. |
test/cgen/type-of.kk.out |
Adds expected output for the new regression test. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Replace the |~> (term substitution) in inferRecDef2 with replaceRecCallEx, which matches TypeApp (Var name) [args] as a unit and replaces the entire construct with the correct type application. This fixes two issues: 1. Forall variable ordering mismatch: when the assumed type's forall order differs from the generalized type's order, the old |~> would replace the Var inside a TypeApp without updating the TypeApp arguments. 2. Forall variable count mismatch: when normalizeX closes effect tail variables (e.g., unifying open effect rows to total), the generalized type has fewer forall variables than the assumed type, but the TypeApp arguments still reflected the assumed type's variable count. Both issues manifested as KindMismatch assertions in typeOf's TypeApp case. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
TimWhiting
force-pushed
the
fix/typeOf-higher-rank
branch
from
0486899 to
7e6197b
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
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.
Summary
Fixes
typeOfcrash (KindMismatchassertion insubNew) when compiling recursive functions with higher-rank effect handler types.Root cause
In
inferRecDef2, the|~>(term substitution) replaces recursiveVarreferences with the final generalized type, but leaves surroundingTypeApparguments unchanged. This causes two issues:Forall variable ordering mismatch: The assumed type's forall variable order (from
createGammas) can differ from the generalized type's order (fromgeneralizeXusingofuv), becauseofuvoccurrence order depends on type structure which changes after unification.Forall variable count mismatch: When
normalizeXcloses effect tail variables (unifying open effect rows tototalfor closed definitions), the generalized type has fewer forall variables than the assumed type, but theTypeApparguments still reflected the assumed type's count.Fix
Replace the
|~>substitution in all threeinferRecDef2cases (TypeLam, divergent, normal) withreplaceRecCallEx, which matchesTypeApp (Var name) [args]as a unit and replaces the entire construct withTypeApp newVar [correct_args], ensuring the TypeApp argument count and order always matches the Var's forall variables.Test plan
stack exec koka -- -e test/cgen/type-of.kkprints "runs" (fresh.kokacache)stack test --fast— 407 examples, 0 new failures (2 pre-existing unicode locale failures)rm -rf .koka && mkdir .kokapasses all testsSupersedes #873. See also #872 for potential future capture-avoiding substitution improvement.
🤖 Generated with Claude Code