My recollection of C++ (possibly outdated since 11 or 14, though that would - pleasantly - surprise me) is that template parameters must be picked at compile ti

My recollection of C++ (possibly outdated since 11 or 14, though that would - pleasantly - surprise me) is that template parameters must be picked at compile time. With Idris, you can pick X and Y at runtime and still get compile time checking.