Thank you, I understand that, but I need a little more detail. Let me explain.<p>Languages that have generics can either erase the generic argument at runtime (like Java or Scala do) or generate a different concrete type for each instantiation (like C++ or Nim do). In either case, you usually know at compile time which concrete instances of the generic parameter are going to be used where.<p>That is, even in Java you may have a single class Stack&lt;A&gt;, but at the final use site this will eventually turn into some concrete type, such as Stack&lt;String&gt; (it may remain generic in intermediate steps). In other words, you are not going to use Stack with a generic parameter that you did not anticipate. You cannot read the runtime type of some instance, call it X, and then start writing functions that work on Stack&lt;X&gt;.<p>Now, let me turn to dependent types. A lot of the techniques that Idris promotes can be simulated in other languages, such as Scala, C++ or Nim. But in each case that I know of, you are required to know at compile time which concrete values you are going to use as generic parameters. That is, in C++ you can write functions that operate on types like Vector&lt;A, N&gt;, where N is the length, but you have to eventually specialize N to a concrete number before compiling.<p>The comment above states that Idris does not have this restriction, but it is not clear to me how that might work. I concede that by using an erasing technique (as opposed to specialization) one is not required to materialize such functions for all N - this is what one does for instance in Scala.<p>But the problem is: what do you do at the usage site? Say you are reading two lists off two JSON files, and you want to concatenate them using the above function. Wouldn&#x27;t you need to provide at compile time a concrete value for N and M? (and consequently cast the unsized vectors to sized ones?).<p>If this is the case, then there is not much difference from letting the compiler materialize a function for concrete values of M and N that are used (because in either case, you have to encode knowledge about concrete values of M and N at compile time).<p>Maybe everything would be more concrete if I saw an Idris program that reads two vectors from external files at runtime, and then concatenates them, whatever their size is.