Making propellor safer with GADTs and type families

I'm currently working on a Java project. The more I read about how much safety one can reap from a decent type system, the more I want to be working on a project that uses one.

I do think, though, that learning about what's possible has helped me to get more benefit from Java's type system -- there are several classes of bugs that our system could suffer from, except that we explicitly designed our types with safety in mind so that code which would fail will fail at compile time rather than run-time. Mostly this involves heavier-than-usual use of generics and lambdas, so we have type information where we need it, and structuring our classes such that it's just not possible to reach unsafe bits of the framework from regular code.