Return MatchIndeterminate (not MatchFailed) for mixed-determinacy matches in Eval and Implies modes#4152
Draft
ehildenb wants to merge 13 commits into
Draft
Return MatchIndeterminate (not MatchFailed) for mixed-determinacy matches in Eval and Implies modes#4152ehildenb wants to merge 13 commits into
ehildenb wants to merge 13 commits into
Conversation
…le-rebind with mixed-determinacy subject When the matcher (in Implies mode) sees a pattern variable bound first to a domain value and then to a function application (or vice versa), it currently returns a decisive MatchFailed VariableConflict, even though the function application could simplify into the domain value (or anything equivalent). The pyk team's recover-mode sweep depends on a sound MatchIndeterminate verdict here so the implies handler's existing simplify-LHS / simplify-RHS retry ladder can attempt the discharge, and a residual non-match can be reported with indeterminate:true rather than as a decisive valid:false. Pin both orderings of the rebind. Tests are expected to fail until Match.bindVariable in Implies mode mirrors Rewrite mode's addIndeterminate. (cherry picked from commit 1700d2d0f5dd89836c86a92f057275ac15756a64)
… mode through addIndeterminate on mixed-determinacy rebind In Match.bindVariable, when a variable is bound a second time and the two terms are not both constructor-like, the matcher previously failed with a decisive VariableConflict in both Eval and Implies modes. That is sound for Eval (the equation evaluator skips to the next priority on MatchFailed) but unsound for Implies: the comment two lines up — "the term in the binding could be equivalent (not necessarily syntactically equal)" — captures exactly why such a decision should be deferred. Routing this case through addIndeterminate lets the existing simplify-LHS / simplify-RHS retry ladder in Pattern.Implies attempt to discharge the equivalence and, on residual failure, mark the implication indeterminate so recover-mode pyk can escalate to a kore-enabled retry. Eval keeps the failWith path pending a separate soundness review of the function-equation evaluator, which currently treats MatchFailed as "skip and try next priority" while it treats MatchIndeterminate as "abort". The comment on the carve-out documents this distinction. Also flip the pre-existing "Matching the same variable in a constructor" test in MatchImplies from MatchFailed to the new MatchIndeterminate expectation, mirroring MatchRewrite's analogous case. (cherry picked from commit 262d49858688eced23a309c7be83489c0a258a09)
…sts for Eval matcher soundness gap
In Eval mode the matcher today returns a decisive MatchFailed when:
- a pattern variable rebinds to two terms that aren't both
constructor-like (Match.hs:825), and
- a function-application pattern is matched against a concrete
structured subject (Injection/KMap/KList/KSet, match1 lines 289,
291, 293, 295).
The "truth" verdict for both shapes is MatchIndeterminate: the function
side could simplify into something equivalent to the constructor-like
side, and the matcher cannot decide that without further work. Because
handleFunctionEquation (ApplyEquations.hs) routes FailedMatch _ to
continue but IndeterminateMatch{} to abort, the current decisive verdict
silently skips a higher-priority equation and commits to a lower-priority
catch-all, violating the priority contract function equations rely on.
This adds six matcher-level tests (MatchEval.hs) and a paired
function/simplification soundness-regression test (ApplyEquations.hs)
that pin the post-fix contract. All seven new tests are expected to fail
until Match.bindVariable and the five Eval-specific match1 lines mirror
the catch-all behaviour. The simplification companion already passes
today and serves to pin that simplifications are unaffected by the
proposed fix.
(cherry picked from commit a61e40fb842f002b1d315b5785b4a61610b332b0)
…through addIndeterminate on mixed-determinacy match
The matcher's job is to return the truth — terms either definitely
cannot match (MatchFailed) or cannot be decided without simplification
(MatchIndeterminate) — and to let the caller decide what to do. Eval
mode previously short-circuited in two places where the terms involved
could in fact simplify to be equivalent:
- Match.bindVariable rebind where the two terms are not both
constructor-like (e.g. a domain value and a function application):
previously failWith $ VariableConflict; now addIndeterminate, like
Rewrite and Implies.
- Five match1 lines that pair a FunctionApplication pattern with a
concrete structured subject (DomainValue, Injection, KMap, KList,
KSet): previously failWith $ DifferentSymbols in Eval mode; the
Eval-specific lines are now dropped so the same catch-all that
handles Rewrite/Implies (addIndeterminate) handles Eval too.
The downstream contract — handleFunctionEquation routes
@IndeterminateMatch{} -> abort@ while @FailedMatch _ -> continue@ — now
correctly stops function-equation iteration at an indeterminate match
instead of silently skipping a higher-priority equation and committing
to a lower-priority catch-all. Function-equation priorities are
"semantically binding" (per the comment on handleFunctionEquation), so
preserving priority order under the matcher's deferred verdict is the
sound thing to do.
handleSimplificationEquation routes both verdicts to @continue@, so
simplification behaviour is unchanged. The simplification companion in
test_soundnessGap pins this.
Also flip the two pre-existing MatchEval tests whose expectations
become stale ("function and something else" and "Matching two
constructor argument to be the same (failing)") from MatchFailed to
the new MatchIndeterminate verdict.
(cherry picked from commit b004b6f5270a57ff620877bbdd783a369c924a24)
The mixed-determinacy rebind comment had grown to a verbose paragraph. Restore master's concise wording, keeping only the one new fact: all modes now defer (a decisive MatchFailed would skip higher-priority equations) rather than re-listing every caller's discharge mechanism. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ehildenb
commented
Jun 11, 2026
…eword test docs to post-fix framing
The test-first commits documented the soundness gap as present ("currently
failing", "under the proposed fix"), and the fix commits never updated the
wording, leaving group names claiming tests fail while they pass. Reword to
describe the pinned contract, mentioning the pre-fix behaviour as history.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ws into a catch-all All non-special-case rows for a FunctionApplication pattern resolve to addIndeterminate in every mode, so replace the per-subject-constructor rows (DomainValue/Injection/KMap/KList/KSet in all modes, ConsApplication and FunctionApplication outside Eval, Var outside Rewrite) with a single trailing catch-all. The mode-specific rows (AndTerm handling, Eval symbol-application descent, Rewrite subject-variable match) stay explicit above it. No behaviour change; addresses review feedback on #4152. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…s-builtin-collection match indeterminate both ways in Eval match1 was asymmetric for Injection paired with a builtin collection (KMap/KList/KSet) under Eval: the collection-pattern/Injection-subject direction returned addIndeterminate while the commuted Injection-pattern/collection-subject direction returned a decisive failWith DifferentSymbols. A spurious MatchFailed silently skips a higher-priority function equation, so the sound verdict is indeterminate in both directions. Add the Eval indeterminate carve-out to the Injection rows; Rewrite/Implies stay decisive. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…: defer matchVar sort mismatch when the subject can narrow A pattern variable matched against a subject whose static sort is not a subsort of the variable's sort decisively failed with DifferentSorts. That is only sound when the subject's sort is exact: a function application may evaluate to a term of a narrower sort (matchInj already defers on exactly this ground), and a subject variable may be instantiated with one. Defer as indeterminate when the subject is a FunctionApplication or Var and the two sorts share a subsort; sort-disjoint pairs and rigid subjects keep the decisive failure. New helper sortsOverlap intersects the reflexive-transitive subsort closures from the SortTable. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…hen a child on the wider-sorted side can narrow The inj-vs-inj fall-through decisively failed with DifferentSorts whenever the sources differed and the special cases (subject function child, pattern variable child) did not apply. That is only sound for rigid children: a subject variable child of the wider sort may be instantiated in the pattern's source sort, and a pattern function child of the wider sort may evaluate into the subject's. Restructure the post-subsort-check dispatch as a single case over both children, deferring those two shapes and keeping the decisive failure for rigid children at incompatible sorts. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…tch-alls, drop dead MatchType params Pure refactor, no behaviour change. The match1 table shrinks from ~108 rows to 46 by: hoisting the per-block \and-subject rows into two generic rows after the \and-pattern block; closing every pattern block with a catch-all (the bulk indeterminate or decisive-fail outcome) so only special rows are explicit; collapsing the Var-pattern block into a single matchVar dispatch; merging the Rewrite/Implies DomainValue-vs-Var rows; and deleting the Eval ConsApplication/FunctionApplication cross-kind descents through matchSymbolAplications, which always resolved to addIndeterminate because constructor and function symbol names never coincide. A header comment states the block order and the rigidity principle governing decisive vs indeterminate outcomes. bindVariable and matchInj no longer inspect their MatchType argument (all modes defer identically since the mixed-determinacy fix), so the dead parameters are removed. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…e generic addIndeterminate fall-through Pure refactor, no behaviour change. Instead of per-pattern blocks each closed by their own catch-all, the table now ends in one generic rule resolving every unhandled pair to addIndeterminate — the always-sound outcome — and every row above it must justify something stronger: \and decomposition, variable binding via matchVar, same-category descent, or decisive failure. The decisive cross-category rule is a single guarded row over a new isRigidCategory predicate (domain values, injections, collections, constructor applications), making the rigidity principle executable rather than commentary. Explicit addIndeterminate rows remain only where they must shadow a more generic stronger row: the Eval \and quirks and the Eval injection-vs-collection carve-out (now two isCollection-guarded rows covering both directions). The subjectVariableMatch marker now uniformly covers all non-Eval rigid-or-function patterns against a variable subject (outcome unchanged: addIndeterminate). 46 rows become 18. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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.
The booster matcher's job is to return the truth — terms either definitely cannot match (
MatchFailed) or cannot be decided without further simplification (MatchIndeterminate) — and leave it to the caller to decide what to do with an indeterminate verdict. InEvalandImpliesmodes the matcher previously short-circuited to a decisiveMatchFailedin cases where the two terms could in fact simplify to something equivalent, so the deferral never reached the caller.Two shapes were affected: a pattern variable rebinding to two terms that are not both constructor-like (e.g. a domain value and a function application), and a
FunctionApplicationpattern matched against a concrete structured subject (DomainValue/Injection/KMap/KList/KSet). Both now route throughaddIndeterminate, matching whatRewritemode already did.This matters most for function-equation evaluation:
handleFunctionEquationroutesFailedMatch _ -> continuebutIndeterminateMatch{} -> abort. The old decisiveMatchFailedcaused the evaluator to silently skip a higher-priority equation and commit to a lower-priority catch-all, violating the priority contract function equations rely on. ForImplies, the indeterminate verdict lets the existing simplify-LHS / simplify-RHS retry ladder inPattern.Impliesattempt the discharge and report a residual non-match asindeterminaterather than a decisivevalid:false. Simplification behaviour is unchanged —handleSimplificationEquationroutes both verdicts tocontinue.Changes:
Match.bindVariable: the mixed-determinacy rebind case now returnsaddIndeterminatefor all match modes instead ofMatchFailed VariableConflictfor everything butRewrite.match1: dropped the fiveEval-specificFunctionApplicationvs structured-subject lines so they fall through to the sharedaddIndeterminatecatch-all already used byRewrite/Implies.MatchEvalandMatchImplies, plus a paired function/simplification soundness-regression test inApplyEquations(test_soundnessGap) that shows a high-priority indeterminate match correctly aborts function-equation evaluation rather than falling through to a lower-priority rule.Validation:
Match.hschanges applied.