As Guido said, while working on type arithmetic I also explored some ideas about how to deal with the exact length of a variadic, as well as dimension specific operations. The idea does not need any sort of dependent typing, just to take advantage of literal types. I did not comment about this earlier since I thought that this PEP should be as minimal as possible. The main idea is that, since we may need a custom operator on variadics for each specific use case, it would be better to have something more abstract.
TLDR: def f(x : Tensor[Ts], y : |Ts|): ... or def f(x : Tensor[Ts[N]], y : N): ...
My initial motivation was to leverage the length operator on variadics (|_|) that I wanted to introduce to also constraint the length of the variadics, so that not more operators would be needed for that task (apart from that operator of course). However, nowadays I think that there is no need to rely on the length operator for that and we could use one of the alternative syntaxes.
Regarding the current PEP, congratulations for the progress so far! However, I might have missed something but: where is specified the constraints that a variadic can have (variance, bound...)? And the subtyping rules for variadics?