scalaz
Singleton improvements
Convince Scalac that all instances of a typeclass or a proposition have the same singleton type. Could be crucial for associated types...
~~Convince Scalac that val x = ...; val y = x implies x.type = y.type.~~
Convince Scalac that val x = ...; val y = x implies x.type = y.type.
You just need to drop the widen for that — but if you extend it to template bodies, that will make val y = x part of the computed APIs and harder to change. And if you don't extend it to bodies, it will make val have context-dependent semantics.
I am fine with context-dependent semantics, but I would prefer x.type = y.type to be visible only within the scope / package / file / module. The second part of this issue is not really important and mostly just for convenience in some very rare cases, so let's just drop it.
IMO there's another thing to solve, which is making x.type#A equal Y#A when Y <: Singleton if x: Y. This is only a problem because of null; I think it's safe to assume that if you're using singleton types with type projections deliberately, null isn't likely a problem for you.
@edmundnoble Even better, make x.type = Y when Y <: Singleton if x: Y, which is stronger. I filed this as https://github.com/lampepfl/dotty/issues/4583 and https://github.com/scala/bug/issues/10905 (and it looks fixable on Dotty). Good points on null (speculation on Dotty in https://github.com/lampepfl/dotty/issues/4583#issuecomment-420875019).