Type mismatch error involving type member

[pweisenburger]

When compiling the following code:

trait C[T] { type U }

object C { type Aux[X, Y] = C[X] { type U = Y } }


def a: C[Int] { type U = Int } = ???

def b[T](c: C[T]): C[T] { type U = c.U } = ???


def test[T, U](c: C.Aux[T, U]) = ???

test(b(a))

Dotty produces the following compiler error:

[E007] Type Mismatch Error
test(b(a))
     ^^^^
     found:    C[Int]{U = Int}
     required: C'.Aux[Int, U']

     where:    C  is a trait
               C' is a object
               U  is a type in trait C with bounds 
               U' is a type variable which is an alias of (param)1#U

There should be no type mismatch. Splitting the last expression like val x = b(a); test(x) works.

[odersky]

It seems that the refinement is not taken into account for type inference, but since there are so many different difficulties at play (generics, refinements, dependent methods) it's hard to tell. I don't think I have the time to track this down. If someone else wants to give it a go, please re-open.

[pweisenburger]

I recently went back to this and tried with the current version of Dotty. The bug still remains. However, I was able to simply the code a bit further:

trait C { type U }
trait B[T]

def a: C { type U = Int } = ???
def b(c: C): B[c.U] = ???

def test[T](c: B[T]) = ???

test(b(a))

This code yields the error message:

1 |    test(b(a))
  |         ^^^^
  |found:    test.B[Int]
  |required: test.B[T]
  |
  |where:    T is a type variable which is an alias of (test.C & Singleton)#U

I'm aware that the code uses some of the more advanced Scala features, but nothing really experimental. So my understanding is that they are supposed to be supported by Dotty. Especially for the simplified example, I think it's pretty obvious that the code should compile. Maybe we could leave the issue open to keep track of this bug?

Further, in case the argument c of test is defined implicit (which it was in my use case when I ran into this bug originally), it's even more difficult to isolate the problem and you don't want to manually write val x = b(a); test(x) to work around this issue as suggested initially (because then, c should be resolved implicitly). This also is an issue, which is hard to solve, when migrating/cross-compiling from Scala 2, since Scala compiles the code without any problems. And I don't think Scala code like this is too esoteric that you won't find it in real-world projects.

[Blaisorblade]

stat:revisit is meant as "we should look at it", but I agree this should be debugged a bit more; your updated example is helpful.

But I've taken a look at the new example and it's very non-obvious that it should compile, because you're trying to use type members of a def. That's why adding a val works. I'm not even sure sound to relax the rules to allow this: it might be, because the type member is an alias, but what if a is overriden to something with inconsistent bounds? I suspect that's fine but I'm not sure. Making a final prevents that, but doesn't convince Dotty.
The more interesting question might be "what if a.U aliases T but T has in turn inconsistent bounds? Not the case here, but only because we alias Int.

I first suspected this would involve modifying TypeAssigner.safeSubstParam to preserve more information during widening, but in fact the only problem is in realizability checking (when working on top of #4036, which I used in all these tests).

• 1st hint: in your error, T aliases (C & Singleton)#U, which isn't known [BTW, the test. in your error is spurious and confused me, I also test different code than I post but I try to make errors match].
• second: since Martin suggested this was a type inference issue, I tried to fix it by specifying the type argument to test (which you need to do to triage such issues).
  1. The obvious solution a.U gives a type error because a is unstable — right now, when PostTyper.PostTyperTransformer.transform runs into a.U it checks that a is realizable, that is, that all selections on a are safe. That'd need to change if we find out it's sound to allow a.U when U is an alias even on unrealizable a.
  2. (C { type U = Int})#U works but I'm not sure type inference can handle this.
  3. However, Int works, and that's enough to make the bug worth leaving open: we reject a.U if written in the source, but the compiler is apparently still able to reduce it to Int...

trait C { type U }
trait B[T]

def a: C { type U = Int } = ???
def b(c: C): B[c.U] = ???

def test[T](c: B[T]) = ???

// test(b(a))
//def res1 = test[a.U](b(a)) // fails
def res2 = test[(C { type U = Int})#U](b(a))
def res3 = test[Int](b(a))

[pweisenburger]

Thanks for the detailed comments!

But I've taken a look at the new example and it's very non-obvious that it should compile, because you're trying to use type members of a def. That's why adding a val works. I'm not even sure sound to relax the rules to allow this: it might be, because the type member is an alias

That clarifies the problem for me. Since U is an alias (and from what you wrote, it seems Dotty can figure this out), I also thought, there shouldn't be a problem.

Not the case here, but only because we alias Int.

Just as a side note: Scalac also accepts the code when we leave U abstract (def a: C { type U } = ???). That is not to say it has to be correct; could also be a scalac issue.

BTW, the test. in your error is spurious and confused me, I also test different code than I post but I try to make errors match

My mistake. I overlooked test. when copying the error message. It shouldn't show up there, sorry.

the obvious solution a.U gives a type error because a is unstable

Note that also making a a val (val a: C { type U = Int } = new C { type U = Int }) does not work for the example.

we reject a.U if written in the source, but the compiler is apparently still able to reduce it to Int...

Right, I also expected that the compiler is able to dealias a.U and work with dealiased type (Int).

[Blaisorblade]

Just as a side note: Scalac also accepts the code when we leave U abstract (def a: C { type U } = ???). That is not to say it has to be correct; could also be a scalac issue.

I expect that falls under "Scala 2 unsoundness bugs fixed in Scala 3", see the blog posts for discussion (https://www.scala-lang.org/blog/2016/02/17/scaling-dot-soundness.html,
https://www.scala-lang.org/blog/2016/02/03/essence-of-scala.html).
IOW: in general e.U must be forbidden if e isn't stable (or in DOT, a value), but maybe it's safe when U is a type alias defined without only through "valid" types (not abstract members of e).

Note that also making a a val (val a: C { type U = Int } = new C { type U = Int }) does not work for the example

"Does not work" is too generic — "inference doesn't work, but a type argument does" is better.

trait C { type U }
trait B[T]

val a: C { type U = Int } = new C { type U = Int }
// final def a: C { type U = Int } = ???
def b(c: C): B[c.U] = ???

def test[T](c: B[T]) = ???

def res0 = test(b(a)) // only this fails, the rest succeeds.
def res1 = test[a.U](b(a))
def res2 = test[(C { type U = Int})#U](b(a))
def res3 = test[Int](b(a))

On one thing I wrote:

(C { type U = Int})#U works but I'm not sure type inference can handle this.

Just realized: Conceivably, Dotty could represent the type of a via a SkolemType around C { type U = Int }, to represent the SkolemType of that call.