Unable to verify function with parameters that are subset types only with '--type-system-refresh'

[alexstaeding]

Dafny version

4.10.0

Code to produce this issue

ghost predicate IsCommutativePartial<T(!new), R>(op: (T, T) --> R) {
  forall x, y :: op.requires(x, y) && op.requires(y, x) ==> op(x, y) == op(y, x)
}

ghost predicate IsCommutativeTotal<T(!new), R>(op: (T, T) -> R) {
  forall x, y :: op(x, y) == op(y, x)
}

function SumInt(a: int, b: int): int { a + b }
function SumNat(a: nat, b: nat): nat { a + b }

lemma SumIsCommutative()
  ensures IsCommutativePartial(SumNat)
  ensures IsCommutativePartial(SumInt)
  ensures IsCommutativeTotal(SumNat)
  ensures IsCommutativeTotal(SumInt)
{}
``

Command to run and resulting output

$ dafny verify Test.dfy

Dafny program verifier finished with 3 verified, 0 errors


$ dafny verify --type-system-refresh Test.dfy
Test.dfy(13,31): Error: value does not satisfy the subset constraints of '(int, int) --> nat' (possible cause: it may have read effects)
   |
13 |   ensures IsCommutativePartial(SumNat)
   |                                ^^^^^^

Test.dfy(15,29): Error: value does not satisfy the subset constraints of '(int, int) -> nat' (possible cause: it may be partial or have read effects)
   |
15 |   ensures IsCommutativeTotal(SumNat)
   |                              ^^^^^^

Test.dfy(17,0): Error: a postcondition could not be proved on this return path
   |
17 | {}
   | ^

Test.dfy(13,30): Related location: this is the postcondition that could not be proved
   |
13 |   ensures IsCommutativePartial(SumNat)
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Test.dfy(2,2): Related location: this proposition could not be proved
  |
2 |   forall x, y :: op.requires(x, y) && op.requires(y, x) ==> op(x, y) == op(y, x)
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Test.dfy(17,0): Error: a postcondition could not be proved on this return path
   |
17 | {}
   | ^

Test.dfy(15,28): Related location: this is the postcondition that could not be proved
   |
15 |   ensures IsCommutativeTotal(SumNat)
   |           ^^^^^^^^^^^^^^^^^^^^^^^^^^

Test.dfy(6,2): Related location: this proposition could not be proved
  |
6 |   forall x, y :: op(x, y) == op(y, x)
  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Dafny program verifier finished with 2 verified, 4 errors

What happened?

It seems that Dafny incorrectly instantiates T using int rather than nat when using the type system refresh. If I instead use only one type paramter, like in:

ghost predicate IsCommutativePartial<T(!new)>(op: (T, T) --> T) {
  forall x, y :: op.requires(x, y) && op.requires(y, x) ==> op(x, y) == op(y, x)
}

(also for IsCommutativePartial), the code verifies.

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

Mac