Skip to content

fix(units): inherit units through alias chains, source-render if/match/struct diagnostics, drop stale report.json on type errors - #542

Merged
AkiraTamai merged 2 commits into
developfrom
devin/1788356041-units-alias-chain
Sep 2, 2026
Merged

fix(units): inherit units through alias chains, source-render if/match/struct diagnostics, drop stale report.json on type errors#542
AkiraTamai merged 2 commits into
developfrom
devin/1788356041-units-alias-chain

Conversation

@AkiraTamai

Copy link
Copy Markdown
Collaborator

Summary

Follow-up to #539/#541 for three issues found while testing the units checker via the CLI on develop.

1. Alias-of-alias lost its unit (bug). type Money = Usd; had unit: None, so m: Money + j: Jpy verified. New ModuleEnv::unit_of_type(name) walks _base_type until a unit tag is found (cycle-safe); units.rs and the proof cache both use it.

// module_env.rs
pub fn unit_of_type(&self, name: &str) -> Option<&String>  // Money -> Usd -> Some("USD")

The cache hash now includes name:base=unit for every alias that resolves to a unit, so re-pointing type B = A; to type B = J; invalidates cached results (unitless modules hash exactly as before).

2. AST Debug in unit diagnostics (cosmetic). expr_to_source_string fell back to {:?} for IfThenElse / Match / StructInit, producing IfThenElse { cond: Variable("c"), then_branch: Block([...]) ... }. Added source rendering: if c { A { amt: u } } else { B { amt: j } }, match x { Some(v) => { v }, _ => { 0 } }.

3. --json polluted by stale report.json (existing behavior, but unit errors make it easy to hit). Atoms rejected before Z3 (type/unit errors) never write report.json; the --json path then reads whatever file was left by a previous run and emits its top-level fields ("status":"success", "atom":..., "span":...) next to exit code 1. Fix: cmd_verify removes <report-dir>/report.json at start, so only this run's output can be read back. Also, type errors were tagged z3_sat (via z3_result_from_error_message(..).unwrap_or("sat")) although Z3 never ran; they are now tagged z3_skipped, same as unverifiable atoms. No Z3 encoding, MIR, or runtime changes.

Tests: tests/test_units.rs gains alias-chain positive/negative fixtures, an alias re-pointing cache-invalidation case, source-rendering assertions on the branch-mismatch fixtures, and a stale-report.json --json regression. docs/LANGUAGE.md notes alias inheritance.

Link to Devin session: https://app.devin.ai/sessions/2eef5afcd69d4e0ab19ada3b22d5cf7e
Open in Devin Desktop: https://app.devin.ai/desktop/session/2eef5afcd69d4e0ab19ada3b22d5cf7e?variant=devin
Requested by: @AkiraTamai

…t exprs in diagnostics, drop stale report.json on type errors

Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
@devin-ai-integration

Copy link
Copy Markdown
Contributor

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

  • Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
  • Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

  • Disable automatic comment, CI, and merge conflict monitoring

@AkiraTamai
AkiraTamai marked this pull request as ready for review September 2, 2026 13:58

@devin-ai-integration devin-ai-integration Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Devin Review found 4 potential issues.

Devin Review

Comment thread src/commands/verify.rs Outdated
Comment thread mumei-core/src/resolver/cache.rs
Comment thread src/commands/verify.rs
Comment thread mumei-core/src/verification/support/call_graph.rs
…r cannot surface an earlier atom's report

Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
@AkiraTamai
AkiraTamai merged commit 024921f into develop Sep 2, 2026
5 checks passed
@AkiraTamai
AkiraTamai deleted the devin/1788356041-units-alias-chain branch September 2, 2026 14:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant