according {AS} on the #idris IRC: #Blodwen will have optimized type checking for Vects and Nats and such, so that eg. large vectors won't eat your RAM up when you run the type checker