Read evidence scopes and backing formals from what earlier stages recorded

[rtfeldman]

Two post-check stages re-derived something a checked module already states, and each derivation disagreed with the statement, so both aborted the compiler on ordinary programs.

roc check aborted with local procedure without a checked evidence scope received use evidence on a local function returning a two-member lambda set — pick = |flag| if flag { |x| x } else { |x| x + 1 } reached through pick(True)(10) is enough. Checking instantiates that definition at its uses and writes a scheme-use record naming the scheme root it instantiated, which is exactly why those uses carry the lambda-set members' dispatch requirements. The table that gives a definition the evidence scope those requirements land in was built instead from the definition's pattern var rank. Rank answers a different question — whether let-generalization ran — and settles at .outermost for a definition whose body defers a dispatch to its caller, so the declaration owned no scope while its uses carried evidence. That table is now built from the recorded scheme uses.

Lowering without specialization aborted with boxy exact descriptor template assigned one backing formal to two actual reps whenever a single descriptor template descends through the same generic nominal at more than one argument set; test/fx/app.roc reaches that through its crypto digests, which is why running it with --specialize=no aborted. A backing shape is written once against its declaration's formals and reached once per instantiation, so each descent binds those formals its own way — already how the sibling walk over the same substitutions in boxy's plan reads them. The template walk instead accumulated every binding into one map for the whole template and asserted that a formal never changed. Bindings now last exactly as long as the descent that made them, and a descriptor is shared only between positions that agree on both the representation and the substitution environment it was emitted under.

Neither failure was reachable from PR CI: the first is only exercised by the Lambda Mono differential harness, which ci_zig.yml gates on inputs.full-run, and the second by a --specialize=no run of an app that no test covered.

[greptile-apps]

Greptile Summary

This PR makes post-check stages consume scheme-use and nominal-backing information recorded by earlier compiler stages instead of re-deriving it.

• Builds local evidence-scope ownership from recorded scheme uses in addition to generalized rank.
• Scopes nominal backing substitutions to individual descriptor descents and keys descriptor reuse by substitution environment.
• Adds eval and CLI regressions for multi-member lambda sets and repeated generic nominal instantiations.

Confidence Score: 5/5

The PR appears safe to merge with no concrete blocking or non-blocking issues identified.

The new evidence-scope lookup and descriptor-substitution scoping are consistent with their downstream consumers, recursive descriptor reuse still terminates, and the boxy regression reaches the intended lowering path.

Important Files Changed

Filename	Overview
src/check/checked_artifact.zig	Extends local evidence-scope discovery to use recorded value and shared-value scheme roots; no actionable defect was established.
src/postcheck/boxy/lower.zig	Introduces descent-scoped nominal substitutions and environment-sensitive descriptor caching while preserving recursive cache termination.
src/cli/test/parallel_cli_runner.zig	Adds an interpreter test whose specialization setting reaches the changed boxy-lowering path.
src/eval/test/eval_regression_repros.zig	Adds a regression covering dispatch through both members of a locally returned lambda set.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Checking records scheme uses] --> B[Checked artifact sealing]
    B --> C[Build local evidence scopes]
    C --> D[Evaluate multi-member lambda set]
    E[Boxy lowering receives nominal substitutions] --> F[Push descent-local bindings]
    F --> G[Key descriptor by representation and environment]
    G --> H[Emit nested descriptors]
    H --> I[Pop and restore outer bindings]

Loading

_{Reviews (1): Last reviewed commit: "Read evidence scopes and backing formals..." | Re-trigger Greptile}