Ordered-clause fundep semantics: commit coherent instance matches#1035
Open
nanavati wants to merge 12 commits into
Open
Ordered-clause fundep semantics: commit coherent instance matches#1035nanavati wants to merge 12 commits into
nanavati wants to merge 12 commits into
Conversation
Collaborator
Author
|
Full-testsuite result at this PR's head (ff27830), as promised in the description:
No failures attributable to this PR. The same suite run at the next branch stacked on this one (SAT-batching, this head + 2 commits) shows the identical 6 artifacts and nothing else. |
This was referenced Jul 10, 2026
nanavati
added a commit
to nanavati/bsc
that referenced
this pull request
Jul 12, 2026
The typeclass-coherence PRs (B-Lang-org#1035/B-Lang-org#1037) claim T0159-T0161, and whichever series merges second would collide. Take the next free numbers here proactively; the tags are otherwise arbitrary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019cqQdWKp7jr73GHQYnvhiq
krame505
reviewed
Jul 14, 2026
krame505
left a comment
krame505
left a comment
Collaborator
There was a problem hiding this comment.
The idea makes sense here and I don't see any obvious issues with the implementation.
Classic has had "class incoherent C a b" / "class coherent C a b" all
along -- and the Prelude uses both -- but BSV had no way to declare
either: every BSV typeclass got Cclass Nothing and followed the
global -incoherent-instance-matches flag. The annotation matters
where resolution is not forced: an incoherent class permits the
compiler to select an instance even when the choice could still
change under refinement (which catch-all dispatch idioms require),
while a coherent class forbids exactly that, regardless of the flag.
A BSV user writing such a class had only the global flag, which flips
every unannotated class in the compilation.
The syntax mirrors Classic:
typeclass incoherent TwoLevel#(type a, type b);
typeclass coherent Bits#(type a, numeric type n);
The words are soft keywords, matched by string in the position between
"typeclass" and the class name -- exactly like "dependencies" and
"determines" -- so they remain valid identifiers everywhere else and
no existing program can change meaning: typeclass names are uppercase,
so a lowercase word in that position could never have parsed before.
The annotation is threaded through ISTypeclass into the Cclass
coherence field, from which it already propagates cross-package.
Tests pin both directions: an incoherent-annotated BSV class keeps
relational semantics (direct calls select the specific instances, a
call through a (Bits#(a,na), Bits#(b,nb)) helper selects the
catch-all, simulated on both backends), and a coherent-annotated
class rejects the under-determined match even under
-incoherent-instance-matches.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
…cies A functional dependency promises that a class's input positions determine its dependent positions, but instance admission never checked that an instance keeps the promise: a variable in a fundep-determined position of an instance head that is not a function of the input positions -- e.g. instance C#(Bool, v) in a class where the first parameter determines the second -- means the same inputs can be satisfied with many different results. Such an instance is worse than unenforced: its determined position unifies with anything, so any checking premised on the dependency is structurally blind to it, and resolution through it silently depends on what the context demands rather than on the inputs. mkSymTab now checks the liberal coverage condition -- every determined-position variable must be in the closure of the input-position variables under the instance's proviso fundeps, numeric classes included -- and warns (T0160; a warning, not an error, until the ecosystem is surveyed), naming the `incoherent' annotation as the sanctioned escape for classes whose resolution is intentionally relational. Classes declared incoherent are exempt. The warning is emitted once, from the first symbol table of the user-written package (mkSymTabWithWarnings); the pipeline's re-derived symbol tables stay quiet. The standard library census is exactly one violator, StmtTifiable in StmtFSM (instance StmtTifiable Action t: an Action statement fits an FSM of any result type), which is genuinely relational and now declared incoherent, with an XXX for investigating a covering formulation. Bug782_TLM2BRAM's expected output gains the warning: its ToBRAMSeverBETC instance genuinely leaves `n' undetermined, and the test exists to document exactly this pathology. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
The T0160 coverage-condition trio (uncovered instance warns, the incoherent annotation silences by declaring relational intent, proviso-covered stays quiet) and the soft-keyword pin (coherent and incoherent remain valid identifiers). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
BSV reference guide: the typeclass grammar gains the optional coherence annotation (coherent | incoherent) with a description of what it declares, and the instance-declaration section documents the new dependency-coverage expectation and its warning, with incoherent as the sanctioned escape for intentionally relational classes. BH reference guide: the class-declaration grammar now shows the coherent/incoherent annotation Classic has accepted all along (a longstanding documentation gap), and the stale note claiming functional dependencies are not checked by the compiler is replaced with a description of the coverage check and the annotation's meaning. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
Pure mechanical refactor, no behavior change. The solver's plumbing
passed unlabeled tuples whose fields only the call sites could name:
sat, sMany, satMany', satisfy', and reducePredsAggressive all
returned ([VPred], SolvedBinds, Subst); reducePred returned a
five-tuple Maybe ([VPred], SolvedBind, Subst, Maybe Pred, Maybe Id);
byInst a four-tuple with a nested substitution pair. As the
resolution behavior grows more distinctions, positional tuples stop
carrying the design.
- SolveResult { solveNeeded, solveBinds, solveSubst }: the outcome of
a reduction pass -- what could not be discharged, with the
accumulated bindings and substitution.
- Reduction { redGoals, redBind, redSubst, redIncoherent,
redPackage }: a successful predicate reduction, naming in
particular the previously anonymous Maybe Pred: the matched
instance head when the match was information-dependent.
- InstMatch { imGoals, imBind, imInstSubst, imFdSubst, imPackage }:
a successful instance match, flattening the nested substitution
pair.
Consumers in TCheck, CtxRed, and ContextErrors updated to the record
patterns.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
A functional dependency declares that a class's determined positions
are a function of its input positions. Resolution previously
violated this: when an instance's input positions matched but its
determined positions conflicted with the predicate, byInst treated
the instance as a non-match and fell through to a later, less
specific instance -- letting the demanded output choose the instance.
This made instance selection unstable under refinement (a matched
instance could be lost when its output position was refined from
elsewhere) and produced order-dependent acceptance: with a specific
instance TC (Maybe a) 5 and a catch-all TC x 6, the same two-pred
program compiled or failed depending on argument order. It is also
the behavior a long-standing comment in matchTopIsReducible worked
around ("we'd like to return Fails, but to support overlapping
instances which disagree on the fundeps...") and that pipeline.exp
asked about ("the typeclass instances break the stated dependency
requirement; why doesn't BSC catch this?").
Under the new semantics, instances form ordered clauses of a
type-level function keyed on input positions: the first instance
whose inputs match is the selected clause; the fundep improvement
always runs; and if the determined positions cannot unify, the
predicate is unsatisfiable as stated -- the walk stops instead of
falling through. The three-way result has one type, Match a
(NoMatch / Conflict / Match with evidence), and the per-row head
comparison lives in one place (matchFDRow); matchTop consumes it and
now distinguishes input mismatch (NoMatch) from determined-position
conflict (Conflict), and reducePred stops on a conflict. sat's
result records the certificate as a two-valued Commitment
(Committable / Provisional). Given-discharge (lookfor) is
unchanged: a conflict against a given just means that given does not
discharge the predicate.
An `incoherent' class annotation is the user's declaration that the
class's resolution is not a function of its inputs -- the Has_tpl_n
tuple machinery is provably not one (a nested tuple can satisfy the
same input shape with different outputs depending on what is known)
-- so the ordered-clause discipline applies only where coherence is
promised: a determined-position conflict on an instance of an
incoherent-allowed class skips the instance (the previous behavior)
instead of stopping the walk. The exemption has a single statement
(outputFallThroughAllowed). Such a fall-through match is marked
information-dependent: an output-conflict skip is the definition of
output-driven selection -- the demanded output just chose against
that clause -- so the eventual match past it must not be treated as
coherent evidence. The WIncoherentMatch warning stays gated on
unannotated classes, so annotated classes are silent.
sat also now reports whether a partial reduction came from a
committable coherent match (no other instance can ever satisfy the
predicate, and no in-scope given unifies with it); nothing consumes
the certificate yet -- committing changes which predicates
unresolved-context errors name, so it waits for residual-to-root
provenance in the next change.
The hidden flag -legacy-defer-instances restores the previous policy
(output-conflict fall-through, unmarked) for bisection and migration.
The stdlib is unaffected: its catch-all-input instances (ToGet (a) a,
WrapMethod a (Bit n)) are guarded by the incoherent-match deferral --
the walk's accumulator flags a match while any earlier clause still
unifies with the predicate, and sat defers flagged matches for
unannotated classes -- so the catch-all is only ever selected when it
is the unique remaining choice, independent of the removed veto. The one in-tree casualty is the pipeline typeclass
example, whose SeriesPipeline instances deliberately dispatch on the
fundep output (a coerce-wrapper catch-all); Tb1.bsv is now rejected
under the default policy, answering the XXX comment there, and is
kept compiling under -legacy-defer-instances.
New tests: FdOrder pins that both argument orders reject; FdStability
flips from pinning the fall-through acceptance to pinning consistent
rejection, with the legacy behavior pinned under the flag.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
Coherent partial reductions are now committed immediately: when byInst finds a coherent match whose context is not yet satisfiable, sat keeps the instance bindings, substitution, and residual subgoals instead of putting the predicate aside for retry, provided no given (explicit or stacked) pred could still unify with the goal. Together with the ordered-clause fundep semantics already on this branch, instance resolution is now first-match-wins for coherent classes. To keep error messages anchored at user-meaningful predicates, residual subgoals now carry their ancestry: PredWithPositions gains a list of PredAncestor entries (the ancestor Pred plus its positions), minted when byInst reduces a goal to its instance context and when a fundep improvement spawns equality subgoals, unioned when duplicate contexts join in joinCtxs. Ancestors are inert for the solver -- substitution, tv, Eq, and Ord all ignore them -- so resolution behavior is unchanged. Context-reduction and weak-context errors report the root-most non-pre-class ancestor (substituted to current knowledge) instead of the leaf residual, restoring curated diagnostics (e.g. Bits/PrimSelect messages with source-level types) that commitment would otherwise degrade, while purely numeric chains keep the normalized residual. If root-mapping makes every pred implied by the declared context, the reporter falls back to the residuals rather than reporting nothing. The -commit-coherent-matches flag is gone; -legacy-defer-instances now disables both the ordered-clause semantics and commitment as a single escape hatch. Expected outputs for eight tests are regenerated where messages improved (more precise positions, restored curated tags). Reporting shares one statement of the root-then-filter protocol (rootedForReport): map residuals to their user-written roots, drop implied predicates, and if rooting left nothing to report, report the residuals themselves. handleAmbiguousContext deliberately stays out (it reports the residual whose variable is ambiguous, not its root). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
Under ordered-clause fundep semantics, a predicate whose input
positions select an instance with conflicting fundep-determined
positions is unsatisfiable as stated, but it was reported with the
generic "there are no instances of the form" (T0031) -- actively
misleading, since an instance matching the inputs exists.
The conflict cannot be reported eagerly at the solver's conflict
site: a predicate with variable inputs may select an earlier (more
specific) clause after refinement, so a conflict-stop only defers the
predicate. Instead, handleContextReduction's generic fallback now
probes each unresolved residual at reporting time, when the predicate
is maximally refined: findFunDepConflict re-walks the instances with
matchTop -- the reporting probe needs only the match verdict, not
byInst's dictionaries and bindings -- and a conflict recovers the
instantiated head of the selected instance. The new EFunDepConflict
message (T0159; T0158 is left reserved for the transitive-incoherence
diagnostics) shows the predicate and the selected instance side by
side and explains that instances are chosen by the fundep input
positions while the instance's determined types differ from what the
context requires. Curated class-specific messages (Bits, BitExtend,
PrimSelectable, ...) keep precedence; only the generic fallback is
upgraded.
Fail-fast context reduction also becomes conclusive:
matchTopIsReducible's conflict case -- inputs match an instance but
its fundep-determined positions do not -- answered "no conclusion",
with a comment explaining that a conclusive failure was desired but
fall-through made it unsound. The fall-through it protected is gone,
so the case now returns Conflict (through the shared row core,
matchFDRow), and
isReduciblePred treats it as conclusive with the same finality guard
as reducePred's walk: only for coherent classes, and only when no
earlier instance could still capture the predicate. That last
judgment is modal (earlierInstanceMayCapture, shared with reducePred's
incoherence accumulator): whether an earlier instance could capture
the predicate is a question about all refinements -- including
call-site instantiation of the definition's rigid variables -- so
judging it against the current bound set would turn "not yet" into
"never" and license a wrong conclusive verdict naming the less
specific clause. byInstIsReducible answers (Match (), Bool)
directly rather than leaking the instantiated head for the caller to
judge. Incoherent classes and -legacy-defer-instances keep the old
inconclusive answer.
The effect is that fail-fast context reduction (updateContexts at
apply nodes) rejects provably-final fundep conflicts at the use site
with the dedicated T0159 message, instead of letting them decay into
later, vaguer reports: Tb1's conflict was previously reported as a
T0033 ambiguity ("not enough explicit type information"); FdOrder's
second error was a T0030 weak-context at the definition line. Both
now name the selected instance and the exact conflict position.
FdStability, FdOrder, ContextReductionRemoveImplied, and GetPut's
Err1 expected outputs upgrade accordingly.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
Rooted reporting moved several diagnostics off their old code paths; four reporting-quality holes surfaced in the full-suite run and are closed here: - reportedPwp carries the residual's accumulated source positions (deduplicated) onto the reported root: the root may have been created at a positionless site (a generated wrapper signature) while the residual collected real positions on its way through the reduction. - The synthesis-failure report (EBadIfcType) falls back to the predicate's carried positions when the report site has none, so the message points at the offending method instead of "Unknown position". - The weak-context "could also be deduced from" hint reduces self-contained (no givens): a hint with members silently discharged against internally deferred predicates would leave its remaining members referencing variables the message never defines (b1225's Bits#(a_T, a__) was dropped this way). - Fail-fast context reduction defers to the definition-level report when neither the site nor the predicate has a source position: commitment moved some failures from the definition-level check (which knows the definition's name and position) into fail-fast probes in generated wrapper code (which know neither). An irreducible predicate cannot escape unreported; the definition-level check is the terminal backstop. The gh221/gh894/BuildList/BuildVector expected outputs are regenerated for root-based reporting: errors anchor at the offending expression instead of the enclosing binder, dropping the one-entry "implied by" indirection lists. The noinline and bsc.codegen/signature synthesis-failure tests now expect both T0043 reports (the definition-level one naming the module, and the rooted one at the method position, upgraded from a positionless T0031). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
Pins for the semantics and reporting of the preceding changes (testsuite/bsc.typechecker/instances/commit): - LegacyHatch: a clause's determined output conflicting with the demanded type is final (T0159) under ordered clauses and falls through under -legacy-defer-instances. (commit.exp erases the .bo before the fail variant: a stale .bo from the legacy-variant pass would let `bsc -u' skip the recompile, making the suite non-idempotent across runs.) - CommitAncestry: a committed match's unsatisfiable numeric proviso is reported as the instance's concrete obligation at the use site (message pinned), rather than backing the match out into an unreduced context. - SynonymInput: a type synonym at an input position selects the clause its expansion selects. - GivenBlocksCommit: a matched catch-all's unresolvable subgoal must not be stranded; the pred defers whole and the enclosing given discharges it. - IncoherentFallThrough: the annotated class falls through on output conflict with no flag (and still under the legacy hatch). - OutputDetermined / PartialOutputCommit: sole-instance output determination through both the full-solve and the coherent-partial commit paths. - CrossBranch: the catch-all is reachable through the instance index's fallback branch and specific clauses are walked before it. - WeakChainRoot: an open residual is rooted as the user-written predicate, its reduction shown as the dependency. - ChainAncestry: the ground-leaf message shape (root, use site, concrete obligation). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
BSV reference guide: the typeclass grammar gains the optional coherence annotation (coherent | incoherent), and a new "Instance selection and coherence" subsection specifies the resolution rules: overlapping instances are ordered most-specific-first (order between incomparable instances unspecified); for classes with dependencies, selection is driven by the determining parameters alone; the selected instance fixes the dependent parameters, and a conflict with the demanded types is an error rather than a fall-through; commitment waits until no more specific instance could match and no proviso in scope could supply the constraint; incoherent classes opt out (output-driven selection, per-context resolution, coverage warning suppressed); instances are expected to cover the class's dependencies (warning otherwise). BH reference guide: same annotation in the class-declaration grammar, and the stale "functional dependencies are not currently checked" NOTE is replaced with the enforcement rules (use-site selection and conflicts, instance coverage) and the annotation's meaning. User guide: the two hidden migration flags are documented in prose (outside the flag blocks that check-flags.pl compares against -help): -legacy-defer-instances (restore output-driven resolution; code relying on it should declare its classes incoherent instead) and -legacy-inst-index (restore the older instance ordering/indexing). For the PR stack: the grammar and coverage/annotation text belongs to the annotation-and-coverage PR, the selection-semantics subsection and flag prose to the commitment PR; the hunks split along those lines at assembly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YMPXjaiFCjeVJv1TbhYfd5
A committed instance reduction's residual context may become
satisfiable only after later unification or fundep improvement
grounds its variables; the previous flow could report it as a
context-reduction failure while it was merely not-yet-reducible.
The invariant, now enforced at both report sites: no predicate is
reported unsatisfiable without a satisfy attempt under the current
substitution.
- tiExpl: ground leftovers ("uds") get one final "satisfy" under the
completed substitution before reporting; the satisfiable ones stay
deferred to the enclosing binding like any other deferred context.
(A residual can arrive here ground-but-unsolved when a sibling
premise's improvement bound its variables inside the last satisfy
pass.)
- matchTopIsReducible: normalize type functions under the trial
substitution before judging the determined positions, and lift the
judgment into TI to do so. A predicate from a derived instance's
context carries ATF applications of its inputs (e.g. "TilePred
tag") that only reduce once the trial substitution grounds the
inputs; comparing them unreduced misjudged
satisfiable-after-refinement predicates as never reducible, letting
fail-fast context reduction report them prematurely.
The regression tests distill the failing shape: a tag that reaches a
derived DefaultValue instance only through a higher-order type
synonym and slot/pred type functions, with the field assignment
forcing the class output. The two-instance variant pins that the
resolution is structural unification, not reverse instance lookup.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KNk7jKzLHwCdvEv1uzGQYJ
nanavati
force-pushed
the
claude/ordered-clause-commitment
branch
from
July 15, 2026 12:13
bf14c22 to
fe137df
Compare
nanavati
added a commit
to nanavati/bsc
that referenced
this pull request
Jul 15, 2026
The typeclass-coherence PRs (B-Lang-org#1035/B-Lang-org#1037) claim T0159-T0161, and whichever series merges second would collide. Take the next free numbers here proactively; the tags are otherwise arbitrary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019cqQdWKp7jr73GHQYnvhiq
Collaborator
Author
|
Rebased onto current main (941eecf) and force-pushed (fe137df). What the rebase resolved: Re-integrated instance commitment with main's new ATF resolution cache ( |
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
2 participants
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.
A functional dependency declares that a class's determined positions are a function of its input positions. BSC's resolution has historically violated this in two ways: an instance whose inputs matched but whose determined positions conflicted with the predicate was treated as a non-match (falling through to a later, less specific instance — letting the demanded output choose the instance), and even a coherently matched instance was backed out and retried rather than committed. This PR makes the ordered-clause semantics explicit and commits coherent matches by default.
Stacked on #1032 and #1033: the first 8 commits here are those two PRs linearized; the 7 commits from "Give the constraint solver's results proper types" onward are this PR's content, and each is written to be reviewable on its own.
Ordered clauses: outputs never bar a match
The old fall-through made instance selection unstable under refinement (a matched instance could be lost when its output position was refined from elsewhere) and produced order-dependent acceptance: with a specific instance
TC (Maybe a) 5and a catch-allTC x 6, the same two-pred program compiled or failed depending on argument order. It is also the behavior a long-standing comment inmatchTopIsReducibleworked around ("we'd like to return Fails, but to support overlapping instances which disagree on the fundeps...") and thatpipeline.expasked about ("the typeclass instances break the stated dependency requirement; why doesn't BSC catch this?").Under the new semantics, a class's instances form ordered clauses of a type-level function keyed on input positions: the first clause whose inputs match is selected, the fundep improvement always runs, and if the determined positions cannot unify the predicate is unsatisfiable as stated — the walk stops instead of falling through. A class annotated
incoherent(#1033) is the user's declaration that resolution is not a function of its inputs (theHas_tpl_ntuple machinery is provably not one), so such classes keep the fall-through behavior. Given-discharge is unchanged: a conflict against a given just means that given does not discharge the predicate.Commit coherent matches by default
When the selected clause is coherent — no earlier clause could still capture the goal under any refinement of its free variables (the
earlierInstanceMayCapturemodal check) — the solver keeps the reduction's bindings and continues with its subgoals, instead of putting the original predicate aside to retry from scratch on a later pass. Predicate ancestry records what each residual was reduced from, so context errors are reported in terms of the user-written predicate, anchored at the offending expression rather than the enclosing binder.-legacy-defer-instancesis the escape hatch: it disables the ordered-clause semantics and commitment together.Fundep conflicts get a dedicated error (T0159)
A committed clause whose determined positions cannot unify with the demanded type was previously reported with the generic "there are no instances of the form" (T0031) — actively misleading, since an instance matching the inputs exists. The new T0159 shows the predicate and the selected instance side by side and explains that instances are chosen by the fundep input positions; the check fails fast when the conflict is final.
Commit-by-commit
SolveResult,Reduction,InstMatchreplacing the solver's positional tuples. No behavior change.Match a(NoMatch / Conflict / Match),firstMatch, thematchFDRowrow core,SatResult'sCommitmentcertificate, and theearlierInstanceMayCapturemodal check.bsc.codegen/signaturesynthesis-failure tests (two T0043s: the definition-level report naming the module, and the rooted one at the method position, upgraded from a positionless T0031).testsuite/bsc.typechecker/instances/commit: legacy-hatch behavior, commitment ancestry messages, synonym inputs, given/commit interaction, incoherent fall-through, output determination through full and partial commits, cross-branch clause walks, weak-context rooting.Validation
bsc.typecheckersweep (1,246 tests, including the new pins) passes clean at this tip.The stack: #1032 (instance-trie fixes) and #1033 (coherence keywords + coverage warning), independent → #1035 (ordered-clause commitment, this PR) → #1036 (SAT settlement) → #1037 (bound-variable discipline) → #1038 (solved-dictionary pool). Each PR contains the ones below it.
🤖 Generated with Claude Code
https://claude.ai/code/session_018wageSF1tZAS25nrsrbPnZ