On Fri May 22, 2026 at 1:34 AM CEST, Danilo Krummrich wrote:
> [ Handle macro_rules! invocations in the ForLt! proc macro's covariance
> and WF checks.
>
> Proc macros cannot expand macro_rules! invocations, so the
> syn::Visit-based has_lifetime() and replace_lifetime() helpers cannot
> inspect types hidden behind macro calls. This caused the covariance
> proof to be silently skipped and lifetime substitution to fail for
> such types.
>
> Add an explicit Type::Macro arm to Prover::prove to conservatively
> require a compiler-assisted covariance proof. Detect macro-containing
> types with has_macro() and use a WithLt trait projection for lifetime
> substitution instead of AST-level replacement. - Danilo ]
I was made aware by Gary that WFness is not actually being checked, which is why
the static expansion was needed in the first place.
Thus macros will remain unsupported (even covariant macros are rejected), yet we
can improve the error message by adding the following diff on top of the
previous v3 patch.
diff --git a/rust/macros/for_lt.rs b/rust/macros/for_lt.rs
index df2027789713..75d0ce450bf0 100644
--- a/rust/macros/for_lt.rs
+++ b/rust/macros/for_lt.rs
@@ -107,6 +107,12 @@ fn visit_lifetime(&mut self, lifetime: &Lifetime) {
self.1 = true;
}
}
+
+ // Macro invocations are opaque; conservatively assume they may
+ // reference the lifetime.
+ fn visit_macro(&mut self, _: &syn::Macro) {
+ self.1 = true;
+ }
}
let mut visitor = HasLifetime(lt, false);
