Scala Singleton Types

Question
#1

I have a function to witness type equivalence:

def typeEq[A, B](a: A, b: B)(implicit ev: A =:= B) = println("happy")
typeEq: [A, B](a: A, b: B)(implicit ev: A =:= B)Unit

It fails to check the following two different singleton types:

class X
val a = new X; val b = new X
val aa:a.type = a; val bb:b.type = b
typeEq(aa, bb)

However, if I write this way, the compiler works fine:

class X
val a = new X; val b = new X
type atype=a.type; type btype=b.type
val aa:atype = a; val bb:btype = b
typeEq(aa, bb)

<console>:15: error: Cannot prove that atype =:= btype.
   typeEq(aa, bb)
         ^

Appreciate your help.

#2

val a = new X is not a singleton. Use final val a = new X or object a extends X

#3 
scala 2.13.0-M5> def typeEq[A, B](a: A, b: B)(implicit ev: A =:= B) = println("happy")
typeEq: [A, B](a: A, b: B)(implicit ev: A =:= B)Unit

scala 2.13.0-M5> class X
defined class X

scala 2.13.0-M5> val a = new X; val b = new X
a: X = X@2cd62003
b: X = X@61ab89b0

scala 2.13.0-M5> val aa:a.type = a; val bb:b.type = b
aa: a.type = X@2cd62003
bb: b.type = X@61ab89b0

scala 2.13.0-M5> typeEq(aa, bb)
happy

scala 2.13.0-M5> def typeEq[A<:Singleton, B<:Singleton](a: A, b: B)(implicit ev: A =:= B) = println("happy")
typeEq: [A <: Singleton, B <: Singleton](a: A, b: B)(implicit ev: A =:= B)Unit

scala 2.13.0-M5> typeEq(aa, bb)
                       ^
                 error: Cannot prove that aa.type =:= bb.type.

scala 2.13.0-M5> typeEq(a, b)
                       ^
                 error: Cannot prove that a.type =:= b.type.

To see what is inferred in REPL, use // print<TAB> completion:

scala 2.13.0-M5> def typeEq[A, B](a: A, b: B)(implicit ev: A =:= B) = println("happy")
typeEq: [A, B](a: A, b: B)(implicit ev: A =:= B)Unit

scala 2.13.0-M5> object x extends X; object y extends X
defined object x
defined object y

scala 2.13.0-M5> typeEq(x,y)
                       ^
                 error: Cannot prove that x.type =:= y.type.

scala 2.13.0-M5> typeEq(x,y) //print
   typeEq[x.type, y.type](x, y) // : (implicit ev: x.type =:= y.type)Unit

scala 2.13.0-M5> typeEq(a,b) //print
   typeEq[X, X](a, b) // : (implicit ev: X =:= X)Unit

It’s a small mystery why it infers x.type for an object. Objects don’t have an explicit type, which is why they don’t make good implicit values.

#4

Thanks for your explanation.
I still do not understand why atype and a.type are not inferred the same, they are a type alias and a type.

#5

I think most of the time the compiler tries to dealias as rarely as possible. In this case that strategy seems to have the side-effect that the singleton types are no longer widened automatically.

#6 
class X
def typeEq[A, B](a: A, b: B)(implicit ev: A =:= B) = println("happy")
object x extends X
object y extends X

OK, so x and y are distinct objects of different types that have a common supertype (a base class X).
However, they are NOT values of the same type.
x is an object, so it has type x.type as dictated by the language spec.
Analogous for y, which has type y.type.

typeEq(x, y) shouldn’t compile.

Objects don’t have an explicit type, which is why they don’t make good implicit values.

This is a confusing statement to me. objects don’t have an explicitly specified type because they cannot have a type annotation. This is true. But they have a singleton type subtyping their template, which requires typechecking to compute. This is a perfectly reasonable (albeit not explicit) type.

Because scalac doesn’t do typechecking for not-yet-typed values in the current file below the point in the file where an implicit is required (this is an old, open compiler bug), this makes implicit objects less than desirable. But that’s a compiler bug.