Extraction troubles with `equals` methods

[mantognini]

object Test {

  case class A()
  def equals(a1: A, a2: A): Boolean = true // extracted as equals$0

  case class B()

  // def foo(a: A, b: B) = equals(a, b) // doesn't compile, good!

  case class Table() {
    def foo(a: A, b: B) = equals(a, b) // there's a typo but it still compiles. :(
    // The compiler understand this statement as:
    //    this.equals( (a, b) )
    // which is legal (although always false), instead of this:
    //    Test.equals(a, b)
    // which doesn't compile, as expected.
    //
    // Also, equals(a, a) yields the same error from stainless.
  }

}

At the moment (*), stainless yields the following error:

[ Error  ] foo$0 depends on missing dependencies: equals$1.
[ Debug  ] @method(Table$0)
[ Debug  ] def foo$0(a$16: A$30, b$13: B$20): Boolean = this.equals$1((a$16, b$13))
[Internal] Missing some nodes in Registry: equals$1

We should probably do something about this. The simplest solution would be to forbid having any function called equals. It's not the best but definitely the cheapest one to implement.

(*) using persistent_cache & options branches.

[jad-hamza]

Should we maybe distinguish between "equals" that can be freely redefined in Stainless, and the equality that corresponds to the semantics of Inox and the underlying SMT solvers?

[mantognini]

I think we should, especially considering the recent discussion you had with @samarion about lambda equality.