Is this agda?

нет Ж(((

Чем?

Явный пример переусложнения языка фичами, которые на самом деле не нужны.

мне нравится, что можно различать невидимое-но-возможно-вы-захотите-предъявить-аргумент-явно и невидимое-и-вы-скорее-всего-не-захотите-предъявить-аргумент-явно

почитал тред, твое предложение сделать visibility levels мне тоже понравилоась, но вряд ли {{a}} будет часто нужно, а вот иметь возможность опускать кайнды и явно писать их в сигнатуре мне нравится

то есть я не берусь увтерждать, что это хороший дизайн, но это лучше чем то, что сейчас есть

как мне кажется

Вот из-за таких как ты...

Про visibility levels это было скорее аргумент не идти в этом направлении вообще

ну аккуратнее надо с такими аргументами, а то они кому-то понравиться могут, как в данном случае

почитал тред. Подумал, что если когда-нибудь буду пилить свой зависимо-типизированный язык (не буду), то разрешу там как раз такие visibility levels. Раздражает в агде писать f {x = x}, когда заранее известно, что юзер может захотеть явно предъявить x, а все остальное — вряд ли. Вот только неявных аргументов бывает много, так что писать {{A}} {{B}} {{C}} ради одного {x} потом — того не стоит, так что я бы развернул синтаксис и сделал {A} {B} {C} {{x}} и потом f {{x}}. Что впрочем тоже довольно уродливо. Над синтаксисом в этом никогда не появившемся на свет языке придется подумать...

what have I done.

А есть какие-нибудь общепринятые способы разруливать инстансами, у которых одинаковые "головы"?

MPTC

Вводишь доп параметр и через него разруливаешь

welcome to олеггинг

Это что?(

Звучит как что-то нехорошее

Техники используемые Олегом Киселёвым

Блин, надо будет генерики переписывать(