engine: robust (partial-result) unit inference and checking#618
Conversation
gen_constraints only ever returned Ok, threading a vestigial UnitResult<Units> whose .unwrap() in gen_all_constraints was a latent panic the day any arm became fallible. Constraint generation is total: you can always walk a well-formed AST and emit linear constraints; dimensional inconsistency is detected later, during solving. Change gen_constraints to return Units, deleting the unwrap and the dead Err arms in the arrayed path. This also closes a propagation gap: the None => continue arm (no parsed equation) skipped the rest of the loop body, including the var.units() declared-units constraint. A variable with declared units but no equation -- e.g. the editor's units-typed-but-equation-not-yet-written state -- now still contributes its units to inference so dependents resolve.
RANK returns an ordinal position (a 1-based index), which is a dimensionless quantity -- like a comparison result -- not the units of the array being ranked. Both the inference and checking paths previously inherited the ranked array's units, so a RANK result silently took on e.g. dollars and declaring it dimensionless was a false-positive mismatch. Walk the ranked array for its internal constraints, but return an explicit empty unit map for the RANK result itself.
units_infer::infer returned a single Result, so the first dimensional conflict aborted inference and discarded every unit it had already resolved; db_units then fell back to an empty inferred-units map, blinding the per-variable unit check for the rest of the model (GH #614). infer now returns InferenceResult { resolved, conflicts }: solving continues past a conflict keeping the first binding -- a contradiction is confined to its connected component of the constraint graph, since substitution only flows along shared metavariables, so this can never corrupt an independent component -- and find_constraint_mismatches collects every residual contradiction rather than the first. check_model_units keeps the resolved units (so the rest of the model is still checked) and surfaces conflicts as one umbrella warning rather than one-per-conflict, since a macro-heavy model can produce hundreds of internal contradictions. Keeping the resolved units unmasked a pre-existing leak: a Vensim macro may annotate body variables' units with the formal parameter names (e.g. `~ xfrom` inside RAMP FROM TO) -- a polymorphic unit, not a concrete base unit. Inference recurses into macro instances, so those parameter names leaked as literal units into every instantiation and conflicted with the real argument units (C-LEARN's xfrom/xto storm). ModelStage0/1 gain an is_macro flag and inference now skips declared-units constraints for macro bodies, letting those units be inferred polymorphically from the equation and cross-module parameter bindings (mirroring check_model_units, which already skips macro models). This restores C-LEARN to its documented 14-diagnostic residual.
Context::new accumulated unit-definition errors in a Vec but then threw away the fully-built context whenever that Vec was non-empty, returning Err; project_units_context then fell back to Default::default() -- an empty context with no units. So a single duplicate or contradictory unit declaration anywhere in a project lost ALL alias normalization (yr/year, person/people, model-defined equivalences) project-wide, re-creating a spurious unit-mismatch flood. This is the context-layer parallel of the inference all-or-nothing discard -- the long-standing units.rs:263 TODO, the same shape as GH #614. new/new_with_builtins now return (Context, Vec<...>): the context is always the one built from the valid declarations, with any conflicting declarations reported alongside it. project_units_context keeps the context and accumulates the errors as diagnostics. Callers that expected success take .0; the tests that exercise the conflict path assert on the returned error vec.
Update the engine CLAUDE.md Unit analysis section and the Last-updated note to describe the partial-result contracts: infer -> InferenceResult, Context::new -> (Context, errors), gen_constraints total, RANK dimensionless, and the is_macro polymorphic-units skip.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
simlin/src/simlin-engine/src/units_infer.rs
Lines 902 to 903 in 16d00b6
Check conflicting bindings before applying substitution
When a metavariable is seen a second time with incompatible units, the solver now records a conflict and keeps going, but it substitutes the new candidate units into pending/finalized before verifying whether that binding conflicts with an existing one. In models where the conflicted variable appears in other equations, those downstream constraints are rewritten using the rejected units, so later inferred units can become order-dependent and inconsistent with the documented “keep the first binding” behavior.
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Review: robust (partial-result) unit inference and checkingI reviewed all 17 files. The change is well-structured and the core reasoning is sound: making Findings[P3] Non-deterministic example conflict in the umbrella warning —
Non-blocking notes (no action needed)
Overall correctness: correctNo blocking issues. Existing tests and the C-LEARN/wrld3 guards should hold (the PR reports |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #618 +/- ##
==========================================
- Coverage 82.86% 82.67% -0.20%
==========================================
Files 261 264 +3
Lines 69836 70047 +211
==========================================
+ Hits 57871 57911 +40
- Misses 11965 12136 +171 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Addresses the PR #618 review: unify substituted the newly-derived units into the remaining constraints BEFORE checking whether the metavariable already had a kept binding, so a conflicting re-derivation would have propagated the rejected units -- inconsistent with the documented keep- the-first-binding behavior. Move substitution into the first-resolution branch so only the accepted binding is ever propagated. This is a defensive correctness fix: the conflict arm is currently unreachable -- substitute removes the metavariable from every remaining constraint, so a metavariable is solved at most once and resolved_fvs never already contains it here; a probe across the full lib suite + C-LEARN + wrld3 confirmed zero hits. A genuine over-constraint surfaces instead as a residual concrete contradiction reported by find_constraint_mismatches. No behavior change on any reachable path; the reorder keeps keep-first correct if that invariant ever changes.
|
Addressed in 26dfffc. The ordering critique is correct: Worth noting for context: the conflict arm is currently unreachable. So there's no observable bug to reproduce with a test today, but the reorder is the correct robustness fix — it keeps "keep the first binding" sound if that invariant ever changes (e.g. a future change to the substitution strategy). The follow-up of removing the now-provably-redundant in- |
Code reviewI reviewed the partial-result rework across
[P3] Stale function name in comment —
|
The previous commit established that unify's in-loop conflict detection is unreachable: substitute removes a metavariable from every remaining constraint, so it is solved at most once and resolved_fvs never already contains it at that check. That detection was therefore dead and fully redundant with find_constraint_mismatches, which already reports every over-constraint as a residual concrete contradiction. Remove it for the simpler end state: unify returns (resolved, leftover) -- no conflicts vec, no resolved_sources -- and keeps the first binding via a vacant-entry guard that also never substitutes a rejected re-derivation. infer collects conflicts from find_constraint_mismatches alone (a single source now, so the dedup just drops identical findings). Behavior is unchanged on every reachable path; full suite + C-LEARN green, C-LEARN holds its documented 14-diagnostic residual.
Review: robust (partial-result) unit inference and checkingI reviewed the partial-result refactor across
Findings[P3] Duplicated docstring on Overall correctness verdict: correctNo behavior-affecting bugs found; existing code/tests should not break. The only issue is the minor docstring duplication above. |
A Vensim macro annotates its body variables' units with the formal parameter NAMES (a polymorphic idiom, e.g. `~ xfrom`, `~ xfrom/tstart` inside C-LEARN's RAMP FROM TO). GH #618 contained the resulting `xfrom`/`xto` error storm by skipping declared-units constraints for macro bodies entirely -- but that neither resolved the parameter-named units to the actual arguments nor checked the body's declared signature. Replace the skip with a precise treatment: `gen_all_constraints` lowers each parameter-named unit identifier to that parameter's per-instantiation metavariable (`lower_macro_unit_to_metavars`), keeping genuine base units (`dmnl`) as-is. Because each instantiation already walks the macro body under a unique prefix, the parameter metavar is the same one the module's input binding ties to the actual argument -- so the unit resolves to the argument per instantiation and the storm cannot return, while a genuine declared-vs-equation inconsistency now surfaces as a conflict. The canonical formal-parameter names are threaded onto ModelStage0/ModelStage1 as `macro_params` (from `MacroSpec`, via `model::macro_param_idents`). End users are modelers, not software developers, so a conflict that touches a synthetic instantiation name (`$⁚{var}⁚{n}⁚{func}·…`) is rewritten by `clarify_macro_conflict`/`synthetic_owner_and_func` into a plain-language message naming the function and the variable using it, instead of synthetic-name/`@`-metavariable text. This also de-gibberishes stdlib-module instantiation conflicts. Checking is at instantiation granularity; checking a macro body once at its definition (free metavars, attributing errors to the macro itself) is left as a follow-up.
1 participant
Summary
Makes the unit subsystem partial-result throughout, so one bad declaration or one dimensional conflict never blinds the rest of the model. Closes #614 and the long-standing
units.rs:263TODO (its context-layer parallel), plus two robustness/semantic fixes surfaced along the way.Five commits, each TDD'd with the full pre-commit gate green:
gen_constraintsis total. It only ever returnedOk, so theUnitResult<Units>was vestigial and its.unwrap()ingen_all_constraintswas a latent panic. Now returnsUnits. This also closes a propagation gap: theNone-armcontinueskipped the declared-units constraint for equation-less variables, so a variable with declared units but no equation (the editor's "units typed, equation not yet written" state) never informed inference of its dependents.RANK results are dimensionless. A rank is an ordinal index, not the units of the ranked array; fixed in both inference and checking.
inferreturns partial results (engine: unit inference is all-or-nothing -- one conflict discards all inferred units for the model (parallels units.rs:263 TODO) #614).InferenceResult { resolved, conflicts }. Solving continues past a conflict keeping the first binding -- a contradiction is confined to its connected component of the constraint graph, since substitution only flows along shared metavariables, so this can never corrupt an independent component -- andfind_constraint_mismatchescollects every residual contradiction rather than the first.check_model_unitskeeps the resolved units (so the rest of the model is still checked) and surfaces conflicts as one umbrella warning rather than one-per-conflict.Keeping the resolved units unmasked a pre-existing leak the old all-or-nothing behavior was accidentally suppressing: a Vensim macro can annotate its body variables' units with the formal parameter names (
~ xfrominsideRAMP FROM TO) -- a polymorphic unit, not a concrete base unit. Inference recurses into macro instances, so those names leaked as literal units into every instantiation and conflicted with the real argument units.ModelStage0/ModelStage1gain anis_macroflag and inference now skips declared-units constraints for macro bodies, letting them be inferred polymorphically from the equation and cross-module parameter bindings (mirroringcheck_model_units, which already skips macro models). This restores C-LEARN to its documented 14-diagnostic residual.Context::newreturns partial context. It built the full context then discarded it on any duplicate/conflicting declaration;project_units_contextthen fell back to an empty context, losing project-wide alias normalization (yr/year, person/people) and re-creating a spurious mismatch flood. Now returns(Context, Vec<errors>): the context always holds every valid declaration, with the conflicting ones reported alongside.Docs. Engine
CLAUDE.mdUnit analysis section updated to describe the new contracts.PL framing
Units form a free abelian group, so a unit-constraint set is a linear system over the integers and an inconsistency is a single unsatisfiable row -- it says nothing about the other rows. The fix mirrors how production type systems accumulate errors and keep a partial result rather than aborting at the first failure (rustc error tainting, GHC deferred type errors, the
Validationapplicative); the natural unit of fault isolation here is the connected component of the constraint graph, which the substitution mechanism already respects.Testing
New tests, each written RED then GREEN: partial-results-survive-conflict (+ a second independent conflict still reported), declared-units-without-equation propagation, macro-polymorphic-units (reproduces the C-LEARN
xfromleak in miniature), RANK dimensionless in inference and in checking, and partial-context-on-conflict. Fullcargo test --workspacepasses; the#[ignore]C-LEARN flood guard (tests/clearn_unit_errors.rs) and the wrld3 unit tests pass unchanged, with C-LEARN holding at its documented 14-diagnostic residual (deterministically).