Type erasure for generics allows unsafe coercions in Hack's strict mode

[pbl64k]

I'm not sure whether this is by design, or at least fundamental enough to be unfixable, but I thought I'd report this anyway. When dealing with generics, instanceof checks allow to subvert the type system with respect to type parameters, effectively allowing unsafe casts. The minimum example can be found in the public gist:

https://gist.github.com/pbl64k/6e936c13e9fb5b625f25

hh_client reports no errors for this code, but running hhvm minimum-test-runme.hh results in BadMethodCallException:

lepin@xub:~/Sandbox/hack/hack-playground$ hh_client 
No errors!
lepin@xub:~/Sandbox/hack/hack-playground$ hhvm minimum-test-runme.hh 

Fatal error: Uncaught exception 'BadMethodCallException' with message 'Call to a member function emit() on a non-object (integer)' in /home/lepin/Sandbox/hack/hack-playground/minimum-test.hh:35
Stack trace:
#0 /home/lepin/Sandbox/hack/hack-playground/minimum-test.hh(40): Unsafe::emit()
#1 /home/lepin/Sandbox/hack/hack-playground/minimum-test-runme.hh(5): Unsafe::test()
#2 {main}
lepin@xub:~/Sandbox/hack/hack-playground$ hhvm --version
HipHop VM 3.9.1 (rel)
Compiler: tags/HHVM-3.9.1-0-g0f72cfc2f0a01fdfeb72fbcfeb247b72998a66db
Repo schema: 6416960c150a4a4726fda74b659105ded8819d9c

The culprit is Unsafe<Tx>::convert: $x instanceof Unsafe should not guarantee that $x is of type Unsafe<Tx> for any Tx, but does so anyway.

[JoelMarcey]

cc @dlreeves @jwatzman

[jwatzman]

This is somewhat by design. We can't allow a proper instanceof due to type erasure, as you point out. The decision then was what to do with instanceof in strict mode... we could disallow it, we could make it set type parameters to mixed or something like that, or we could make it set type parameters to the "trust me" type of untyped values. We made a call that the other options were too restrictive and went with the last.

It might be worth revisiting this. Poke poke, @dlreeves.

[pbl64k]

This is quite useful in its current form, because when used responsibly (i.e. when the library author can prove using the information not available to the type checker that the invariant actually holds) it allows emulation of higher-kinded polymorphism which wouldn't be possible in Hack's type system otherwise. But as it's also quite a landmine, personally I think this should be disallowed unless explicitly suppressed by HH_FIXME.

[dlreeves]

Let's compare with the JVM that also erases generics. In Java the type safe way to do this is to utilize the wildcard type ?.

class Box<T> {
  public static Box<?> test(Object obj) {
    return (Box)obj;
  }
}

If you do not use the wildcard type the Java compiler will issue a warning. Hack doesn't have the concept of a warning, but I have been thinking about adding an option to hhconfig that says to ignore certain errors. At that point it could essentially be treated as a warning.

On the other in Scala it doesn't emit a warning or anything at all

class Box[T] {
  def test(obj: Any): Box[String] = obj.asInstanceOf[Box[String]]
}

[pbl64k]

The slight difference -- strictly from human reader's point of view -- is that both of those are clearly casts, which should trigger the blaring sirens in programmer's mind more readily than invariant(... instanceof ..., ...). Which serves exactly the same role, of course, but is not an expression, and also happens to have a non-local effect.

[mofarrell]

https://github.com/facebook/hhvm/commit/603cbd7cbf79f059365a1ff7787fef7b193e7ec3 allows this to be flagged as an unsafe use of instanceof with generics.

[lexidor]

I am going over old issues on this repository, to see which ones apply to the current versions of hhvm.

Your repro is now a typechecker error, in the exact way you were hoping for. This changed when is and as expressions replaced instanceof in hhvm 3.28.0. The $x is Unsafe<_> requires you to specify, "please infer the generic at this _ position to the best of your ability". Hack infers mixed, since there is no better type that has been proven to be correct. With instanceof, Hack would infer [unresolved], which is the unpure, we don't know anything yet, type.

Typing[4110] Invalid return type
   --> file.hack
 20 |     final public static function convert(ITest $x): Unsafe<Tx> {
    |                                                            ^^ Expected Tx
    |                                                            ^^ Considering that this type argument is invariant with respect to Unsafe
 21 |         invariant($x is Unsafe<_>, '...or else');
    |                         ^^^^^^^^^ But got Tx#2 from this `is` expression test
 22 |         return $x;
    |                ^^

1 error found.