Return MatchIndeterminate (not MatchFailed) for mixed-determinacy matches in Eval and Implies modes

[ehildenb]

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. In Eval and Implies modes the matcher previously short-circuited to a decisive MatchFailed in several cases where the two terms could in fact simplify or instantiate to something equivalent, so the deferral never reached the caller. The unifying principle applied here: a decisive MatchFailed is sound only when the mismatch is between rigid shapes or sorts that cannot change under evaluation or instantiation; every other mismatch must defer.

This matters most for function-equation evaluation: handleFunctionEquation routes FailedMatch _ -> continue but IndeterminateMatch{} -> abort. A spurious decisive MatchFailed caused 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. For Implies, the indeterminate verdict lets the existing simplify-LHS / simplify-RHS retry ladder in Pattern.Implies attempt the discharge and report a residual non-match as indeterminate rather than a decisive valid:false. Simplification behaviour is unchanged — handleSimplificationEquation routes both verdicts to continue.

Behavioural changes (each previously a decisive MatchFailed, now addIndeterminate):

• bindVariable: a pattern variable rebinding to two terms that are not both constructor-like (e.g. a domain value and a function application), in all modes — matching what Rewrite already did.
• match1: a FunctionApplication pattern against a concrete structured subject (DomainValue/Injection/KMap/KList/KSet) in Eval — falls through to the shared catch-all.
• match1: an Injection pattern against a builtin collection (KMap/KList/KSet) in Eval, making both directions of this pair indeterminate (the reverse direction already was).
• matchVar: a pattern variable against a subject whose static sort is not a subsort of the variable's, when the subject is a FunctionApplication or Var and the two sorts share a subsort (the subject can still narrow). Sort-disjoint pairs and rigid subjects keep the decisive DifferentSorts failure.
• matchInj: an injection-vs-injection pair with differing sources where a child on the wider-sorted side can narrow (a subject variable child, or a pattern function child). Rigid children at incompatible sorts keep the decisive failure.

Refactor (no behaviour change):

• match1 is inverted to defer-by-default: the table now ends in one generic addIndeterminate fall-through — the always-sound outcome — and every row above it justifies something stronger (\and decomposition, variable binding, same-category descent, or decisive failure). The decisive cross-category rule is a single guarded row over a new isRigidCategory predicate, making the rigidity principle executable rather than commentary. The table shrinks from ~108 rows to 18. bindVariable and matchInj no longer inspect their now-dead MatchType argument.

Tests:

• Matcher-level cases pinning the post-fix contract in MatchEval, MatchImplies, and MatchRewrite, plus a paired function/simplification soundness-regression test in ApplyEquations (test_soundnessGap) showing a high-priority indeterminate match correctly aborts function-equation evaluation rather than falling through to a lower-priority rule.
• A new exhaustive dispatch-class grid test (MatchDispatch) pinning the result class (S/F/I) of all 3 × 9 × 9 = 243 (mode, pattern-constructor, subject-constructor) combinations, so any future match1 change surfaces as a reviewable grid-cell diff.

Validation:

• Full booster unit-test suite passes (979 tests). The behavioural tests were authored to fail against the pre-fix matcher and turn green only with the Match.hs changes applied; the MatchDispatch grid was first pinned on master and shows exactly the eight Eval cells (Injection-vs-collection and FunctionApplication-vs-rigid) that this branch flips from F to I.
• Tested downstream on KMIR and KEVM and saw that it does not cause any proofs to fail or performance regressions.