Retroactive conformances + dynamic downcast => type unsoundness

Development Compiler
, ,
1

<type system nerd alert>
Soundness issue with dynamic downcasts · Issue #75824 · swiftlang/swift · GitHub demonstrates a type soundness problem we discovered while thinking about scoped conformances in Hylo. Because Swift allows different modules to declare conflicting conformances and you can declare a stored property of associated type, it's possible for SomeModule.A<Int> to have entirely different layouts in different contexts. When instances created in those different contexts come together, disaster ensues.

Curiously, I wasn't able to find a problematic example that didn't involve some dynamic downcasts—all attempts to do so would fail to link. To better understand what's going on and what might be needed to close a hole like this one, I'd like to discover whether such an example exists. So, I'm offering 1000 kudos to anyone who can show me that example or who can explain why that example can't exist, and my general thanks for any insight you can add to the picture.
</type system nerd alert>

Thanks all!

-Dave

5 Likes
2

I believe the place that's supposed to catch this is the downcast: A<Int where Int: P via M1> and A<Int where Int: P via M2> are intended to be distinct types, even though that's not visible in the user-visible syntax. You can see this in the expanded mangled names for makeA in each module if you try to return the concrete A<Int> instead of Any:

% xcrun swift-demangle -expand s2M15makeA2M01AVyS2iAC1PAAyHCg_GyF
Demangling for $s2M15makeA2M01AVyS2iAC1PAAyHCg_GyF
kind=Global
  kind=Function
    kind=Module, text="M1"
    kind=Identifier, text="makeA"
    kind=Type
      kind=FunctionType
        kind=ArgumentTuple
          kind=Type
            kind=Tuple
        kind=ReturnType
          kind=Type
            kind=BoundGenericStructure
              kind=Type
                kind=Structure
                  kind=Module, text="M0"
                  kind=Identifier, text="A"
              kind=TypeList
                kind=Type
                  kind=Structure
                    kind=Module, text="Swift"
                    kind=Identifier, text="Int"
              kind=TypeList
                kind=RetroactiveConformance
                  kind=Number, index=0
                  kind=ConcreteProtocolConformance
                    kind=Type
                      kind=Structure
                        kind=Module, text="Swift"
                        kind=Identifier, text="Int"
                    kind=ProtocolConformanceRefInOtherModule
                      kind=Type
                        kind=Protocol
                          kind=Module, text="M0"
                          kind=Identifier, text="P"
                      kind=Module, text="M1"
                    kind=AnyProtocolConformanceList
$s2M15makeA2M01AVyS2iAC1PAAyHCg_GyF ---> M1.makeA() -> M0.A<Swift.Int>

% xcrun swift-demangle -expand s2M25makeA2M01AVyS2iAC1PAAyHCg_GyF
Demangling for $s2M25makeA2M01AVyS2iAC1PAAyHCg_GyF
kind=Global
  kind=Function
    kind=Module, text="M2"
    kind=Identifier, text="makeA"
    kind=Type
      kind=FunctionType
        kind=ArgumentTuple
          kind=Type
            kind=Tuple
        kind=ReturnType
          kind=Type
            kind=BoundGenericStructure
              kind=Type
                kind=Structure
                  kind=Module, text="M0"
                  kind=Identifier, text="A"
              kind=TypeList
                kind=Type
                  kind=Structure
                    kind=Module, text="Swift"
                    kind=Identifier, text="Int"
              kind=TypeList
                kind=RetroactiveConformance
                  kind=Number, index=0
                  kind=ConcreteProtocolConformance
                    kind=Type
                      kind=Structure
                        kind=Module, text="Swift"
                        kind=Identifier, text="Int"
                    kind=ProtocolConformanceRefInOtherModule
                      kind=Type
                        kind=Protocol
                          kind=Module, text="M0"
                          kind=Identifier, text="P"
                      kind=Module, text="M2"
                    kind=AnyProtocolConformanceList
$s2M25makeA2M01AVyS2iAC1PAAyHCg_GyF ---> M2.makeA() -> M0.A<Swift.Int>

(specifically, notice the ProtocolConformanceRefInOtherModule a few lines from the end in each expansion)

The Any sidesteps the link error by keeping the real fully-qualified name of A<Int> out of the signature. But that means the as! likewise should have a fully-qualified A<Int via M1> or A<Int via M2> that it's targeting (when I compile your example I get true and false in the printout, so I guess it picked M1), and the runtime should take that into account when it does a downcast. Even though it might make downcasts slower.

That said, in the concrete case this ought to also be detectable at compile time rather than link time: if the swiftmodule files for M1 and M2 recorded which conformance was used, M3 would be able to tell that the types don't match.

I don't know/remember if it's possible for the uses in M1 and M2 to actually get mixed up due to runtime caching of what A<Int> is, or which conformance to use for Int: P, but in the model I believe the only thing that does global lookups of conformances is downcasts to protocol types (any types). To actually support that model well we'd need a way to communicate A<Int where Int: P via M1> to users, though, and possibly even a way to spell it in source. @Joe_Groff has talked about explicitly supporting that before (presumably much like your scoped conformances), but as far as I know very little work has actually been done in that direction.

5 Likes
3

Today’s compiler performs conformance lookups in various places and is not entirely principled about recording references to conformances and carrying them around, so it should be possible to construct such a test case.

In theory, a sufficiently advanced representation, for example having all BoundGenericTypes store conformances, could eliminate these lookups.

If I was designing a language from scratch for greenfield projects I would probably ban retroactive conformances unless I had a good reason not to. Do you feel their introduction solves a sufficiently important problem in Hylo?

4 Likes
4

But is this only due to their global scope? Would module-private retroactive conformance be objectionable? (or is it well-understood that that's not possible?) E.g., in AspectJ, inter-type declarations can be made visible only to the aspect.

(Asking in part because I use them in Swift and want to believe they are safe when uncontested; if not I need to wean myself...)

5

Yeah, but even if the implementation could handle it, I think ergonomics are a problem.

Eg, think about diagnostics. You have to explain why a Set<Int> and a Set<Int> are two distinct types, by pointing at a conformance requirement in a where clause, and two extension declarations or something.

To have good support for this kind of thing, you probably want to have some way of naming your conformances explicitly, and that completely changes the model. You get something like ML functors.

4 Likes
6

It would be interesting to have named conformance witnesses instead of retroactive conformances, because in one particular case retroactive conformances are useful tools when otherwise you would have to write a wrapper type.
Suppose we have a foreign class without conformance to Hashable and want some algorithm to use it with Set, and calculate the hash based on a public property of the type:

struct Foo {
  var id: Int
}

// In the other module
func doSomething(foos: [Foo]) {
  var set = Set<Foo>(foos)
}

To make it work we have to either retroactively conform Foo to Hashable or use a wrapper on Foo.

struct FooHashable: /* list of all the other conformances of Foo */ {
  var underlying: Foo
  init(underlying: Foo) { ... }
  func hash(into hasher: inout Hasher) {
    hasher.combine(foo.id)
  }
  // ... proxy to all the other conformances of Foo ...
}

Having a named conformance witness would allow a scoped use of a type like if it had the conformance. Something like

conformance_witness FooHashable of Foo: Hashable {
  func hash(into hasher: inout Hasher) {
    hasher.combine(id)
  }
}

func doSomething(foos: [Foo]) {
  var set = Set<Foo via FooHashable>(foos)
}

The compiler would know how to convert Foo via FooHashable to/from Foo. It could also check access level of the FooHashable allowing such conformances to be internal/public/private or even scope-local.
Kinda niche feature though.

4 Likes
7

I do think regardless of any such feature, having better tools for forwarding conformances to make wrapper types easier to write would help a lot. Such features are tricky to design as well, but would be useful for other uses of wrapper types.

5 Likes
8

Not retroactive conformances so much, but scoped conformances—which raise all the same issues—address an important issue that comes up when you truly eliminate reference semantics: some conformances need to use data that is only available in a local scope. @Alvae can provide examples.

Unless and until we figure out how to make them sound, though, we are going with the approach you suggest.

9

I am not convinced that naming conformances necessarily changes the model. We could say that all scoped conformances are named and the only difference is that the names show up in diagnostics.

Also, since Swift only allows conformances at module scope, can't you already say they are named…after the module?

Maybe I'm missing something.

1 Like
10

Naming the witness of a conformance is a nice idea. In fact, there's even no reason conformances (or witnesses thereof) can't be first-class values. That is how Scala implements typeclasses (i.e. protocols) and there is more than enough code out there to prove it is a solid design.

Now there are a few caveats:

  1. You need path-dependent types to make that work, otherwise there is no way to name associated types in type signatures.
  2. Dependent functions are very well understood but dependent types create some complications when we're as serious about encapsulation as Swift is.
  3. Reasoning about equality between associated types becomes tricky. The example that @dabrahams has linked came out of a long discussion in which I wanted to demonstrate that with scoped (or module-based) conformance, one can no longer deduce that T.X = U.X if T = U (assuming X is the associated type of some protocol to which T conforms).
  4. You probably need implicit parameters to make the whole design ergonomic.

I think we can make global conformances work together with "first-class" conformances, and add rules to Swift to eliminate the unsoundness reported by @dabrahams. FWIW, that is most likely the plan we'll follow for Hylo, at least for now (Swift-like global conformances in a first step, first-class conformances with path-dependent types in the future).

First-class conformances will require more explicit plumbing but they could help solve some of the issues one faces when trying to implement protocols for notional values in a pure MVS world.

2 Likes
11

Yeah, that’s exactly what I meant by named conformances, but you explained it better. I’m imagining an explicit syntax like Set<Int, Int: Hashable => MyFooHashAlgorithm> to completely fill in the substitution map. (I’m not pitching this syntax or feature in Swift, just a hypothetical language.)

Yeah, it’s interesting. In the formal system for Swift generics, we have an inference rule to derive [T.A == U.A] from [U: P] and [T == U]. This is no longer possible with overlapping conformances, and you’d need to introduce “same-conformance requirements” or similar, then the equivalent inference rule would also require you to first prove [T: P] == [U: P].

You’d also need to watch out for situations with recursive conformances where everything can be reasoned about if you assume conformances are unique, but once you relax the assumption you suddenly need to prove an infinite set of same-conformance requirements to make something type check.

12

I think you can, if you say, as Swift seems to be doing with its mangling, that T == U only holds when T and U depend on the same conformances, provided there is no dynamic casting hole. These two things seem easy to me also (at least in a new language):

  1. As @jrose mentioned, the errors could be pushed to compile-time.
  2. Closing the dynamic casting hole without major performance impact.

I think the simple/mostly-understandable system says that satisfying a generic T == U constraint implies that T and U have the same conformances.

13

We should do that, though. The runtime was implemented with room for these same-conformance constraints, whenever the compiler representation can finally catch up to it.

For a new language, I would argue that it's better not to have dynamic protocol conformance checks at all. Even though they're convenient, and you could put restrictions on them to make them sound in the face of multiple conformances such as to say that dynamic checks only find non-retroactive conformances, I think you'll have trouble keeping developers from running into problems anywhere dynamic conformance checks mix with static conformance resolution and gives different results.

In many of the places Swift developers use dynamic conformance lookup, I think it would be possible to instead capture optional conformance requirements that the compiler can resolve, potentially with a scoped or named alternative conformance, and store directly in the witness table for more efficient lookup. Like instead of having an [Any] and doing dynamic as? P or as? Q checks on the elements, you could have a protocol PQ where Self :? P, Self :? Q, for which the compiler would attempt to resolve the P and Q conformances any time a type conforms to PQ, and then dynamic checks for those capabilities on the elements of a [PQ] would pick up the conformance chosen by the compiler, if any was found.

2 Likes
14

By the way, I have developed a simple rewrite rule that allows programs without global coherence—multiple conformances of a type to the same protocol—(and in fact full-on scoped conformances) to be typechecked in terms of Swift's current type system.

15

Actually I think it's the opposite: conformance checks don't create any issues, but as my example shows, dynamic casting to concrete types does. Can you describe a specific problem that comes from checking conformances?

16

If you're looking up conformances dynamically, I don't think there's a way to do so in a way that would match the developer's expectation of context in all situations. For instance, you might have some homogeneous storage for registering different kinds of components like:

var components: [Any]

func register<T: Runcible>(runcer: T) { components.append(runcer) }
func register<T: Fungible>(funger: T) { components.append(funger) }

The code that processes the components and does dynamic lookups is in one context:

extension Int: Runcible { /* Int: Runcible conformance A */ }
extension String: Fungible {  /* String: Fungible conformance A */ }

func processComponents() {
  for component in components {
    switch component {
    case let runcer as Runcible: 
      runcer.runce()
    case let funger as Fungible:
      funger.funge()
    default:
      continue
    }
  }
}

But the registration APIs can be called with a different context:

func registerComponents() {
  extension Int: Runcible { /* local Int: Runcible conformance B */ }
  register(runcer: 1738) // uses conformance B
  register(funger: "hello world") // uses conformance A
}

func registerMoreComponents() {
  extension String: Fungible { /* local String: Fungible conformance B */ }
  register(runcer: 1738) // uses conformance A
  register(funger: "hello world") // uses conformance B
}

but those caller contexts gets lost in the type erasure and can't be reliably reassociated with their original context. If instead of Any and dynamic casting, we used an enum Component { case runcible(Runcible), fungible(Fungible) }, or there was a common meta-protocol that captured the conditional requirements at the point of use, then that context could be preserved.

17

I'm not sure I understand what you're saying happens here. In my world, the Any that holds a String from registerMoreComponents downcasts successfully to Fungible using the local semantics from registerMoreComponents because the conformance is captured at the point where String is bound to a generic parameter. (I know Doug has taken issue with that semantics on implementability grounds).

Regardless, that's all mechanics; you haven't described a programmer expectation that is violated.

Also, I'm not sure that matching the developer's expectation in all situations is a reasonable goal for a language, if by “the developer” you mean “every developer.” A developer that understands the language rules will expect every program to do what it actually does. The real question is whether the rules describe a system for which most people can form a coherent mental model.

The “component processing” code doesn't say Int and String are going to be the only models of Runcible and Fungible respectively, nor that other conformances won't be created. Someone could always make each of them conform to both protocols. Would that surprise the developer? I'm guessing, by your definition, it would. AFAICT, the only way to even plausibly hold a reasonable expectation that would be violated by this code is to put a loud comment on these protocols that says not to create conformances to them, or make them private to a local context.

18

I'm not sure there is a semantics that anyone can understand for what happens here. The Any doesn't have any information about what context it came from; it only holds a String, which is the same String type that can come from anywhere in the program, so the runtime doesn't have any sense of where to look for conformances when asked to look for one globally. Some possibilities would be:

  • it does a global search and just stops at the first one it finds, so it's arbitrary which one wins
  • it does the search from the perspective of where the dynamic cast is written. In the example above, the context of processComponents() only sees the A conformances for Int and String, which would be different from the B conformance used in the local contexts that registered the components.
  • some global rule states that only "canonical" non-local, non-retroactive conformances can be discovered dynamically. This would also mean that processComponents() finds the A conformances, and any local conformances would be disregarded.

Maybe you could also say that existential types like Any capture their context at the point of type erasure, and use that when dynamic conformance checks are done. That still only works to contextualize lookups for conformances that are visible at the point of type erasure. It also would make it so that existential values are potentially semantically different even if the type, value, and statically captured conformances are identical, which seems like it introduces its own realm of difficult-to-understand behavior. It seems to me like, if you're going to encourage multiple conformances, it would be better overall not to provide the attractive nuisance of global dynamic conformance lookups, and encourage instead language features that reliably capture and propagate needed conformance information at point of use.

1 Like
19

I assure there's one I can understand :slight_smile:. Whether others can understand it remains to be seen.

The Any doesn't have any information about what context it came from; it only holds a String, which is the same String type that can come from anywhere in the program, so the runtime doesn't have any sense of where to look for conformances when asked to look for one globally.

That's not about what's understandable, that's a description of how you think this can work, probably specific to Swift's current implementation. In Hylo, every existential carries a bundle of all the known conformances of the type from the context where the existential was formed. There's nothing to search for.

Maybe you could also say that existential types like Any capture their context at the point of type erasure, and use that when dynamic conformance checks are done.

That's exactly what we say.

That still only works to contextualize lookups for conformances that are visible at the point of type erasure.

Those are the only ones you get through the existential. If you downcast it to a concrete non-generic type, then you get the ones visible in the local context. A concrete generic type—unfortunately as my example shows—can differ depending on the conformances of its parameters in the context where it was formed, which is… troublesome… but unavoidable as long as you don't have global coherence. In that case trying to cast to the concrete type would fail if the conformances don't match those you'd get in the local context.

It also would make it so that existential values are potentially semantically different even if the type, value, and statically captured conformances are identical

I must be missing something. In my world, It's only the captured conformances that can distinguish them if the type and value are the same.

if you're going to encourage multiple conformances,

Seems to me that whether it's encouraged or not makes little difference to Swift's situation as long as Swift doesn't have global coherence.

it would be better overall not to provide the attractive nuisance of global dynamic conformance lookups, and encourage instead language features that reliably capture and propagate needed conformance information at point of use.

I'm afraid I can't imagine what “capture and propagate needed conformance information at point of use” would mean. Care to elaborate?

20

OK then! That might give you the least surprising behavior overall, but I can still imagine cases where a user tries to extend your system by introducing their own protocol and conformances, and then trying to cast out the conformances to that protocol that were unknown from the context that the existential was formed in. It also seems like you'd have to reify and capture a lot of context metadata that might not ever be used since you don't know at the point of erasure what casts might be done.

Instead of throwing away the static conformance information and dynamically recovering it, represent the conformances you conditionally need in the data types you use. Instead of an Any, you could have an enum { case p(any P), q(any Q) } (or if you want to get fancier than Swift, add GADTs so you can have generic cases likeenum { case p<T: P>(T), q<T: Q>(T) }). Alternatively, protocols could have up-front optional requirements like protocol PQ where Self :? P, Self :? Q, so that dynamically querying whether a PQ conforms to P or Q is a local query of the conformance rather than a context-dependent or global lookup.

1 Like