Equalities to be rejected: Double, functions, allocatable non-case classes, type vars

[vkuncak]

Whereas we reject some uses of equality, such as https://github.com/epfl-lara/stainless/issues/710 we do not reject this example and instead treat it as if A was a case class, leading to proving assertion that fails at runtime:

object Test:
  class A

  val x1 = new A
  val x2 = new A
  val ok = x1 == x2

  @main
  def testEq =
    assert(x1 == x2)

end Test

I propose that we reject this for now. Allowing it would require at least a minimal global state of an allocator (a counter) and is perhaps best handled along with some notion of heap references.

[vkuncak]

Maybe a similar check should be done as for https://github.com/epfl-lara/stainless/issues/710 (except that we don't want this in non-ghost code either). When do we even want non-case classes to start with?

[mario-bucev]

Note that this snippet should be rejected as well, but isn't:

object i1483c {
  case class A(l: BigInt => BigInt)

  def test: Unit = {
    val a1 = A(_ + 1)
    val a2 = A(_ + 1)
    // true for Stainless, but false at runtime
    assert(a1 == a2)
  }
}

So we could check for classes whose == align with Stainless. In the above case, we would not allow the assertion, unless we import StaticChecks.

However, this is not sufficient due to the presence of type parameters...

object i1483f {
  case class Wrapper(l: BigInt => BigInt)
  case class A[T](t: T)

  def test: Unit = {
    val a1 = A(Wrapper(_ + 1))
    val a2 = A(Wrapper(_ + 1))
    // true for Stainless, but false at runtime
    assert(a1 == a2)
  }
}

[vkuncak]

Note that also this assertion fails during execution,

    val naan = Double.NaN
    assert(naan == naan)

hence we should similarly disable things that flow into Double, much like function types.

To account for type parameters, we can use @noEq annotation. The noEq types and rules for them are defined as follows:

• Double is noEq
• A => B is noEq
• a class that is not a case class is noEq (due to new A != new A)
• a type variable marked by @noEq is a noEq
• when calling a generic function the type parameters annotated with noEq may only be instantiated with noEq types
• for every expression p==q, the types of p and q must be the same and are not allowed to be noEq

[vkuncak]

Note that the reason we have equality by default and opt into its absence with noEq, in contrast to ML and Haskell is that we want to have equality by default and we want to put syntactic burden on those evil non-equality types. This is analogous to how we treat @mutable.