Plugging a minor soundness hole in conformance checking

Hi all,

Consider the following protocols:

protocol P {
  associatedtype A : Q where A.B == Self
}

protocol Q {
  associatedtype B

  static func getB() -> B
}

Now suppose we have a pair of classes conforming to P and Q:

class C : P {
  typealias A = D
}

class D : Q {
  typealias B = C

  static func getB() -> C { return C() }
}

Today, Swift allows this conformance, but let's look carefully to see what it actually means. Since P requires that 'Self == Self.A.B', then we should be able to define the following protocol extension method on P:

extension P {
  static func getAB() -> Self {
    return Self.A.getB()
  }
}

Self.A.getB() has type Self.A.B, which we know is equal to Self, so this code is correct.

However, now imagine we define a subclass of C:

class SubC : C {}

Calling SubC.getAB() should return an instance of SubC, since the type of getAB() is (Self.Type) -> () -> Self and we substitute Self := SubC (protocol conformances in Swift are covariant!).

However, the implementation of getB() on class D returns an instance of C, not an instance of SubC.

The problem is the same-type requirement in protocol P -- it requires that the conforming Self type is exactly C, not C or some subclass of C.

I don't think there's any way to make this construction sound, but also I'm sure it comes up in real code, so I'm introducing a compiler warning:

warning: non-final class 'C' cannot safely conform to protocol 'P', which requires that 'Self' is exactly equal to 'Self.A.B'; this is an error in Swift 6

As the diagnostic suggests, declaring the class as final closes the soundness hole. Also, I have made this an error in a (hypothetical) future -swift-version 6, using the standard trick we've been using for newly-introduced type safety diagnostics that ban previously-allowed but invalid code patterns.

I'm of the opinion that this is a bug fix and not a real language change, so I don't think it warrants a pitch and a proposal; a forum post and changelog entry seems sufficient, but maybe I'm wrong.

If you have a legitimate reason to use a non-final class in this manner, we can discuss introducing some other way to muffle the warning while leaving the class non-final.

Let me know if you have questions or concerns.

23 Likes

Hmm, interesting.

I have a couple of half-baked ideas that I haven’t thought all the way through yet:

• Does the protocol actually want to require an “invariant Self”, meaning something like, “The exact type which declares conformance to this protocol”? I have a vague suspicion this might be a common theme for non-final classes conforming to protocols with Self requirements, where subclasses are expected to “act like” the superclass.

• For the opposite case, when the Self requirement really is intended to be covariant, would it make sense to use the “required” keyword (on the witnessing member of the conforming superclass) to indicate that subclasses must override it?

1 Like

Nasty case. Makes sense, as dimly as I’m able to understand it. Yes, does seem like a bug fix.

It would be nice if the error message could give a concise example of a specific type error the soon-to-be-invalid type structure would allow — although perhaps that’s too complicated to express clearly in an error message. It is certainly one of those errors that would feel like a brick wall if encountered in the wild.

This does ring true.

Would supporting where Self: A.B (which means allowing : to mean == for non-protocol, non-class RHS types) be sufficient to resolve this need?

I thought static protocol members weren’t dynamically dispatched? It seems strange for Self to be dynamic when the dispatch is not…

All protocol requirements are dynamically dispatched. Perhaps you're thinking of static class methods, which cannot be overridden in a subclass?

Note that the same problem would occur if the getB() and getAB() functions were instance methods and not 'static'. Think of a protocol requirement or extension method as a generic function with a generic parameter Self that conforms to the protocol; if the method returns Self, then we substitute in whatever concrete type we have at the call site (here, SubC), and we know the result is of that type.

Perhaps, but these hypothetical 'abstract subtype requirements' would be tricky to design and implement. I certainly do not understand the full implications of such a feature :-)

Is this part of any snapshot yet, I'd like to check if our code base could run into this issue or not?!

Not yet, the PR is still being tested by CI: Sema: Warn about non-final classes conforming to protocols with a same-type requirement on 'Self' by slavapestov · Pull Request #41545 · apple/swift · GitHub

Once I merge it, it will be in the next snapshot.

In that it's a soundness hole and that it was not intended as part of any design, I agree. Not sure I see any other alternative.

10 Likes

Nor do I! For another discussion, then.


With type problems like this, I always like to work out the example mapped to some real-world-ish domain. I find it helpful to find a correspondence between the type problem and a modeling problem.

I’ll share that here, in case it’s useful to anyone else. It sounds like the discussion is already decided, but…just in case it helps others! This is Slava’s sample code from the OP, with the types renamed:

protocol Pooled {
  associatedtype Pool : ResourcePool where Pool.Resource == Self
}

protocol ResourcePool {
  associatedtype Resource

  static func checkOutResource() -> Resource
}

// –––––––––––––––––––––––––––––––––––––––––––––––

class Tupperware : Pooled {
  typealias Pool = TupperCabinet
}

class TupperCabinet : ResourcePool {
  typealias Resource = Tupperware

  static func checkOutResource() -> Tupperware {
    return Tupperware()
  }
}

class MicrowaveSafeTupperware : Tupperware {
  // Only put this subtype in the microwave, or else!
}

// –––––––––––––––––––––––––––––––––––––––––––––––

// This gives Tupperware, but we’d want it to
// give MicrowaveSafeTupperware:
print(MicrowaveSafeTupperware.Pool.Resource.self)

// Because of the above, this extension:
extension Pooled {
  static func checkOutResource() -> Self {
    return Self.Pool.checkOutResource()
  }
}
// ...means that MicrowaveSafeTupperware.checkOutResource()
// will return non-microwave-safe tupperware.

This example helps convince me that Slava’s solution of prohibiting the construction makes modeling sense as well as type sense:

  • We’ve said that every pooled resource type needs to know statically what kind of pool it has: associatedtype Pool : ResourcePool.

    The Tupperware type says its resource pool is always a TupperwareCabinet.

  • We’ve also said that a resource type’s pool should return instances of that resource: where Pool.Resource == Self.

    That means MicrowaveSafeTupperware’s ResourcePool should return MicrowaveSafeTupperware; there’s no other reasonable reading here. Makes sense!

  • We also say that all resource pools of a given type much choose statically what type of resource they return.

    All TupperCabinets can promise is that they return Tupperware.

  • Now we’ve painted ourselves into a corner. All Tupperware is pooled in a TupperwareCabinet, so if MicrowaveSafeTupperware isn’t, then it isn’t tupperware. But if a TupperwareCabinet must only promise to return Tupperware; if it specifically promises MicrowaveSafeTupperware, it’s not a TupperwareCabinet anymore.

This convinces me the model is nonsensical.

6 Likes