Some GAT questions (2022-08-23)

Question Set A

https://github.com/rust-lang/rust/pull/96709#issuecomment-1181931456

poses the following example:

The distinction between ensures clauses and where clauses.
Given a trait like this:

trait WidgetFactory {
    type Item<T>: Display
    where
        T: Debug;
}

The Display bound indicates the impl must prove that Item is Display, but the T: Debug bound must be satisfied at the point where the type F::Item<X> is written (i.e., we must show that X: Debug to reference the GAT). This has led to some confusion in the past, and to some extent this is inherent in the syntax.

First, I assume that the above is equivalent to:

type WidgetFactory {
    type Item<T: Debug>: Display;
}

Second: Does the above imply that

type Item<T: Debug>: Display;

has different semantics from

type Item<T: Debug> where Self::Item<T>: Display;

Question Set B

https://github.com/rust-lang/rust/pull/96709#issuecomment-1120050703

has several examples, which pnkfelix has reduced down to the following key observations:

https://play.rust-lang.org/?version=nightly&mode=debug&edition=2021&gist=9e8bf78224a44138c0382d984bc86b3e

#![feature(generic_associated_types)]

pub trait LifetimeGenericConcreteMethod<'a> {
    type Item<'c>;
    //            ~~~~~~~~+~~~~~~
    //                    |
    //            so far so good; no need to relate 'a and 'c.
    //
    fn f(&self) -> Self::Item<'static>;
}

pub trait LifetimeGenericConcreteMethodWhereSelf<'a> {
    type Item<'c> where Self: 'a;
    //            ~~~~~~~~+~~~~~~
    //                    |
    //            required because of just this: \
    //                                 ----------+---
    fn f(&self) -> Self::Item<'static> where Self: 'a;
}

pub trait LifetimeGenericConcreteMethodWhereItem<'a> {
    type Item<'c>;
    //            ~~~~~~~~+~~~~~~
    //                    |
    //            look ma, no where clause here
    //
    fn f(&self) -> Self::Item<'static> where Self::Item<'static>: 'a;
}

pub trait TypeGenericConcreteMethod<'a> {
    type Item<T> where T:'a;
    //           ~~~~+~~~~~
    //               |
    //           required because of ...?
    //
    // (How is this different from LifetimeGenericConcreteMethod?)
    //
    fn f(&self) -> Self::Item<()>;
}

pub trait TypeGenericParametericMethod<'a> {
    type Item<T>;
    //           ~~~~~~~~~+~~~
    //                    |
    //           look ma, no where clause here
    //
    fn f<T>(&self) -> Self::Item<T>; // where Self::Item<T>: 'a;
}

pub trait TypeGenericParametericMethodWhereItem<'a> {
    type Item<T>;
    //           ~~~~~~~~~+~~~
    //                    |
    //           look ma, no where clause here still
    //
    fn f<T>(&self) -> Self::Item<T> where Self::Item<T>: 'a;
}

pub trait TypeGenericParametericMethodWhereSelf<'a> {
    type Item<T> where Self:'a;
    //           ~~~~+~~~~~~~~
    //               |
    //            required because of this: \
    //                              --------+-----
    fn f<T>(&self) -> Self::Item<T> where Self: 'a;
}

There are three axes that seem to be significant for reasons I do not yet understand:

1. Sometimes a concrete method will force a where clause on the GAT. Compare
   TypeGenericConcreteMethod against TypeGenericParametricMethod.

2. Sometimes a where clause constraining Self in a method will force a
   constraint on the GAT, but an analogous where clause constrainting
   Self::Item in the method does not force any analogous constraint on the
   GAT. Compare TypeGenericParametricMethodWhereSelf against
   TypeGenericParametericMethodWhereItem.

3. But also: a lifetime-generic GAT doesn't seem to get any implicit forced
   constraint between it and lifetime params attached to its associating trait,
   but a type-generic GAT does. Compare LifetimeGenericConcreteMethod
   against TypeGenericConcreteMethod.

Nota Bene: Please forgive me if this was all previously spelled out in other documents about GATs. They strike me as discrepancies in the user's experience of the feature, but if there are good reasons for all of these discrepancies, then I guess this is a matter of improving our diagnostics or even changing the surface syntax to make such differences in the static semantic more immediately apparent.