When are interface requirements enforced for an impl?

[josh11b]

Summary of issue:

Given an interface with a requirement, for example:

interface I {}
interface J {
  require Self impl I;
}

When do we need to see an implementation of I before allowing an implementation of J? Does it matter if the implementation of I is complete? Is the answer different for a impl declaration of J compared to a definition of J?

Some possible answers:

• I needs to be implemented at some point in the same file, possibly after J.
• [4 different possible rules] An implementation of I needs to be {declared or defined} before a {declaration or definition} of an implementation of J.

Details:

For example, we might say an implementation of I needs to be declared before the implementation of J is defined, as in:

// ✅ Forward declarations allowed
impl C as J;

// ❌ Definition of `J` before declaration of `I`
impl C as J { }

// ✅ Forward declarations of `I` enough to define `J`.
impl D as I;
impl D as J { }

Or we could have a more restrictive rule like I needs to be defined before an implementation of J can be declared: as in:

// ❌ Forward declaration of `J` without implementation of `I` being defined
impl C as J;

impl D as I;
//  ❌ Forward declarations of `I` not enough to declare `J`.
impl D as J;

// ✅ Definition of `I` allows declaration of `J`
impl E as I { }
impl E as J;

[josh11b]

I personally think:

• The least restrictive rule ("I needs to be implemented at some point in the same file, possibly after J") is too permissive. It will create work in the compiler implementation, and isn't philosophically aligned with Carbon's information accumulation principle.
• I think the most restrictive rules that require a definition of I are too restrictive. I think that would be a burden on users, making the order that things may be legally declared into a puzzle, which may be difficult or impossible to solve when there are other dependencies or constraints.
• That leaves two possible rules: I needs to be declared (though not necessarily defined) as implemented before J is {declared or defined}. Of these two possibilities, I prefer the less restrictive (before J is defined), but I think either is viable.

[chandlerc]

Agree with the reason for excluding the least and most restrictive options.

Agree with declared before defined. It seems nice that the two otherwise independent forward declarations can be independently ordered. And it seems nice that we shouldn't have completely arbitrary restrictions -- they should be motivated in some way. Either better code, clearer code, alignment with some principle, or simplifying the implementation. Until we have such a motivation, we leave off the added restriction. It also seems cheap to revisit this, a generally low-stakes decision here.