Should impls with maximal type structure be allowed to be declared `final`?

[zygoloid]

Summary of issue:

It's possible for an impl to have a type structure that cannot be further refined (depending on your perspective it'd be maximal or minimal under the partial ordering by type structure; I'm going to consider "more refined" to be "greater" so that such type structures are maximal), and this can occur without the impl being unparameterized. This happens if the impl's only parameters are non-type parameters. For example, in the prelude:

class Int(N:! IntLiteral()) {
  adapt MakeInt(N);
}

impl forall [To:! IntLiteral()] IntLiteral() as ImplicitAs(Int(To)) {
  fn Convert[self: Self]() -> Int(To) = "int.convert_checked";
}

Here, the type structure of this impl is IntLiteral() as ImplicitAs(Int(?)). The impl is parameterized, but this type structure is still maximal: at the type structure level, the value for a non-type argument of a type is always a ?. It can still be specialized -- there could be an impl for IntLiteral() as ImplicitAs(Int(32)), for example -- but only in the same file, and any such impl would need to be in a prioritization block with the above impl.

The consequence of this is that it is sound to permit such an impl to be declared as final. And it's useful to do so: this allows

final impl forall [N:! IntLiteral()]
    IntLiteral() as AddWith(Int(N)) where .Result = Int(N);

... to be declared final, allowing us to know that the type of 1 + n (for n: Int(N)) is Int(N) early in type-checking.

We should consider changing the final rules to allow maximal but parameterized impls to be declared final even if the root type or interface is not owned by the current file.

Details:

It's tempting to treat such impls as being effectively final, but we probably shouldn't: final implies that information from the impl can be used earlier in type-checking, so probably should require an explicit opt-in from the author of the impl.

Any other information that you want to share?

No response

[zygoloid]

Alternative: instead of changing the rules for final, we could conceivably note that the only library in which a query for IntLiteral() as AddWith(Int(N)) could ever find an impl (for any N) is the library that owns Int (or AddWith), and therefore if we find a unique best result in that library, we could treat that result as final even though it wasn't declared final.

That would give the advantage of also supporting

impl forall [N:! IntLiteral(), T:! ImplicitAs(Int(N))]
    T as AddWith(Int(N)) where .Result = Int(N) {
  fn Op[self: Int(N)](other: Int(N)) -> Int(N) = "int.sadd";
}

... where the impl is treated as final for 1 + n while still allowing specialization for my_type_that_converts_to_i32 + n.

[danakj]

IIUC this alternative would produce different behaviour for uses inside the library where a type is named in the generic parameters vs outside the library - since outside you could get a conclusive result and decide to treat it as final.

That seems probably okay, but want to clarify that this is based on the library, and in this case library != file. If we were to concatenate files together, they would still be parsed as being separate libraries, and the behaviour wouldn't change for the code concatenated into the library's file?