Запрет равенства в теле оказался засидевшимся, а не границей: довод «запрет держит цену видимой» падает от двух прогонов, а спека языка требовала обратного

Одна и та же операция над одними и теми же значениями в утверждении разрешалась, а в теле отвергалась:

тотальная функция «Тождество» от «А»          → код 0, «проверено»
  ...
  обеспечивает «то же значение» результат равен значение

тотальная функция «Совпадают» от «А»          → код 1
  ...                                            FLANG_TYPE: сравнивать на
  левое равен правое                             равенство можно только скаляры

Запрет жил в одной функции — «Сказать о скалярах», flang/self/types.flang, — и молчал, когда сравнение стояло в утверждении. Довод при нём был записан такой: равен в теле — это работа, сличение двух списков стоит их длины, двух записей — их глубины, и запрет держит эту цену на виду.

Довод не выдержал замера, и падает он дважды.

1. куча содержит что над список «А» проходит проверку в теле, код 0. Это то же самое сличение двух непрозрачных значений, только в цикле по длине списка, — то есть в N раз дороже запрещённого. Цену запрет не держит: она уходит через соседнюю операцию, и молча.
2. равен на двух строках проходит в теле: строка считается скаляром. Сличение строк — сверка всех их байтов, цена ничем не ограничена. Значит и сам знак равен уже несёт неограниченную цену, а запрет отделял не дешёвое от дорогого.

А спека языка требовала ровно обратного. flang/SPEC.md, раздел «Семантика, которая обязана совпадать у всех слоёв»: «равенство списков, записей, вариантов — структурное». То есть структурное равенство непрозрачных значений — объявленное поведение языка, а отвергал его только слой типов.

Опасение «представление неизвестно, поэтому при работе невыразимо» — неверно, и это проверено запуском, а не рассуждением. Программа «Есть среди» от «А» с телом куча содержит что напечатана в C, собрана и запущена на вариантах объявленной суммы:

{"fn":"Показать","args":[{"n":"0"}]}
{"ok":true,"value":{"s":"вариант «Есть» 7 среди: да | вариант «Есть» 8: нет | вариант «Нет»: да"}}

Внутри — fl_equal рантайма: обход по имени варианта и полям. Значение несёт свой тег при работе, представление известно всегда.

Со снятым запретом то же самое печатают все восемь целей, и это снято прогоном уже ПОСЛЕ правки — равен над списком в теле напечатан во все восемь, код 0 везде:

Ни одна цель не использует родное ==: структурное сличение стояло в рантайме и до правки.

Сколько мест писали своё сличение — обходом, а не списком руками. По 958 файлам .flang дерева: 75 функций, возвращающих признак, с именем про равенство и непрозрачными параметрами. Они делятся на три разных класса, и смешивать их нельзя:

Семь — это stdlib/lists.flang, stdlib/utf8.flang, examples/rosetta/palindrome, examples/rosetta/hundred-doors, examples/leetcode/100-same-tree, scripts/corpus-runner.flang и сама подделка. Показателен progonshchik-korpusa: он сличает два списка строк через скалярную проекцию — (соединить левый по "\n") равен (соединить правый по "\n"). Ровно тот обход, который шапка stdlib/strlists.flang описывает как единственный доступный.

Сверх них — 21 функция sets.flang, dictionary.flang и трёх функций lists.flang, оставшихся немоноформными из-за того же запрета (замер 20 августа, equality-on-a-type-parameter-is-banned-only-in-bodies).

Что осталось запрещённым, и это уже граница, а не остаток. Значения-функции. Функция снимается перед печатью в имя и запомненные ею значения, поэтому сличение отвечает не на тот вопрос: две разные записи одного и того же расчёта выйдут неравными, а равенство обещало бы «одно и то же». Спека структурное равенство обещает для списков, записей и вариантов — про функции она не обещает ничего. Отказ теперь называет это словами:

FLANG_TYPE: сравнивать на равенство значения-функции нельзя, а обе стороны здесь
функция из числа в число: сличались бы имя функции и запомненные ею значения, а
не поведение, и две разные записи одного и того же расчёта вышли бы неравными.
Сравнивайте то, что функции возвращают, а не сами функции

Границу видно насквозь, и это сказано вслух в самом правиле: «А» можно подставить функцией, и тогда сличение пройдёт мимо запрета. Закрыть это нечем, пока у языка нет способа сказать «этот параметр умеет сравниваться», а содержит над списком функций мимо того же запрета проходил и до правки.

Чего снятие НЕ дало — и это ожидалось. Ни одного нового доказательства. Тело — не цель, ядро от разрешённого в теле равенства выводить больше не начинает. Мерить успех здесь надо снятыми копиями сличения, а не числом доказанных утверждений.

Две соседние стены — это НЕ та же работа, и проверено это прогоном. Их подозревали в общей причине с равенством: «типизатор разрешает в одном месте и запрещает в другом».

То есть расхождение «в утверждении можно, в теле нельзя» было ровно одно — у равенства. Работы здесь три, а не одна.

Чем подтверждено. Ветка u/ravenstvo-v-tele над github/main 0446d33f, bootstrap/flang 0.5.1, собран make -C bootstrap. Все прогоны — с показанным кодом возврата.

Семя перепечатано и СХОДИТСЯ: sh scripts/raskrutka.sh --check → «точка раскрутки bootstrap/ совпадает с печатью: 7 файлов, 25 899 669 байт», код 0, пик 25,5 ГиБ.

Примеры библиотеки пройдены ПОФАЙЛОВО (одной командой по каталогу прогон стоит часы и молча пропускает отказавший файл): 172 файла flang/stdlib и examples, прошло 4949. Красных файлов 8, и все восемь — НАСЛЕДСТВЕННЫЕ: каждый повторён на нетронутом дереве базового коммита 0446d33f отдельной рабочей копией и даёт там тот же отказ дословно.

Правило идёт с двумя подделками: poddelka-ravenstvo-v-tele.flang (значения-функции обязаны быть отвергнуты) и poddelka-ravenstvo-v-tele-ne-dokazyvaet.flang (сличение списков, вариантов и параметра типа обязано пройти, а две лжи про него — остаться недоказанными).

Чем ограничено. Замер числа мест механический: он ищет функции по имени и по непрозрачности параметров, а деление на три класса сделано чтением. Снятие запрета библиотеку само не переписывает — 7 копий и 21 немоноформная функция остаются работой, и работа эта не сделана.

Связано: equality-on-a-type-parameter-is-banned-only-in-bodies, three-of-five-named-postcondition-walls-are-already-gone, chto-nelzya-napisat-v-obespechivaet