Missing downcasts

[RustanLeino]

Dafny version

4.7.0

Code to produce this issue

method Main() {
  var n: set<Number> := {};
  var s: set<Integer>;
  s := DoItWithAssignment(n);
  print |s|, " ";
  s := DoItWithPlainLet(n);
  print |s|, " ";
  s := DoItWithOptimizedLet(n);
  print |s|, " ";
  s := DoItViaFunctionBodyResult(n);
  print |s|, "\n";
}

trait Number {
  const value: int
}

class Integer extends Number {
  constructor(value: int) {
    this.value := value;
  }
}

method DoItWithAssignment(numbers: set<Number>) returns (integers00: set<Integer>)
  requires |numbers| == 0
{
  integers00 := numbers;
}

function DoItWithPlainLet(numbers: set<Number>): set<Integer>
  requires |numbers| == 0
{
  {} +
  var integers11: set<Integer> := numbers;
  integers11
}

function DoItWithOptimizedLet(numbers: set<Number>): set<Integer>
  requires |numbers| == 0
{
  var integers22: set<Integer> := numbers;
  integers22
}

function DoItViaFunctionBodyResult(numbers: set<Number>): set<Integer>
  requires |numbers| == 0
{
  numbers
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 5 verified, 0 errors
Errors compiling program into test
source(5770,43): error CS0266: Cannot implicitly convert type 'Dafny.ISet<_module.Number>' to 'Dafny.ISet<_module.Integer>'. An explicit conversion exists (are you missing a cast?)

source(5774,14): error CS0266: Cannot implicitly convert type 'Dafny.ISet<_module.Number>' to 'Dafny.ISet<_module.Integer>'. An explicit conversion exists (are you missing a cast?)

What happened?

Dafny emits malformed code for the bodies of DoItWithOptimizedLet and DoItViaFunctionBodyResult.

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

Mac