Datatype erasure and traits don't play together

[RustanLeino]

Dafny version

4.5.0

Code to produce this issue

trait Trait {
  function Value(): string
}

datatype Dt extends Trait = Dt(s: string)
{
  function Value(): string { s }
}

method Main() {
  var d: Dt := Dt("hello");
  var y: Trait := d;
  print d.Value(), " ", y.Value(), "\n";
}

Command to run and resulting output

% dafny run test.dfy --type-system-refresh --general-traits=datatype

Dafny program verifier finished with 2 verified, 0 errors
Errors compiling program into test
source(5726,21): error CS0535: 'Dt' does not implement interface member 'Trait.Value()'

What happened?

Since the datatype has 1 constructor with 1 argument, the compiler optimizes Dt to be just that argument. But this optimization should be used only if the datatype does not implement any traits.

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

Mac