Equatability of Nothing with types which are otherwise unequatable

[jcracknell]

I have been experimenting with strict equality in 3.0.2 and immediately ran into the issue where you cannot pattern match against Nil/None. I see the efforts to address this in 3.1.0 in 3e963c0 and 32a99fd, however I am not sure that this is the correct approach, as the following is still illegal:

class NotEquatable

List(new NotEquatable) match
  case Nil => ???

This can be addressed by instead adding the following givens permitting equating Nothing with any type regardless of the equatability of that type, on the basis that you could never actually invoke the equality test:

given canEqualNothingL: CanEqual[Nothing, Any] = CanEqual.derived
given canEqualNothingR: CanEqual[Any, Nothing] = CanEqual.derived

With this addition it appears you can remove the supplementary CanEqual.canEqual{Seq,Option} previously added to address matching Nil/None in the above-mentioned commits.

I will note that you do get this awkward behavior already present in 2.x:

??? == 42 // runtime error
42 == ??? // compile error, ambiguous overload

this could perhaps be addressed by adding an overload to Any, however I am uncertain of the viability of such an approach:

def equals(nothing: Nothing): Boolean = ???

[odersky]

Strict equality is not really set up to work with the current standard library. You can use it to experiment with your own types. The idea is that with enough experience gained we can do a better job on the next redesign of the standard library.

We need a lot more experiments with what the right givens for the various bits of equality would be. But I won't have the time to do it myself. But if others want to add new givens, run the community build and report back, that would be welcome!

[jcracknell]

@odersky after posting this I had the nagging thought that it should be possible to derive CanEqual for equatable types with Nothing, as CanEqual is contravariant. Indeed under 3.0.2:

scala> implicitly[CanEqual[String, Nothing]]
val res0: CanEqual[String, Nothing] = scala.CanEqual$derived$@7c6b997b

scala> given [A, B](using CanEqual[A, B]): CanEqual[Option[A], Option[B]] = CanEqual.derived
def given_CanEqual_Option_Option
  [A, B](using x$1: CanEqual[A, B]): CanEqual[Option[A], Option[B]]

scala> Option.empty[String] match { case None => "works" }
val res1: String = works

scala> implicitly[CanEqual[Int, Nothing]]                                                                          
-- Error:
1 |implicitly[CanEqual[Int, Nothing]]
  |                                  ^
  |          Values of types Int and Nothing cannot be compared with == or !=

So there is a real bug here in that synthetic CanEqual for primitives fails to consider Nothing as a possible subtype:

https://github.com/lampepfl/dotty/blob/cf600613d96e676136363fd0de8e31a2ff998408/compiler/src/dotty/tools/dotc/typer/Synthesizer.scala#L102-L114

[jcracknell]

I've opened an issue for synthetic CanEqual in #13739 so it doesn't get missed, however the question of whether or not Nothing should be equatable with any other type regardless of its equatability remains.

[SethTisue]

PR: #13828