Ну что тебя устроит

в С++ функция может поражать уникальные типы для каждого вызова. В С++ в тип можно записать что угодно. В С++ на уровне типов можно выполнять произвольную логику. Функции можно типизировать предикатами

Экзистенциального равенства нет в Idris
https://nickdrozd.github.io/2020/04/23/idris-interfaces.html

единственная проблема в том, что никакой проработки завтипов нет. Вся эта бездарная скриптуха - ничего не делает. Как я уже выше сказал - всё там, кроме идриса(и может ещё какого нонейм-дерьма) вообще не явзыки. А все завтипы - это просто ещё один недоязычок реализованный в виде типизации

к тому же всё это неважно. Ни С++, ни раст не должно волновать то, что там у запарты. Потому что запарта никогда и калькулятор не напишет. Никому не интересна типизация сама по себе, если её нельзя применить в реальной разработке, а не лаб и распиле.

Я уже приводил множество примеров сравнения С++ и раста в этом плане

Самый просто - это ренжи. В С++ они на уровне типа хранят некие свойства итераторов. Т.е. есть взять RA объект и применить к нему sort - он породит RA-последовательность. Есть применить фильтр - признак RA потеряется.

Это то, что существует в С++ множество лет ещё тогда, когда дошколята с идрисами на горшках сидели. Другое дело, что это далеко от мейнстрима по тем самым причинам. Лоулевел язык никому не нужен, если для него нельзя написать биндинги

А где здесь завтиповость?

я не говорю, что здесь завтиповость. К тому же - она здесь есть

Это ведь просто закрепление семантики за типом.

я говорю о том, что нет смысла о ней говорить. Потому как её нет, а она есть только в фантазиях дошколят и обсуждаемой теме отношения не имеет

Где именно - ткни носом, пожалуйста.

завтипы так и работают.

Завтипы это когда один тип зависит от другого. Например:
add1: n -> n + 1

Создай пожалуйста такую функцию на с++

И, они и так зависят. К тому же, что здесь и от чего зависит и в чём проблема с выражением этого на С++?

Или такую:
oneTwo: ((n: Int) ** n + 1)

Так ты сделай,

так ты ответь для начала. Раз начал.

На что?

В том, что числа только константные можно будет описать в C++ с такой функцией, а в Idris — и те числа, полученные в рантайме

К тому же, что здесь и от чего зависит и в чём проблема с выражением этого на С++?