Reference types in comprehension soundness issue

[MikaelMayer]

trait Tr { }
class A extends Tr { }
class B extends Tr { }

function method test(x: Tr): bool
  requires x is A
{
  if x is B then 1/0 == 0 else true
}

method Main() {
  var a := new A;
  var b := new B;
  var s: set<Tr> := {a, b};
  var aa := forall a': A :: a' in s ==> test(a');
  assert(aa);
  print "ok";
}

In the case above, the verifier passes and

1. C#'s compilation complains that error CS1503: Argument 1: cannot convert from 'System.Collections.Generic.IEnumerable<_module.Tr>' to 'System.Collections.Generic.IEnumer able<_module.A>', which is something that @fabiomadge is working on right now, so that could explain why nobody found this error before.
2. JavaScript it silently fails and "ok" is never printed;
3. Java: Exception in thread "main" java.lang.ArithmeticException: BigInteger divide by zero
4. Go: Running... [Program halted] reflect: Call using *main.B as type *main.A and nothing else displayed

The problem comes again from the fact that the type inference infers that a' is of type A and the bounds are a set of type Tr, and whereas there is some check for the foreach statement in every compiler, there is no check for compiling the forall because it compiles to a true mapping expression.

I'd say, all these errors would be automatically fixed if I implement my right solution..

Originally posted by @MikaelMayer in #1522 (comment)