Re: [PATCH v4 2/7] rust: types: introduce ForLt base trait for CovariantForLt
From: Gary Guo
Date: Tue Jun 30 2026 - 09:55:26 EST
On Fri Jun 26, 2026 at 7:36 PM BST, Danilo Krummrich wrote:
> Add a new ForLt trait as a base for CovariantForLt:
>
> - ForLt (non-unsafe): represents a type generic over a lifetime, with
> no covariance guarantee.
>
> - CovariantForLt (unsafe): becomes a subtrait of ForLt that
> additionally proves the type is covariant over its lifetime
> parameter, providing a safe cast_ref() method.
>
> This split allows non-covariant types (e.g. types behind a Mutex) to
> implement ForLt and participate in DevresLt / registration data patterns
> that use HRTB closures for sound access, without requiring a covariance
> proof that would fail to compile.
>
> Both macros share the UnsafeForLtImpl helper type, distinguished by
> a const generic N: ForLt! emits N = 0 (no covariance proof),
> CovariantForLt! emits N = 1 (with compile-time covariance proof).
>
> Signed-off-by: Danilo Krummrich <dakr@xxxxxxxxxx>
> ---
> rust/kernel/types.rs | 1 +
> rust/kernel/types/for_lt.rs | 72 +++++++++++++++++++++++++++++--------
> rust/macros/for_lt.rs | 68 ++++++++++++++++++++++++-----------
> rust/macros/lib.rs | 19 +++++++++-
> 4 files changed, 123 insertions(+), 37 deletions(-)
>
> diff --git a/rust/kernel/types.rs b/rust/kernel/types.rs
> index cbe6907042d3..c1ed05d1046c 100644
> --- a/rust/kernel/types.rs
> +++ b/rust/kernel/types.rs
> @@ -14,6 +14,7 @@
> #[doc(hidden)]
> pub mod for_lt;
> pub use for_lt::CovariantForLt;
> +pub use for_lt::ForLt;
Import style
>
> /// Used to transfer ownership to and from foreign (non-Rust) languages.
> ///
> diff --git a/rust/macros/for_lt.rs b/rust/macros/for_lt.rs
> index 9487a9352f1c..9270a069cd3a 100644
> --- a/rust/macros/for_lt.rs
> +++ b/rust/macros/for_lt.rs
> @@ -176,8 +176,10 @@ fn prove(&mut self, ty: &'a Type) {
> }
> }
>
> -pub(crate) fn covariant_for_lt(input: HigherRankedType) -> TokenStream {
> - let (ty, lifetime) = match input {
> +/// Resolve the higher-ranked type into a concrete `(ty, lifetime)` pair, expanding elided
> +/// lifetimes as needed. Shared by both `for_lt` and `covariant_for_lt`.
> +fn resolve_hrt(input: HigherRankedType) -> (Type, Lifetime) {
> + match input {
> HigherRankedType::Explicit { lifetime, ty, .. } => (ty, lifetime),
> HigherRankedType::Implicit { ty } => {
> // If there's no explicit `for<'a>` binder, inject a synthetic `'__elided` lifetime
> @@ -188,14 +190,33 @@ pub(crate) fn covariant_for_lt(input: HigherRankedType) -> TokenStream {
> };
> (ty.expand_elided_lifetime(&lifetime), lifetime)
> }
> - };
> + }
> +}
> +
> +/// Produce the `'static`-substituted type for the WF check. Shared by both macros.
> +fn ty_static(ty: &Type, lifetime: &Lifetime) -> Type {
> + ty.replace_lifetime(
> + lifetime,
> + &Lifetime {
> + apostrophe: Span::mixed_site(),
> + ident: format_ident!("static"),
> + },
> + )
> +}
I suppose this code motion is no longer necessary. If they're just part of
`for_lt_inner` then the diff is going to be much smaller.
Regardless the code looks correct to me:
Reviewed-by: Gary Guo <gary@xxxxxxxxxxx>
> +
> +/// Shared implementation for both `ForLt!` and `CovariantForLt!`.
> +///
> +/// Both macros run the prover and emit `ProveWf` structs to check well-formedness for all lifetime
> +/// instances (workaround for <https://github.com/rust-lang/rust/issues/152489>). `CovariantForLt!`
> +/// additionally emits covariance proof functions and sets `N = 1`.
> +fn for_lt_inner(input: HigherRankedType, prove_covariance: bool) -> TokenStream {
> + let (ty, lifetime) = resolve_hrt(input);
>
> let mut prover = Prover(&lifetime, Vec::new());
> prover.prove(&ty);
>
> let mut proof = Vec::new();
>
> - // Emit proofs for every type that requires additional compiler help in proving covariance.
> for (idx, required_proof) in prover.1.into_iter().enumerate() {
> // Insert a proof that the type is well-formed.
> //
> @@ -210,15 +231,16 @@ struct #wf_proof_name<#lifetime>(
> );
> ));
>
> - // Insert a proof that the type is covariant.
> - let cov_proof_name = format_ident!("prove_covariant_{idx}");
> - proof.push(quote!(
> - fn #cov_proof_name<'__short, '__long: '__short>(
> - long: #wf_proof_name<'__long>
> - ) -> #wf_proof_name<'__short> {
> - long
> - }
> - ));
> + if prove_covariance {
> + let cov_proof_name = format_ident!("prove_covariant_{idx}");
> + proof.push(quote!(
> + fn #cov_proof_name<'__short, '__long: '__short>(
> + long: #wf_proof_name<'__long>
> + ) -> #wf_proof_name<'__short> {
> + long
> + }
> + ));
> + }
> }
>
> // Make sure that the type is wellformed when substituting lifetime with `'static`.
> @@ -226,13 +248,9 @@ fn #cov_proof_name<'__short, '__long: '__short>(
> // Currently the Rust compiler doesn't check this, see the above `ProveWf` documentation.
> //
> // We prefer to use this way of proving WF-ness as it can work when generics are involved.
> - let ty_static = ty.replace_lifetime(
> - &lifetime,
> - &Lifetime {
> - apostrophe: Span::mixed_site(),
> - ident: format_ident!("static"),
> - },
> - );
> + let ty_static = ty_static(&ty, &lifetime);
> +
> + let n: usize = prove_covariance.into();
>
> quote!(
> ::kernel::types::for_lt::UnsafeForLtImpl::<
> @@ -241,8 +259,16 @@ fn #cov_proof_name<'__short, '__long: '__short>(
> {
> #(#proof)*
>
> - 0
> + #n
> }
> >
> )
> }