This PR adds tests and a benchmark exercising `instantiateMVars` on
metavariable assignment graphs with nested delayed assignments, in
preparation for optimizing the delayed mvar resolution path.
- `tests/elab/instantiateMVarsShadow.lean`: Two test cases for
correctness when the same fvar is bound to different values at different
scope levels (fvar shadowing and late-bind patterns). A buggy cache
could return a stale result from one scope level in another.
- `tests/elab/instantiateMVarsSharing.lean`: Verifies correct resolution
and object sharing on a graph with nested delayed mvars producing `∀ s,
(s = s → (s = s) ∧ (s = s)) ∧ (s = s)`.
- `tests/elab_bench/delayed_assign.lean`: Constructs an O(n²) delayed
mvar graph (n=700) and measures `instantiateMVars` resolution time,
calibrated to ~1s total elaboration.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
---------
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
