The scope of associated existential types

[Centril]

Given the following snippet (playground):

#![feature(existential_type)]

trait A { type B; }

mod enclosing {
    struct C;
    
    impl crate::A for C { existential type B: Copy; }
    
    pub fn make() -> <C as crate::A>::B {
        42u8 // This is a defining use.
    }
}

It seems that rustc considers the scope of seeing the underlying type to be impl crate::A for C and not enclosing:

error: could not find defining uses
 --> src/lib.rs:8:27
  |
8 |     impl crate::A for C { existential type B: Copy; }
  |                           ^^^^^^^^^^^^^^^^^^^^^^^^^

The RFC states that:

Each existential type declaration must be constrained by at least one function body or const/static initializer. A body or initializer must either fully constrain or place no constraints upon a given existential type.

Existential types are similar to normal type aliases, except that their concrete type is determined from the scope in which they are defined (usually a module or a trait impl).

The latter quote suggests that the behavior seen above may be correct.
However, in a comment, the RFC also states:

impl Iterator for MyStruct {
    // Here we can declare an associated type whose concrete type is hidden
    // to other modules.
    //
    // External users only know that `Item` implements the `Debug` trait.
    existential type Item: Debug;

   ...
}

This suggests (note the word module) that the current implementation is wrong and that the snippet should be allowed.

So which behavior is correct? And why? cc @cramertj @nikomatsakis @alexreg

As a final note, currently, the user has a recourse in writing:

#![feature(existential_type)]

trait A { type B; }

mod enclosing {
    struct C;

    existential type B: Copy;

    impl crate::A for C { type B = B; }
    
    pub fn make() -> B {
        42u8
    }
}

[alexreg]

The latter quote suggests that the behavior seen above may be correct.

Yes, I believe the implemented behaviour is correct. Both intuitively and according to the RFC.

This suggests (note the word module) that the current implementation is wrong and that the snippet should be allowed.

I think this is just a slip: it should read "scope". Or perhaps the author intentionally used the word "module" loosely to mean any defining scope. But I think the point is more that the concrete type is hidden, in any case.

[cramertj]

+1 -- the intention is that the scope of associated existential types is limited to the trait impl itself. If you want to define them outside, you can write the existential type outside the trait impl and then refer to the type in the associated type declaration.

[Centril]

Thanks @cramertj for the clarification. Was there specific reasons behind this intent? Does it simplify the implementation substantially or something else perhaps?

[alexreg]

@Centril I don't want to speak for Taylor, but myself I think this allows for the maximal control of scope (as he points out, you can simply move the scope of the existential type under the current implementation) -- and is also the most intuitive behaviour, in my opinion.

[Centril]

I think this allows for the maximal control of scope

Not so; you get equal amount of scope control. If you want to limit the scope of the trait implementation, wrap the implementation in an inline module.

as he points out, you can simply move the scope of the existential type under the current implementation

There's an example of doing just that here: #57933 (comment).

and is also the most intuitive behaviour, in my opinion.

Can you say why you find it most intuitive? The behavior seems more complex than if the scope was at the module, at least from a user's perspective (more rules...). Essentially, this makes trait implementations into pseudo-modules in the sense of existential type but not wrt. visibility and use.

That said, I think the current behavior is more conservative in the sense that we could extend it later if we wanted.

[alexreg]

If you want to limit the scope of the trait implementation, wrap the implementation in an inline module.

This seems very artificial though.

Can you say why you find it most intuitive?

The syntactical scoping is just obvious this way. The existential type is "defined" by its immediate scope.

[cramertj]

And in particular, I think this will be the most common thing to want for these types (also in impl blocks when we get inherent associated types), so giving it the good syntax (rather than nesting in a mod) seems preferable to me.

[cramertj]

In any case, this is the behavior the RFC specified and is backwards-compatible with expansion in the future. If you want to change this, I think we should leave it for discussion on a future RFC.

[alexreg]

Yeah, I'm with Taylor on this. Shall we close this, at least for now, Centril?

[Centril]

I am concerned about having so many rules around existential type, but I find:

The existential type is "defined" by its immediate scope.

to be compelling; so let's close for now.

(cc #34511 to make sure this is recorded...)