var of type FacetType

[danakj]

Summary of issue:

Is it legal in the design to declare a var pattern with a type of a FacetType?

A small example:

interface N {}

class X {
  fn F[self: Self]() {
    let a: N = self.n;
  }
  var n: N;
}

Here the code has no idea how big n should be, so this seems like it should not be possible.

Whereas, a type of a "type defined by a FacetType" aka a FacetAccessType in the toolchain impl, seems fine:

interface Z {}

class C(I:! Z) {
  fn F[self: Self]() {
    let a: I = self.i;
  }
  var i: I;
}

The values design only says the type portion of the var pattern is an "expression": https://docs.carbon-lang.dev/docs/design/values.html#local-variables

The generics design has no example or mention of a var of a facet type afaict: https://docs.carbon-lang.dev/docs/design/generics/details.html

A full example that typechecks in the current impl, using a FacetAccessType, rather than a FacetType:

interface Z {}

class C(I:! Z) {
  fn F[self: Self]() {
    let a: I = self.i;
  }
  var i: I;
}

class D { adapt {}; }
impl D as Z {}

fn F() {
  ({.i = {} as D} as C(D)).F();
}

Details:

No response

Any other information that you want to share?

No response

[danakj]

The implementation of var requires the type to be "Concrete" which explicitly accepts facet types. I guess all facet values and type values are the same size...

Here the code has no idea how big n should be, so this seems like it should not be possible.

...so this is not correct.

Perhaps this should be valid?

interface N {}

class X {
  fn F[self: Self]() {
    let a: N = self.n;
  }
  var n: N;
}

class C {}
impl C as N {}

fn G() {
  ({.n = C} as X).F();
}

And the value repr of a facet value would just be copy/itself?

[danakj]

The toolchain/lower/testdata/interface/basic.carbon test seems to suggest as well that this should be possible, I guess. Currently the ir there is incorrect, the return type of the function should be a facet value, but it's void.

Making it possible to initialize a value from an EphemeralRef to a class member var of a facet value also seems to improve that test, so mentioning it here.

-// CHECK:STDOUT: define void @_CF.Main() !dbg !4 {
+// CHECK:STDOUT: define {} @_CF.Main({} %T) !dbg !4 {

[danakj]

I want to raise one consequence on the toolchain implementation if facet values can indeed be passed around as runtime values, stored in var etc, which is that it seems we would need to support narrowing runtime facet values (e.g. from I & J to I) but impl lookup currently assumes that the self value is a constant value. It would need to be adjusted to also handle runtime values - looking only at the type (the FacetType) in that case.

[zygoloid]

What we do elsewhere for such types (eg, type, IntLiteral) is to use an empty runtime object representation for such types. While this seems like a bit of an odd case, disallowing a var of such types may prove a hinderance in generic code in cases where you wouldn't actually use that value at runtime. (Presumably such disallowance would also extend to disallowing a class with such a type as a field being used as the type of a var, etc.)

If we have good reasons to disallow it, I don't think it'd be a great loss, but we'd need some description of how that disallowance would fit into the bigger picture -- for example, would we treat these types as being abstract? Or introduce some new set of rules for types that are complete, concrete, but still not usable as the type of a var? A proposal here would need to figure that out.

I could imagine cases arising in the future that would motivate stopping treating facets as empty at runtime -- for example, if we have some way to indicate that an associated function in an interface is intentionally object-safe, it might make sense for the corresponding facet to include a runtime version of the witness table that contains just the object-safe functions. But I think that's a compatible extension.

[zygoloid]

I want to raise one consequence on the toolchain implementation if facet values can indeed be passed around as runtime values, stored in var etc, which is that it seems we would need to support narrowing runtime facet values (e.g. from I & J to I) but impl lookup currently assumes that the self value is a constant value. It would need to be adjusted to also handle runtime values - looking only at the type (the FacetType) in that case.

Given the relatively small amount of known utility here, I think we should pick whatever rule is easiest to implement -- if we want to say that conversion between different facet types always requires that the source to be constant, I think that's OK.