New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

problem with type comparison (`<:`) transitiveness when `.type` was used as upper-type-boundaries (`>:`) and then `|`-ed together #5878

Open
ibaklan opened this Issue Feb 8, 2019 · 0 comments

Comments

Projects
None yet
1 participant
@ibaklan
Copy link

ibaklan commented Feb 8, 2019

Problem was disclosed when I was making experiments with possible different implementations of HasThisType (As I can know from error messages direct |-ing of .type-types is prohibited, but taking into account possibility of definition of upper-bounded (>:) abstract types, one still can compose some quasi-|-ing of that .type-types which ends up with problems/inconsistencies - in particular <:-relationship transitiveness happen to be missing - automatic interference of constraints by transitiveness of <: does't work here)

Initially problem was found in following form (complete demonstrating snippet here)

    trait HasThisType {
      type ThisB >: this.type

      type ThisC1 >: ThisB
      type ThisC2 >: ThisB
      type ThisD >: ThisC1 | ThisC2
      type ThisD1 = ThisC1 | ThisC2

      def testThisTypeInner(): Unit = {
        val thisB: ThisB = this
        val thisC: ThisC1 = this
        // fails with "[E007] Type Mismatch Error"
        //val thisD: ThisD = this
        val thisDProven: ThisD = this : ThisC1

        // test with "pure" `|` of abstract types (without `>:`) gives the same result

        // fails with "[E007] Type Mismatch Error"
        //val thisD1: ThisD1 = this
        val thisD1Proven: ThisD1 = this : ThisC1
      }
    }

Here one could observe that this.type <: this.ThisB <: this.ThisD1 so taking into account transitiveness of <: one may expect that this.type <: this.ThisD1 - but "it doesn't" (compiler could not infer that relationship).
So that assignment val thisD1: ThisD1 = this treated as invalid, while "down-casting" this to ThisB for example, "resolves the problem", and val thisD1: ThisD1 = this : ThisB become compile-able again.

After looking closer to that problem it is clearly seen that transitiveness is broken only on the step
this.type <: ThisB, other relationship - like
ThisB <: ThisC1 <: ThisD1 <: ThisD works as expected (compiler easily infer that ThisB <: ThisD for example)

Other form of this problem (which one may immediately compose from previous one) could be formulated in terms of 2-wo separate val-s (like val foo1 and val foo2) and 2-wo upper bounded abstract types (like type Foo1ThisB >: foo1.type and type Foo2ThisB >: foo2.type)
Then demonstration snippet could look like following (complete snippet here)

    trait HasDoubleFooLike {
      val foo1: Any
      val foo2: Any

      type Foo1ThisB >: foo1.type
      type Foo2ThisB >: foo2.type

      type FooXThisB >: Foo1ThisB | Foo2ThisB
      type FooXThisB1 = Foo1ThisB | Foo2ThisB

      def testFooThisTypeInner(): Unit = {
        val fooLike1: Foo1ThisB = foo1
        val fooLike2: Foo2ThisB = foo2
        // fails with "[E007] Type Mismatch Error"
        //val fooXLike1: FooXThisB = foo1
        val fooXLike1Proven: FooXThisB = foo1: Foo1ThisB
        // fails with "[E007] Type Mismatch Error"
        //val fooXLike2: FooXThisB = foo2
        val fooXLike2Proven: FooXThisB = foo2: Foo2ThisB

        // test with "pure" `|` (without `>:`) gives the same result

        // fails with "[E007] Type Mismatch Error"
        //val fooX1Like1: FooXThisB1 = foo1
        val fooX1Like1Proven: FooXThisB1 = foo1: Foo1ThisB
        // fails with "[E007] Type Mismatch Error"
        //val fooX1Like2: FooXThisB1 = foo2
        val fooX1Like2Proven: FooXThisB1 = foo2: Foo2ThisB
      }
    }

Here again transitiveness is broken on step foo1.type <: Foo1ThisB and foo2.type <: Foo2ThisB so that
foo1.type <: this.Foo1ThisB <: this.FooXThisB and foo2.type <: this.Foo2ThisB <: this.FooXThisB - are OK.
But that could not be reduced to foo1.type <: this.FooXThisB and foo2.type <: this.FooXThisB - compiler fails to infer that, disregarding that it should directly follow from transitiveness of <: relationship.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment