unsound and non-transitive subtyping behavior with qualified types

[jvasileff]

Given an interface I and a nested interface I.J, it's possible to define a type A.B.C which satisfies I.J as both <A of I>.<C of J> and <A.B of I>.<C of J>.

This is possible when

• A, A.B, and A.B.C extend ASup, ASup.BSup, and ASup.BSup.CSup respectively
• A and A.B both satisfy I
• ASup.BSup does not satisfy I
• A.B.C and ASup.BSup.CSup both satisfy I.J

If I has type parameters, the two supertypes I.J may differ.

Two problems occur in 1.3.4-SNAPSHOT:

• The typechecker doesn't require A.B.C to refine I.J's members to properly satisfy the requirements of <A.B of I>.<C of J>. This can result in unsound behavior.
• Transitive subtyping is violated; A.B.C can be widened to ASup.BSup.CSup which can be widened the (generic) type that correspends to <A of I>.<C of J>, but A.B.C cannot be widened to <A of I>.<C of J> directly.

Sample code for 1.3.4-SNAPSHOT (the behavior in 1.3.3 is slightly different):

interface I<out T> {
    shared interface J {
        shared formal T getT;
    }
}

class ASup<T>(T t) satisfies I<T> {
    shared default class BSup() {
        shared default class CSup() satisfies J { // J's outer is ASup<T>
            shared actual T getT => t;
        }
    }
}

class A<T>(T t) extends ASup<T>(t) {
    shared class B<U>() extends super.BSup() satisfies I<U> {
        shared class C() extends super.CSup() satisfies J {} // J's outer is B<U>
    }
}

shared void run() {
    A<String>.B<Integer>.C abc = A<String>("x").B<Integer>().C();
    ASup<String>.BSup.CSup abcSup= abc;

    noop((abc of I<Integer>.J).getT of Integer); // Assigning a String to an Integer!
    noop((abcSup of I<String>.J).getT of String);  // ok

    noop((abc of ASup<String>.BSup.CSup) of I<String>.J); // ok
    noop( abc of I<String>.J); // error (subtyping is not transitive)
    // error: specified type does not cover the cases of the operand expression: 'I<String>.J' does not cover 'A<String>.B<Integer>.C'
}

[jvasileff]

I'm not sure the ability to "skip" outer types when satisfying a nested type (e.g. allowing CSup satisfies J despite BSup being in the way) is worth the typesystem and backend complexity, although maybe I'm missing some obviously useful example.

Without this "skipping", inner classes would only ever have a single outer capture that would be applicable for all supertypes that are nested types, and a conceptual Outer type would exist (as envisioned by @Zambonifofex in https://gitter.im/ceylon/user?at=5a673dd298927d57452691ba), which would simply be the qualifying type.

(Edit: actually, I suppose a change to the subtyping rules would also be required to support @Zambonifofex's Outer type)