Gabriel,

 

It took me two days to understand that this actually solved the problem because it fulfils type erasure and induction on dimension, just like functions.

Actually, that's the type of a reified curried function value -> value -> value -> ... -> value

        Diego Olivier