Narrowing to opaque types

[kyouko-taiga]

There's one thing we can't do in Swift that's a little annoying. Imagine I have this setup:

protocol P {}
protocol Q: P {}

struct A: Q {}
struct B: Q {}
struct C: P {}

func foo<T: P>(_ x: T) {
  if let y = x as? any Q {
    // can't call `bar` on `y`
  } else {
    otherwise()
  }
}

func bar<T: Q>(_ x: T) { ... }

It makes sense that an existential type doesn't conform to its bounds but that forces us to opt in type erasure when we want to narrow a type to a refinement. AFAIK, the only way to deal with this situation is to narrow to concrete types, i.e.:

switch x {
  case y as A: bar(y)
  case y as B: bar(y)
  default: otherwise()
}

That's not only boilerplate but also high-maintenance in cases where it's likely that new conformances to Q might be defined.

In the real world, I hit this problem quite often in hc because we have many protocols describing categories of declarations, like GenericDecl , TypeExtendingDecl, or ExposableDecl. You can look in the type checker for all the case ConformanceDecl.self that are next to case ExtensionDecl.self to see examples, but even more generally we can't easily narrow a T: DeclID to a generic U: ScopeID without erasure. That is, we need to transform our T: DeclID to a AnyScopeID, which involves a change of representation (AnyScopeID must store the kind of the node in its payload; U: ScopeID does not).

I think we could get around this issue in Hylo by supporting narrowing casts to opaque types:

fun foo<T: P>(_ x: T) {
  if let y: some Q = x { bar(y) } else { otherwise() }
}

Such casts would be zero cost because they don't involve any change of representation, unlike erasure. For code generation we wouldn't be able to use monomorphization but the existentialized form of the function should work fine because anyway it would take an arbitrary pointer along with a witness table, which is exactly the representation I expect for an opaque type.

[dabrahams]

This code compiles in Swift and prints bar\nelse:

protocol P {}
protocol Q: P {}

struct A: Q {}
struct C: P {}

func foo<T: P>(_ x: T) {
  if let y = x as? any Q
  {
    bar(y)
  } else {
    print("else")
  }
}

func bar<T: Q>(_ x: T) {
  print("bar")
}

foo(A())
foo(C())

There's an "implicit opening" feature that I always had reservations about (see my many posts here). If you look at the Detailed Design section you can see the rules for when and how you can use this are quite complicated for users. I haven't analyzed your proposal yet beyond this initial example but if it creates a more consistent world for users while supporting the important use-cases for implicitly-opened existentials, I would be strongly in favor.

One problem is that I think nobody has actually laid out the use cases for implicit opening.

I seem to remember there was a workaround for the lack of implicit opening, too, before it was added. I'll see if I can find that…

[dabrahams]

It would be interesting to know why you couldn't use implicit opening in the compiler.

Unrelated to that, also see this explicit opening proposal.

[kyouko-taiga]

Wow, I wasn't aware of implicit opening! I didn't even care to try compiling my example because I was convinced it wouldn't type check. Sorry.

To a first approximation I think my proposal is simpler, though. I also think it goes in the same direction as the explicit opening proposal you linked. One think I don't like from SE-0352 and guess it's causing confusion is that it's trying to be too clever. For example here:

func openSimple<T: P>(_ value: T) {}
func testOpenSimple(p: any P) {
  openSimple(p) // okay, opens to 'p' and binds 'T' to its underlying type
}

I don't think we should be able to call openSimple because allowing the call here will inevitably leave the user puzzled as to why the compiler complains that any P doesn't conform to P later. Maybe that is part of the arguments you had against the proposal, I didn't go through all of them.

In my proposal we would first have to open p under an opaque existential and then call openSimple.

fun open_simple<T: P>(_ v: T) {}
fun test_open_simple(p: any P) {
  let y = p as some P
  open_simple(y)
}

Because of the explicit step, it gets also simpler to explain why this situation would be ill-typed:

func cannotOpen<T: P>(_ v1: T, _ v2: T) {}
func testCannotOpen(p: any P, q: any P) {
  cannotOpen(p, q)
}

Clearly the issue is that p and q are not guaranteed to have the same witness. At least with the explicit syntax we can explain that any new occurrence of some P denotes a statically distinct type.

[dabrahams]

I'm not sure if that really changes anything. I think it might be just as easy to say any opening of any X results in a potentially-distinct type that conforms to X.