If that 3 can be decided at runtime rather than at compile time, yes. Like, if I can have a type Array<Type,Length> and have a function f which has as its inpu

If that 3 can be decided at runtime rather than at compile time, yes. Like, if I can have a type Array<Type,Length> and have a function f which has as its input type Int, with the name of the input variable being n, and as its return type Array<Bool,n> and when you give the return value to something else, it checks (at compile time) that the length of the array (i.e. , n ) matches what the other thing is expecting, that would be using dependent types.