Dafny can't model C# classes without public constructors

[samuelgruetter]

Suppose I have the following C# classes, which are given by some library and I can't change:

class Bar{}

class Foo {
    Bar x;
    private Foo() {}
}

Note that the constructor of Foo is private, and some part of the library I know nothing about will construct new Foo objects.

I try to model this in Dafny as follows:

class {:extern} Bar{}

class {:extern} Foo {
    var {:extern} x: Bar
}

But I get the error

class 'Foo' with fields without known initializers, like 'x' of type 'Bar', must declare a constructor

The obvious workaround is to just add a constructor in Dafny, but then if I write a Dafny file which uses this constructor, it will verify and successfully compile to a C# program, but compiling the C# program will fail. This is undesirable. It would be better if Dafny did not require a constructor for fully extern classes.

[robin-aws]

Relevant to #469: it may be better to have a different annotation to refer to an existing type.