What should we do about casts to instances of generic types?

The spec says:

Specifically, all casts to instances of generic types are forbidden.

The following code needs to be, and is, statically
rejected. It constructs an array `a` of `Int{self==3}`'s – integers
which
are statically known to be 3.
The only number that can be stored into `a` is `3`.
Then (in the line that is rejected) it attempts to trick the compiler into
thinking that it is an array of `Int`, without restriction on the
elements, giving it the name `b` at that type.
The cast aa as Array[Int]` is a cast to an instance of a generic type,
and hence is forbidden.

But, if that cast were allowed to work, it could store `1` into the array
under the alias
`b`, thereby violating
the invariant that all the elements of the array are 3.
This could lead to program failures, as illustrated by the failing assertion.

Here's the code:

public class forb {
  public static def main(argv:Array[String](1)) {
  val a = new Array[Int{self==3}](0..10, 3);
  // a(0) = 1; would be illegal
  a(0) = 3; // LEGAL
  val aa = a as Any;

  val b = aa as Array[Int]; // Line 8
  b(0) = 1;   // Line 9
  val x : Int{self==3} = a(0);
  assert x == 3 : "This would fail at runtime.";

  }
}

But the compiler doesn't do what the spec says.

~/x10/tmp: x10c -VERBOSE_CHECKS forb.x10 
/Users/bard/x10/tmp/forb.x10:9: Generated a dynamic check for the method call.
~/x10/tmp: x10 forb
x10.lang.AssertionError: This would fail at runtime.
	at forb.main(forb.java:66)
	at forb$$Main.runtimeCallback(forb.java:29)
	at x10.runtime.impl.java.Runtime$$Closure$Main.$apply(Runtime.java:118)
	at x10.lang.Runtime$$Closure$147.$apply(Runtime.java:3004)
	at x10.lang.Activity.run(Activity.java:422)
	at x10.lang.Runtime$Worker.loop$O(Runtime.java:1088)
	at x10.lang.Runtime$Worker.$apply(Runtime.java:1035)
	at x10.lang.Runtime$Pool.$apply(Runtime.java:1380)
	at x10.lang.Runtime.start(Runtime.java:1833)
	at x10.runtime.impl.java.Runtime.$apply(Runtime.java:162)
	at x10.runtime.impl.java.Thread.run(Thread.java:64)

Notice:

• There is no protection on line 8. The cast succeeds. This is the "instance of a generic type" which the spec said was forbidden.

• Although a dynamic check is inserted in line 9, it is not triggered. I'm not sure what precisely is being checked, even, but I don't think it's the issue I'm worried about.

• Igor thought that the compiler would issue a warning message about the cast. I thought that it would forbid the cast. It actually seems to peacefully allow the cast.

We need to decide what the right behavior here is, and either fix the compiler or the spec. So I'm posting this as a language design issue, but it should get redirected after we know what we're doing.