Path dependency on trait/class-parameters in class parent uses constructor argument instead of member

[b-studios]

Using path-dependent types as type parameters fails. The following example

class A
trait Bar[X] {
  // same for `val foo: X = ???`
  def foo: X = ???
}
// same for `class Foo(...)...`
trait Foo(val a: A) extends Bar[a.type] {
  val same: a.type = foo
}

gives a type error:

[error] required: A(Foo.this.a)
[error]     val same: a.type = foo

[Blaisorblade]

I played a bit with this time ago. The problem is that there are two distinct as, the constructor parameter and the field, and a priori they are not given the same singleton type (tho of course they could). And when the super call is typechecked, a refers to the constructor argument, not the field, which matches the runtime semantics. When I tried changing that, I ended up producing a super call that accessed the field instead of the constructor parameter, which failed the bytecode verifier.

I have more extensive notes somewhere on what I tried and what else I thought one might try, I hope I can get to them.

[b-studios]

Hey, are there any new insights on this problem?

[b-studios]

Just to make that clear, the problem not only occurs with singleton types, but of course also extends to type members as in:

class A { type M }
  trait Bar[X] {
    // same for `val foo: X = ???`
    def foo: X = ???
  }
  class Foo(val a: A) extends Bar[a.M] {
    val same: a.M = foo
  }

which in 0.17.0-bin-20190622-b5a6963-NIGHTLY gives

[error] 187 |    val same: a.M = foo
[error]     |                    ^^^
[error]     |                    Found:    a.M
[error]     |                    Required: Foo.this.a.M

[b-studios]

@Blaisorblade I don't understand why you would change the runtime semantics (the bytecode modifications you mentioned above).

they are not given the same singleton type (tho of course they could)

Is there a reason why (immutable) field and constructor argument are not given the same singleton type?

[Blaisorblade]

Just to make that clear, the problem not only occurs with singleton types, but of course also extends to type members as in:

Yeah, that's indeed the natural consequence.

@Blaisorblade I don't understand why you would change the runtime semantics (the bytecode modifications you mentioned above).

Let's ignore that — I tried a certain fix, and it had the wrong effects. IIRC, I changed some references to a to refer to this.a instead of the argument a, and that change also affected the bytecode.

Is there a reason why (immutable) field and constructor argument are not given the same singleton type?

Because you'd need to write special code for that. Constructor arguments and fields are different variables. After val x = ...; val y = x, you get different singleton types for x and y, unless y's type mentions x. The scenario here is the same, as the initializer copies a variable (this.x = x), except that you cannot give this.x type x.type. Maybe the type of x should transform from T to T & this.x.type, but that's odd before this.x is initialized. And you don't want that to be visible at the constructor call site, but only when typechecking the class body?
Either choice would also require adding singleton types that aren't declared, something we don't do. And that'd have to happen locally, which is also hard — most of Dotty assumes everything has the same type everywhere, except for GADT bounds.

I now wonder if/how this relates to "double vision" or is distinct — a tricky problem that showed up when implementing opaque types, and is known in the literature (and solved in Dreyer MixML papers, and others).

Fixing this would probably require a dedicated type rule to use in constructors. And I don't know how easy it'd be to make that algorithmic.

Now, maybe this still takes Martin an afternoon, but dunno.

[b-studios]

And you don't want that to be visible at the constructor call site, but only when type checking the class body?

Actually, why not? Would this cause unsoundness or problems with type inference?

trait B { type M }
class A(val b: B)
val b = new B { type M = Int }
val a = new A(b)
val x: a.b.M = 42

Of course the above does not type check for very similar reasons. It again comes down to:

adding singleton types that aren't declared, something we don't do.

Expressing a similar scenario with functions

def f(b: B) = b
val b = new B { type M = Int }
val b2 = f(b)
val x: b2.M = 42

obviously shows the same behavior, since no singleton type is inferred as result type of the function. From an engineering point of view we don't want that since this leaks implementation details, right? So maybe the same argument also holds for the constructor case?

However, the function can easily be changed to return a singleton type, while for the constructor case we have to go down a much more involved path:

trait B { type M }
class A[BB <: B & Singleton](val b: BB)
val b = new B { type M = Int }
val a = new A[b.type](b)
val x: a.b.M = 42

[Blaisorblade]

And you don't want that to be visible at the constructor call site, but only when type checking the class body?

Actually, why not? Would this cause unsoundness or problems with type inference?

What I mean is: If we replaced class A(val b: B) by class A(val b: B & this.b.type), you couldn't construct A. Writing val z = new A(y) would require y: z.b.type, which seems to require a bit too much circularity/time travel 😅 . Do I miss something? If so, can you spell out more what you have in mind, on the original example?

I've looked a bit at your example, but it doesn't share the problematic circularity. Maybe it should be a separate issue?

Re double vision, see page 7 of https://people.mpi-sws.org/~rossberg/mixml/mixml-icfp08.pdf, for why I think the problem is at least analogous.

[b-studios]

I am way too far away from the compiler internals to make precise statements here, but I would have actually proposed it the other way around. Something like class A(_b: B)(val b: _b.type = _b) -- but then the type of b refers to a non-private value.

Oh, actually. For the original example, this is somewhat a workaround:

trait Foo(val _a: A)(val a: _a.type = _a) extends Bar[a.type] {
  val same: a.type = foo
}

I guess I am using the constructor argument in _a.type, specifying that the field will also have the very same type.

[Blaisorblade]

Something like class A(_b: B)(val b: _b.type = _b) -- but then the type of b refers to a non-private value.

Oh yeah, I also thought of that direction, but indeed that doesn't work as-is... but maybe somebody more expert could add code to simulate that, but only inside the constructor. IIRC I've even seen code doing similar hacks, but it's subtle.

Oh, actually. For the original example, this is somewhat a workaround:

trait Foo(val _a: A)(val a: _a.type = _a) extends Bar[a.type] {
  val same: a.type = foo
}

I guess I am using the constructor argument in _a.type, specifying that the field will also have the very same type.

Uh, can you use Singleton somehow? Something like

trait Foo[AT <: Singleton & A](val a: AT = _a) extends Bar[AT] {
  val same: AT = foo // easy
  // val same: a.type = foo //maybe needs a fix for #4583
}

Now, #4583 has also been open for a while, but it's maybe a bit easier to imagine a fix.

[b-studios]

Yes, I sometimes used Singleton for similar purposes. But in my codebase this blows up in size, since I easily have constructors with 3-10 different fields that need mentioning the singleton type in Bar.

[smarter]

The problem is that there are two distinct as, the constructor parameter and the field, and a priori they are not given the same singleton type (tho of course they could). And when the super call is typechecked, a refers to the constructor argument, not the field, which matches the runtime semantics.

I thought so too but that's not actually the case, the extends clause is typechecked in this context: https://github.com/lampepfl/dotty/blob/10526a7d0aa8910729b6036ee51942e05b71abf6/compiler/src/dotty/tools/dotc/core/Contexts.scala#L366 note in particular the comment:

     *  - At the same time the context should see the parameter accessors of the current class,
     *    that's why they get added to the local scope. An alternative would have been to have the
     *    context see the constructor parameters instead, but then we'd need a final substitution step
     *    from constructor parameters to class parameter accessors.

So the singleton type we see should really be this.a.type, however the subtype check did not go through for some obscure technical reason I think I've fixed: #6746

[Blaisorblade]

Ah, I remember I saw that code and considered trying to patch that — but it seemed far too complex for my knowledge level! @smarter thanks!!!

@b-studios can you please make sure to stress-test the PR, in particular with the original non-minimized code (if you have any)?

[b-studios]

Thanks @smarter for looking into it. @Blaisorblade I'm happy to stress test it and will report on the results here, later.

[b-studios]

I tested it on my codebase and it looks good to me 👍

I am now left with the (mostly) unrelated problem, that the following does not type check:

  val a: A = ???
  val a2: a.type = new Foo(a).same

Since the field is not refined to the singleton type per-se, a.type and Foo(a).same.type don't unify.
I know that the class Foo[AA <: A & Singleton](val a: AA) trick exists but it is very heavy weight (syntactically and conceptually).

Anyways: Thanks for fixing the current issue :)

[Blaisorblade]

Since the field is not refined to the singleton type per-se, a.type and Foo(a).same.type don't unify.

Ooh, that's where we'd try using new Foo { val a : outer.a.type = outer.a }, but that would be hard here. Would Scala 2 early definitions have helped? Worse, a fix for #5854 might interfere with:

// same for `class Foo(...)...`
trait Foo[AA <: A & Singleton] extends Bar[a.type] {
  val a: AA
  val same: a.type = foo // a.type might have bad bounds
}

[smarter]

@b-studios see #3920 for some related discussions.