datatype doesn't correctly compute equality-support

[tjhance]

In the following, T doesn't have equality support, so X shouldn't either:

type T

method m(t1: T, t2: T) {
  var x := t1 == t2; // correctly gives error
}

datatype X = X(t: T)

method m2(x1: X, x2: X) {
  var y := x1 == x2; // doesn't error but should
}

As far as I can tell, it only seems to apply to opaque types (e.g., if T is a datatype with a ghost field or something, then X will correctly compute that it doesn't have equality support).

[tjhance]

I should probably provide a little more context: the reason this came up is that I have an extern type (defined via C++) with no operator== defined. In the C++ backend, this results in compile errors. (Because when generating code for type X, it tries to call out to T's operator== which does not exit.) I think in the C# backend it falls back to object equality ("pointer equality") so fails silently.

This is inconsistent across the backends, and we should think about which is the desired behavior. Personally I'd argue that failing to compile makes more sense - I can't really think of any reason why falling back to pointer equality would make sense.

[cpitclaudel]

The issue here is that the test in https://github.com/dafny-lang/dafny/blob/b5ad10a2f184f966e9d621732b59ca1ebed324ab/Source/Dafny/Resolver.cs#L9683 is to weak: it only eliminates codatatypes, function types, and datatypes that are never equatable (e.g. those that contain ghost fields. It does not check that datatypes that may support equality depending on their parameters indeed do support equality, and it doesn't check for other types, like opaque types.

[cpitclaudel]

I will merge #1429 and #2070 with this issue. There's no obvious way to fix any one of these without fixing the two others, so it's much better to fix all three at once and have the discussion in a single place.