Debug Equality

[jtristan]

Fixes #1427 #1429

[jtristan]

• The two soundness bugs addressed by this PR are due to types incorrectly determined to potentially support equality, when they definitely cannot.
• In essence, the fix consists in making the test of equality non-support more stringent, as follows

1. If a datatype D refers to an opaque type that has not been declared to support equality, then D cannot support equality
2. The test is made recursive, considering both type operators and type operands

• For this fix to be complete, we also needed to update the calculation of the datatype graph so that it contains edges not only for type operators, but also for type operands.

[cpitclaudel]

This is a great improvement but a few things are still missing.

First, the check is a bit too strict: not all type parameters participate in equality, and hence not we do not need to check for equality (or add a dependency edge) between all type parameters. Your code rejects this, but I think it should be accepted?

type DoesNotSupportEq = int -> int
type AlwaysSupportsEq<A> = int
datatype SupportsEqDespiteParameter =
  SupportsEq(a: AlwaysSupportsEq<DoesNotSupportEq>)
type T_SupportsEqDespiteParameter(==) =
  SupportsEqDespiteParameter

On the other hand, the check is not strict enough wrt opaque types, because it does not skip past subtype constraints. Your code accepts this, but I think it should be rejected:

type foo
type foo' = f: foo | true witness *
datatype NeverEq' = NeverEq'(f: foo')
type T_NeverEq'(==) = NeverEq'

I believe this PR covers the same issues as #2066, so it would be good to see what is done there (and probably import the tests, too).

In particular, I think you may want to use the NecessaryForEqualitySupportOfSurroundingInductiveDatatype field of type arguments, but only in the case where the datatype is marked as ConsultTypeArgs.

[cpitclaudel]

I've gone through the code, but I don't understand everything fully yet. In particular:

• I'm puzzled by the loop on the type arguments of the original type inside the loop on the type arguments of the construct's argument,
• I'm confused by the use of AsRedirectingType, which is an internal property that I'm not sure we should be using here.
• I don't fully understand why we're computing whether a type definitely can't support equality (instead of possibly can't support equality / definitely supports equality)

[cpitclaudel]

Following up on my confusion, here's a program that still crashes in the current implementation:

class C<T> {}
datatype Pair<T, Q> = P2(T, Q)
type S<T, Q> = Pair<C<T>, Q>
datatype DS<T, Q> = DS(s: S<T, Q>)
type Final(==) = DS<int, int -> int>

function method MakeId(u: int): int -> int { x => u }

method Main() {
  var c := new C<int>;
  var f := MakeId(0);
  var g := MakeId(0);
  assert f == g;
  var ds0 := DS(P2(c, f));
  var ds1 := DS(P2(c, g));
  if (ds0 != ds1) {
    assert false;
    print 1 / 0;
  }
}

[jtristan]

To give some context, the goal of this PR is not to fix all know issues with the equality support. For example, I am not trying to address #2070. The goal is only to address some issues such as #1427 or #1429, where the problem is that the existing code that filters out datatypes that are known for sure not to support equality is too weak. It is possible that it is not overall the best approach to first filter out such datatypes, but my goal has not been to rethink the equality support determination entirely, only to fix errors in the existing one.

[jtristan]

I've gone through the code, but I don't understand everything fully yet. In particular:

• I'm puzzled by the loop on the type arguments of the original type inside the loop on the type arguments of the construct's argument,

As you should, it was an error.

• I'm confused by the use of AsRedirectingType, which is an internal property that I'm not sure we should be using here.

I do this to access the type parameters of the underlying type definition, but I will try to see if there is a better way to do this.

• I don't fully understand why we're computing whether a type definitely can't support equality (instead of possibly can't support equality / definitely supports equality)

CF other comment on scope of this PR

[jtristan]

It was decided not to pursue with this PR and that #1427 #1429 and #2070 should all be solved at once by determining what the precise rules should be for equality support and then implementing these rules as part of the supportEquality method.