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 <[email protected]>
> ---
>  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 <[email protected]>

> +
> +/// 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
>              }
>          >
>      )
>  }

Reply via email to