Idris is not a Lisp and I've never used it, but it has dependent types (types incorporating values) and encodes matrix dimensions into the type system (I think only matrix multiplications which can be proven to have matching dimensions can compile). I think the dimension parameters are erased, and generic at runtime (whereas C++ template int parameters are hard-coded at compile time). IDK if it uses dependent types for optimization.