Missing cast when creating a `datatype` in C#

[fabiomadge]

class C { 
  constructor () {}
}

datatype Co = Co(C)

method Main() {
  var i: object := new C();
  var a := Co(i);
}

The necessary downcast of i is missing, so csc fails.

[RustanLeino]

Here's another test program that fails for the same reason. This program assumes https://github.com/dafny-lang/dafny/pull/1755 has been merged.

datatype Dt<-X, +Y> = Ctor(h: X -> Y)

trait Trait { }
class Class extends Trait { }

method Main() {
  TestFunction();
  TestContravariance();
}

method TestFunction() {
  var c: Class := new Class;
  var t: Trait := c;
  var f: Class -> bool := (c: Class) => true;
  var g: Trait -> bool := (t: Trait) => false;

  print f(c), " ", /*BUG*/ f(t), "\n"; // true true
  print g(c), " ", g(t), "\n"; // false false

  f := g;
  print f(c), " ", /*BUG*/ f(t), "\n"; // false false
}

method TestContravariance() {
  var c: Class := new Class;
  var t: Trait := c;
  var f: Class -> bool := (c: Class) => true;
  var g: Trait -> bool := (t: Trait) => false;
  var a: Dt<Class, bool>;
  var b: Dt<Trait, bool>;

  a := Ctor(g);
  print a.h(c), " ", /*BUG*/ a.h(t), "\n"; // false false
  a := Ctor(f);
  print a.h(c), " ", /*BUG*/ a.h(t), "\n"; // true true

  b := Ctor(g);
  print b.h(c), " ", b.h(t), "\n"; // false false

  a := b;
  print a.h(c), " ", /*BUG*/ a.h(t), "\n"; // false false
  b := a;
  print b.h(c), " ", b.h(t), "\n"; // false false
}