Равенство над параметром типа запрещено только в ТЕЛЕ: в утверждении оно разрешено, и упирается в него девять мест, а не вся библиотека
Запись «равен над параметром типа отвергается» (flang/cat/POLY.md, фаза 5; шапки stdlib/sets.flang, stdlib/dictionary.flang, stdlib/optional.flang) верна наполовину и потому вводит в заблуждение. Запрет живёт в одной функции — «Сказать о скалярах» (flang/self/types.flang:4616) — и она пропускает сравнение, когда оно стоит в утверждении:
если «в утверждении» то «беды» иначе (… «сравнивать на равенство можно только скаляры …»)Довод записан там же: утверждение — не вычисление, доказанное утверждение в напечатанный код не попадает вовсе, и запрещать в нём нечего.
Что из этого следует, и это не мелочь. Семь функций optional.flang и result.flang, у которых сегодня нет ни одного обеспечивает, немы не из-за системы типов. Прогон: постусловие если («Есть значение» от опция) то да иначе (результат равен запасное) на полиморфной «Значение или запасное» от «А» проверку типов проходит; ведомость называет его «сетка 3», то есть недостача теперь в силе ядра, а не в праве говорить. А круговое утверждение («Развернуть» от («Обернуть» от значение) и значение) равен значение ядро закрывает целиком — «доказано сведением цели с телом функции».
Сколько мест упирается в запрет — измерено прогоном, а не списком. Модули механически параметризованы (строка → «А», ключ словаря → «Ключ») и пропущены через bootstrap/flang check:
| модуль | отказов | функций станет обобщёнными |
|---|---|---|
stdlib/sets.flang | 2 | 9 |
stdlib/dictionary.flang | 3 | 9 |
три функции stdlib/lists.flang | 3 | 3 |
| итого по этому запрету | 8 | 21 |
Девятое место — другое правило: начальное значение свёртки типизируется без ожидаемого типа, и свёртка … начиная с (вариант «Нет») в полиморфной функции даёт FLANG_TYPE_PARAM.
stdlib/strlists.flang в счёт не входит: он параметризуется с 50 отказами, и почти все — разделить, соединить, содержит над строкой. Это модуль про строки по существу, а не жертва запрета.
Чем ограничено. Числа сняты 20 августа 2026 на ветке u/ssylka, bootstrap/flang 0.5.1. Параметризация механическая: она показывает, где компилятор упрётся, и не утверждает, что после снятия запрета все 21 функция останутся доказуемыми — доказуемость мерялась только на утверждениях выше.
ЗАПРЕТ СНЯТ 21 августа 2026 — разбор, замеры и то, что от запрета осталось (значения-функции), в equality-in-a-body-was-a-stale-restriction-not-a-boundary. Ниже — состояние на 20 августа, как оно было записано тогда.
Снятие запрета — развилка владельца, а не работа. Запрет держит цену видимой: сличение двух списков стоит их длины, двух записей — их глубины. Все восемь целей печати структурное равенство уже умеют (fl_equal в C, Value.equal в Java), то есть ограничивает только типизатор.
Связано: typed-process-reference-is-already-expressible, chto-nelzya-napisat-v-obespechivaet, round-trip-claims-are-unstatable-in-postconditions