Dotty: Cant use compiletime.ops.any.== with String when type of a value

[bishabosha]

minimized code

scala> import compiletime.ops.any._

scala> summon["" == "" =:= true]                                                                                        
val res1: true =:= true = generalized constraint

scala> val t: "" == "" = true
1 |val t: "" == "" = true
  |       ^
  |       Type argument ("" : String) does not conform to upper bound AnyVal 
1 |val t: "" == "" = true
  |             ^
  |       Type argument ("" : String) does not conform to upper bound AnyVal 

expectation

EDIT: the second example behaves according to its definition of type ==[X <: AnyVal, Y <: AnyVal] <: Boolean. However it should behave like the first. The type signature should be changed so that t can be typed

[smarter]

Comparing string literals is a legitimate thing to do, so can't this be fixed by changing the signature of ==to type ==[X <: Singleton, Y <: Singleton] ?

[bishabosha]

what would you say for this case, is the left side of =:= meant to be reduced first?:

scala> import compiletime.ops.int._

scala> class Foo
// defined class Foo

scala> summon[Foo * Foo =:= 0]
1 |summon[Foo * Foo =:= 0]
  |                       ^
  |Cannot prove that Foo * Foo =:= (0 : Int)..
  |I found:
  |
  |    <:<.refl[Nothing]
  |
  |But method refl in object <:< does not match type Foo * Foo =:= (0 : Int).

[smarter]

Honestly no idea, but that's a separate problem from getting == to work with string which is what https://github.com/lampepfl/dotty/issues/8721 was about, and it was closed in favor of this issue.

[bishabosha]

updated the context

[MaximeKjaer]

Singleton might also be overly restrictive, as it then doesn't allow for String == String to be modeled. But it may allow for (String & Singleton) == (String & Singleton), so perhaps that's equivalent?

If the parameter type bounds change to Singleton, it could make sense to change the result type of the operation to Singleton as well (e.g. Boolean & Singleton for ==).

[smarter]

Yeah, so we could also just have no bounds at all if that's simpler.

[soronpo]

It's better to have no bounds at all in this context, or to change == from any package to string and int, etc. with the proper bounds. So we will have int.== and string.==.

[soronpo]

It is my intention to update the singleton-ops library to dotty, so it will take of combining generic == for all the various operation types using match type.

[MaximeKjaer]

Moving them to type-specific subpackages means that we lose the ability to do 1 == "1". I don't know how useful that is in the first place though, as you're guaranteed that constants of different types are not equal, so perhaps that's a trade-off worth making.

[MaximeKjaer]

I actually thought String would be a subtype of AnyVal when I wrote those bounds. So no type bounds is also fine by me. It would fit the package name of ops.any, and the semantics are preserved when you apply a compiletime op with something else than a primitive singleton type (i.e. the type is not folded in those cases).

[soronpo]

Moving them to type-specific subpackages means that we lose the ability to do 1 == "1"

I don't think that is useful, but again in singleton-ops I will be able to do

type ==[L, R] <: Boolean = (L, R) match {
  case (Int, Int) => int.==[L, R]
  case (String, String) => string.==[L, R]
  case (Int, String) => string.==[string.ToString[L], R]
}

[smarter]

@MaximeKjaer Can you take care of making a PR for this ?

[MaximeKjaer]

Yep, no problem. I'll make a PR later tonight.

[noelwelsh]

I have implemented most of a fix, which may be useful:

https://github.com/noelwelsh/dotty/tree/bugfix-singleton-ops-8392

The commit comment details what I have done. I think the most important part of my change is what I have done to the tests. As far as I can tell from the Dotty documentation and my own experiments the existing tests were not actually performing any testing. Which is to say the test would pass regardless of the type tests succeeding or failing.

[smarter]

@noelwelsh

The tests were in the neg directory without a check
file so it was irrelevant if they compiled or not

Dotty's testing infrastructure looks for // error marker at the end of lines in neg tests and use that to verify which lines produced an error.

[noelwelsh]

I see. That would explain why my tests are failing.

[MaximeKjaer]

It seems to me that there is something slightly broken about how errors are handled in compiletime ops. Here is the example from #8271 that fails because the bounds of == are AnyVal:

import scala.compiletime.ops.any._
val eq3: "1" == "1" = true
// -- [E057] Type Mismatch Error: tests/neg/singleton-ops-any.scala:2:9 -----------
// 2 |val eq3: "1" == "1" = true
//   |         ^
//   |       Type argument ("1" : String) does not conform to upper bound AnyVal
// -- [E057] Type Mismatch Error: tests/neg/singleton-ops-any.scala:2:16 ----------
// 2 |val eq3: "1" == "1" = true
//   |                ^
//   |       Type argument ("1" : String) does not conform to upper bound AnyVal
// 2 errors found

However, it seems that the type-level constant fold still is taking place, as assigning false to eq3 raises an error:

import scala.compiletime.ops.any._
val eq3: "1" == "1" = false
// -- [E007] Type Mismatch Error: tests/neg/singleton-ops-any.scala:2:22 ----------
// 2 |val eq3: "1" == "1" = false
//   |                      ^^^^^
//   |                      Found:    (false : Boolean)
//   |                      Required: (true : Boolean)
// 1 error found

In fact, if there is another type mismatch error in the file, the fact that == is applied with arguments that don't match the bounds isn't even reported:

import scala.compiletime.ops.any._

val eq2: 1 == 2 = true
val eq3: "1" == "1" = true
// -- [E007] Type Mismatch Error: tests/neg/singleton-ops-any.scala:4:20 ----------
// 4 |  val eq2: 1 == 2 = true
//   |                    ^^^^
//   |                    Found:    (true : Boolean)
//   |                    Required: (false : Boolean)
// 1 error found

With no type bounds on the parameters of == this should in essence be "fixed". But it does seem like that fix is hiding a bug somewhere else.