[dllthomas]

Per my understanding, what's so exciting about this is precisely that you're wrong - it does not need to be known at compile time, but can prove symbolically that the resulting length will be X + Y. And of course, given that, it's not statically creating a distinct instantiation of the Vect type for every N at compile time!

[rfw]

Really? Color me corrected, then :) Does the compiler need a SAT solver then to make sure all the constraints hold?

[dllthomas]

I'm not sure the exact approach, but there's definitely some heavy lifting. My understanding is that most (all?) dependently typed languages are essentially theorem provers at heart.

[chenglou]

See my answer here: https://news.ycombinator.com/item?id=10856736

[pzone]

It should be able to use a Hindley-Milner algorithm.

[dllthomas]

As I understand it, type inference breaks down on dependent types.