Type completeness in extend

[danakj]

Define rules for extend declarations (extend require and extend impl as) that say the facet type they name must be complete at the point of the declaration. Define completeness for a facet type to include all interfaces and named constraints that can be reached though extend require declarations.

[chandlerc]

This generally LG on my end.

[danakj]

PTAL

[zygoloid]

Do we already have a rule for extend base and extend adapt declarations? If not, would it be worth adding them here too, so that we have complete coverage of all extend declarations?

[zygoloid]

It'd be nice if we could say something broader here, and while I don't think we can avoid facet types being a special case, perhaps we can make them reuse the broader notion. What I'm thinking is something along the lines of:

"""
An extend declaration

extend base: X;
extend adapt X;
extend impl as X;
extend require impls X;

declares that the enclosing scope extends the scope associated with X. The extend declaration requires X to be complete, or, if X is a generic parameter, requires the type of X to be complete.

The scope of a facet type formed by a where declaration extends the scope of its first operand. The scope of a facet type formed by an & operator extends the scopes of both of its operands. In either case, the facet type is complete if every scope it extends is complete. The facet type type is associated with an empty scope and is complete.
"""

[zygoloid]

I would expect this to apply immediately, not at the end of the definition of Y. For example:

base class Z {
   class X {}
}
class Y {
  extend base: Z;
  // Finds `X` in `Z`.
  fn F() -> X;
}