Precise captures in ITIAT are not refining

[QuineDot]

I tried this code:

#![feature(impl_trait_in_assoc_type)]

pub trait Trait {}
impl<T> Trait for T {}
pub struct Context;

pub trait Component {
    type Creation<'a>: Trait;
    fn create(self, ctx: &Context) -> Self::Creation<'_>;
}

impl Component for String {
    // `+ use<>` is allowed without triggering this lint
    // #[allow(refining_impl_trait)]
    type Creation<'a> = impl Trait + use<>;
    fn create(self, _ctx: &Context) -> Self::Creation<'_> {
        self
    }
}

impl Component for &str {
    // `+ use<>` correctly rejects the defining use here
    type Creation<'a> = impl Trait /*+ use<>*/;
    fn create(self, ctx: &Context) -> Self::Creation<'_> {
        ctx
    }
}

// This should accept `T = String` and not `T = &str`, but it
// accepts neither
pub fn component<T, R>(prop: T)
where
    T: for<'a> Component<Creation<'a> = R>,
{
    move |ctx: &Context| prop.create(ctx);
}

fn main() {
    let but_does_it_work = component(String::new());
    // let but_does_it_work = component("");
}

I expected to see this happen: successful compilation

Instead, this happened:

error[E0308]: mismatched types
  --> src/main.rs:39:28
   |
15 |     type Creation<'a> = impl Trait + use<>;
   |                         ------------------
   |                         |
   |                         the expected opaque type
   |                         the found opaque type
...
39 |     let but_does_it_work = component(String::new());
   |                            ^^^^^^^^^^^^^^^^^^^^^^^^ one type is more general than the other
   |
   = note: expected opaque type `<String as Component>::Creation<'a>`
              found opaque type `<String as Component>::Creation<'_>`
   = note: distinct uses of `impl Trait` result in different opaque types
note: the lifetime requirement is introduced here
  --> src/main.rs:33:26
   |
33 |     T: for<'a> Component<Creation<'a> = R>,
   |                          ^^^^^^^^^^^^^^^^

Why the expectation

The analogous refinement works with RPITIT and RTN.

Meta

Playground 1.86.0-nightly (2025-01-04 1891c28)

@rustbot label +F-impl_trait_in_assoc_type +A-traits +T-types +requires-nightly

[compiler-errors]

This is a bit of a technical explanation, so it's probably not much for anyone not on the types team, but has to with the fact that "invariant xform bivariant = invariant" today.

---

// `+ use<>` is allowed without triggering this lint
// #[allow(refining_impl_trait)]

Also, for the record, refining_impl_trait only makes sense for RPITITs. There's nothing to refine here.

[traviscross]

Minimized:

#![feature(impl_trait_in_assoc_type)]

pub trait Tr {
    type Ty<'a>;
    fn f(_: &()) -> Self::Ty<'_>;
}

impl Tr for () {
    type Ty<'a> = impl Sized + use<>;
    fn f(_: &()) -> Self::Ty<'_> {}
}

fn test<U>()
where
    (): for<'a> Tr<Ty<'a> = U>,
{
}

fn main() {
    test();
    //~^ ERROR mismatched types
    //~| NOTE one type is more general than the other
}

The comparative working RTN example, minimized a bit:

#![feature(precise_capturing_in_traits)]
#![feature(return_type_notation)]
#![allow(refining_impl_trait)]

pub trait Tr {
    fn f(_: &()) -> impl Sized;
}

impl Tr for () {
    fn f(_: &()) -> impl Sized + use<> {}
}

trait TyEq {
    type Ty;
}
impl<T> TyEq for T {
    type Ty = T;
}

fn test<U>()
where
    (): Tr<f(..): TyEq<Ty = U>>,
{
}

fn main() {
    test();
}

Note also, tangentially, that this works without error:

#![feature(impl_trait_in_assoc_type)]

pub trait Tr {
    type Ty<'a>;
    fn f(_: &()) -> Self::Ty<'_>;
}

impl Tr for () {
    type Ty<'a> = impl Sized + use<>;
    fn f(_: &()) -> Self::Ty<'_> {}
}

fn test<T>(_: T)
where
    T: for<'a> Tr<Ty<'a>: 'static>,
{
}

fn main() {
    test(());
}

That is, the caller can rely on the use<> in the impl to prove that 'static bound.