Я тут кое что осознал. Когда мы пишем Foo<Type1, Type2> мы на самом деле под этим подразумеваем Foo { field1: Type1, field2: Type2 }. Почему бы эту неявность не перевести в явность и дать возможность заабузить?

Шаг первый: разрешение на получение доступа к полям на уровне типов.
Можно предложить такой синтаксис (здесь и далее примеры на псевдо-Haskell):
data Vect s t = MkVect { size :: s, ... }
head :: Vect (size :: Nat) t -> t
Таким образом мы объявляем структуру данных Vect с обобщённым параметром size - размером вектора и t - типом элемента.

Шаг второй: обобщенные параметры по умолчанию.
С предыдущей записью нам пришлось бы записывать для каждого использования типа size :: Nat, что выглядит вербозно. Обобщенные параметры по умолчанию уже реализованы в языке Rust. Перепишем наш прошлый пример:
data Vect (size :: Nat) t = ...
head :: Vect size t -> t
Выглядит довольно симпатично!

Шаг третий: посыпаем refinement типами.
Здесь я буду использовать синтаксис очень схожий с refinementd, где вы можете почитать…