Obligatory note: In this case you don't need HRTB, you can just use the same 'a throughout.
impl<'a, T> From<&'a T> for S
where
&'a T: IntoRef,
Self: From<<&'a T as IntoRef>::Ref>,
{
fn from(value: &'a T) -> Self {
<Self as From<<&T as IntoRef>::Ref>>::from(value.into_ref())
}
}
But that still leaves the question on why the original code didn't compile: I think this may just be a limitation of the trait system.
The compiler sometimes can't prove a universal proposition ("for all 'a, P<'a>") even when it could prove any specific instance of the proposition (e.g. P<'static>). I think this is one of those times.
It's not exactly a bug per se, because there will always be things the compiler cannot prove, but it is a current limitation and it could be fixed in theory. Maybe with Chalk?