Shadowing conformance is unsound?

[kyouko-taiga]

I think this program demonstrates that shadowing conformance with the semantics we currently envision is unsound:

trait P { type E }
conformance Int: P { typealias E = Self }

typealias X<T: P> = {P, P.E}

let g: X<Int> = (0, 0)

public fun main() {
  conformance Int: P { typealias E = String }
  let h: X<Int> = (0, "empty")

  let x: String = h.1 // OK
  let y: String = g.1 // This is awkward
}

I think we can fix this problem by saying that types have a scope which can play a role in their equivalence relationship. So X<Int> at file scope and X<Int> in main are not equivalent because they capture different conformances in their respective scope.

For the sake of sanity, I think we should further demand that a shadowing conformance be a refinement of the conformance it shadows. That way, a conformance cannot invalidate positive deductions that can be made outside of its scope. In the above example, that would mean the nested conformance is illegal.

Or ... we could ban conformance shadowing. AFAICT, it's not the reason why we wanted scoped conformances.

[dabrahams]

I don't see why you say it's unsound. Making the final line legal is not the semantics I envisioned. In my world, g has a different type from h. Their types are, after all, just aliases.

[dabrahams]

I've made this argument before: nested scopes should act the same whether the declarations in them are conformances or something else. There's nothing particularly tricky about this shadowing AFIACT.

[kyouko-taiga]

This is an "ought" argument.

• Are you disputing the fact that my example is confusing?
• If you aren't, what concrete example do you think justifies tolerating this source of confusion?

I don't mind making exceptions to a rule if I think the rule might be harmful without offering benefits other than "being the rule".

[nickpdemarco]

I don't think the example is confusing. If we know that we capture the relevant conformances at the declaration site, and we know more "recent" conformances shadow prior ones, it's clear that g and h have different types.

For the sake of sanity, I think we should further demand that a shadowing conformance be a refinement of the conformance it shadows.

What insanity is this preventing? As a developer, if I hit this compiler error (cannot convert Int to String), the utility I'd want is a typeof() operator that let me inspect g, which includes the conformances (ideally with file and line number info) it captured.

[kyouko-taiga]

Without conformance shadowing, we can look at the definitions of x and y and conclude that both have the "same type" in the sense that anything that holds true for x also holds true for y (except negative predicates). Both y and y are annotated with X<Int> and neither X nor Int has been shadowed in any of the scopes exposed their respective declarations. So we don't need a lot of context to make this determination, only the definition sites of X and Int.

Conformance shadowing dramatically increases the size of this context because it essentially says that the API of a type for a specific use can be modified in any scope exposed to that use. As a consequence, we have to consider every exposed scope for every type occurring in a type expression. In the example, that means the definition sites of X and Int as well as the local scope of main. In more complex examples, we could have tall stacks of scopes to consider, including scopes "bridged" by conformance, with possible conditional clauses brought in the mix.

trait P { type E }
conformance Int: P { typealias E = Self }
typealias X<T: P> = {P, P.E}

type A<Y> {
  fun foo() -> X<Int>.E {
    // What is the type of `X<Int>.E` here?
  }
}

extension A where Y: Int {
  conformance Int { typealias E = String }
}

My claim is that, though it can be made sound, this feature introduces a lot of complexity for use cases that have yet to be presented.

Without shadowing, nested conformances can be seen as only being allowed to "add" information to a type's API without ever contradicting previous facts. My point with restricting shadowed conformance to only those that are refinements is to uphold this property.

[kyouko-taiga]

Dave convinced that the complexity is justified. Here is a compelling example:

Assume I have written this deep inside a helper function in large library:

fun helper(_ x: UInt64) -> Optional<Int> {
  conformance UInt64: Collection {
    typealias Element = Bool
    ...
  }
  return x.first_index(of: true)
}

Assume someone later writes this conformance in a scope exposed to helper(_:) but otherwise unrelated:

conformance UInt64: Collection {
  typelias Element = UInt8
  ...
}

If conformance shadowing is banned, this new definition breaks the code in helper(_:).