when are facet types equal?

[zygoloid]

Summary of issue:

As described in the generics design, there is a subtyping relationship between facet types when one has a subset of the constraints of another. But it's not clear when facet types are equal: should two facet types with the same set of constraints and the same lookup behavior be "the same", or merely be two different types that have the same behavior?

Details:

One place where this comes up is with the definition of the type type. For example:

constraint IsThisTheSameAsType {}
class X {
  impl X as ImplicitAs(IsThisTheSameAsType) { ... }
}
var v: ({} as X);

The use of an expression of type X after a : causes us to look for ImplicitAs(type), which raises the question of whether type is the same value as IsThisTheSameAsType, or a different value that has the same behavior.

Any other information that you want to share?

We could use a structural rule that says that two facet types are the same value if they have the same set of constraints and the same lookup behavior. This may be challenging to specify in a way that implementations agree on, for example because the facet type may have an unresolved set of rewrites, or because it would matter whether vacuous constraints like .Self is type are retained or discarded, or because this would require us to precisely define what it means for two facet types to have the same lookup behavior. This is the approach that explorer currently takes, with a fairly arbitrary set of decisions for the implementation questions.

We could use a lexical nominal rule that says that two facet types are the same value if they were created in the same way (naming the same interface, combining constraints with & in the same order, etc). That rule may also be challenging to support, because it would likely require implementations to track the provenance of each facet type.

We could use a more semantic nominal rule that says that each & or where evaluation creates a unique new facet type, as does each constraint or interface declaration. That approach seems to provide both a reasonable level of simplicity for implementations and an easily understandable user model. This would mean that IsThisTheSameAsType is not the same as type, and nor is type & type or type where .Self is type. That's the approach that seems most promising to me.