Навелосипедил зависимые типы в Shen и написал в "бложек": http://4da.livejournal.com/10464.html#cutid1 Теперь система типов может таскать размер с массивом, помимо его типа. Интерес, конечно, скорее теоретический, нежели практический.