2026
Verus — ghost/tracked macro fix
A merged contribution to the Verus compiler: type arguments were being dropped during Ghost/Tracked macro expansion, so a turbofish written in the source vanished before the type checker saw it.
Upstream, in the verifier itself
2026-03-10
Merged upstream
6
Generated paths fixed
Detail
- `Ghost::<int>(1)` failed with `error[E0283]: type annotations needed` — an odd thing to be told when the annotation is right there in the source. Verus issue #2013, filed by a core developer.
- The fix extracts the path arguments off the call before the visitor rewrites the expression, then interpolates the turbofish into all six generated code paths — Ghost and Tracked, each across erase, spec, and exec.
- Three tests, including a negative one: `Ghost::<bool>(1int)` must still be rejected.
- Merged into `verus-lang/verus` on 10 March 2026. Not a system verified in Verus — a patch to the machinery that erases ghost code, which is a different and smaller claim.
Stack
Underlined entries link to the writing on that topic.