A singleton type is not a subtype of its refined type

[LPTK]

Minimized code

class A:
  val x: AnyRef

@main def m: Unit =
  val a = new A
  a.x: a.x.type // ok
  a: A { val x: a.x.type } // nope

https://scastie.scala-lang.org/0PCX1TY0TxCO1Voo5NohLQ

Output

Found:    (a : A)
Required: A{x: (a.x : AnyRef)}

Expectation

Should type check. This is crucially needed for more advanced dependent-typing use cases.

[odersky]

@LPTK Do you think you can give this a go?

[LPTK]

Ok I'll try to have a look when I have some time (in the coming weeks). Also, I seem to remember that this used to work in a previous version of Dotty.

[LPTK]

Ok, so I had a look and apparently I misremembered – this never worked in Dotty, even as far back as the first RC versions.

I believe the problem is that TypeComparer accesses the underlying type of the singleton type

https://github.com/lampepfl/dotty/blob/eb7b6326bc560830cff998c70592f0da6026b01f/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L787

and that returns the denotation's info field.

What could be done would be to return a refinement/intersection of this type info with the precise types of the singleton's members. In our example, this would be A { val x: a.x.type }.

However, this goes well beyond the type of changes I'm comfortable doing in Dotty, and I predict that a naive approach would break lots of things and potentially degrade performance, so it'd have to be done very carefully and with better knowledge of Dotty's inner workings than I have.