придётся сначала идрис выучить

Иначе это будет не лучше обычного наезда на хаскель от гошников

я написал "какой тип должен выводиться?", а не "какой тип должен быть?". Потому что в зависимости от контекста полезным можем быть выводить как более-менее общий зависимый тип, так и тип без зависимостей. И потом показал, что бывает, если всегда по умолчанию выводить общие зависимые типы. Поинт в том, что тайпчекер не должен этим заниматься, это слишком неявно и может быть слишком дорого. Этим должна заниматься тулза, встроенная в компилятор, которая генерирует код по запросу от юзера, и чтобы юзер мог указать, какой тип он хочет, чтобы вывелся

а наоборот, из идрисострадальцев кто-нибудь агду прилично знает?

ну переопыление между агдой и идрисом есть. Например рефлекшон в агду утащали из идриса

насколько я понял, в несколько измененном виде, но все же

Его и в идрисе переписали

Што такое агда

Вкрации

што такое хаскель?

Токой езык

На котором пишут умные люди

токой помогатель доказывания

Спасибо

а умные ли люди пишут на нём

На скале пишут скалисты

Я их видел в чати

не факт

Умные тоже пишут?

почему я никогда не видел, чтобы вот эта ахинея:

test :: Bool
test = b where b = _

--     • Found hole: _ :: t
--       Where: ‘t’ is a rigid type variable bound by
--                the inferred type of x :: t

людей бесила? А не отсутствие вывода полиморфных типов в тайпчекере, который там не нужен и который должен делаться другими средствами