Bonsai is a tool that symbolically checks for soundness errors in type systems. It constructs a symbolic space of syntactically-correct programs and evaluates them on the actual typechecker and interpreter, looking for a program that passes the former but fails in the latter. Being a bounded model checker, Bonsai does not prove correctness of a type system, but it finds counterexamples twice as large as those found by experts. We demonstrate how to use Bonsai to find the recently-discovered Scala soundness issue SI-9633 (Amin & Tate), which is related to the interaction between null and path-dependent types.