Restrictive type in pattern causes malformed target code

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

datatype Record = Record(o: object)

class C { }

method M(r: Record)
  requires r.o is C
{
  match r
  case Record(c: C) =>
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 1 verified, 0 errors
Errors compiling program into test
(5068,18): error CS0266: Cannot implicitly convert type 'object' to '_module.C'. An explicit conversion exists (are you missing a cast?)

What happened?

The example above goes through both the resolver and verifier. Alas, the C# and Java backends do not generate correct code for it.

One possibility would be to fix the C# and Java compilers. However, eventually, we anticipate a new "type case" feature (see #1715). Therefore, a viable solution to the problem above would be to forbid, already in the type system, the use of classes/traits where the source type has a parent trait thereof.

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

Mac