"compilation of seq<TRAIT> is not supported"; consider introducing a ghost

[robin-aws]

To trigger (as long as the /compile flag is 1 or higher):

trait MyTrait {}

class MyClass extends MyTrait {}

class MyOtherClass {
    var mySeqOfClass : seq<MyClass>; 
}

From looking at the compiler source it looks like this is just a "not implemented yet" case rather than a fundamental limitation, but I'd love to hear confirmation of this.

In my case the state needs to be reified at runtime so I can't make it a ghost var. Is there a better workaround than using an array instead?

[robin-aws]

It seems like this is due to the fact that the translations of seq<T> in most of the target runtimes do not support co-variance:

dafny/Test/dafny0/RuntimeTypeTests0.dfy

Lines 4 to 12 in 54799fc

	// The code in this file demonstrates complications in compiling to C# if a
	// trait (like "object") is allowed as a type parameter to something compiled.
	// The problem is that an assignment like a "set<MyClass>" to a "set<object>", which
	// is allowed in Dafny, would require a deep copy in C#. Another example is an
	// assignment of a "MyDatatype<MyClass>" to a "MyDatatype<object>".
	// Currently, the Dafny compiler enforces restrictions that rule out the expensive
	// cases. A possibly more friendly approach would be to emit code that performs
	// the deep copies.
	// Note that this is not a problem in JavaScript, which lacks type parameters.