Shen's powerful T* type system using sequent calculus which is turing complete is revolutionary.

Also, Shen's approach doesn't have a huge performance hit. See benchmarks for Qi implemented in SBCL. http://www.lambdassociates.org/studies/study10.htm