Missing type-characteristic checks

[RustanLeino]

Dafny version

4.6.0

Code to produce this issue

datatype Pair<T(==)> = MakePair(0: T, 1: T) {
  function Same(): bool {
    this.0 == this.1
  }
}

method ReturnFalse() returns (b: bool)
  ensures !b
{
  var c := (2, ghost 5);
  var d := (2, ghost 6);
  assert c != d;
  b := MakePair(c, d).Same(); // BOGUS: this should not be allowed, because it uses the type Pair incorrectly

  print MakePair(c, d); // BOGUS: this should not be allowed, because it uses the type Pair incorrectly
  print "\n";
}

method Main() {
  var b := ReturnFalse();
  if b {
    // we should never get here
    print 10 / 0;
  }
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 2 verified, 0 errors
Unhandled exception. System.DivideByZeroException: Attempted to divide by zero.
   at System.Numerics.BigInteger.op_Division(BigInteger dividend, BigInteger divisor)
   at System.Numerics.BigInteger.Divide(BigInteger dividend, BigInteger divisor)
   at Dafny.Helpers.EuclideanDivision(BigInteger a, BigInteger b)
   at _module.__default._Main(ISequence`1 __noArgsParameter)
   at __CallToMain.<>c__DisplayClass0_0.<Main>b__0()
   at Dafny.Helpers.WithHaltHandling(Action action)
   at __CallToMain.Main(String[] args)
Pair.MakePair(2, 2)

What happened?

Type Pair says that its type parameter must support equality in compiled contexts. The type (int, ghost int) does not support equality in compiled context, so it should not be possible to use that type as the type argument to Pair. Alas, those checks are missing for the DatatypeValue AST nodes. The program should have been rejected by the resolver, but instead sails through both the verifier and compiler and ends up in a run-time crash.

What type of operating system are you experiencing the problem on?

Mac