Я в идрис, увы не шарю. Только мимокрокодилил. В расте я точно знаю что такие штуки НЕ выражаются. И я не НЕ понимаю КАК это сделать в С++ даже с учётом того свойства ньютайпности, которое ты показал.
Покажи, пожалуйста, пример. Код. Либо n+1. Либо как выше описали гарантию того, что списки имеют одинаковую длинну.
Очевидно не выражается, потому что раст бездарное говно с мусорной системой типов.
Кода n + 1 - не существует. Ты пытаешься прикрутить левую семантику, семантики арифметики и тысячи всяких базовых операций над нею, которые уже реализованы в твоём недоязычке.
От завтипов нужно не это. А нужна возможность выражения это семантики.
