Identification of a named constraint during definition

[danakj]

Allow identifying a named constraint inside its definition so that you can perform impl lookup on Self and find require decls that have been written earlier in the named constraint. This allows the named constraint to be used to provide witnesses from inside its definition.

But disallow using the name of the named constraint inside its definition, to prevent it from being used as a requirement for a type before all its requirements are known.

This was discussed in open discussion on 2026-03-12.

[danakj]

I updated this to disallow using the name of the named constraint (as a requirement) inside its definition, which is implemented in #6906.

[zygoloid]

This restriction seems possible to circumvent. Given a TypeOf function:

eval fn TypeOf[T:! type](x: T) -> type { return T; }

it seems we could circumvent the restriction by using of TypeOf(Self) instead of the name of the constraint, or similarly by using an alias or other indirection:

constraint A;
alias B = A;
constraint A {
  require C impls B;
}

Is that OK? (Are we trying to create a speed bump or a hard barrier here?)

If that is a problem, I wonder if we could allow only Self as N to be identified (where Self is the self of N) while the named constraint N is being defined, and not any other identification of N. I think that may be the same as what you're proposing except in these corner cases.

[danakj]

Yeah that sounds like a better way to say it, thanks.

[danakj]

We do want a hard barrier, because other uses of the constraint lead to what could be seen as incorrect output, where a constraint on A doesn't actually include all the requirements that A does.

[danakj]

I am struggling with how to make this a rule around the facet type of Self being identified. If it's the facet type, then TypeOf(Self) seems like it must return a facet type that is identified, but we don't want that.

As such I think the rule has to be instead that impl lookup does not require an identified facet type for Self in a named constraint? But that's much further from what the toolchain is doing - which is that it is identifying Self and accepting that inside the definition.

Maybe TypeOf(Self) should be okay, since it's related to Self it's more clear that it changes over the definition, unlike using the name of the constraint.

[danakj]

I am struggling with how to make this a rule around the facet type of Self being identified. If it's the facet type, then TypeOf(Self) seems like it must return a facet type that is identified, but we don't want that.

I guess it may be because the previous rule around identifying a facet type is written in terms of the type only. Whereas what you're thinking about here is the self+type pair.

Nonetheless, I think I am happy with a rule that says the type of Self can be identified (generally), since you've gone through Self you are acknowledging the incremental/incomplete nature.

[danakj]

The alias case already worked, but added a test in #6922

[zygoloid]

Just so I'm clear on what this means:

class C(T:! type) {}
constraint N {
  require impls X;
  require C(Self) impls TypeOf(Self);
  require impls Y;
}

... is equivalent to:

constraint N {
  require impls X;
  require C(Self) impls X;
  require impls Y;
}

(That is: C(Self) is required to implement X but not Y, because the type of Self at that point includes the X constraint but not the Y constraint.)

Also, given:

class C[T:! type](U:! T) {}
constraint N {
  require impls X;
  require C(Self) impls X;
  require impls Y;
  require C(Self) impls Y;
}

... we require that C(Self as X) impls X but that C(Self as (X & Y where C(.Self) impls X)) impls Y. And given T:! N, we do not know that C(T) impls X nor C(T) impls Y. (To be clear: I think that's OK, albeit a little subtle. I just want to ensure I understand the model.)

[danakj]

First one: yes.
Second one: yes-ish?

That's complicated but I think what you're doing there gives us a constraint on "whatever the facet type of Self is" which would be the N up to that point which is the things you wrote, but it's not like that is stored in the facet type itself. It's affects the identification of that facet type at that point in time, so like if C had a constraint C(T:! X) then we'd identify Self as N and find a witness for X, and construct a Self as X facet value.

If we somehow stored the facet type T (which is a reference to N) inside C and identified it later outside the definition, we'd see all of N.

Could you clarify what you mean by "And given T:! N? That's a constraint in C(T:! N) or in something else like D(T:! N) and we have a require impls D(C(Self))? Or what did you mean?

[zygoloid]

If we somehow stored the facet type T (which is a reference to N) inside C and identified it later outside the definition, we'd see all of N.

Is there any risk that we'll form a concrete witness for that facet type while N is still incomplete? If we did, that witness would be missing elements if we somehow look at it later. It's not very easy to write an example of this, but I think it could be something like:

eval fn TypeOf[T:! type](t: T) -> type { return T; }
class C(template T:! type, U:! T) {
  fn F() { T.YF(); }
}
interface X { let XT:! type; }
interface Y { fn YF(); }
constraint N {
  require impls X where .XT = C(TypeOf(Self), i32);
  extend require impls Y;
}
fn G(T:! N) { T.XT.F(); }

What I'm concerned about here is:

• We allow C(TypeOf(Self), i32) because we identify TyepOf(Self) as containing no constraints at that moment, so i32 impls TypeOf(Self).
• We form the type C(N, i32), and pass an empty witness table as the facet value for the second argument.
• We therefore allow the first requires declaration.
• When type-checking G, we find XT within T, resolve it to C(N, i32), and call its function F.
• This triggers template instantiation, which looks for YF in the type of T, and finds it within the extended interface Y.
• Finally, we try to extract the function YF from the second interface within N, and presumably crash because the facet value doesn't have enough elements in its witness table.

I think we can address this by rejecting concrete impl lookups for N while it's being defined, even though we otherwise treat N as identified, and would allow symbolic impl lookups.

[zygoloid]

Could you clarify what you mean by "And given T:! N? That's a constraint in C(T:! N) or in something else like D(T:! N) and we have a require impls D(C(Self))? Or what did you mean?

What I meant was, given the above N and fn F(U:! N) { ... }, can we conclude from within the body of F that C(U) impls X or that C(U) impls Y? I was thinking the answer would be no, becauseC(U) would have T = N whereas in the named constraint, the T would be something else. But I think you're saying that's not how it works: within N, the type of Self is indeed still N throughout, and we treat it as being identified even though we don't yet know what it's identified as.

[danakj]

I think we can address this by rejecting concrete impl lookups for N while it's being defined, even though we otherwise treat N as identified, and would allow symbolic impl lookups.

Hmm. So I agree this is a problem, but the solution here produces a weird state. We would have a symbolic witness for i32 as N but nothing will ever specify/monomorphize that further, so the lookup/witness won't get re-evaluated later. We'll never find a concrete witness.

[danakj]

within N, the type of Self is indeed still N throughout, and we treat it as being identified even though we don't yet know what it's identified as.

That is how I was intending it to work yeah

[zygoloid]

I think we can address this by rejecting concrete impl lookups for N while it's being defined, even though we otherwise treat N as identified, and would allow symbolic impl lookups.

Hmm. So I agree this is a problem, but the solution here produces a weird state. We would have a symbolic witness for i32 as N but nothing will ever specify/monomorphize that further, so the lookup/witness won't get re-evaluated later. We'll never find a concrete witness.

My suggestion would be to make the i32 as N impl lookup fail, rather than giving it a symbolic witness.

[danakj]

Oh okay, yes. I think that sounds good. I really only want symbolic lookups with Self to work. That's a way to not quite limit it to Self (other symbolic would work), without requiring a definition of identified that involves more than the facet type. Let me see how that looks written down.

(I had thought this through earlier and concluded that only symbolic witnesses/lookups were possible, because you can't write typeof. But of course we can now write typeof with eval fn so yeah, updating mental model.)

[danakj]

within N, the type of Self is indeed still N throughout, and we treat it as being identified even though we don't yet know what it's identified as.

That is how I was intending it to work yeah

I think maybe we need to introduce "partially identified".