"Mismatched type" with `#[marker]` + coinductive trait impl

I tried this code:

#![feature(marker_trait_attr)]
#[marker]
pub trait Foo<'a> {}

impl<'a, T: Copy> Foo<'a> for T {}
impl<'a, T: ?Sized> Foo<'a> for &'a mut T {}
impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}

I expected to see this happen: It compiles

Instead, this happened:

Old solver

error[E0283]: type annotations needed: cannot satisfy `T: Foo<'a>`
 --> src/lib.rs:5:31
  |
5 | impl<'a, T: Copy> Foo<'a> for T {}
  |                               ^
  |
note: multiple `impl`s satisfying `T: Foo<'a>` found
 --> src/lib.rs:5:1
  |
5 | impl<'a, T: Copy> Foo<'a> for T {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
6 | impl<'a, T: ?Sized> Foo<'a> for &'a mut T {}
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error[E0283]: type annotations needed: cannot satisfy `&'a mut T: Foo<'a>`
 --> src/lib.rs:6:33
  |
6 | impl<'a, T: ?Sized> Foo<'a> for &'a mut T {}
  |                                 ^^^^^^^^^
  |
note: multiple `impl`s satisfying `&'a mut T: Foo<'a>` found
 --> src/lib.rs:6:1
  |
6 | impl<'a, T: ?Sized> Foo<'a> for &'a mut T {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

error[E0308]: mismatched types
 --> src/lib.rs:7:60
  |
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  |                                                            ^ lifetime mismatch
  |
  = note: expected trait `Foo<'long>`
             found trait `Foo<'short>`
note: the lifetime `'short` as defined here...
 --> src/lib.rs:7:6
  |
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  |      ^^^^^^
note: ...does not necessarily outlive the lifetime `'long` as defined here
 --> src/lib.rs:7:14
  |
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  |              ^^^^^

-Znext-solver

error[E0275]: overflow evaluating the requirement `&'a mut T: Foo<'a>`
 --> src/lib.rs:6:33
  |
6 | impl<'a, T: ?Sized> Foo<'a> for &'a mut T {}
  |                                 ^^^^^^^^^

error[E0308]: mismatched types
  |
  = note: expected lifetime `'long`
             found lifetime `'short`
note: the lifetime `'short` as defined here...
 --> src/lib.rs:7:6
  |
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  |      ^^^^^^
note: ...does not necessarily outlive the lifetime `'long` as defined here
 --> src/lib.rs:7:14
  |
7 | impl<'short, 'long: 'short, T: Foo<'short>> Foo<'long> for T {}
  |              ^^^^^

Meta

rustc --version --verbose:

rustc 1.80.0-nightly (9c9b56879 2024-05-05)
binary: rustc
commit-hash: 9c9b568792ef20d8459c745345dd3e79b7c7fa8c
commit-date: 2024-05-05
host: x86_64-unknown-linux-gnu
release: 1.80.0-nightly
LLVM version: 18.1.4

@rustbot label T-types A-traits A-coinduction F-marker_trait_attr requires-nightly

Start by reproducing the example in src/lib.rs with the reported nightly rustc version, testing both the old solver and -Znext-solver. Read the diagnostics around the #[marker] trait and the three impls. Done means the example compiles without the mismatched-lifetime, ambiguity, or overflow errors.