Verification: unknown length array should not be verified(?)

[sorawee]

method Main() {
  var a := new array<int>;
}

verifies. However, it results in a compilation error in every backend.

C#:

(1748,41): error CS1586: Array creation must have array size or array initializer

Java:

/Users/sorawee/projects/dsmith/tmp-java/_System/__default.java:13: error: array dimension missing
    java.math.BigInteger[] _nw0 = new java.math.BigInteger[](dafny.TypeDescriptor.BIG_INTEGER);
                                                            ^
/Users/sorawee/projects/dsmith/tmp-java/_System/__default.java:13: error: not a statement
    java.math.BigInteger[] _nw0 = new java.math.BigInteger[](dafny.TypeDescriptor.BIG_INTEGER);
                                                                                 ^
/Users/sorawee/projects/dsmith/tmp-java/_System/__default.java:13: error: ';' expected
    java.math.BigInteger[] _nw0 = new java.math.BigInteger[](dafny.TypeDescriptor.BIG_INTEGER);
                                                                                             ^

JS:

[stdin]:1086
      let _nw0 = new BigNumber[]();
                               ^

SyntaxError: Unexpected token ']'

Go:

tmp-go/src/tmp.go:46:28: undefined: _System.New_Array_

Instead of letting the program attempts to compile, the verifier should fail it.

Also note that this code is taken from the documentation:

Caveat: The type of the array created by new T[n] is array. A mistake that is simple to make and that can lead to befuddlement is to write array instead of T after new. For example, consider the following: var a := new array<T>; ... The first statement allocates an array of type array, but of unknown length.

which misleadingly sounds like the code is fine.

[robin-aws]

Sounds more like the issue is the statement should have been rejected at resolution time, as array is a reference to an unknown type.