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

4 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.

4 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?

2 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.

2 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.

2 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.

3 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.

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.

1 Like
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. Each of the distinct types with the same name (assuming conformances are not somehow visibly included in the name) can have a different dynamic type identifier value based on the mangled name it currently gets.

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