-
Notifications
You must be signed in to change notification settings - Fork 48
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Equalities to be rejected: Double, functions, allocatable non-case classes, type vars #1483
Comments
Maybe a similar check should be done as for #710 (except that we don't want this in non-ghost code either). When do we even want non-case classes to start with? |
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 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)
}
} |
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
|
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 |
Whereas we reject some uses of equality, such as #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:
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.
The text was updated successfully, but these errors were encountered: