I think dependent types are amazing, but even the tiny subset of dependent types known as refinement types opens up huge avenues for optimization. Some optimiza

I think dependent types are amazing, but even the tiny subset of dependent types known as refinement types opens up huge avenues for optimization. Some optimizations (loop nest optimizations for a simple example) might only be feasible with static range definitions or with profile guided optimization...but if you throw in refinement types, you now have static guarantees as to the cardinality or range of a variable, and loop nest optimizations can be statically determined. I think full dependent typing could be great, but compilers can still be improved with small language improvements.