Never retry a failed fixed-point machine run naively - #543
Open
LPTK wants to merge 13 commits into
Open
Conversation
A fixed-point definition without a trailing wildcard, `pattern S = P as S | a`,
does not mean "normalize, then match `a`": since `|` is left-biased with
backtracking and `Chain` hands the same alternative to both of its halves, `a`
is tried against every intermediate result, latest first. The machine only ever
produces the normal form, so `makeFixedPointMatchSplit` used to recover the
missing candidates by re-running the whole pattern naively on a failed run.
That duplicated every rewriting step, which is observable as soon as a
transformation has side effects, along three routes:
- machine-then-naive, doubling the work of every failing run;
- for a body-annotated definition, whose own `unapply` embeds machine plus
fallback, the fallback's self-reference re-entered that `unapply`, giving a
quadratic number of contractions;
- a machine run that succeeded only to have the match-site output
sub-pattern fail, since the `Split.End` consequent was filled with the
fallback.
Instead, only ever compile a machine that is a complete implementation of the
pattern, so a failed run simply fails the match. `unmatchedIntermediates`
decides this before any machine is built, from two conditions: the step
pattern and the trailing alternatives cannot match the same value — every
strict intermediate is in the step's domain, so nothing else could have
matched — and, with several recursive alternatives, the steps are mutually
exclusive, without which the naive search is a tree whose other leaves the
machine never visits. Definitions failing either check are rejected with a
warning and compiled naively, which is the option the FIXME in NonCatchAll.mls
asked for; supporting them properly needs the machine to identify the matching
intermediate without materializing it, since plugging the focus back through
the context spine allocates.
The decision rests on a new `Pattern.matchableHeads`, an over-approximation of
the heads covering a pattern, fed to the UCS normalizer's own disjointness
knowledge. Note that a cover is not intersected across a conjunction: covers
are closed downwards, and that does not commute with intersection.
Two further bugs surfaced on the way, both of which could silently change the
meaning of a match:
- `areProvablyDisjoint` reported two occurrences of the same class as
provably disjoint, because `isSubclassOf` is strict;
- `recognizeCycle` discarded `requireProgress`, so a cycle link written
`s as (Next | _)` was compiled as zero-or-more and accepted a scrutinee on
which its very first step could not fire.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR tightens the semantics of @compile fixed-point pattern compilation in HKMC2 UPS: instead of naively retrying a failed machine run (which replays rewrites and can be observably wrong with side effects), it only builds a machine when it is a complete implementation of the pattern, otherwise warning and falling back to the naive translation.
Changes:
- Remove “machine-then-naive retry” for fixed-point machines; reject/diagnose unsupported non-catch-all and overlapping-step shapes up front.
- Add
Pattern.isTotalandPattern.matchableHeadsto conservatively decide when intermediates can/can’t affect results, and reuse UCS disjointness knowledge. - Fix two correctness bugs: class disjointness treating identical classes as disjoint, and rejecting indirect cycles that require at-least-one step (
requireProgress).
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| hkmc2/shared/src/test/mlscript/ups/fixpoint/UnsupportedShapes.mls | Updates golden warning text for unsupported fixed-point compilation. |
| hkmc2/shared/src/test/mlscript/ups/fixpoint/RecursionAlternatives.mls | Adds/updates tests documenting non-catch-all semantics and overlap-triggered fallback. |
| hkmc2/shared/src/test/mlscript/ups/fixpoint/NonCatchAll.mls | Expands explanation and updates golden output to reflect “no naive retry” behavior. |
| hkmc2/shared/src/test/mlscript/ups/fixpoint/IndirectRecursion.mls | Adds coverage for mixed-total cycle links and one-or-more links; updates warning snapshots. |
| hkmc2/shared/src/test/mlscript/ups/fixpoint/FixedPointPatterns.mls | Updates golden warning text for unsupported compilation phrasing. |
| hkmc2/shared/src/main/scala/hkmc2/semantics/ups/SplitCompiler.scala | Drops retry-on-failure embedding logic when calling fixed-point machines at match sites. |
| hkmc2/shared/src/main/scala/hkmc2/semantics/ups/Pattern.scala | Introduces isTotal and matchableHeads to support conservative overlap checks. |
| hkmc2/shared/src/main/scala/hkmc2/semantics/ups/FixedPointCompiler.scala | Removes fallback plumbing; adds overlap/missing-intermediate rejection logic + improved cycle handling. |
| hkmc2/shared/src/main/scala/hkmc2/semantics/ucs/Normalization.scala | Fixes provable disjointness for identical classes; refactors strict vs non-strict subclass checks. |
| hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala | Simplifies memoized fixedPointMachine storage to remove “needsFallback” boolean. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Three follow-ups from the PR review, none of which changes what gets
compiled:
- The rejection diagnostics put every message on one location, taken
from the trailing alternatives — so the step-step overlap one, which
complains about the *recursive* alternatives, pointed at the post
pattern. A rejection always names two patterns that are not adjacent
in the source, and a `Loc` is a single contiguous range, so it is now
reported as several bits: a head bit stating the failure at the
pattern declaration, then one bit per pattern at fault.
Their locations have to come from the source patterns, since the
instantiated ones are rebuilt nodes — most carry no location at all,
and a synonym's is its definition rather than its use. `recognizeShape`
therefore hands the steps down one by one instead of merging them into
a disjunction, which instantiation would flatten beyond recovery, and
`Halves` keeps each source pattern paired with its instantiation. A
step written as `(P1 | P2) as S` is still split, so the checks stay
exactly as conservative as they were.
- The note in `areProvablyDisjoint` still said `isSubclassOf` is
strict, which stopped being true when this PR split it into the
reflexive `isSubclassOf` and `isStrictSubclassOf`; the branch it
annotates uses the latter.
- `makeFixedPointMatchSplit`'s Scaladoc pointed at a
`rejectsOverlappingPost` that never existed.
Golden output: the three rejection warnings gain their extra bits.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The previous commit kept a step written as a disjunction split into its
alternatives, so that the mutual-exclusion check between recursive
alternatives stayed as conservative as before. The conservatism turns out
to be unnecessary, and it rejected definitions the machine implements
exactly.
Check the semantics rather than assume it. With `UnBox = Box(x) => x` and
`Rewrap = Box(x) => Tag(x)`, matching `Box(5)` against
pattern SplitSteps = UnBox as S | Rewrap as S | Tag(_)
pattern JoinedSteps = (UnBox | Rewrap) as S | Tag(_)
gives `Tag(5)` for the first and no match for the second: the chain hands
its continuation to the disjunction as a whole, which commits to the first
of its alternatives that applies and does not reconsider when the rest of
the chain fails. It is still the first *applicable* one, re-chosen at every
iteration — `(UnBox | UnTag) as S | 42` peels `Box(Tag(42))` down to `42`.
So a joined step stays a chain, which is exactly what the machine runs, and
only distinct recursive alternatives branch the search into the tree whose
other leaves the machine never visits. `recognizeShape` therefore hands each
step down as its own list of alternatives and the check compares the steps
group by group; the diagnostic still names the two alternatives in conflict,
one from each group. The trailing-alternatives check is unaffected: a strict
intermediate is one that some step produced, whichever, so it stays flat.
This relaxes rejection only — nothing that compiled before compiles
differently, `entry` being the same flattened disjunction either way — so
neither the absence of backtracking nor the absence of duplicated rewriting
is at stake. All four readings above are pinned in
`RecursionAlternatives.mls`, together with a mixed definition whose joined
step does overlap a later one and is still rejected.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The head bit pointed at the definition, which is not where the warning comes from: a definition is only machine-compiled because some `@compile` asked for it, and for the match-site form that request is somewhere else entirely — `runPeelA`'s warning named neither the line it was reported for nor the file position a reader would look at first. It now points at the pattern under compilation, the same location the generic `unsupported` warning already used, so the two agree. The bits keep pointing at the individual patterns at fault, which is how the definition still gets named. For the body-annotated form the two coincide, the `@compile` being on the declaration itself, so those warnings are unchanged. This also makes repeated warnings distinguishable: a rejected definition is never memoized, so every match site re-attempts the compilation and warns again — previously all of them at the same declaration. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Rejections decided before a machine was built reported only that the
pattern was unsupported, with no reason. Three causes reached that bare
warning, all of them explicable:
- a one-or-more link of a recursion cycle, `step as (Next | rest)`, which
fails outright when its step does not apply while the cycle machine has
no notion of required progress;
- a chain whose tail is an ordinary pattern, so the recursion never comes
back and the definition is a chain rather than a fixed point;
- `@compile` placed on a definition's recursive alternative instead of on
its whole body.
The warning could say nothing because the two recognition steps that decide
these — `classifyRest` and `recognizeCycle` — returned a bare `N`, and by
the time `compile` reported, all it had left were two booleans saying that
*something* was shaped and that nothing had warned yet. Both now return the
reason instead, and `compile` threads it through as `Attempt`, whose four
cases spell out what the old booleans encoded: not fixed-point shaped at
all, rejected with a reason before any build, a build that gave up having
reported itself, or a machine.
`classifyRest` gains reasons for its own three rejections, which were
reachable but untested; `recognizeCycle` names the definition at fault,
which for a cycle is not the one being compiled.
No behaviour change: the same definitions are rejected, and the same ones
compile.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The message said `AtLeastOneA` "cannot match without applying its recursive part at least once". What has to apply at least once is `UnBox`, the pattern *before* the `as` — the recursive part is `AtLeastOneB`, which is not what the check is about. So the sentence stated a condition other than the one being tested, on top of being long. `pattern AtLeastOneA = UnBox as (AtLeastOneB | _)` puts the `| _` inside the `as`, so the wildcard only ever sees a value `UnBox` has already produced and the pattern matches nothing when `UnBox` does not apply. It now says that: "does not match unless its first pattern does". Also check the trailing alternatives before this, so that `P as Next`, which has none at all, reports that instead — it can never match for a more basic reason than this one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Ten of the messages had no test at all. All ten turn out to be reachable, and each now has one, in `UnsupportedShapes.mls`: the shapes turned down before a machine is built, and the shapes the recursive context cannot have. Writing them turned up three things. `isTotal` and `matchableHeads` still read the pattern-lattice units the way round they had before 4b854d7 corrected them, which the merge left stale: they treat `Or(Nil)` as the wildcard when it is `Never`, and `And(Nil)` as `Never` when it is the wildcard. So a definition whose trailing wildcard makes its post pattern total was not seen to be total, and its steps were required to be mutually exclusive for nothing — `PeelOrRewrapTotal` was rejected though no intermediate is ever consulted. Dually a wildcard read as matching nothing was disjoint from everything, so `WildStep`'s step, which matches every value, overlapped nothing. Both are pinned. The units need no case of their own: the empty conjunction requires nothing of a value and the empty disjunction offers it no alternative, which is what the general cases already compute. Spelling them out separately is how they came to disagree with the encoding, so they are gone rather than corrected. The four rejections of the recursive context take the location of an *instantiated* pattern, whose nodes belong to every definition it was built from. A location has to sit in a single origin and every block is its own, so these crash on an assertion unless the definitions share a block. The tests keep them in one block, and the crash is pinned with `:fixme`. It predates this branch: `classify` is untouched here. Co-Authored-By: Claude Opus 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
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.
PR created by Claude Opus 2.8 under my directions.
A fixed-point definition without a trailing wildcard,
pattern S = P as S | a, does not mean "normalize, then matcha": since|is left-biased with backtracking andChainhands the same alternative to both of its halves,ais tried against every intermediate result, latest first. The machine only ever produces the normal form, somakeFixedPointMatchSplitused to recover the missing candidates by re-running the whole pattern naively on a failed run.That duplicated every rewriting step, which is observable as soon as a transformation has side effects, along three routes:
unapplyembeds machine plus fallback, the fallback's self-reference re-entered thatunapply, giving a quadratic number of contractions;Split.Endconsequent was filled with the fallback.Instead, only ever compile a machine that is a complete implementation of the pattern, so a failed run simply fails the match.
unmatchedIntermediatesdecides this before any machine is built, from two conditions: the step pattern and the trailing alternatives cannot match the same value — every strict intermediate is in the step's domain, so nothing else could have matched — and, with several recursive alternatives, the steps are mutually exclusive, without which the naive search is a tree whose other leaves the machine never visits. Definitions failing either check are rejected with a warning and compiled naively, which is the option the FIXME in NonCatchAll.mls asked for; supporting them properly needs the machine to identify the matching intermediate without materializing it, since plugging the focus back through the context spine allocates.The decision rests on a new
Pattern.matchableHeads, an over-approximation of the heads covering a pattern, fed to the UCS normalizer's own disjointness knowledge. Note that a cover is not intersected across a conjunction: covers are closed downwards, and that does not commute with intersection.Two further bugs surfaced on the way, both of which could silently change the meaning of a match:
areProvablyDisjointreported two occurrences of the same class as provably disjoint, becauseisSubclassOfis strict;recognizeCyclediscardedrequireProgress, so a cycle link writtens as (Next | _)was compiled as zero-or-more and accepted a scrutinee on which its very first step could not fire.